awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
mp₁₅ : c → a → b → ¬b → ¬c → a
mp₁₆ : c → ¬a → ¬b → b → c → a
mp₁₇ : c → ¬a → ¬b → ¬b → ¬c → a
mp₁₈ mp₁₉ : c → a → b → b → c → a
mp₂₀ : ¬c → a → ¬a → b → (b ↔ c)
mp₂₁ 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
mp₂₆ : ¬c → ¬a → b → ¬b → ¬c → a
mp₂₇ : ¬c → ¬¬a → ¬b → b → c → a
mp₂₈ mp₂₉ mp₃₀ : ¬c → ¬¬a → ¬b → ¬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₁₃ mpr₁₄ : a → b → c → a → b → c
mpr₁₅ : a → c → b → c → (a ↔ b)
mpr₁₆ : a → c → ¬b → ¬c → (a ↔ b)
mpr₁₇ : a → c → b → c → (a ↔ b)
mpr₁₈ : a → c → b → c → a → b
mpr₁₉ : a → c → b → c → b → 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)
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
mp₁₅ : c → a → b → ¬b → ¬c → a
mp₁₆ : c → ¬a → ¬b → b → c → a
mp₁₇ : c → ¬a → ¬b → ¬b → ¬c → a
mp₁₈ mp₁₉ : c → a → b → b → c → a
mp₂₀ : ¬c → a → ¬a → b → (b ↔ c)
mp₂₁ 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
mp₂₆ : ¬c → ¬a → b → ¬b → ¬c → a
mp₂₇ : ¬c → ¬¬a → ¬b → b → c → a
mp₂₈ mp₂₉ mp₃₀ : ¬c → ¬¬a → ¬b → ¬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₁₃ mpr₁₄ : a → b → c → a → b → c
mpr₁₅ : a → c → b → c → (a ↔ b)
mpr₁₆ : a → c → ¬b → ¬c → (a ↔ b)
mpr₁₇ : a → c → b → c → (a ↔ b)
mpr₁₈ : a → c → b → c → a → b
mpr₁₉ : a → c → b → c → b → 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)
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
mp₁₅ : c → a → b → ¬b → ¬c → a
mp₁₆ : c → ¬a → ¬b → b → c → a
mp₁₇ : c → ¬a → ¬b → ¬b → ¬c → a
mp₁₈ mp₁₉ : c → a → b → b → c → a
mp₂₀ : ¬c → a → ¬a → b → (b ↔ c)
mp₂₁ 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
mp₂₆ : ¬c → ¬a → b → ¬b → ¬c → a
mp₂₇ : ¬c → ¬¬a → ¬b → b → c → a
mp₂₈ mp₂₉ mp₃₀ : ¬c → ¬¬a → ¬b → ¬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₁₃ mpr₁₄ : a → b → c → a → b → c
mpr₁₅ : a → c → b → c → (a ↔ b)
mpr₁₆ : a → c → ¬b → ¬c → (a ↔ b)
mpr₁₇ : a → c → b → c → (a ↔ b)
mpr₁₈ : a → c → b → c → a → b
mpr₁₉ : a → c → b → c → b → a
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
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
mp₁₅ : c → a → b → ¬b → ¬c → a
mp₁₆ : c → ¬a → ¬b → b → c → a
mp₁₇ : c → ¬a → ¬b → ¬b → ¬c → a
mp₁₈ mp₁₉ : c → a → b → b → c → a
mp₂₀ : ¬c → a → ¬a → b → (b ↔ c)
mp₂₁ 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
mp₂₆ : ¬c → ¬a → b → ¬b → ¬c → a
mp₂₇ : ¬c → ¬¬a → ¬b → b → c → a
mp₂₈ mp₂₉ mp₃₀ : ¬c → ¬¬a → ¬b → ¬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₁₃ mpr₁₄ : a → b → c → a → b → c
mpr₁₅ : a → c → b → c → (a ↔ b)
mpr₁₆ : a → c → ¬b → ¬c → (a ↔ b)
mpr₁₇ : a → c → b → c → (a ↔ b)
mpr₁₈ : a → c → b → c → a → b
mpr₁₉ : a → c → b → c → b → a
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
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
mp₁₅ : c → a → b → ¬b → ¬c → a
mp₁₆ : c → ¬a → ¬b → b → c → a
mp₁₇ : c → ¬a → ¬b → ¬b → ¬c → a
mp₁₈ mp₁₉ : c → a → b → b → c → a
mp₂₀ : ¬c → a → ¬a → b → (b ↔ c)
mp₂₁ 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
mp₂₆ : ¬c → ¬a → b → ¬b → ¬c → a
mp₂₇ : ¬c → ¬¬a → ¬b → b → c → a
mp₂₈ mp₂₉ mp₃₀ : ¬c → ¬¬a → ¬b → ¬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₁₃ mpr₁₄ : a → b → c → a → b → c
mpr₁₅ : a → c → b → c → (a ↔ b)
mpr₁₆ : a → c → ¬b → ¬c → (a ↔ b)
mpr₁₇ : a → c → b → c → (a ↔ b)
mpr₁₈ : a → c → b → c → a → b
mpr₁₉ : a → c → b → c → b → 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₂₄ mpr₂₅ : ¬a → ¬b → c → ¬a → ¬b → c
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mpr₂₆ : ¬a → c → ¬b → 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)
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
mp₁₅ : c → a → b → ¬b → ¬c → a
mp₁₆ : c → ¬a → ¬b → b → c → a
mp₁₇ : c → ¬a → ¬b → ¬b → ¬c → a
mp₁₈ mp₁₉ : c → a → b → b → c → a
mp₂₀ : ¬c → a → ¬a → b → (b ↔ c)
mp₂₁ 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
mp₂₆ : ¬c → ¬a → b → ¬b → ¬c → a
mp₂₇ : ¬c → ¬¬a → ¬b → b → c → a
mp₂₈ mp₂₉ mp₃₀ : ¬c → ¬¬a → ¬b → ¬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₁₃ mpr₁₄ : a → b → c → a → b → c
mpr₁₅ : a → c → b → c → (a ↔ b)
mpr₁₆ : a → c → ¬b → ¬c → (a ↔ b)
mpr₁₇ : a → c → b → c → (a ↔ b)
mpr₁₈ : a → c → b → c → a → b
mpr₁₉ : a → c → b → c → b → 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₂₄ mpr₂₅ : ¬a → ¬b → c → ¬a → ¬b → c
mpr₂₆ : ¬a → c → ¬b → c → (a ↔ b)
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mpr₂₇ : ¬a → c → ¬¬b → ¬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)
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
mp₁₅ : c → a → b → ¬b → ¬c → a
mp₁₆ : c → ¬a → ¬b → b → c → a
mp₁₇ : c → ¬a → ¬b → ¬b → ¬c → a
mp₁₈ mp₁₉ : c → a → b → b → c → a
mp₂₀ : ¬c → a → ¬a → b → (b ↔ c)
mp₂₁ 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
mp₂₆ : ¬c → ¬a → b → ¬b → ¬c → a
mp₂₇ : ¬c → ¬¬a → ¬b → b → c → a
mp₂₈ mp₂₉ mp₃₀ : ¬c → ¬¬a → ¬b → ¬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₁₃ mpr₁₄ : a → b → c → a → b → c
mpr₁₅ : a → c → b → c → (a ↔ b)
mpr₁₆ : a → c → ¬b → ¬c → (a ↔ b)
mpr₁₇ : a → c → b → c → (a ↔ b)
mpr₁₈ : a → c → b → c → a → b
mpr₁₉ : a → c → b → c → b → 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₂₄ mpr₂₅ : ¬a → ¬b → c → ¬a → ¬b → c
mpr₂₆ : ¬a → c → ¬b → c → (a ↔ b)
mpr₂₇ : ¬a → c → ¬¬b → ¬c → (a ↔ b)
mpr₂₈ : ¬a → c → ¬b → c → (a ↔ b)
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mpr₂₉ : ¬a → c → ¬b → 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)
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
mp₁₅ : c → a → b → ¬b → ¬c → a
mp₁₆ : c → ¬a → ¬b → b → c → a
mp₁₇ : c → ¬a → ¬b → ¬b → ¬c → a
mp₁₈ mp₁₉ : c → a → b → b → c → a
mp₂₀ : ¬c → a → ¬a → b → (b ↔ c)
mp₂₁ 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
mp₂₆ : ¬c → ¬a → b → ¬b → ¬c → a
mp₂₇ : ¬c → ¬¬a → ¬b → b → c → a
mp₂₈ mp₂₉ mp₃₀ : ¬c → ¬¬a → ¬b → ¬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₁₃ mpr₁₄ : a → b → c → a → b → c
mpr₁₅ : a → c → b → c → (a ↔ b)
mpr₁₆ : a → c → ¬b → ¬c → (a ↔ b)
mpr₁₇ : a → c → b → c → (a ↔ b)
mpr₁₈ : a → c → b → c → a → b
mpr₁₉ : a → c → b → c → b → 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₂₄ mpr₂₅ : ¬a → ¬b → c → ¬a → ¬b → c
mpr₂₆ : ¬a → c → ¬b → c → (a ↔ b)
mpr₂₇ : ¬a → c → ¬¬b → ¬c → (a ↔ b)
mpr₂₈ : ¬a → c → ¬b → c → (a ↔ b)
mpr₂₉ : ¬a → c → ¬b → c → a → b
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
have mpr₃₀ : ¬a → c → ¬b → c → b → 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
mp₁₅ : c → a → b → ¬b → ¬c → a
mp₁₆ : c → ¬a → ¬b → b → c → a
mp₁₇ : c → ¬a → ¬b → ¬b → ¬c → a
mp₁₈ mp₁₉ : c → a → b → b → c → a
mp₂₀ : ¬c → a → ¬a → b → (b ↔ c)
mp₂₁ 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
mp₂₆ : ¬c → ¬a → b → ¬b → ¬c → a
mp₂₇ : ¬c → ¬¬a → ¬b → b → c → a
mp₂₈ mp₂₉ mp₃₀ : ¬c → ¬¬a → ¬b → ¬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₁₃ mpr₁₄ : a → b → c → a → b → c
mpr₁₅ : a → c → b → c → (a ↔ b)
mpr₁₆ : a → c → ¬b → ¬c → (a ↔ b)
mpr₁₇ : a → c → b → c → (a ↔ b)
mpr₁₈ : a → c → b → c → a → b
mpr₁₉ : a → c → b → c → b → 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₂₄ mpr₂₅ : ¬a → ¬b → c → ¬a → ¬b → c
mpr₂₆ : ¬a → c → ¬b → c → (a ↔ b)
mpr₂₇ : ¬a → c → ¬¬b → ¬c → (a ↔ b)
mpr₂₈ : ¬a → c → ¬b → c → (a ↔ b)
mpr₂₉ : ¬a → c → ¬b → c → a → b
mpr₃₀ : ¬a → c → ¬b → c → b → a
mp₃₁ mp₃₂ mp₃₃ : c → a → a → b → b → c
mp₃₄ mp₃₅ mp₃₆ : c → a → a → b → c → 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)
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
mp₁₅ : c → a → b → ¬b → ¬c → a
mp₁₆ : c → ¬a → ¬b → b → c → a
mp₁₇ : c → ¬a → ¬b → ¬b → ¬c → a
mp₁₈ mp₁₉ : c → a → b → b → c → a
mp₂₀ : ¬c → a → ¬a → b → (b ↔ c)
mp₂₁ 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
mp₂₆ : ¬c → ¬a → b → ¬b → ¬c → a
mp₂₇ : ¬c → ¬¬a → ¬b → b → c → a
mp₂₈ mp₂₉ mp₃₀ : ¬c → ¬¬a → ¬b → ¬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₁₃ mpr₁₄ : a → b → c → a → b → c
mpr₁₅ : a → c → b → c → (a ↔ b)
mpr₁₆ : a → c → ¬b → ¬c → (a ↔ b)
mpr₁₇ : a → c → b → c → (a ↔ b)
mpr₁₈ : a → c → b → c → a → b
mpr₁₉ : a → c → b → c → b → 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₂₄ mpr₂₅ : ¬a → ¬b → c → ¬a → ¬b → c
mpr₂₆ : ¬a → c → ¬b → c → (a ↔ b)
mpr₂₇ : ¬a → c → ¬¬b → ¬c → (a ↔ b)
mpr₂₈ : ¬a → c → ¬b → c → (a ↔ b)
mpr₂₉ : ¬a → c → ¬b → c → a → b
mpr₃₀ : ¬a → c → ¬b → c → b → a
mp₃₁ mp₃₂ mp₃₃ : c → a → a → b → b → c
mp₃₄ mp₃₅ mp₃₆ : c → a → a → b → c → b
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
mp₁₄ : c → a → b → b → c → a
mp₁₅ : c → a → b → ¬b → ¬c → a
mp₁₆ : c → ¬a → ¬b → b → c → a
mp₁₇ : c → ¬a → ¬b → ¬b → ¬c → a
mp₁₈ mp₁₉ : c → a → b → b → c → a
mp₂₀ : ¬c → a → ¬a → b → (b ↔ c)
mp₂₁ 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
mp₂₆ : ¬c → ¬a → b → ¬b → ¬c → a
mp₂₇ : ¬c → ¬¬a → ¬b → b → c → a
mp₂₈ mp₂₉ mp₃₀ : ¬c → ¬¬a → ¬b → ¬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₁₃ mpr₁₄ : a → b → c → a → b → c
mpr₁₅ : a → c → b → c → (a ↔ b)
mpr₁₆ : a → c → ¬b → ¬c → (a ↔ b)
mpr₁₇ : a → c → b → c → (a ↔ b)
mpr₁₈ : a → c → b → c → a → b
mpr₁₉ : a → c → b → c → b → 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₂₄ mpr₂₅ : ¬a → ¬b → c → ¬a → ¬b → c
mpr₂₆ : ¬a → c → ¬b → c → (a ↔ b)
mpr₂₇ : ¬a → c → ¬¬b → ¬c → (a ↔ b)
mpr₂₈ : ¬a → c → ¬b → c → (a ↔ b)
mpr₂₉ : ¬a → c → ¬b → c → a → b
mpr₃₀ : ¬a → c → ¬b → c → b → a
mp₃₁ mp₃₂ mp₃₃ : c → a → a → b → b → c
mp₃₄ mp₃₅ mp₃₆ : c → a → a → b → c → b
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
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mp₅ : a → (b ↔ c) → b → (a ↔ c)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mp₆ : a → (b ↔ c) → (a ↔ c) → b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
mp₆ : a → (b ↔ c) → (a ↔ c) → b
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mp₇ : ¬a → ¬(b ↔ c) → b → (a ↔ c)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
mp₆ : a → (b ↔ c) → (a ↔ c) → b
mp₇ : ¬a → ¬(b ↔ c) → b → (a ↔ c)
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mp₈ : ¬a → ¬(b ↔ c) → (a ↔ c) → b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
mp₆ : a → (b ↔ c) → (a ↔ c) → b
mp₇ : ¬a → ¬(b ↔ c) → b → (a ↔ c)
mp₈ : ¬a → ¬(b ↔ c) → (a ↔ c) → b
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
have mpr₁ : b → (a ↔ c) → (a ↔ (b ↔ c))
Tactic: tauto