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

open Classical

theorem not_not_from { P : Prop } : P → ¬ ¬ P := by
  intro hp
  intro hnp
  contradiction

theorem from_not_not { P : Prop } : ¬ ¬ P → P := by
  intro hnnp
  have emp := em P
  apply Or.elim emp
  · intro hp
    exact hp
  · intro hnp
    contradiction

theorem iff_not_not { P : Prop } : P ↔ ¬ ¬ P := by
  apply Iff.intro
  · intro hp
    apply not_not_from
    exact hp
  · intro hnnp
    apply from_not_not
    exact hnnp

theorem exists_not_from_not_forall 
  { S : Type } { P : S → Prop } 
  (h : ¬ ∀ x : S, P x )
  : ∃ x : S, ¬ P x := by
    apply byContradiction
    intro h1
    apply h
    intro t
    apply byContradiction
    intro hnpt
    apply h1
    apply Exists.intro t
    exact hnpt

  
theorem or_not_from_not_and
  { P Q : Prop }
  ( h : ¬ ( P ∧ Q ) )
  : ¬ P ∨ ¬ Q := by
    apply byContradiction
    intro hn
    apply h
    apply And.intro
    · apply byContradiction 
      intro hnp
      apply hn
      apply Or.intro_left
      exact hnp
    · apply byContradiction
      intro hnq
      apply hn
      apply Or.intro_right
      exact hnq

theorem contrapositive ( P Q : Prop ) ( h : ¬ Q → ¬ P )
  : P → Q := by
    intro hp
    apply byContradiction
    intro hnq
    have hnp := h hnq
    contradiction

example { P Q R : Prop } 
  ( h : Q → ¬ P )
  : P → ¬ (Q ∧ R)  := by
    apply contrapositive
    intro h1
    apply h
    have h2 := from_not_not h1
    have ⟨ hq, hr ⟩ := h2
    exact hq



example { P Q R : Prop } 
  ( h : Q → ¬ P )
  : P → ¬ (Q ∧ R)  := by
    intro hp
    intro hqr
    have ⟨ hq, hr ⟩ := hqr
    have hnp := h hq
    contradiction




example { P Q : Prop } :
  ¬ ( P ∧ Q ) → ( ¬ P ∨ ¬ Q ) := by
    have emp := em P
    have emq := em Q
    apply Or.elim emp
    · intro hp
      apply Or.elim emq
      · intro hq
        simp [hp,hq]
      · intro hnq
        simp [hp,hnq]
    · intro hnp
      apply Or.elim emq
      · intro hq
        simp [hnp,hq]
      · intro hnq
        simp [hnp,hnq]