awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
have rw : a ⊓ b ⊓ c ⊔ a \ (b ⊔ c) ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
Tactic: rw [sdiff_symmDiff', sup_comm (a ⊓ b ⊓ c), symmDiff_sdiff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
rw : a ⊓ b ⊓ c ⊔ a \ (b ⊔ c) ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
⊢ a \ b ∆ c ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
have rw₁ : a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
Tactic: rw [sdiff_symmDiff', sup_comm (a ⊓ b ⊓ c), symmDiff_sdiff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
rw : a ⊓ b ⊓ c ⊔ a \ (b ⊔ c) ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
rw₁ : a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
⊢ a \ b ∆ c ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
have rw₂ : a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a)) = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
Tactic: rw [sdiff_symmDiff', sup_comm (a ⊓ b ⊓ c), symmDiff_sdiff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ b ∆ c ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
have rw : a ⊓ b ⊓ c ⊔ a \ (b ⊔ c) ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
Tactic: { rw [sdiff_symmDiff', sup_comm (a ⊓ b ⊓ c), symmDiff_sdiff] }
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
rw : a ⊓ b ⊓ c ⊔ a \ (b ⊔ c) ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
⊢ a \ b ∆ c ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
have rw₁ : a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
Tactic: { rw [sdiff_symmDiff', sup_comm (a ⊓ b ⊓ c), symmDiff_sdiff] }
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
rw : a ⊓ b ⊓ c ⊔ a \ (b ⊔ c) ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
rw₁ : a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
⊢ a \ b ∆ c ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
have rw₂ : a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a)) = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
Tactic: { rw [sdiff_symmDiff', sup_comm (a ⊓ b ⊓ c), symmDiff_sdiff] }
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b ∆ c = a ∆ (b ∆ c)
have rw : a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c = a ∆ (b ∆ c)
Tactic: rw [symmDiff_symmDiff_left, symmDiff_symmDiff_right]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
rw : a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c = a ∆ (b ∆ c)
⊢ a ∆ b ∆ c = a ∆ (b ∆ c)
have rw₁ : a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c
Tactic: rw [symmDiff_symmDiff_left, symmDiff_symmDiff_right]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ (b ∆ c) = b ∆ (a ∆ c)
have simp_rw : a ∆ b ∆ c = b ∆ a ∆ c
Tactic: simp_rw [← symmDiff_assoc, symmDiff_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b ∆ c = a ∆ c ∆ b
have simp_rw : a ∆ (b ∆ c) = a ∆ (c ∆ b)
Tactic: simp_rw [symmDiff_assoc, symmDiff_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b ∆ (c ∆ d) = a ∆ c ∆ (b ∆ d)
have simp_rw : a ∆ (b ∆ (c ∆ d)) = a ∆ (c ∆ (b ∆ d))
Tactic: simp_rw [symmDiff_assoc, symmDiff_left_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ b ∆ a = b
have rw : a ∆ (a ∆ b) = b
Tactic: rw [symmDiff_comm, symmDiff_symmDiff_cancel_left]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw : a ∆ (a ∆ b) = b
⊢ a ∆ b ∆ a = b
have rw₁ : b = b
Tactic: rw [symmDiff_comm, symmDiff_symmDiff_cancel_left]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ b = a ↔ a ∆ b = a ∆ ⊥
have rw : a ∆ b = a ↔ a ∆ b = a
Tactic: rw [symmDiff_bot]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ b = a ∆ ⊥ ↔ b = ⊥
have rw : b = ⊥ ↔ b = ⊥
Tactic: rw [symmDiff_right_inj]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ b = b ↔ a = ⊥
have rw : b ∆ a = b ↔ a = ⊥
Tactic: rw [symmDiff_comm, symmDiff_eq_left]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw : b ∆ a = b ↔ a = ⊥
⊢ a ∆ b = b ↔ a = ⊥
have rw₁ : a = ⊥ ↔ a = ⊥
Tactic: rw [symmDiff_comm, symmDiff_eq_left]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
ha : Disjoint a c
hb : Disjoint b c
⊢ Disjoint (a ∆ b) c
have rw : Disjoint ((a ⊔ b) \ (a ⊓ b)) c
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 : α
ha : a ≤ c
⊢ a ∆ b = c ↔ c \ a = b
have rw : a ∆ b = c ↔ a ∆ c = b
Tactic: rw [← symmDiff_of_le ha]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
⊢ a ⇔ (b ⇔ c) = b ⇔ (a ⇔ c)
have simp_rw : a ⇔ b ⇔ c = b ⇔ a ⇔ c
Tactic: simp_rw [← bihimp_assoc, bihimp_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
⊢ a ⇔ b ⇔ c = a ⇔ c ⇔ b
have simp_rw : a ⇔ (b ⇔ c) = a ⇔ (c ⇔ b)
Tactic: simp_rw [bihimp_assoc, bihimp_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c d : α
⊢ a ⇔ b ⇔ (c ⇔ d) = a ⇔ c ⇔ (b ⇔ d)
have simp_rw : a ⇔ (b ⇔ (c ⇔ d)) = a ⇔ (c ⇔ (b ⇔ d))
Tactic: simp_rw [bihimp_assoc, bihimp_left_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ a ⇔ b ⇔ a = b
have rw : a ⇔ (a ⇔ b) = b
Tactic: rw [bihimp_comm, bihimp_bihimp_cancel_left]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
rw : a ⇔ (a ⇔ b) = b
⊢ a ⇔ b ⇔ a = b
have rw₁ : b = b
Tactic: rw [bihimp_comm, bihimp_bihimp_cancel_left]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
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, sdiff_eq, compl_inf]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
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) ⊓ (aᶜ ⊔ bᶜ)
Tactic: rw [symmDiff_eq_sup_sdiff_inf, sdiff_eq, compl_inf]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
rw : (a ⊔ b) \ (a ⊓ b) = (a ⊔ b) ⊓ (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) ⊓ (aᶜ ⊔ bᶜ)
Tactic: rw [symmDiff_eq_sup_sdiff_inf, sdiff_eq, compl_inf]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ (a ∆ b)ᶜ = a ⇔ b
have simp_rw : (a \ b ⊔ b \ a)ᶜ = a ⇔ b
Tactic: simp_rw [symmDiff, compl_sup_distrib, compl_sdiff, bihimp, inf_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
simp_rw : (a \ b ⊔ b \ a)ᶜ = a ⇔ b
⊢ (a ∆ b)ᶜ = a ⇔ b
have simp_rw₁ : (a \ b)ᶜ ⊓ (b \ a)ᶜ = a ⇔ b
Tactic: simp_rw [symmDiff, compl_sup_distrib, compl_sdiff, bihimp, inf_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
simp_rw : (a \ b ⊔ b \ a)ᶜ = a ⇔ b
simp_rw₁ : (a \ b)ᶜ ⊓ (b \ a)ᶜ = a ⇔ b
⊢ (a ∆ b)ᶜ = a ⇔ b
have simp_rw₂ : (a ⇨ b) ⊓ (b ⇨ a) = a ⇔ b
Tactic: simp_rw [symmDiff, compl_sup_distrib, compl_sdiff, bihimp, inf_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
simp_rw : (a \ b ⊔ b \ a)ᶜ = a ⇔ b
simp_rw₁ : (a \ b)ᶜ ⊓ (b \ a)ᶜ = a ⇔ b
simp_rw₂ : (a ⇨ b) ⊓ (b ⇨ a) = a ⇔ b
⊢ (a ∆ b)ᶜ = a ⇔ b
have simp_rw₃ : (a ⇨ b) ⊓ (b ⇨ a) = (b ⇨ a) ⊓ (a ⇨ b)
Tactic: simp_rw [symmDiff, compl_sup_distrib, compl_sdiff, bihimp, inf_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ bᶜ \ aᶜ ⊔ aᶜ \ bᶜ = a ∆ b
have simp_rw : a \ b ⊔ b \ a = a ∆ b
Tactic: simp_rw [compl_sdiff_compl, sdiff_eq, symmDiff_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
simp_rw : a \ b ⊔ b \ a = a ∆ b
⊢ bᶜ \ aᶜ ⊔ aᶜ \ bᶜ = a ∆ b
have simp_rw₁ : a ⊓ bᶜ ⊔ b ⊓ aᶜ = a ∆ b
Tactic: simp_rw [compl_sdiff_compl, sdiff_eq, symmDiff_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ a ∆ b = ⊤ ↔ IsCompl a b
have rw : (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ) = ⊤ ↔ IsCompl a b
Tactic: rw [symmDiff_eq', ← compl_inf, inf_eq_top_iff, compl_eq_top, isCompl_iff, disjoint_iff,
    codisjoint_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
rw : (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ) = ⊤ ↔ IsCompl a b
⊢ a ∆ b = ⊤ ↔ IsCompl a b
have rw₁ : (a ⊔ b) ⊓ (a ⊓ b)ᶜ = ⊤ ↔ IsCompl a b
Tactic: rw [symmDiff_eq', ← compl_inf, inf_eq_top_iff, compl_eq_top, isCompl_iff, disjoint_iff,
    codisjoint_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
rw : (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ) = ⊤ ↔ IsCompl a b
rw₁ : (a ⊔ b) ⊓ (a ⊓ b)ᶜ = ⊤ ↔ IsCompl a b
⊢ a ∆ b = ⊤ ↔ IsCompl a b
have rw₂ : a ⊔ b = ⊤ ∧ (a ⊓ b)ᶜ = ⊤ ↔ IsCompl a b
Tactic: rw [symmDiff_eq', ← compl_inf, inf_eq_top_iff, compl_eq_top, isCompl_iff, disjoint_iff,
    codisjoint_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
rw : (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ) = ⊤ ↔ IsCompl a b
rw₁ : (a ⊔ b) ⊓ (a ⊓ b)ᶜ = ⊤ ↔ IsCompl a b
rw₂ : a ⊔ b = ⊤ ∧ (a ⊓ b)ᶜ = ⊤ ↔ IsCompl a b
⊢ a ∆ b = ⊤ ↔ IsCompl a b
have rw₃ : a ⊔ b = ⊤ ∧ a ⊓ b = ⊥ ↔ IsCompl a b
Tactic: rw [symmDiff_eq', ← compl_inf, inf_eq_top_iff, compl_eq_top, isCompl_iff, disjoint_iff,
    codisjoint_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
rw : (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ) = ⊤ ↔ IsCompl a b
rw₁ : (a ⊔ b) ⊓ (a ⊓ b)ᶜ = ⊤ ↔ IsCompl a b
rw₂ : a ⊔ b = ⊤ ∧ (a ⊓ b)ᶜ = ⊤ ↔ IsCompl a b
rw₃ : a ⊔ b = ⊤ ∧ a ⊓ b = ⊥ ↔ IsCompl a b
⊢ a ∆ b = ⊤ ↔ IsCompl a b
have rw₄ : a ⊔ b = ⊤ ∧ a ⊓ b = ⊥ ↔ Disjoint a b ∧ Codisjoint a b
Tactic: rw [symmDiff_eq', ← compl_inf, inf_eq_top_iff, compl_eq_top, isCompl_iff, disjoint_iff,
    codisjoint_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
rw : (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ) = ⊤ ↔ IsCompl a b
rw₁ : (a ⊔ b) ⊓ (a ⊓ b)ᶜ = ⊤ ↔ IsCompl a b
rw₂ : a ⊔ b = ⊤ ∧ (a ⊓ b)ᶜ = ⊤ ↔ IsCompl a b
rw₃ : a ⊔ b = ⊤ ∧ a ⊓ b = ⊥ ↔ IsCompl a b
rw₄ : a ⊔ b = ⊤ ∧ a ⊓ b = ⊥ ↔ Disjoint a b ∧ Codisjoint a b
⊢ a ∆ b = ⊤ ↔ IsCompl a b
have rw₅ : a ⊔ b = ⊤ ∧ a ⊓ b = ⊥ ↔ a ⊓ b = ⊥ ∧ Codisjoint a b
Tactic: rw [symmDiff_eq', ← compl_inf, inf_eq_top_iff, compl_eq_top, isCompl_iff, disjoint_iff,
    codisjoint_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
rw : (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ) = ⊤ ↔ IsCompl a b
rw₁ : (a ⊔ b) ⊓ (a ⊓ b)ᶜ = ⊤ ↔ IsCompl a b
rw₂ : a ⊔ b = ⊤ ∧ (a ⊓ b)ᶜ = ⊤ ↔ IsCompl a b
rw₃ : a ⊔ b = ⊤ ∧ a ⊓ b = ⊥ ↔ IsCompl a b
rw₄ : a ⊔ b = ⊤ ∧ a ⊓ b = ⊥ ↔ Disjoint a b ∧ Codisjoint a b
rw₅ : a ⊔ b = ⊤ ∧ a ⊓ b = ⊥ ↔ a ⊓ b = ⊥ ∧ Codisjoint a b
⊢ a ∆ b = ⊤ ↔ IsCompl a b
have rw₆ : a ⊔ b = ⊤ ∧ a ⊓ b = ⊥ ↔ a ⊓ b = ⊥ ∧ a ⊔ b = ⊤
Tactic: rw [symmDiff_eq', ← compl_inf, inf_eq_top_iff, compl_eq_top, isCompl_iff, disjoint_iff,
    codisjoint_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
rw : (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ) = ⊤ ↔ IsCompl a b
rw₁ : (a ⊔ b) ⊓ (a ⊓ b)ᶜ = ⊤ ↔ IsCompl a b
rw₂ : a ⊔ b = ⊤ ∧ (a ⊓ b)ᶜ = ⊤ ↔ IsCompl a b
rw₃ : a ⊔ b = ⊤ ∧ a ⊓ b = ⊥ ↔ IsCompl a b
rw₄ : a ⊔ b = ⊤ ∧ a ⊓ b = ⊥ ↔ Disjoint a b ∧ Codisjoint a b
rw₅ : a ⊔ b = ⊤ ∧ a ⊓ b = ⊥ ↔ a ⊓ b = ⊥ ∧ Codisjoint a b
rw₆ : a ⊔ b = ⊤ ∧ a ⊓ b = ⊥ ↔ a ⊓ b = ⊥ ∧ a ⊔ b = ⊤
⊢ a ∆ b = ⊤ ↔ IsCompl a b
have rw₇ : a ⊓ b = ⊥ ∧ a ⊔ b = ⊤ ↔ a ⊓ b = ⊥ ∧ a ⊔ b = ⊤
Tactic: rw [symmDiff_eq', ← compl_inf, inf_eq_top_iff, compl_eq_top, isCompl_iff, disjoint_iff,
    codisjoint_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ a ⇔ b = ⊥ ↔ IsCompl a b
have rw : a ⊓ b ⊔ aᶜ ⊓ bᶜ = ⊥ ↔ IsCompl a b
Tactic: rw [bihimp_eq', ← compl_sup, sup_eq_bot_iff, compl_eq_bot, isCompl_iff, disjoint_iff,
    codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
rw : a ⊓ b ⊔ aᶜ ⊓ bᶜ = ⊥ ↔ IsCompl a b
⊢ a ⇔ b = ⊥ ↔ IsCompl a b
have rw₁ : a ⊓ b ⊔ (a ⊔ b)ᶜ = ⊥ ↔ IsCompl a b
Tactic: rw [bihimp_eq', ← compl_sup, sup_eq_bot_iff, compl_eq_bot, isCompl_iff, disjoint_iff,
    codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
rw : a ⊓ b ⊔ aᶜ ⊓ bᶜ = ⊥ ↔ IsCompl a b
rw₁ : a ⊓ b ⊔ (a ⊔ b)ᶜ = ⊥ ↔ IsCompl a b
⊢ a ⇔ b = ⊥ ↔ IsCompl a b
have rw₂ : a ⊓ b = ⊥ ∧ (a ⊔ b)ᶜ = ⊥ ↔ IsCompl a b
Tactic: rw [bihimp_eq', ← compl_sup, sup_eq_bot_iff, compl_eq_bot, isCompl_iff, disjoint_iff,
    codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
rw : a ⊓ b ⊔ aᶜ ⊓ bᶜ = ⊥ ↔ IsCompl a b
rw₁ : a ⊓ b ⊔ (a ⊔ b)ᶜ = ⊥ ↔ IsCompl a b
rw₂ : a ⊓ b = ⊥ ∧ (a ⊔ b)ᶜ = ⊥ ↔ IsCompl a b
⊢ a ⇔ b = ⊥ ↔ IsCompl a b
have rw₃ : a ⊓ b = ⊥ ∧ a ⊔ b = ⊤ ↔ IsCompl a b
Tactic: rw [bihimp_eq', ← compl_sup, sup_eq_bot_iff, compl_eq_bot, isCompl_iff, disjoint_iff,
    codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
rw : a ⊓ b ⊔ aᶜ ⊓ bᶜ = ⊥ ↔ IsCompl a b
rw₁ : a ⊓ b ⊔ (a ⊔ b)ᶜ = ⊥ ↔ IsCompl a b
rw₂ : a ⊓ b = ⊥ ∧ (a ⊔ b)ᶜ = ⊥ ↔ IsCompl a b
rw₃ : a ⊓ b = ⊥ ∧ a ⊔ b = ⊤ ↔ IsCompl a b
⊢ a ⇔ b = ⊥ ↔ IsCompl a b
have rw₄ : a ⊓ b = ⊥ ∧ a ⊔ b = ⊤ ↔ Disjoint a b ∧ Codisjoint a b
Tactic: rw [bihimp_eq', ← compl_sup, sup_eq_bot_iff, compl_eq_bot, isCompl_iff, disjoint_iff,
    codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
rw : a ⊓ b ⊔ aᶜ ⊓ bᶜ = ⊥ ↔ IsCompl a b
rw₁ : a ⊓ b ⊔ (a ⊔ b)ᶜ = ⊥ ↔ IsCompl a b
rw₂ : a ⊓ b = ⊥ ∧ (a ⊔ b)ᶜ = ⊥ ↔ IsCompl a b
rw₃ : a ⊓ b = ⊥ ∧ a ⊔ b = ⊤ ↔ IsCompl a b
rw₄ : a ⊓ b = ⊥ ∧ a ⊔ b = ⊤ ↔ Disjoint a b ∧ Codisjoint a b
⊢ a ⇔ b = ⊥ ↔ IsCompl a b
have rw₅ : a ⊓ b = ⊥ ∧ a ⊔ b = ⊤ ↔ a ⊓ b = ⊥ ∧ Codisjoint a b
Tactic: rw [bihimp_eq', ← compl_sup, sup_eq_bot_iff, compl_eq_bot, isCompl_iff, disjoint_iff,
    codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
rw : a ⊓ b ⊔ aᶜ ⊓ bᶜ = ⊥ ↔ IsCompl a b
rw₁ : a ⊓ b ⊔ (a ⊔ b)ᶜ = ⊥ ↔ IsCompl a b
rw₂ : a ⊓ b = ⊥ ∧ (a ⊔ b)ᶜ = ⊥ ↔ IsCompl a b
rw₃ : a ⊓ b = ⊥ ∧ a ⊔ b = ⊤ ↔ IsCompl a b
rw₄ : a ⊓ b = ⊥ ∧ a ⊔ b = ⊤ ↔ Disjoint a b ∧ Codisjoint a b
rw₅ : a ⊓ b = ⊥ ∧ a ⊔ b = ⊤ ↔ a ⊓ b = ⊥ ∧ Codisjoint a b
⊢ a ⇔ b = ⊥ ↔ IsCompl a b
have rw₆ : a ⊓ b = ⊥ ∧ a ⊔ b = ⊤ ↔ a ⊓ b = ⊥ ∧ a ⊔ b = ⊤
Tactic: rw [bihimp_eq', ← compl_sup, sup_eq_bot_iff, compl_eq_bot, isCompl_iff, disjoint_iff,
    codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
⊢ a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
have rw : a ⊓ (b ∆ c)ᶜ ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
Tactic: rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
rw : a ⊓ (b ∆ c)ᶜ ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
⊢ a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
have rw₁ : a ⊓ b ⇔ c ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
Tactic: rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
rw : a ⊓ (b ∆ c)ᶜ ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
rw₁ : a ⊓ b ⇔ c ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
⊢ a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
have rw₂ : a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
Tactic: rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
rw : a ⊓ (b ∆ c)ᶜ ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
rw₁ : a ⊓ b ⇔ c ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
rw₂ : a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
⊢ a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
have rw₃ : a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
Tactic: rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
⊢ a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
have rw : a ⊓ (b ∆ c)ᶜ ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
Tactic: { rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq] }
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
rw : a ⊓ (b ∆ c)ᶜ ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
⊢ a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
have rw₁ : a ⊓ b ⇔ c ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
Tactic: { rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq] }
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
rw : a ⊓ (b ∆ c)ᶜ ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
rw₁ : a ⊓ b ⇔ c ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
⊢ a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
have rw₂ : a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
Tactic: { rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq] }
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
rw : a ⊓ (b ∆ c)ᶜ ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
rw₁ : a ⊓ b ⇔ c ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
rw₂ : a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
⊢ a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
have rw₃ : a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
Tactic: { rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq] }
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
⊢ a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
have rw : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
Tactic: rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
rw : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
⊢ a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
have rw₁ : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ) = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
Tactic: rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
rw : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
rw₁ : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ) = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
⊢ a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
have rw₂ : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
Tactic: rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
rw : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
rw₁ : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ) = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
rw₂ : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
⊢ a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
have rw₃ : a ⊓ b ⊓ c ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
Tactic: rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
rw : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
rw₁ : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ) = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
rw₂ : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
rw₃ : a ⊓ b ⊓ c ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
⊢ a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
have rw₄ : a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
Tactic: rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc]