example (A B C : Prop) : ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) := by
  tauto

example : 42 = 42 := by
  rfl

example (n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n := by
  assumption

example (A : Prop) (hA : A) : A := by
  assumption

example : True := by
  decide

example : ¬False := by
  decide

example (A : Prop) (h : False) : A := by
  contradiction

example (n : ℕ) (h : n ≠ n) : n = 37 := by
  contradiction

example (n : ℕ) (h : n = 10) (g : n ≠ 10) : n = 42 := by
  contradiction

example (A B : Prop) (hA : A) (hB : B) : A ∧ B := by
  constructor
  assumption
  assumption

example (A B C : Prop) (h : A ∧ (B ∧ C)) : B := by
  obtain ⟨h₁, h₂⟩ := h
  obtain ⟨h₃, h₄⟩ := h₂
  assumption

example (A B : Prop) (hA : A) : A ∨ (¬ B) := by
  left
  assumption

example (A B : Prop) (h : (A ∧ B) ∨ A) : A := by
  obtain h | h := h
  obtain ⟨h₁, h₂⟩ := h
  assumption
  assumption

example (A B C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) := by
  constructor
  obtain h | h := h
  left
  assumption
  obtain ⟨h₁, h₂⟩ := h
  right
  assumption
  obtain h | h := h
  left
  assumption
  obtain ⟨h₁, h₂⟩ := h
  right
  assumption

example (A B : Prop) (hB : B) : A → (A ∧ B) := by
  intro hA
  constructor
  assumption
  assumption

example (A B : Prop) (hA : A) (h : A → B) : B := by
  revert hA
  assumption

example (A B : Prop) (h : A) (hAB : A → B) : B := by
  apply hAB at h
  assumption

example (A B C : Prop) (f : A → B) (g : B → C) : A → C := by
  intro h
  apply f at h
  apply g at h
  assumption

example
    (A B C D E F G H I : Prop)
    (f : A → B) (g : C → B) (h : A → D) (i : B → E) 
    (j : C → F) (k : E → D) (l : E → F) (m : G → D)
    (n : H → E) (p : F → I) (q : H → G) (r : H → I) :
    A → I := by
  intro hA
  apply f at hA
  apply i at hA
  apply l at hA
  apply p at hA
  assumption

example (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by
  constructor
  assumption
  assumption

example (A B : Prop) (h : A ↔ B) : B ↔ A := by
  symm at h
  assumption

example (A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C := by
  rw [h₁]
  rw [←h₂]
  assumption

example (A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C := by
  trans A
  symm at h₂
  assumption
  trans D
  assumption
  symm at h₁
  assumption

example (A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by
  intro f
  apply (h.mp) at f
  apply g at f
  assumption

example (A B : Prop) : (A ↔ B) → (A → B) := by
  intro h
  obtain ⟨mp, mpr⟩ := h
  assumption

example (A : Prop) : ¬A ∨ A := by
  by_cases h : A
  right
  assumption
  left
  assumption

example (A B C : Prop) : (A ∧ (¬¬C)) ∨ (¬¬B) ∧ C ↔ (A ∧ C) ∨ B ∧ (¬¬C) := by
  rw [not_not, not_not]

theorem imp_iff_not_or {A B : Prop} : (A → B) ↔ ¬ A ∨ B := by
  constructor
  by_cases hA: A
  intro hAB
  apply hAB at hA
  right
  assumption
  intro hAB
  left
  assumption
  intro hNAB
  intro hA
  obtain hNAB | hNAB := hNAB
  contradiction
  assumption

example (x y : ℚ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
  ring

example (P : MvPolynomial (Fin 2) ℚ) : (X 0) * P = P * (X 0) := by
  ring

example (a b c : MvPolynomial (Fin 4) ℕ ) : a * b * c = a * (b * c) := by
  ring

example (a b c d : ℝ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
  rw [←h₂, h₁, h₃]

example
    (A B : MvPolynomial (Fin 4) ℝ)
    (hA : A = (X 0)*(X 3) - (X 1)*(X 2))
    (hB : B = (X 0)*(X 2) + (X 1)*(X 3)) :
    ((X 0)^2 + (X 1)^2) * ((X 2)^2 + (X 3)^2) = A^2 + B^2 := by
  rw [hA, hB]
  ring

example : Nonempty ℕ := by
  use 42

example (A : Type) (h : Nonempty A) : ∃ a : A, a = a := by
  obtain ⟨a⟩ := h
  use a

example : Even 42 := by
  decide

theorem Nat.even_square (n : ℕ) (h : Even n) : Even (n ^ 2) := by
  unfold Even at *
  choose s hs using h
  let r := 2 * s^2
  use r
  rw [hs]
  ring

example (i : ℕ) (h : Odd i): (-1 : ℤ)^i + 1 = 0 := by
  unfold Odd at *
  choose s hs using h
  rw [hs]
  rw [Odd.neg_pow]
  ring
  tauto

example (i : ℕ): (-1 : ℤ)^i + (-1 : ℤ)^(i+1) = 0 := by
  ring

example : ∀ (x : ℕ), (Even x) → Odd (1 + x) := by
  intro x
  unfold Even
  unfold Odd
  intro h
  choose s hs using h
  use s
  rw [hs]
  ring

example {X : Type} (P : X → Prop) : ¬ (∃ x : X, P x) ↔ ∀ x : X, ¬ P x := by
  push_neg
  ring

example : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , Odd (n + k) := by
  push_neg
  intro n
  use n
  rw [← even_iff_not_odd]
  tauto

example
    {People : Type}
    [h_nonempty : Nonempty People]
    (isDrinking : People → Prop) :
    ∃ (x : People), isDrinking x → ∀ (y : People), isDrinking y := by
  by_cases h : ∀ (y : People), isDrinking y
  · obtain ⟨p⟩ := h_nonempty
    use p
    intro
    assumption
  · push_neg at h
    obtain ⟨p, h⟩ := h
    use p
    intro h_false
    contradiction

example (A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by
  obtain ⟨k₁, k₂⟩ := k

  have g : ¬ B := by
    apply h at k₁
    assumption

  contradiction

example (A B : Prop) (h : A → ¬ B) (k₁ : A) (k₂ : B) : False := by
  suffices g : ¬ B
  contradiction
  apply h at k₁
  assumption

example (A B : Prop) (g : A → B) (b : ¬ B) : ¬ A := by
  by_contra h
  suffices k : B
  contradiction
  apply g at h
  assumption

theorem not_imp_not (A B : Prop) : A → B ↔ (¬ B → ¬ A) := by
  constructor
  intro h
  intro g
  by_contra f
  apply h at f
  contradiction
  intro h
  intro g
  by_contra f
  apply h at f
  contradiction

example (n : ℕ) (h : Odd (n ^ 2)): Odd n := by
  revert h
  contrapose
  rw [← even_iff_not_odd]
  rw [← even_iff_not_odd]
  apply even_square

example (n : ℕ) (h : Odd (n ^ 2)) : Odd n := by
  by_contra g
  suffices f : ¬ Odd (n^2)
  contradiction
  rw [← even_iff_not_odd] at g
  rw [← even_iff_not_odd]
  apply even_square at g
  assumption