awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)
have refine_1 : a ≤ a \ b ⊔ b \ a ⊔ b
Tactic: refine sup_le (le_inf le_sup_right ?_) (le_inf ?_ le_sup_right)
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
refine_1 : a ≤ a \ b ⊔ b \ a ⊔ b
⊢ a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)
have refine_2 : b ≤ a \ b ⊔ b \ a ⊔ a
Tactic: refine sup_le (le_inf le_sup_right ?_) (le_inf ?_ le_sup_right)
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ a \ b ⊔ b \ a ⊔ b
have refine_1 : a ≤ a \ b ⊔ b ⊔ b \ a
Tactic: rw [sup_right_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ b ≤ a \ b ⊔ b \ a ⊔ a
have refine_2 : b ≤ a \ b ⊔ (b \ a ⊔ a)
Tactic: rw [sup_assoc]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊓ b ⊔ a ∆ b = a ⊔ b
have rw : a ∆ b ⊔ a ⊓ b = a ⊔ b
Tactic: rw [sup_comm, symmDiff_sup_inf]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a ∆ b ⊔ a ⊓ b = a ⊔ b
⊢ a ⊓ b ⊔ a ∆ b = a ⊔ b
have rw₁ : a ⊔ b = a ⊔ b
Tactic: rw [sup_comm, symmDiff_sup_inf]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b ∆ (a ⊓ b) = a ⊔ b
have rw : (a ∆ b \ (a ⊓ b)) ∆ (a ⊓ b) = a ⊔ b
Tactic: rw [← symmDiff_sdiff_inf a, sdiff_symmDiff_eq_sup, symmDiff_sup_inf]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : (a ∆ b \ (a ⊓ b)) ∆ (a ⊓ b) = a ⊔ b
⊢ a ∆ b ∆ (a ⊓ b) = a ⊔ b
have rw₁ : a ∆ b ⊔ a ⊓ b = a ⊔ b
Tactic: rw [← symmDiff_sdiff_inf a, sdiff_symmDiff_eq_sup, symmDiff_sup_inf]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : (a ∆ b \ (a ⊓ b)) ∆ (a ⊓ b) = a ⊔ b
rw₁ : a ∆ b ⊔ a ⊓ b = a ⊔ b
⊢ a ∆ b ∆ (a ⊓ b) = a ⊔ b
have rw₂ : a ⊔ b = a ⊔ b
Tactic: rw [← symmDiff_sdiff_inf a, sdiff_symmDiff_eq_sup, symmDiff_sup_inf]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a ⊓ b) ∆ (a ∆ b) = a ⊔ b
have rw : a ∆ b ∆ (a ⊓ b) = a ⊔ b
Tactic: rw [symmDiff_comm, symmDiff_symmDiff_inf]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a ∆ b ∆ (a ⊓ b) = a ⊔ b
⊢ (a ⊓ b) ∆ (a ∆ b) = a ⊔ b
have rw₁ : a ⊔ b = a ⊔ b
Tactic: rw [symmDiff_comm, symmDiff_symmDiff_inf]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ∆ c ≤ a ∆ b ⊔ b ∆ c
have refine : a \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ c
Tactic: refine (sup_le_sup (sdiff_triangle a b c) <| sdiff_triangle _ b _).trans_eq ?_
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ c
have rw : a \ b ⊔ b \ c ⊔ (b \ a ⊔ c \ b) = a ∆ b ⊔ b ∆ c
Tactic: rw [sup_comm (c \ b), sup_sup_sup_comm, symmDiff, symmDiff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
rw : a \ b ⊔ b \ c ⊔ (b \ a ⊔ c \ b) = a ∆ b ⊔ b ∆ c
⊢ a \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ c
have rw₁ : a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b) = a ∆ b ⊔ b ∆ c
Tactic: rw [sup_comm (c \ b), sup_sup_sup_comm, symmDiff, symmDiff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
rw : a \ b ⊔ b \ c ⊔ (b \ a ⊔ c \ b) = a ∆ b ⊔ b ∆ c
rw₁ : a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b) = a ∆ b ⊔ b ∆ c
⊢ a \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ c
have rw₂ : a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b) = a \ b ⊔ b \ a ⊔ b ∆ c
Tactic: rw [sup_comm (c \ b), sup_sup_sup_comm, symmDiff, symmDiff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
rw : a \ b ⊔ b \ c ⊔ (b \ a ⊔ c \ b) = a ∆ b ⊔ b ∆ c
rw₁ : a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b) = a ∆ b ⊔ b ∆ c
rw₂ : a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b) = a \ b ⊔ b \ a ⊔ b ∆ c
⊢ a \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ c
have rw₃ : a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b) = a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b)
Tactic: rw [sup_comm (c \ b), sup_sup_sup_comm, symmDiff, symmDiff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ a ∆ b ⊔ b
have h : a = a ∆ ⊥
Tactic: convert! symmDiff_triangle a b ⊥
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : a = a ∆ ⊥
⊢ a ≤ a ∆ b ⊔ b
have h₁ : b = b ∆ ⊥
Tactic: convert! symmDiff_triangle a b ⊥
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a = a ∆ ⊥
have h : a = a
Tactic: rw [symmDiff_bot]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ b = b ∆ ⊥
have h : b = b
Tactic: rw [symmDiff_bot]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a : α
⊢ a ⇔ a = ⊤
have rw : (a ⇨ a) ⊓ (a ⇨ a) = ⊤
Tactic: rw [bihimp, inf_idem, himp_self]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a : α
rw : (a ⇨ a) ⊓ (a ⇨ a) = ⊤
⊢ a ⇔ a = ⊤
have rw₁ : a ⇨ a = ⊤
Tactic: rw [bihimp, inf_idem, himp_self]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a : α
rw : (a ⇨ a) ⊓ (a ⇨ a) = ⊤
rw₁ : a ⇨ a = ⊤
⊢ a ⇔ a = ⊤
have rw₂ : Eq.{u_2 + 1} (α := α) ⊤ ⊤
Tactic: rw [bihimp, inf_idem, himp_self]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a : α
⊢ a ⇔ ⊤ = a
have rw : (⊤ ⇨ a) ⊓ (a ⇨ ⊤) = a
Tactic: rw [bihimp, himp_top, top_himp, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a : α
rw : (⊤ ⇨ a) ⊓ (a ⇨ ⊤) = a
⊢ a ⇔ ⊤ = a
have rw₁ : (⊤ ⇨ a) ⊓ ⊤ = a
Tactic: rw [bihimp, himp_top, top_himp, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a : α
rw : (⊤ ⇨ a) ⊓ (a ⇨ ⊤) = a
rw₁ : (⊤ ⇨ a) ⊓ ⊤ = a
⊢ a ⇔ ⊤ = a
have rw₂ : a ⊓ ⊤ = a
Tactic: rw [bihimp, himp_top, top_himp, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a : α
rw : (⊤ ⇨ a) ⊓ (a ⇨ ⊤) = a
rw₁ : (⊤ ⇨ a) ⊓ ⊤ = a
rw₂ : a ⊓ ⊤ = a
⊢ a ⇔ ⊤ = a
have rw₃ : a = a
Tactic: rw [bihimp, himp_top, top_himp, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a : α
⊢ ⊤ ⇔ a = a
have rw : a ⇔ ⊤ = a
Tactic: rw [bihimp_comm, bihimp_top]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a : α
rw : a ⇔ ⊤ = a
⊢ ⊤ ⇔ a = a
have rw₁ : a = a
Tactic: rw [bihimp_comm, bihimp_top]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : a ≤ b
⊢ a ⇔ b = b ⇨ a
have rw : (b ⇨ a) ⊓ (a ⇨ b) = b ⇨ a
Tactic: rw [bihimp, himp_eq_top_iff.2 h, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : a ≤ b
rw : (b ⇨ a) ⊓ (a ⇨ b) = b ⇨ a
⊢ a ⇔ b = b ⇨ a
have rw₁ : (b ⇨ a) ⊓ ⊤ = b ⇨ a
Tactic: rw [bihimp, himp_eq_top_iff.2 h, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : a ≤ b
rw : (b ⇨ a) ⊓ (a ⇨ b) = b ⇨ a
rw₁ : (b ⇨ a) ⊓ ⊤ = b ⇨ a
⊢ a ⇔ b = b ⇨ a
have rw₂ : b ⇨ a = b ⇨ a
Tactic: rw [bihimp, himp_eq_top_iff.2 h, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : b ≤ a
⊢ a ⇔ b = a ⇨ b
have rw : (b ⇨ a) ⊓ (a ⇨ b) = a ⇨ b
Tactic: rw [bihimp, himp_eq_top_iff.2 h, top_inf_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : b ≤ a
rw : (b ⇨ a) ⊓ (a ⇨ b) = a ⇨ b
⊢ a ⇔ b = a ⇨ b
have rw₁ : ⊤ ⊓ (a ⇨ b) = a ⇨ b
Tactic: rw [bihimp, himp_eq_top_iff.2 h, top_inf_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : b ≤ a
rw : (b ⇨ a) ⊓ (a ⇨ b) = a ⇨ b
rw₁ : ⊤ ⊓ (a ⇨ b) = a ⇨ b
⊢ a ⇔ b = a ⇨ b
have rw₂ : a ⇨ b = a ⇨ b
Tactic: rw [bihimp, himp_eq_top_iff.2 h, top_inf_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b
have simp_rw : a ≤ (c ⇨ b) ⊓ (b ⇨ c) ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b
Tactic: simp_rw [bihimp, le_inf_iff, le_himp_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
simp_rw : a ≤ (c ⇨ b) ⊓ (b ⇨ c) ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b
⊢ a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b
have simp_rw₁ : a ≤ c ⇨ b ∧ a ≤ b ⇨ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b
Tactic: simp_rw [bihimp, le_inf_iff, le_himp_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
simp_rw : a ≤ (c ⇨ b) ⊓ (b ⇨ c) ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b
simp_rw₁ : a ≤ c ⇨ b ∧ a ≤ b ⇨ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b
⊢ a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b
have simp_rw₂ : a ⊓ c ≤ b ∧ a ⊓ b ≤ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b
Tactic: simp_rw [bihimp, le_inf_iff, le_himp_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ a ⇔ b = a ⊓ b
have rw : (b ⇨ a) ⊓ (a ⇨ b) = a ⊓ b
Tactic: rw [bihimp, h.himp_eq_left, h.himp_eq_right]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
rw : (b ⇨ a) ⊓ (a ⇨ b) = a ⊓ b
⊢ a ⇔ b = a ⊓ b
have rw₁ : (b ⇨ a) ⊓ b = a ⊓ b
Tactic: rw [bihimp, h.himp_eq_left, h.himp_eq_right]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
rw : (b ⇨ a) ⊓ (a ⇨ b) = a ⊓ b
rw₁ : (b ⇨ a) ⊓ b = a ⊓ b
⊢ a ⇔ b = a ⊓ b
have rw₂ : a ⊓ b = a ⊓ b
Tactic: rw [bihimp, h.himp_eq_left, h.himp_eq_right]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
have rw : a ⇨ (c ⇨ b) ⊓ (b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
Tactic: rw [bihimp, himp_inf_distrib, himp_himp, himp_himp]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
rw : a ⇨ (c ⇨ b) ⊓ (b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
⊢ a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
have rw₁ : (a ⇨ c ⇨ b) ⊓ (a ⇨ b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
Tactic: rw [bihimp, himp_inf_distrib, himp_himp, himp_himp]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
rw : a ⇨ (c ⇨ b) ⊓ (b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
rw₁ : (a ⇨ c ⇨ b) ⊓ (a ⇨ b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
⊢ a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
have rw₂ : (a ⊓ c ⇨ b) ⊓ (a ⇨ b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
Tactic: rw [bihimp, himp_inf_distrib, himp_himp, himp_himp]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
rw : a ⇨ (c ⇨ b) ⊓ (b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
rw₁ : (a ⇨ c ⇨ b) ⊓ (a ⇨ b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
rw₂ : (a ⊓ c ⇨ b) ⊓ (a ⇨ b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
⊢ a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
have rw₃ : (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
Tactic: rw [bihimp, himp_inf_distrib, himp_himp, himp_himp]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊔ b ⇨ a ⇔ b = a ⇔ b
have rw : ((a ⊔ b) ⊓ b ⇨ a) ⊓ ((a ⊔ b) ⊓ a ⇨ b) = a ⇔ b
Tactic: rw [himp_bihimp]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
⊢ (￢a) ∆ a = ⊤
have rw : ⊤ ≤ ￢a ⊔ a
Tactic: rw [eq_top_iff, symmDiff, hnot_sdiff, sup_sdiff_self]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
⊢ a ∆ (￢a) = ⊤
have rw : (￢a) ∆ a = ⊤
Tactic: rw [symmDiff_comm, hnot_symmDiff_self]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
rw : (￢a) ∆ a = ⊤
⊢ a ∆ (￢a) = ⊤
have rw₁ : Eq.{u_2 + 1} (α := α) ⊤ ⊤
Tactic: rw [symmDiff_comm, hnot_symmDiff_self]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
h : IsCompl a b
⊢ a ∆ b = ⊤
have rw : (￢b) ∆ b = ⊤
Tactic: rw [h.eq_hnot, hnot_symmDiff_self]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
h : IsCompl a b
rw : (￢b) ∆ b = ⊤
⊢ a ∆ b = ⊤
have rw₁ : Eq.{u_2 + 1} (α := α) ⊤ ⊤
Tactic: rw [h.eq_hnot, hnot_symmDiff_self]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
h : IsCompl a b
⊢ a ⇔ b = ⊥
have rw : bᶜ ⇔ b = ⊥
Tactic: rw [h.eq_compl, compl_bihimp_self]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
h : IsCompl a b
rw : bᶜ ⇔ b = ⊥
⊢ a ⇔ b = ⊥
have rw₁ : Eq.{u_2 + 1} (α := α) ⊥ ⊥
Tactic: rw [h.eq_compl, compl_bihimp_self]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ (a ⊔ b) \ (a ⊓ b) = a ∆ b
have rw : (a ⊔ b) \ (a ⊓ b) = (a ⊔ b) \ (a ⊓ b)
Tactic: rw [symmDiff_eq_sup_sdiff_inf]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ Disjoint (a ∆ b) (a ⊓ b)
have rw : Disjoint ((a ⊔ b) \ (a ⊓ b)) (a ⊓ b)
Tactic: rw [symmDiff_eq_sup_sdiff_inf]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ⊓ b ∆ c = (a ⊓ b) ∆ (a ⊓ c)
have rw : a ⊓ (b ⊔ c) \ (b ⊓ c) = (a ⊓ b) ∆ (a ⊓ c)
Tactic: rw [symmDiff_eq_sup_sdiff_inf, inf_sdiff_distrib_left, inf_sup_left, inf_inf_distrib_left,
    symmDiff_eq_sup_sdiff_inf]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
rw : a ⊓ (b ⊔ c) \ (b ⊓ c) = (a ⊓ b) ∆ (a ⊓ c)
⊢ a ⊓ b ∆ c = (a ⊓ b) ∆ (a ⊓ c)
have rw₁ : (a ⊓ (b ⊔ c)) \ (a ⊓ (b ⊓ c)) = (a ⊓ b) ∆ (a ⊓ c)
Tactic: rw [symmDiff_eq_sup_sdiff_inf, inf_sdiff_distrib_left, inf_sup_left, inf_inf_distrib_left,
    symmDiff_eq_sup_sdiff_inf]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
rw : a ⊓ (b ⊔ c) \ (b ⊓ c) = (a ⊓ b) ∆ (a ⊓ c)
rw₁ : (a ⊓ (b ⊔ c)) \ (a ⊓ (b ⊓ c)) = (a ⊓ b) ∆ (a ⊓ c)
⊢ a ⊓ b ∆ c = (a ⊓ b) ∆ (a ⊓ c)
have rw₂ : (a ⊓ b ⊔ a ⊓ c) \ (a ⊓ (b ⊓ c)) = (a ⊓ b) ∆ (a ⊓ c)
Tactic: rw [symmDiff_eq_sup_sdiff_inf, inf_sdiff_distrib_left, inf_sup_left, inf_inf_distrib_left,
    symmDiff_eq_sup_sdiff_inf]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
rw : a ⊓ (b ⊔ c) \ (b ⊓ c) = (a ⊓ b) ∆ (a ⊓ c)
rw₁ : (a ⊓ (b ⊔ c)) \ (a ⊓ (b ⊓ c)) = (a ⊓ b) ∆ (a ⊓ c)
rw₂ : (a ⊓ b ⊔ a ⊓ c) \ (a ⊓ (b ⊓ c)) = (a ⊓ b) ∆ (a ⊓ c)
⊢ a ⊓ b ∆ c = (a ⊓ b) ∆ (a ⊓ c)
have rw₃ : (a ⊓ b ⊔ a ⊓ c) \ (a ⊓ b ⊓ (a ⊓ c)) = (a ⊓ b) ∆ (a ⊓ c)
Tactic: rw [symmDiff_eq_sup_sdiff_inf, inf_sdiff_distrib_left, inf_sup_left, inf_inf_distrib_left,
    symmDiff_eq_sup_sdiff_inf]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
rw : a ⊓ (b ⊔ c) \ (b ⊓ c) = (a ⊓ b) ∆ (a ⊓ c)
rw₁ : (a ⊓ (b ⊔ c)) \ (a ⊓ (b ⊓ c)) = (a ⊓ b) ∆ (a ⊓ c)
rw₂ : (a ⊓ b ⊔ a ⊓ c) \ (a ⊓ (b ⊓ c)) = (a ⊓ b) ∆ (a ⊓ c)
rw₃ : (a ⊓ b ⊔ a ⊓ c) \ (a ⊓ b ⊓ (a ⊓ c)) = (a ⊓ b) ∆ (a ⊓ c)
⊢ a ⊓ b ∆ c = (a ⊓ b) ∆ (a ⊓ c)
have rw₄ : (a ⊓ b ⊔ a ⊓ c) \ (a ⊓ b ⊓ (a ⊓ c)) = (a ⊓ b ⊔ a ⊓ c) \ (a ⊓ b ⊓ (a ⊓ c))
Tactic: rw [symmDiff_eq_sup_sdiff_inf, inf_sdiff_distrib_left, inf_sup_left, inf_inf_distrib_left,
    symmDiff_eq_sup_sdiff_inf]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b ⊓ c = (a ⊓ c) ∆ (b ⊓ c)
have simp_rw : c ⊓ a ∆ b = (c ⊓ a) ∆ (c ⊓ b)
Tactic: simp_rw [inf_comm _ c, inf_symmDiff_distrib_left]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
⊢ c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)
have rw : c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)
Tactic: rw [sdiff_symmDiff, sdiff_sup]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
rw : c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)
⊢ c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)
have rw₁ : c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b = c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b
Tactic: rw [sdiff_symmDiff, sdiff_sup]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ b \ a = b \ a
have rw : (a \ b ⊔ b \ a) \ a = b \ a
Tactic: rw [symmDiff_def, sup_sdiff, sdiff_idem, sdiff_sdiff_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw : (a \ b ⊔ b \ a) \ a = b \ a
⊢ a ∆ b \ a = b \ a
have rw₁ : (a \ b) \ a ⊔ (b \ a) \ a = b \ a
Tactic: rw [symmDiff_def, sup_sdiff, sdiff_idem, sdiff_sdiff_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw : (a \ b ⊔ b \ a) \ a = b \ a
rw₁ : (a \ b) \ a ⊔ (b \ a) \ a = b \ a
⊢ a ∆ b \ a = b \ a
have rw₂ : (a \ b) \ a ⊔ b \ a = b \ a
Tactic: rw [symmDiff_def, sup_sdiff, sdiff_idem, sdiff_sdiff_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw : (a \ b ⊔ b \ a) \ a = b \ a
rw₁ : (a \ b) \ a ⊔ (b \ a) \ a = b \ a
rw₂ : (a \ b) \ a ⊔ b \ a = b \ a
⊢ a ∆ b \ a = b \ a
have rw₃ : ⊥ ⊔ b \ a = b \ a
Tactic: rw [symmDiff_def, sup_sdiff, sdiff_idem, sdiff_sdiff_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw : (a \ b ⊔ b \ a) \ a = b \ a
rw₁ : (a \ b) \ a ⊔ (b \ a) \ a = b \ a
rw₂ : (a \ b) \ a ⊔ b \ a = b \ a
rw₃ : ⊥ ⊔ b \ a = b \ a
⊢ a ∆ b \ a = b \ a
have rw₄ : b \ a = b \ a
Tactic: rw [symmDiff_def, sup_sdiff, sdiff_idem, sdiff_sdiff_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ b \ b = a \ b
have rw : b ∆ a \ b = a \ b
Tactic: rw [symmDiff_comm, symmDiff_sdiff_left]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw : b ∆ a \ b = a \ b
⊢ a ∆ b \ b = a \ b
have rw₁ : a \ b = a \ b
Tactic: rw [symmDiff_comm, symmDiff_sdiff_left]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ b \ a ∆ b = a ⊓ b
have rw : b \ b ∆ a = a ⊓ b
Tactic: rw [symmDiff_comm, inf_comm, sdiff_symmDiff_left]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw : b \ b ∆ a = a ⊓ b
⊢ b \ a ∆ b = a ⊓ b
have rw₁ : b \ b ∆ a = b ⊓ a
Tactic: rw [symmDiff_comm, inf_comm, sdiff_symmDiff_left]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw : b \ b ∆ a = a ⊓ b
rw₁ : b \ b ∆ a = b ⊓ a
⊢ b \ a ∆ b = a ⊓ b
have rw₂ : b ⊓ a = b ⊓ a
Tactic: rw [symmDiff_comm, inf_comm, sdiff_symmDiff_left]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ b = a ⊔ b ↔ Disjoint a b
have refine : ∀ (h : a ∆ b = a ⊔ b), Disjoint a b
Tactic: refine ⟨fun h => ?_, Disjoint.symmDiff_eq_sup⟩
-- Lean 4 proof step from Mathlib.Order.SymmDiff (hypothesis)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
h : a ∆ b = a ⊔ b
⊢ Disjoint a b
have h₁ : Disjoint (a ⊓ b) (a ⊔ b)
Tactic: rw [symmDiff_eq_sup_sdiff_inf, sdiff_eq_self_iff_disjoint] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ a ≤ a ∆ b ↔ Disjoint a b
have refine : ∀ (h : a ≤ a ∆ b), Disjoint a b
Tactic: refine ⟨fun h => ?_, fun h => h.symmDiff_eq_sup.symm ▸ le_sup_left⟩
-- Lean 4 proof step from Mathlib.Order.SymmDiff (hypothesis)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
h : a ≤ a ∆ b
⊢ Disjoint a b
have h₁ : a ≤ (a ⊔ b) \ (a ⊓ b)
Tactic: rw [symmDiff_eq_sup_sdiff_inf] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ b ≤ a ∆ b ↔ Disjoint a b
have rw : b ≤ b ∆ a ↔ Disjoint a b
Tactic: rw [symmDiff_comm, le_symmDiff_iff_left, disjoint_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw : b ≤ b ∆ a ↔ Disjoint a b
⊢ b ≤ a ∆ b ↔ Disjoint a b
have rw₁ : Disjoint b a ↔ Disjoint a b
Tactic: rw [symmDiff_comm, le_symmDiff_iff_left, disjoint_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw : b ≤ b ∆ a ↔ Disjoint a b
rw₁ : Disjoint b a ↔ Disjoint a b
⊢ b ≤ a ∆ b ↔ Disjoint a b
have rw₂ : Disjoint a b ↔ Disjoint a b
Tactic: rw [symmDiff_comm, le_symmDiff_iff_left, disjoint_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b \ c ⊔ c \ a ∆ b = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)
have rw : a ∆ b \ c ⊔ (c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)
Tactic: rw [sdiff_symmDiff', sup_comm (c ⊓ a ⊓ b), symmDiff_sdiff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
rw : a ∆ b \ c ⊔ (c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)
⊢ a ∆ b \ c ⊔ c \ a ∆ b = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)
have rw₁ : a ∆ b \ c ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)
Tactic: rw [sdiff_symmDiff', sup_comm (c ⊓ a ⊓ b), symmDiff_sdiff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
rw : a ∆ b \ c ⊔ (c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)
rw₁ : a ∆ b \ c ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)
⊢ a ∆ b \ c ⊔ c \ a ∆ b = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)
have rw₂ : a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)
Tactic: rw [sdiff_symmDiff', sup_comm (c ⊓ a ⊓ b), symmDiff_sdiff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b \ c ⊔ c \ a ∆ b = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)
have rw : a ∆ b \ c ⊔ (c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)
Tactic: { rw [sdiff_symmDiff', sup_comm (c ⊓ a ⊓ b), symmDiff_sdiff] }