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 ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₉ : ¬c → b → ¬a → b → a → c
mp₃₀ : ¬c → b → ¬a → b → c → a
mpr₉ : b → a → c → a → b → c
mpr₁₀ : b → a → c → ¬a → ¬b → c
mpr₁₁ : b → ¬a → ¬c → a → b → c
mpr₁₂ : b → ¬a → ¬c → ¬a → ¬b → c
mpr₁₃ mpr₁₄ : b → a → c → a → b → c
mpr₁₅ : b → c → a → c → (a ↔ b)
mpr₁₆ : b → c → ¬a → ¬c → (a ↔ b)
mpr₁₇ : b → c → a → c → (a ↔ b)
mpr₁₈ : b → c → a → c → a → b
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mpr₁₉ : b → c → a → c → b → a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₉ : ¬c → b → ¬a → b → a → c
mp₃₀ : ¬c → b → ¬a → b → c → a
mpr₉ : b → a → c → a → b → c
mpr₁₀ : b → a → c → ¬a → ¬b → c
mpr₁₁ : b → ¬a → ¬c → a → b → c
mpr₁₂ : b → ¬a → ¬c → ¬a → ¬b → c
mpr₁₃ mpr₁₄ : b → a → c → a → b → c
mpr₁₅ : b → c → a → c → (a ↔ b)
mpr₁₆ : b → c → ¬a → ¬c → (a ↔ b)
mpr₁₇ : b → c → a → c → (a ↔ b)
mpr₁₈ : b → c → a → c → a → b
mpr₁₉ : b → c → a → c → b → a
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
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) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₉ : ¬c → b → ¬a → b → a → c
mp₃₀ : ¬c → b → ¬a → b → c → a
mpr₉ : b → a → c → a → b → c
mpr₁₀ : b → a → c → ¬a → ¬b → c
mpr₁₁ : b → ¬a → ¬c → a → b → c
mpr₁₂ : b → ¬a → ¬c → ¬a → ¬b → c
mpr₁₃ mpr₁₄ : b → a → c → a → b → c
mpr₁₅ : b → c → a → c → (a ↔ b)
mpr₁₆ : b → c → ¬a → ¬c → (a ↔ b)
mpr₁₇ : b → c → a → c → (a ↔ b)
mpr₁₈ : b → c → a → c → a → b
mpr₁₉ : b → c → a → c → b → a
mpr₂₀ : ¬b → ¬a → c → a → b → c
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
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) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₉ : ¬c → b → ¬a → b → a → c
mp₃₀ : ¬c → b → ¬a → b → c → a
mpr₉ : b → a → c → a → b → c
mpr₁₀ : b → a → c → ¬a → ¬b → c
mpr₁₁ : b → ¬a → ¬c → a → b → c
mpr₁₂ : b → ¬a → ¬c → ¬a → ¬b → c
mpr₁₃ mpr₁₄ : b → a → c → a → b → c
mpr₁₅ : b → c → a → c → (a ↔ b)
mpr₁₆ : b → c → ¬a → ¬c → (a ↔ b)
mpr₁₇ : b → c → a → c → (a ↔ b)
mpr₁₈ : b → c → a → c → a → b
mpr₁₉ : b → c → a → c → b → a
mpr₂₀ : ¬b → ¬a → c → a → b → c
mpr₂₁ : ¬b → ¬a → c → ¬a → ¬b → c
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
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) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₉ : ¬c → b → ¬a → b → a → c
mp₃₀ : ¬c → b → ¬a → b → c → a
mpr₉ : b → a → c → a → b → c
mpr₁₀ : b → a → c → ¬a → ¬b → c
mpr₁₁ : b → ¬a → ¬c → a → b → c
mpr₁₂ : b → ¬a → ¬c → ¬a → ¬b → c
mpr₁₃ mpr₁₄ : b → a → c → a → b → c
mpr₁₅ : b → c → a → c → (a ↔ b)
mpr₁₆ : b → c → ¬a → ¬c → (a ↔ b)
mpr₁₇ : b → c → a → c → (a ↔ b)
mpr₁₈ : b → c → a → c → a → b
mpr₁₉ : b → c → a → c → b → a
mpr₂₀ : ¬b → ¬a → c → a → b → c
mpr₂₁ : ¬b → ¬a → c → ¬a → ¬b → c
mpr₂₂ : ¬b → ¬¬a → ¬c → a → b → c
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
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) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₉ : ¬c → b → ¬a → b → a → c
mp₃₀ : ¬c → b → ¬a → b → c → a
mpr₉ : b → a → c → a → b → c
mpr₁₀ : b → a → c → ¬a → ¬b → c
mpr₁₁ : b → ¬a → ¬c → a → b → c
mpr₁₂ : b → ¬a → ¬c → ¬a → ¬b → c
mpr₁₃ mpr₁₄ : b → a → c → a → b → c
mpr₁₅ : b → c → a → c → (a ↔ b)
mpr₁₆ : b → c → ¬a → ¬c → (a ↔ b)
mpr₁₇ : b → c → a → c → (a ↔ b)
mpr₁₈ : b → c → a → c → a → b
mpr₁₉ : b → c → a → c → b → a
mpr₂₀ : ¬b → ¬a → c → a → b → c
mpr₂₁ : ¬b → ¬a → c → ¬a → ¬b → c
mpr₂₂ : ¬b → ¬¬a → ¬c → a → b → c
mpr₂₃ : ¬b → ¬¬a → ¬c → ¬a → ¬b → c
mpr₂₄ mpr₂₅ : ¬b → ¬a → c → ¬a → ¬b → c
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mpr₂₆ : ¬b → c → ¬a → c → (a ↔ b)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₉ : ¬c → b → ¬a → b → a → c
mp₃₀ : ¬c → b → ¬a → b → c → a
mpr₉ : b → a → c → a → b → c
mpr₁₀ : b → a → c → ¬a → ¬b → c
mpr₁₁ : b → ¬a → ¬c → a → b → c
mpr₁₂ : b → ¬a → ¬c → ¬a → ¬b → c
mpr₁₃ mpr₁₄ : b → a → c → a → b → c
mpr₁₅ : b → c → a → c → (a ↔ b)
mpr₁₆ : b → c → ¬a → ¬c → (a ↔ b)
mpr₁₇ : b → c → a → c → (a ↔ b)
mpr₁₈ : b → c → a → c → a → b
mpr₁₉ : b → c → a → c → b → a
mpr₂₀ : ¬b → ¬a → c → a → b → c
mpr₂₁ : ¬b → ¬a → c → ¬a → ¬b → c
mpr₂₂ : ¬b → ¬¬a → ¬c → a → b → c
mpr₂₃ : ¬b → ¬¬a → ¬c → ¬a → ¬b → c
mpr₂₄ mpr₂₅ : ¬b → ¬a → c → ¬a → ¬b → c
mpr₂₆ : ¬b → c → ¬a → c → (a ↔ b)
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mpr₂₇ : ¬b → c → ¬¬a → ¬c → (a ↔ b)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₉ : ¬c → b → ¬a → b → a → c
mp₃₀ : ¬c → b → ¬a → b → c → a
mpr₉ : b → a → c → a → b → c
mpr₁₀ : b → a → c → ¬a → ¬b → c
mpr₁₁ : b → ¬a → ¬c → a → b → c
mpr₁₂ : b → ¬a → ¬c → ¬a → ¬b → c
mpr₁₃ mpr₁₄ : b → a → c → a → b → c
mpr₁₅ : b → c → a → c → (a ↔ b)
mpr₁₆ : b → c → ¬a → ¬c → (a ↔ b)
mpr₁₇ : b → c → a → c → (a ↔ b)
mpr₁₈ : b → c → a → c → a → b
mpr₁₉ : b → c → a → c → b → a
mpr₂₀ : ¬b → ¬a → c → a → b → c
mpr₂₁ : ¬b → ¬a → c → ¬a → ¬b → c
mpr₂₂ : ¬b → ¬¬a → ¬c → a → b → c
mpr₂₃ : ¬b → ¬¬a → ¬c → ¬a → ¬b → c
mpr₂₄ mpr₂₅ : ¬b → ¬a → c → ¬a → ¬b → c
mpr₂₆ : ¬b → c → ¬a → c → (a ↔ b)
mpr₂₇ : ¬b → c → ¬¬a → ¬c → (a ↔ b)
mpr₂₈ : ¬b → c → ¬a → c → (a ↔ b)
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mpr₂₉ : ¬b → c → ¬a → c → a → b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₉ : ¬c → b → ¬a → b → a → c
mp₃₀ : ¬c → b → ¬a → b → c → a
mpr₉ : b → a → c → a → b → c
mpr₁₀ : b → a → c → ¬a → ¬b → c
mpr₁₁ : b → ¬a → ¬c → a → b → c
mpr₁₂ : b → ¬a → ¬c → ¬a → ¬b → c
mpr₁₃ mpr₁₄ : b → a → c → a → b → c
mpr₁₅ : b → c → a → c → (a ↔ b)
mpr₁₆ : b → c → ¬a → ¬c → (a ↔ b)
mpr₁₇ : b → c → a → c → (a ↔ b)
mpr₁₈ : b → c → a → c → a → b
mpr₁₉ : b → c → a → c → b → a
mpr₂₀ : ¬b → ¬a → c → a → b → c
mpr₂₁ : ¬b → ¬a → c → ¬a → ¬b → c
mpr₂₂ : ¬b → ¬¬a → ¬c → a → b → c
mpr₂₃ : ¬b → ¬¬a → ¬c → ¬a → ¬b → c
mpr₂₄ mpr₂₅ : ¬b → ¬a → c → ¬a → ¬b → c
mpr₂₆ : ¬b → c → ¬a → c → (a ↔ b)
mpr₂₇ : ¬b → c → ¬¬a → ¬c → (a ↔ b)
mpr₂₈ : ¬b → c → ¬a → c → (a ↔ b)
mpr₂₉ : ¬b → c → ¬a → c → a → b
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
have mpr₃₀ : ¬b → c → ¬a → c → b → a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
⊢ (dite p a fun (hp : ¬p) ↦ dite q (b hp) (c hp)) =
    if hq : q then dite p a fun (hp : ¬p) ↦ b hp hq else dite p a fun (hp : ¬p) ↦ c hp hq
have pos : ∀ (h : p), q → a h = a h
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
pos : ∀ (h : p), q → a h = a h
⊢ (dite p a fun (hp : ¬p) ↦ dite q (b hp) (c hp)) =
    if hq : q then dite p a fun (hp : ¬p) ↦ b hp hq else dite p a fun (hp : ¬p) ↦ c hp hq
have neg : ∀ (h : p), ¬q → a h = a h
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
pos : ∀ (h : p), q → a h = a h
neg : ∀ (h : p), ¬q → a h = a h
⊢ (dite p a fun (hp : ¬p) ↦ dite q (b hp) (c hp)) =
    if hq : q then dite p a fun (hp : ¬p) ↦ b hp hq else dite p a fun (hp : ¬p) ↦ c hp hq
have pos₁ : ∀ (h : ¬p) (h_1 : q), b h h_1 = b h sorry
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
pos : ∀ (h : p), q → a h = a h
neg : ∀ (h : p), ¬q → a h = a h
pos₁ : ∀ (h : ¬p) (h_1 : q), b h h_1 = b h ⋯
⊢ (dite p a fun (hp : ¬p) ↦ dite q (b hp) (c hp)) =
    if hq : q then dite p a fun (hp : ¬p) ↦ b hp hq else dite p a fun (hp : ¬p) ↦ c hp hq
have neg₁ : ∀ (h : ¬p) (h_1 : ¬q), c h h_1 = c h sorry
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
⊢ dite p (fun (hp : p) ↦ dite q (a hp) (b hp)) c =
    if hq : q then dite p (fun (hp : p) ↦ a hp hq) c else dite p (fun (hp : p) ↦ b hp hq) c
have pos : ∀ (h : p) (h_1 : q), a h h_1 = a h sorry
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
pos : ∀ (h : p) (h_1 : q), a h h_1 = a h ⋯
⊢ dite p (fun (hp : p) ↦ dite q (a hp) (b hp)) c =
    if hq : q then dite p (fun (hp : p) ↦ a hp hq) c else dite p (fun (hp : p) ↦ b hp hq) c
have neg : ∀ (h : p) (h_1 : ¬q), b h h_1 = b h sorry
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
pos : ∀ (h : p) (h_1 : q), a h h_1 = a h ⋯
neg : ∀ (h : p) (h_1 : ¬q), b h h_1 = b h ⋯
⊢ dite p (fun (hp : p) ↦ dite q (a hp) (b hp)) c =
    if hq : q then dite p (fun (hp : p) ↦ a hp hq) c else dite p (fun (hp : p) ↦ b hp hq) c
have pos₁ : ∀ (h : ¬p), q → c h = c h
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
pos : ∀ (h : p) (h_1 : q), a h h_1 = a h ⋯
neg : ∀ (h : p) (h_1 : ¬q), b h h_1 = b h ⋯
pos₁ : ∀ (h : ¬p), q → c h = c h
⊢ dite p (fun (hp : p) ↦ dite q (a hp) (b hp)) c =
    if hq : q then dite p (fun (hp : p) ↦ a hp hq) c else dite p (fun (hp : p) ↦ b hp hq) c
have neg₁ : ∀ (h : ¬p), ¬q → c h = c h
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
⊢ f p
have pos : ∀ (hp : p), f p
Tactic: by_cases hp : p
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
pos : ∀ (hp : p), f p
⊢ f p
have neg : ∀ (hp : ¬p), f p
Tactic: by_cases hp : p
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
f : Prop → Prop
h_1 : ∃ (p : Prop), f p
p : Prop
h : f p
⊢ f True ∨ f False
have refine_1 : p → f True
Tactic: refine (em p).imp ?_ ?_
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
f : Prop → Prop
h_1 : ∃ (p : Prop), f p
p : Prop
h : f p
refine_1 : p → f True
⊢ f True ∨ f False
have refine_2 : ¬p → f False
Tactic: refine (em p).imp ?_ ?_
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
f : Prop → Prop
h_1 : ∃ (p : Prop), f p
p : Prop
h : f p
H : p
⊢ f True
have h₁ : True ↔ p
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Logic.Lemmas (goal)
Goal:
f : Prop → Prop
h_1 : ∃ (p : Prop), f p
p : Prop
h : f p
H : ¬p
⊢ f False
have h₁ : False ↔ p
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Basic (goal)
Goal:
α : Type u_3
inst : Nontrivial α
inst_1 : LinearOrder α
⊢ ∃ (x : α), ∃ (y : α), x < y
have rcases : ∀ (x y : α) (hxy : x ≠ y), ∃ (x : α), ∃ (y : α), x < y
Tactic: rcases exists_pair_ne α with ⟨x, y, hxy⟩
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Basic (goal)
Goal:
α : Type u_3
inst : Nontrivial α
inst_1 : LinearOrder α
x y : α
hxy : x ≠ y
⊢ ∃ (x : α), ∃ (y : α), x < y
have inl : x < y → ∃ (x : α), ∃ (y : α), x < y
Tactic: cases lt_or_gt_of_ne hxy
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Basic (goal)
Goal:
α : Type u_3
inst : Nontrivial α
inst_1 : LinearOrder α
x y : α
hxy : x ≠ y
inl : x < y → ∃ (x : α), ∃ (y : α), x < y
⊢ ∃ (x : α), ∃ (y : α), x < y
have inr : y < x → ∃ (x : α), ∃ (y : α), x < y
Tactic: cases lt_or_gt_of_ne hxy
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : Inhabited α
h : ¬Nontrivial α
x : α
⊢ x = default
have by_contra : ∀ (H : ¬x = default), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
⊢ Nontrivial.{u_1} (Option α)
have inhabit : ∀ (inhabited_h : Inhabited α), Nontrivial.{u_1} (Option α)
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial α
f : α → β
hf : Injective f
y : β
⊢ ∃ (x : α), f x ≠ y
have rcases : ∀ (x₁ x₂ : α) (hx : x₁ ≠ x₂), ∃ (x : α), f x ≠ y
Tactic: rcases exists_pair_ne α with ⟨x₁, x₂, hx⟩
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
⊢ ∃ (x : α), f x ≠ y
have pos : ∀ (h : f x₂ = y), ∃ (x : α), f x ≠ y
Tactic: by_cases h : f x₂ = y
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
pos : ∀ (h : f x₂ = y), ∃ (x : α), f x ≠ y
⊢ ∃ (x : α), f x ≠ y
have neg : ∀ (h : ¬f x₂ = y), ∃ (x : α), f x ≠ y
Tactic: by_cases h : f x₂ = y
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (goal)
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : DecidableEq α
x : α
⊢ ∃ (y : α), y ≠ x
have rcases : ∀ (y y' : α) (h : y ≠ y'), ∃ (y : α), y ≠ x
Tactic: rcases exists_pair_ne α with ⟨y, y', h⟩
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (goal)
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : DecidableEq α
x y y' : α
h : y ≠ y'
⊢ ∃ (y : α), y ≠ x
have pos : ∀ (hx : x = y), ∃ (y : α), y ≠ x
Tactic: by_cases hx : x = y
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (goal)
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : DecidableEq α
x y y' : α
h : y ≠ y'
pos : ∀ (hx : x = y), ∃ (y : α), y ≠ x
⊢ ∃ (y : α), y ≠ x
have neg : ∀ (hx : ¬x = y), ∃ (y : α), y ≠ x
Tactic: by_cases hx : x = y