This post is a work in progress.
World: Logo
Level 1
example (A B C : Prop) : ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) := by
tauto
Level 2
example : 42 = 42 := by
rfl
Level 3
example (n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n := by
assumption
Level 4
example (A : Prop) (hA : A) : A := by
assumption
Level 5
example : True := by
decide
Level 6
example : ¬False := by
decide
Level 7
example (A : Prop) (h : False) : A := by
contradiction
Level 8
example (n : ℕ) (h : n ≠ n) : n = 37 := by
contradiction
Level 9
example (n : ℕ) (h : n = 10) (g : n ≠ 10) : n = 42 := by
contradiction
Level 10
example (A B : Prop) (hA : A) (hB : B) : A ∧ B := by
constructor
assumption
assumption
Level 11
example (A B C : Prop) (h : A ∧ (B ∧ C)) : B := by
obtain ⟨h₁, h₂⟩ := h
obtain ⟨h₃, h₄⟩ := h₂
assumption
Level 12
example (A B : Prop) (hA : A) : A ∨ (¬ B) := by
left
assumption
Level 13
example (A B : Prop) (h : (A ∧ B) ∨ A) : A := by
obtain h | h := h
obtain ⟨h₁, h₂⟩ := h
assumption
assumption
Level 14
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
World: Implis
Level 1
example (A B : Prop) (hB : B) : A → (A ∧ B) := by
intro hA
constructor
assumption
assumption
Level 2
example (A B : Prop) (hA : A) (h : A → B) : B := by
revert hA
assumption
Level 3
example (A B : Prop) (h : A) (hAB : A → B) : B := by
apply hAB at h
assumption
Level 4
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
Level 5
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
Level 6
example (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by
constructor
assumption
assumption
Level 7
example (A B : Prop) (h : A ↔ B) : B ↔ A := by
symm at h
assumption
Level 8
example (A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C := by
rw [h₁]
rw [←h₂]
assumption
Level 9
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
Level 10
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
Level 11
example (A B : Prop) : (A ↔ B) → (A → B) := by
intro h
obtain ⟨mp, mpr⟩ := h
assumption
Level 12
example (A : Prop) : ¬A ∨ A := by
by_cases h : A
right
assumption
left
assumption
Level 13
example (A B C : Prop) : (A ∧ (¬¬C)) ∨ (¬¬B) ∧ C ↔ (A ∧ C) ∨ B ∧ (¬¬C) := by
rw [not_not, not_not]
Level 14
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
