/-

Test an exotic have syntax, from https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Behavior.20of.20'have'.20tactic.20changing.20with.20imports

-/
theorem test_have3: ∀ (p q : Prop), p ∧ ¬q ∨ q ∧ ¬p ↔ (p ∨ q) ∧ ¬(p ∧ q)
test_have3Warning: declaration uses 'sorry' (p: Prop
p q: Prop
q : Prop: Type
Prop) : ((p: Prop
p ∧ ¬q: Prop
q) ∨ (q: Prop
q ∧ ¬p: Prop
p)) ↔ ((p: Prop
p ∨ q: Prop
q) ∧ ¬(p: Prop
p ∧ q: Prop
q)) := byGoals accomplished! 🐙
  have my_p: p ∧ ¬q ∨ q ∧ ¬p → (p ∨ q) ∧ ¬(p ∧ q)
my_p (h₁: p ∧ ¬q ∨ q ∧ ¬p
h₁ : ((p: Prop
p ∧ ¬q: Prop
q) ∨ (q: Prop
q ∧ ¬p: Prop
p))) : (p: Prop
p ∨ q: Prop
q) ∧ ¬(p: Prop
p ∧ q: Prop
q) :=p, q: Prop
p ∧ ¬q ∨ q ∧ ¬p ↔ (p ∨ q) ∧ ¬(p ∧ q) byGoals accomplished! 🐙
    sorryGoals accomplished! 🐙
  sorryGoals accomplished! 🐙