awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
β : Type v
f : α → α
b : β
l : List β
H : ∀ (a : α), foldl (fun (b : α) (x : β) ↦ f b) a l = f^[l.length] a
a : α
cons : foldl (fun (b : α) (x : β) ↦ f b) a (b :: l) = f^[l.length + 1] a
⊢ foldl (fun (b : α) (x : β) ↦ f b) a (b :: l) = f^[(b :: l).length] a
have cons₁ : foldl (fun (b : α) (x : β) ↦ f b) (f a) l = f^[l.length + 1] a
Tactic: rw [length_cons, foldl, iterate_succ_apply, H]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
β : Type v
f : α → α
b : β
l : List β
H : ∀ (a : α), foldl (fun (b : α) (x : β) ↦ f b) a l = f^[l.length] a
a : α
cons : foldl (fun (b : α) (x : β) ↦ f b) a (b :: l) = f^[l.length + 1] a
cons₁ : foldl (fun (b : α) (x : β) ↦ f b) (f a) l = f^[l.length + 1] a
⊢ foldl (fun (b : α) (x : β) ↦ f b) a (b :: l) = f^[(b :: l).length] a
have cons₂ : foldl (fun (b : α) (x : β) ↦ f b) (f a) l = f^[l.length] (f a)
Tactic: rw [length_cons, foldl, iterate_succ_apply, H]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
β : Type v
f : α → α
b : β
l : List β
H : ∀ (a : α), foldl (fun (b : α) (x : β) ↦ f b) a l = f^[l.length] a
a : α
cons : foldl (fun (b : α) (x : β) ↦ f b) a (b :: l) = f^[l.length + 1] a
cons₁ : foldl (fun (b : α) (x : β) ↦ f b) (f a) l = f^[l.length + 1] a
cons₂ : foldl (fun (b : α) (x : β) ↦ f b) (f a) l = f^[l.length] (f a)
⊢ foldl (fun (b : α) (x : β) ↦ f b) a (b :: l) = f^[(b :: l).length] a
have cons₃ : f^[l.length] (f a) = f^[l.length] (f a)
Tactic: rw [length_cons, foldl, iterate_succ_apply, H]
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
β : Type v
f : α → α
a : α
l : List β
⊢ foldl (fun (b : α) (x : β) ↦ f b) a l = f^[l.length] a
have nil : ∀ (a : α), foldl (fun (b : α) (x : β) ↦ f b) a [] = f^[length.{v} (α := β) []] a
Tactic: induction l generalizing a with
  | nil => rfl
  | cons b l H => rw [length_cons, foldl, iterate_succ_apply, H]
Cleared hypotheses: a, l
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
β : Type v
f : α → α
a : α
l : List β
nil : ∀ (a : α), foldl (fun (b : α) (x : β) ↦ f b) a [] = f^[length.{v} (α := β) []] a
⊢ foldl (fun (b : α) (x : β) ↦ f b) a l = f^[l.length] a
have cons : ∀ (b : β) (l : List β) (H : ∀ (a : α), foldl (fun (b : α) (x : β) ↦ f b) a l = f^[l.length] a) (a : α),
  foldl (fun (b : α) (x : β) ↦ f b) a (b :: l) = f^[(b :: l).length] a
Tactic: induction l generalizing a with
  | nil => rfl
  | cons b l H => rw [length_cons, foldl, iterate_succ_apply, H]
Cleared hypotheses: a, l
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
β : Type v
f : β → β
b : β
a : α
l : List α
⊢ foldr (fun (x : α) ↦ f) b (a :: l) = f^[(a :: l).length] b
have rw : foldr (fun (x : α) ↦ f) b (a :: l) = f^[l.length + 1] b
Tactic: rw [length_cons, foldr, foldr_const f b l, iterate_succ_apply']
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
β : Type v
f : β → β
b : β
a : α
l : List α
rw : foldr (fun (x : α) ↦ f) b (a :: l) = f^[l.length + 1] b
⊢ foldr (fun (x : α) ↦ f) b (a :: l) = f^[(a :: l).length] b
have rw₁ : f (foldr (fun (x : α) ↦ f) b l) = f^[l.length + 1] b
Tactic: rw [length_cons, foldr, foldr_const f b l, iterate_succ_apply']
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
β : Type v
f : β → β
b : β
a : α
l : List α
rw : foldr (fun (x : α) ↦ f) b (a :: l) = f^[l.length + 1] b
rw₁ : f (foldr (fun (x : α) ↦ f) b l) = f^[l.length + 1] b
⊢ foldr (fun (x : α) ↦ f) b (a :: l) = f^[(a :: l).length] b
have rw₂ : f (f^[l.length] b) = f^[l.length + 1] b
Tactic: rw [length_cons, foldr, foldr_const f b l, iterate_succ_apply']
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
α : Type u
β : Type v
f : β → β
b : β
a : α
l : List α
rw : foldr (fun (x : α) ↦ f) b (a :: l) = f^[l.length + 1] b
rw₁ : f (foldr (fun (x : α) ↦ f) b l) = f^[l.length + 1] b
rw₂ : f (f^[l.length] b) = f^[l.length + 1] b
⊢ foldr (fun (x : α) ↦ f) b (a :: l) = f^[(a :: l).length] b
have rw₃ : f (f^[l.length] b) = f (f^[l.length] b)
Tactic: rw [length_cons, foldr, foldr_const f b l, iterate_succ_apply']
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
n : ℕ
⊢ (Pi.map (α := α) (β := α) f)^[n] = Pi.map (α := α) (β := α) fun (i : ι) ↦ (f i)^[n]
have zero : (Pi.map (α := α) (β := α) f)^[0] = Pi.map (α := α) (β := α) fun (i : ι) ↦ (f i)^[0]
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Logic.Function.Iterate (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
n : ℕ
zero : (Pi.map (α := α) (β := α) f)^[0] = Pi.map (α := α) (β := α) fun (i : ι) ↦ (f i)^[0]
⊢ (Pi.map (α := α) (β := α) f)^[n] = Pi.map (α := α) (β := α) fun (i : ι) ↦ (f i)^[n]
have succ : ∀ (n : ℕ),
  ((Pi.map (α := α) (β := α) f)^[n] = Pi.map (α := α) (β := α) fun (i : ι) ↦ (f i)^[n]) →
    (Pi.map (α := α) (β := α) f)^[n + 1] = Pi.map (α := α) (β := α) fun (i : ι) ↦ (f i)^[n + 1]
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Logic.Function.ULift (goal)
Goal:
α : Type u_1
a b : ULift.{u_2, u_1} α
h : a = b
⊢ a.down = b.down
have rw : b.down = b.down
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Logic.Function.ULift (goal)
Goal:
α : Sort u_1
a b : PLift α
h : a = b
⊢ a.down = b.down
have rw : b.down = b.down
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Logic.Godel.GodelBetaFunction (hypothesis)
Goal:
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
⊢ False
have this : p ∣ (m - n) * a
Tactic: have : p ∣ (m - n) * a := by
      simpa [Nat.succ_sub_succ, ← Nat.mul_sub_right_distrib] using
        Nat.dvd_sub hm hn
-- Lean 4 proof step from Mathlib.Logic.Godel.GodelBetaFunction (goal)
Goal:
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
⊢ p ∣ a
have inl : ∀ (hp : p ∣ m - n), p ∣ a
Tactic: rcases (Nat.Prime.dvd_mul pp).mp this with (hp | hp)
-- Lean 4 proof step from Mathlib.Logic.Godel.GodelBetaFunction (goal)
Goal:
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
inl : ∀ (hp : p ∣ m - n), p ∣ a
⊢ p ∣ a
have inr : ∀ (hp : p ∣ a), p ∣ a
Tactic: rcases (Nat.Prime.dvd_mul pp).mp this with (hp | hp)
-- Lean 4 proof step from Mathlib.Logic.Godel.GodelBetaFunction (hypothesis)
Goal:
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
⊢ False
have this₁ : p ∣ a
Tactic: have : p ∣ a := by
      rcases (Nat.Prime.dvd_mul pp).mp this with (hp | hp)
      · exact Nat.dvd_trans hp ha
      · exact hp
-- Lean 4 proof step from Mathlib.Logic.Godel.GodelBetaFunction (goal)
Goal:
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this_1 : p ∣ (m - n) * a
this : p ∣ a
⊢ False
have apply : p = 1
Tactic: apply pp.ne_one
-- Lean 4 proof step from Mathlib.Logic.Godel.GodelBetaFunction (hypothesis)
Goal:
m : ℕ
a : Fin m → ℕ
i : Fin m
⊢ a i < coprimes a i
have h₁ : a i < supOfSeq a
Tactic: have h₁ : a i < supOfSeq a :=
    Nat.lt_add_one_iff.mpr (le_max_of_le_right <| Finset.le_sup (by simp))
-- Lean 4 proof step from Mathlib.Logic.Godel.GodelBetaFunction (hypothesis)
Goal:
m : ℕ
a : Fin m → ℕ
i : Fin m
h₁ : a i < supOfSeq a
⊢ a i < coprimes a i
have h₂ : supOfSeq a ≤ ((↑i : ℕ) + 1) * (supOfSeq a)! + 1
Tactic: have h₂ : supOfSeq a ≤ (i + 1) * (supOfSeq a)! + 1 :=
    le_trans (self_le_factorial _) (le_trans (Nat.le_mul_of_pos_left (supOfSeq a)! (succ_pos i))
      (le_add_right _ _))
-- Lean 4 proof step from Mathlib.Logic.Godel.GodelBetaFunction (goal)
Goal:
m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
⊢ (Coprime on coprimes a) i j
have inr : ∀ (this : ∀ {m : ℕ} (a : Fin m → ℕ) ⦃i j : Fin m⦄ (hij : i ≠ j) (ltij : i < j), (Coprime on coprimes a) i j)
  (ltij : j ≤ i), (Coprime on coprimes a) i j
Tactic: wlog! ltij : i < j
-- Lean 4 proof step from Mathlib.Logic.Godel.GodelBetaFunction (goal)
Goal:
m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
inr :
  ∀ (this : ∀ {m : ℕ} (a : Fin m → ℕ) ⦃i j : Fin m⦄ (hij : i ≠ j) (ltij : i < j), (Coprime on coprimes a) i j)
    (ltij : j ≤ i), (Coprime on coprimes a) i j
⊢ (Coprime on coprimes a) i j
have wlog! : ∀ {m : ℕ} (a : Fin m → ℕ) ⦃i j : Fin m⦄ (hij : i ≠ j) (ltij : i < j), (Coprime on coprimes a) i j
Tactic: wlog! ltij : i < j
Cleared hypotheses: a, i, j, hij
-- Lean 4 proof step from Mathlib.Logic.Godel.GodelBetaFunction (hypothesis)
Goal:
m_1 m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
ltij : i < j
⊢ (((↑i : ℕ) + 1) * (supOfSeq a)! + 1).Coprime (((↑j : ℕ) + 1) * (supOfSeq a)! + 1)
have hja : (↑j : ℕ) < supOfSeq a
Tactic: have hja : j < supOfSeq a := lt_of_lt_of_le j.prop (le_succ_of_le (le_max_left _ _))
-- Lean 4 proof step from Mathlib.Logic.IsEmpty.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
⊢ IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β
have rw : (∃ (a : α), IsEmpty β) ↔ Nonempty α ∧ IsEmpty β
Tactic: rw [isEmpty_pi, ← exists_true_iff_nonempty, ← exists_and_right, true_and]
-- Lean 4 proof step from Mathlib.Logic.IsEmpty.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
rw : (∃ (a : α), IsEmpty β) ↔ Nonempty α ∧ IsEmpty β
⊢ IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β
have rw₁ : (∃ (a : α), IsEmpty β) ↔ (∃ (x : α), True) ∧ IsEmpty β
Tactic: rw [isEmpty_pi, ← exists_true_iff_nonempty, ← exists_and_right, true_and]
-- Lean 4 proof step from Mathlib.Logic.IsEmpty.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
rw : (∃ (a : α), IsEmpty β) ↔ Nonempty α ∧ IsEmpty β
rw₁ : (∃ (a : α), IsEmpty β) ↔ (∃ (x : α), True) ∧ IsEmpty β
⊢ IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β
have rw₂ : (∃ (a : α), IsEmpty β) ↔ ∃ (x : α), True ∧ IsEmpty β
Tactic: rw [isEmpty_pi, ← exists_true_iff_nonempty, ← exists_and_right, true_and]
-- Lean 4 proof step from Mathlib.Logic.IsEmpty.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
rw : (∃ (a : α), IsEmpty β) ↔ Nonempty α ∧ IsEmpty β
rw₁ : (∃ (a : α), IsEmpty β) ↔ (∃ (x : α), True) ∧ IsEmpty β
rw₂ : (∃ (a : α), IsEmpty β) ↔ ∃ (x : α), True ∧ IsEmpty β
⊢ IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β
have rw₃ : (∃ (a : α), IsEmpty β) ↔ ∃ (x : α), IsEmpty β
Tactic: rw [isEmpty_pi, ← exists_true_iff_nonempty, ← exists_and_right, true_and]
-- Lean 4 proof step from Mathlib.Logic.IsEmpty.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
⊢ ¬Nonempty (α → β) ↔ ¬(IsEmpty α ∨ Nonempty β)
have rw : ¬Nonempty (α → β) ↔ ¬IsEmpty α ∧ ¬Nonempty β
Tactic: rw [not_or, not_nonempty_iff, not_nonempty_iff, isEmpty_fun, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Logic.IsEmpty.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
rw : ¬Nonempty (α → β) ↔ ¬IsEmpty α ∧ ¬Nonempty β
⊢ ¬Nonempty (α → β) ↔ ¬(IsEmpty α ∨ Nonempty β)
have rw₁ : IsEmpty (α → β) ↔ ¬IsEmpty α ∧ ¬Nonempty β
Tactic: rw [not_or, not_nonempty_iff, not_nonempty_iff, isEmpty_fun, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Logic.IsEmpty.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
rw : ¬Nonempty (α → β) ↔ ¬IsEmpty α ∧ ¬Nonempty β
rw₁ : IsEmpty (α → β) ↔ ¬IsEmpty α ∧ ¬Nonempty β
⊢ ¬Nonempty (α → β) ↔ ¬(IsEmpty α ∨ Nonempty β)
have rw₂ : IsEmpty (α → β) ↔ ¬IsEmpty α ∧ IsEmpty β
Tactic: rw [not_or, not_nonempty_iff, not_nonempty_iff, isEmpty_fun, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Logic.IsEmpty.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
rw : ¬Nonempty (α → β) ↔ ¬IsEmpty α ∧ ¬Nonempty β
rw₁ : IsEmpty (α → β) ↔ ¬IsEmpty α ∧ ¬Nonempty β
rw₂ : IsEmpty (α → β) ↔ ¬IsEmpty α ∧ IsEmpty β
⊢ ¬Nonempty (α → β) ↔ ¬(IsEmpty α ∨ Nonempty β)
have rw₃ : Nonempty α ∧ IsEmpty β ↔ ¬IsEmpty α ∧ IsEmpty β
Tactic: rw [not_or, not_nonempty_iff, not_nonempty_iff, isEmpty_fun, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Logic.IsEmpty.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
rw : ¬Nonempty (α → β) ↔ ¬IsEmpty α ∧ ¬Nonempty β
rw₁ : IsEmpty (α → β) ↔ ¬IsEmpty α ∧ ¬Nonempty β
rw₂ : IsEmpty (α → β) ↔ ¬IsEmpty α ∧ IsEmpty β
rw₃ : Nonempty α ∧ IsEmpty β ↔ ¬IsEmpty α ∧ IsEmpty β
⊢ ¬Nonempty (α → β) ↔ ¬(IsEmpty α ∨ Nonempty β)
have rw₄ : Nonempty α ∧ IsEmpty β ↔ Nonempty α ∧ IsEmpty β
Tactic: rw [not_or, not_nonempty_iff, not_nonempty_iff, isEmpty_fun, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mp₂ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₂ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₃ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₄ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mp₅ : (a ↔ b) → c → a → (b ↔ c)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₂ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₃ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₄ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₅ : (a ↔ b) → c → a → (b ↔ c)
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mp₆ : (a ↔ b) → c → (b ↔ c) → a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₂ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₃ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₄ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₅ : (a ↔ b) → c → a → (b ↔ c)
mp₆ : (a ↔ b) → c → (b ↔ c) → a
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mp₇ : ¬(a ↔ b) → ¬c → a → (b ↔ c)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₂ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₃ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₄ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₅ : (a ↔ b) → c → a → (b ↔ c)
mp₆ : (a ↔ b) → c → (b ↔ c) → a
mp₇ : ¬(a ↔ b) → ¬c → a → (b ↔ c)
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mp₈ : ¬(a ↔ b) → ¬c → (b ↔ c) → a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₂ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₃ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₄ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₅ : (a ↔ b) → c → a → (b ↔ c)
mp₆ : (a ↔ b) → c → (b ↔ c) → a
mp₇ : ¬(a ↔ b) → ¬c → a → (b ↔ c)
mp₈ : ¬(a ↔ b) → ¬c → (b ↔ c) → a
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mpr₁ : a → (b ↔ c) → ((a ↔ b) ↔ c)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₂ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₃ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₄ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₅ : (a ↔ b) → c → a → (b ↔ c)
mp₆ : (a ↔ b) → c → (b ↔ c) → a
mp₇ : ¬(a ↔ b) → ¬c → a → (b ↔ c)
mp₈ : ¬(a ↔ b) → ¬c → (b ↔ c) → a
mpr₁ : a → (b ↔ c) → ((a ↔ b) ↔ c)
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mpr₂ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₂ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₃ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₄ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₅ : (a ↔ b) → c → a → (b ↔ c)
mp₆ : (a ↔ b) → c → (b ↔ c) → a
mp₇ : ¬(a ↔ b) → ¬c → a → (b ↔ c)
mp₈ : ¬(a ↔ b) → ¬c → (b ↔ c) → a
mpr₁ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₂ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₃ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₄ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mpr₅ : a → (b ↔ c) → (a ↔ b) → c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₂ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₃ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₄ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₅ : (a ↔ b) → c → a → (b ↔ c)
mp₆ : (a ↔ b) → c → (b ↔ c) → a
mp₇ : ¬(a ↔ b) → ¬c → a → (b ↔ c)
mp₈ : ¬(a ↔ b) → ¬c → (b ↔ c) → a
mpr₁ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₂ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₃ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₄ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₅ : a → (b ↔ c) → (a ↔ b) → c
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mpr₆ : a → (b ↔ c) → c → (a ↔ b)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₂ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₃ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₄ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₅ : (a ↔ b) → c → a → (b ↔ c)
mp₆ : (a ↔ b) → c → (b ↔ c) → a
mp₇ : ¬(a ↔ b) → ¬c → a → (b ↔ c)
mp₈ : ¬(a ↔ b) → ¬c → (b ↔ c) → a
mpr₁ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₂ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₃ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₄ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₅ : a → (b ↔ c) → (a ↔ b) → c
mpr₆ : a → (b ↔ c) → c → (a ↔ b)
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mpr₇ : ¬a → ¬(b ↔ c) → (a ↔ b) → c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₂ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₃ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₄ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₅ : (a ↔ b) → c → a → (b ↔ c)
mp₆ : (a ↔ b) → c → (b ↔ c) → a
mp₇ : ¬(a ↔ b) → ¬c → a → (b ↔ c)
mp₈ : ¬(a ↔ b) → ¬c → (b ↔ c) → a
mpr₁ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₂ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₃ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₄ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₅ : a → (b ↔ c) → (a ↔ b) → c
mpr₆ : a → (b ↔ c) → c → (a ↔ b)
mpr₇ : ¬a → ¬(b ↔ c) → (a ↔ b) → c
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mpr₈ : ¬a → ¬(b ↔ c) → c → (a ↔ b)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₂ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₃ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₄ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₅ : (a ↔ b) → c → a → (b ↔ c)
mp₆ : (a ↔ b) → c → (b ↔ c) → a
mp₇ : ¬(a ↔ b) → ¬c → a → (b ↔ c)
mp₈ : ¬(a ↔ b) → ¬c → (b ↔ c) → a
mpr₁ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₂ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₃ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₄ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₅ : a → (b ↔ c) → (a ↔ b) → c
mpr₆ : a → (b ↔ c) → c → (a ↔ b)
mpr₇ : ¬a → ¬(b ↔ c) → (a ↔ b) → c
mpr₈ : ¬a → ¬(b ↔ c) → c → (a ↔ b)
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mp₉ : c → a → a → b → (b ↔ c)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₂ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₃ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₄ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₅ : (a ↔ b) → c → a → (b ↔ c)
mp₆ : (a ↔ b) → c → (b ↔ c) → a
mp₇ : ¬(a ↔ b) → ¬c → a → (b ↔ c)
mp₈ : ¬(a ↔ b) → ¬c → (b ↔ c) → a
mpr₁ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₂ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₃ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₄ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₅ : a → (b ↔ c) → (a ↔ b) → c
mpr₆ : a → (b ↔ c) → c → (a ↔ b)
mpr₇ : ¬a → ¬(b ↔ c) → (a ↔ b) → c
mpr₈ : ¬a → ¬(b ↔ c) → c → (a ↔ b)
mp₉ : c → a → a → b → (b ↔ c)
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mp₁₀ : c → a → ¬a → ¬b → (b ↔ c)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₂ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₃ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₄ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₅ : (a ↔ b) → c → a → (b ↔ c)
mp₆ : (a ↔ b) → c → (b ↔ c) → a
mp₇ : ¬(a ↔ b) → ¬c → a → (b ↔ c)
mp₈ : ¬(a ↔ b) → ¬c → (b ↔ c) → a
mpr₁ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₂ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₃ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₄ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₅ : a → (b ↔ c) → (a ↔ b) → c
mpr₆ : a → (b ↔ c) → c → (a ↔ b)
mpr₇ : ¬a → ¬(b ↔ c) → (a ↔ b) → c
mpr₈ : ¬a → ¬(b ↔ c) → c → (a ↔ b)
mp₉ : c → a → a → b → (b ↔ c)
mp₁₀ : c → a → ¬a → ¬b → (b ↔ c)
mp₁₁ : c → a → a → b → (b ↔ c)
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mp₁₂ : c → a → a → b → b → c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₂ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₃ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₄ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₅ : (a ↔ b) → c → a → (b ↔ c)
mp₆ : (a ↔ b) → c → (b ↔ c) → a
mp₇ : ¬(a ↔ b) → ¬c → a → (b ↔ c)
mp₈ : ¬(a ↔ b) → ¬c → (b ↔ c) → a
mpr₁ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₂ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₃ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₄ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₅ : a → (b ↔ c) → (a ↔ b) → c
mpr₆ : a → (b ↔ c) → c → (a ↔ b)
mpr₇ : ¬a → ¬(b ↔ c) → (a ↔ b) → c
mpr₈ : ¬a → ¬(b ↔ c) → c → (a ↔ b)
mp₉ : c → a → a → b → (b ↔ c)
mp₁₀ : c → a → ¬a → ¬b → (b ↔ c)
mp₁₁ : c → a → a → b → (b ↔ c)
mp₁₂ : c → a → a → b → b → c
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mp₁₃ : c → a → a → b → c → b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₂ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₃ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₄ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₅ : (a ↔ b) → c → a → (b ↔ c)
mp₆ : (a ↔ b) → c → (b ↔ c) → a
mp₇ : ¬(a ↔ b) → ¬c → a → (b ↔ c)
mp₈ : ¬(a ↔ b) → ¬c → (b ↔ c) → a
mpr₁ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₂ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₃ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₄ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₅ : a → (b ↔ c) → (a ↔ b) → c
mpr₆ : a → (b ↔ c) → c → (a ↔ b)
mpr₇ : ¬a → ¬(b ↔ c) → (a ↔ b) → c
mpr₈ : ¬a → ¬(b ↔ c) → c → (a ↔ b)
mp₉ : c → a → a → b → (b ↔ c)
mp₁₀ : c → a → ¬a → ¬b → (b ↔ c)
mp₁₁ : c → a → a → b → (b ↔ c)
mp₁₂ : c → a → a → b → b → c
mp₁₃ : c → a → a → b → c → b
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mp₁₄ : c → a → b → b → c → a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₂ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₃ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₄ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₅ : (a ↔ b) → c → a → (b ↔ c)
mp₆ : (a ↔ b) → c → (b ↔ c) → a
mp₇ : ¬(a ↔ b) → ¬c → a → (b ↔ c)
mp₈ : ¬(a ↔ b) → ¬c → (b ↔ c) → a
mpr₁ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₂ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₃ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₄ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₅ : a → (b ↔ c) → (a ↔ b) → c
mpr₆ : a → (b ↔ c) → c → (a ↔ b)
mpr₇ : ¬a → ¬(b ↔ c) → (a ↔ b) → c
mpr₈ : ¬a → ¬(b ↔ c) → c → (a ↔ b)
mp₉ : c → a → a → b → (b ↔ c)
mp₁₀ : c → a → ¬a → ¬b → (b ↔ c)
mp₁₁ : c → a → a → b → (b ↔ c)
mp₁₂ : c → a → a → b → b → c
mp₁₃ : c → a → a → b → c → b
mp₁₄ : c → a → b → b → c → a
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mp₁₅ : c → a → b → ¬b → ¬c → a
Tactic: tauto