macro "conj_elim" hp:ident hq:ident "from" h:ident : tactic =>
  `(tactic|(have ⟨$hp,$hq⟩ := $h))

macro "conj_intro" h:ident "from" hp:ident hq:ident : tactic =>
  `(tactic|(have $h : _∧_ := And.intro $hp $hq))

macro "disj_elim" hp:ident hq:ident "from" h:term:arg : tactic =>
  `(tactic|(refine Or.elim $h (fun $hp => ?_) (fun $hq => ?_)))

macro "disj_intro_left" h:ident "from" hp:ident q:term:arg : tactic =>
  `(tactic|(have $h : _∨($q) := Or.inl $hp))

macro "disj_intro_right" h:ident "from" p:term:arg hq:ident : tactic =>
  `(tactic|(have $h : ($p)∨_ := Or.inr $hq))

macro "impl_elim" hq:ident "from" hp:ident hpq:ident : tactic =>
  `(tactic|(have $hq := $hpq $hp))

namespace And
theorem elim' {P Q : Prop} {R : Sort} (h : P ∧ Q) (f : P → Q → R) : R :=
  And.elim f h
end And

variable (S:Type) 
variable (P Q R : S → Prop)

example ( h : ( ∀ x : S, P x → Q x ) ∧ ( ∀ y : S, P y → R y ) ) : (∀ x : S, P x → Q x ∧ R x) := by
  intro t -- We are using universal introduction.  Now our goal is P t → Q t ∧ R t.
  intro hpt -- Our goal is an implication, so we use implication introduction.  We assume P t and the goal becomes Q t ∧ R t.
  conj_elim h₁ h₂ from h -- We break our hypothesis into two using conjunction elimination.
  apply And.intro -- We need to prove a conjunction, so we split it into two goals : Q t and R t.
  · have h₃  := h₁ t -- We prove Q t first.  By universal elimination, we get P t → Q t from h₁ applied to t.
    apply h₃ -- Our goal is Q t and we have P t → Q t, so we can simplify the goal to P t.
    exact hpt -- And we already know P t!
  · have h₄ := h₂ t -- Our second goal is R t.  Use use universal elimination again to get P t → R t from h₂ applied to t.
    apply h₄ -- We simplify the goal from R t to P t using P t → R t.
    exact hpt -- And again, P t is something we know.

/- The same proof using another idiom for conjunction elimination -/
example ( h : ( ∀ x : S, P x → Q x ) ∧ ( ∀ y : S, P y → R y ) ) : (∀ x : S, P x → Q x ∧ R x) := by
  intro t
  intro hpt
  have ⟨ h₁ , h₂ ⟩ := h -- This is another way of doing the conjunction elimination.
  apply And.intro
  · have h₃  := h₁ t
    apply h₃ 
    exact hpt
  · have h₄ := h₂ t
    apply h₄
    exact hpt

/- The same proof using even another idiom for conjunction elimination -/
example ( h : ( ∀ x : S, P x → Q x ) ∧ ( ∀ y : S, P y → R y ) ) : (∀ x : S, P x → Q x ∧ R x) := by
  intro t
  intro hpt
  apply And.elim _ h -- This is still another way of turning h into h₁ and h₂
  intro h₁ h₂ -- It takes two lines and you can't forget the _ symbol.
  apply And.intro
  · have h₃  := h₁ t
    apply h₃ 
    exact hpt
  · have h₄ := h₂ t
    apply h₄
    exact hpt

/- This example shows existential introduction, existential elimination, and universal elimination. -/
example ( h : ( ∃ x : S, P x ) ∧ ( ∀ x : S, Q x ) ) : ∃ x : S, P x ∧ Q x := by
  conj_elim h₁ h₂ from h -- First break apart the conjunction h into h₁ : ∃ x, P x and h₂ : ∀ (x:S), Q x.
  apply Exists.elim h₁ -- Apply existential elimination to h₁ : ∃ x, P x...
  intro t -- ... that gives us a t : S ... 
  intro hpt -- ... such that P t is true.
  apply Exists.intro t -- Our goal is to show ∃ x, P x ∧ Q x.  We'll use x = t.  Our goal becomes P t ∧ Q t.
  apply And.intro -- Our goal is a conjunction so we use conjunction introduction.  That gives two goals.
  exact hpt -- The first goal is P t, which we got when we introduced t.
  exact h₂ t -- The second goal is Q t, which we have by universal elimination on h₂ : ∀ t:S, Q t and t:S.

/- Here is another proof, using a different idiom for the existential elimination -/
example ( h : ( ∃ x : S, P x ) ∧ ( ∀ x : S, Q x ) ) : ∃ x : S, P x ∧ Q x := by
  conj_elim h₁ h₂ from h
  have ⟨ t, hpt ⟩ := h₁ -- You can do the whole existential elimination in one step like this.
  apply Exists.intro t
  apply And.intro
  exact hpt
  have hqt := h₂ t
  exact hqt