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 := by
  sorry
end And

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

/- The first group of examples show how quantifiers work in Lean -/




example ( h : ∀ x : S, P x ) ( t : S ) : P t := by
  sorry


example ( h : ∀ x : S, P x ) ( t : S ) : P t := by
  sorry

example : ∀ x : S, P x := by
  sorry

example ( t : S ) ( h : P t ) : ∃ x : S, P x := by
  sorry

example {Q:Prop} 
        ( h1 : ∃ x : S, P x )
        ( h2 : ∀ x : S, P x → Q )
        : Q := by
  sorry




/- The second group involves problems we have already done in English in class. -/


  

example ( h : ( ∀ x : S, P x → Q x ) 
              ∧ ( ∀ y : S, P y → R y ) ) 
        : (∀ x : S, P x → Q x ∧ R x) := by
  sorry



/- 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
  sorry



example ( h : ∀ x : S, P x ∧ Q x ) 
        : ( ∀ x : S, P x ) ∧ ( ∀ x : S, Q x )
        := by
  sorry


example ( h : ∃ x : S, P x ∨ Q x ) 
        : ( ∃ x : S, P x ) ∨ ( ∃ x : S, Q x ) 
        := by
  sorry





 

 /- The third group will require combining even more ideas.  We haven't done these in class yet. -/


open Classical 
/- This is a hint that we'll need the excluded middle or proof by contradiction somewhere. -/

theorem not_forall_from_exists_not { P:T → Prop }
  (h : ∃ x:T, ¬ P x) : ¬ ∀ x:T, P x := by
  sorry
  /- Our goal is to show ¬ ∀ x:T, P x. -/


theorem not_exists_from_forall_not { P:T → Prop }
  (h : ∀ x:T, ¬ P x) : ¬ ∃ x:T, P x := by
  sorry



theorem forall_not_from_not_exists { P:T → Prop }
  (h : ¬ ∃ x:T, P x) : ∀ x:T, ¬ P x := by
  sorry
    /- Our goal is ∀ x:T, ¬ P x. -/
    /- Now we need a plan.  Where will the contradiction come from?  The goal will be to contradict ¬ ∃ x, P x. -/



theorem exists_not_from_not_forall { P:T → Prop }
  (h : ¬ ∀ x:T, P x) : ∃ x:T, ¬ P x := by
  sorry
  /- Our goal is ∃ x:T, ¬ P x. -/





example ( h1 : ∀ x : S, P x ∨ Q x )
        ( h2 : ∃ x : S, ¬ Q x )
        : ∃ x : S, P x := by
  sorry