awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
hb : a ⊓ b ≤ c
hc : a ⊓ c ≤ b
⊢ a ≤ b ⇔ c

Tactic:
le_inf (le_himp_iff.2 hc) <| le_himp_iff.2 hb

Premises used: Iff.mpr, le_inf, bihimp, le_himp_iff
-- Module: Mathlib.Order.SymmDiff
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
simp_rw₂ : a ⊓ c ≤ b ∧ a ⊓ b ≤ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b
⊢ a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b

Tactic:
simp_rw [bihimp, le_inf_iff, le_himp_iff, and_comm]

Premises used: and_comm, bihimp, le_inf_iff, le_himp_iff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊓ b ≤ a ⇔ b

Tactic:
inf_le_inf le_himp le_himp

Premises used: inf_le_inf, bihimp, le_himp
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⇔ b = a ⊔ b ⇨ a ⊓ b

Tactic:
simp [himp_inf_distrib, bihimp]

Premises used: himp_inf_distrib, bihimp
-- Module: Mathlib.Order.SymmDiff
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
rw₂ rw₃ : a ⊓ b = a ⊓ b
⊢ a ⇔ b = a ⊓ b

Tactic:
rw [bihimp, h.himp_eq_left, h.himp_eq_right]

Premises used: Codisjoint.himp_eq_left, Codisjoint.himp_eq_right, bihimp
-- Module: Mathlib.Order.SymmDiff
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)
rw₃ rw₄ : (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
⊢ a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)

Tactic:
rw [bihimp, himp_inf_distrib, himp_himp, himp_himp]

Premises used: himp_inf_distrib, himp_himp, bihimp
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
rw : ((a ⊔ b) ⊓ b ⇨ a) ⊓ ((a ⊔ b) ⊓ a ⇨ b) = a ⇔ b
⊢ a ⊔ b ⇨ a ⇔ b = a ⇔ b

Tactic:
rw [himp_bihimp]

Premises used: himp_bihimp
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ ((a ⊔ b) ⊓ b ⇨ a) ⊓ ((a ⊔ b) ⊓ a ⇨ b) = a ⇔ b

Tactic:
simp [bihimp]

Premises used: bihimp
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⇔ (a ⇨ b) = a ⊓ b

Tactic:
@symmDiff_sdiff_eq_sup αᵒᵈ _ _ _

Premises used: bihimp, symmDiff_sdiff_eq_sup, OrderDual
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ (b ⇨ a) ⇔ b = a ⊓ b

Tactic:
@sdiff_symmDiff_eq_sup αᵒᵈ _ _ _

Premises used: bihimp, sdiff_symmDiff_eq_sup, OrderDual
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⇔ b ⊓ (a ⊔ b) = a ⊓ b

Tactic:
@symmDiff_sup_inf αᵒᵈ _ _ _

Premises used: symmDiff_sup_inf, bihimp, OrderDual
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ (a ⊔ b) ⊓ a ⇔ b = a ⊓ b

Tactic:
@inf_sup_symmDiff αᵒᵈ _ _ _

Premises used: bihimp, inf_sup_symmDiff, OrderDual
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⇔ b ⇔ (a ⊔ b) = a ⊓ b

Tactic:
@symmDiff_symmDiff_inf αᵒᵈ _ _ _

Premises used: bihimp, symmDiff_symmDiff_inf, OrderDual, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b : α
⊢ (a ⊔ b) ⇔ (a ⇔ b) = a ⊓ b

Tactic:
@inf_symmDiff_symmDiff αᵒᵈ _ _ _

Premises used: bihimp, OrderDual, inf_symmDiff_symmDiff, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ⇔ b ⊓ b ⇔ c ≤ a ⇔ c

Tactic:
@symmDiff_triangle αᵒᵈ _ _ _ _

Premises used: symmDiff_triangle, bihimp
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
⊢ a ∆ ⊤ = ￢a

Tactic:
simp [symmDiff]

Premises used: symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
⊢ ⊤ ∆ a = ￢a

Tactic:
simp [symmDiff]

Premises used: symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
rw : ⊤ ≤ ￢a ⊔ a
⊢ (￢a) ∆ a = ⊤

Tactic:
rw [eq_top_iff, symmDiff, hnot_sdiff, sup_sdiff_self]

Premises used: eq_top_iff, hnot_sdiff, sup_sdiff_self, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
⊢ ⊤ ≤ ￢a ⊔ a

Tactic:
Codisjoint.top_le codisjoint_hnot_left

Premises used: Codisjoint.top_le, codisjoint_hnot_left
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
⊢ ⊤ ≤ ￢a ⊔ a

Tactic:
exact Codisjoint.top_le codisjoint_hnot_left

Premises used: Codisjoint.top_le, codisjoint_hnot_left
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
rw : (￢a) ∆ a = ⊤
rw₁ rw₂ : Eq.{u_2 + 1} (α := α) ⊤ ⊤
⊢ a ∆ (￢a) = ⊤

Tactic:
rw [symmDiff_comm, hnot_symmDiff_self]

Premises used: hnot_symmDiff_self, symmDiff_comm
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
h : IsCompl a b
rw : (￢b) ∆ b = ⊤
rw₁ rw₂ : Eq.{u_2 + 1} (α := α) ⊤ ⊤
⊢ a ∆ b = ⊤

Tactic:
rw [h.eq_hnot, hnot_symmDiff_self]

Premises used: hnot_symmDiff_self, IsCompl.eq_hnot
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
⊢ a ⇔ ⊥ = aᶜ

Tactic:
simp [bihimp]

Premises used: bihimp
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
⊢ ⊥ ⇔ a = aᶜ

Tactic:
simp [bihimp]

Premises used: bihimp
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
⊢ aᶜ ⇔ a = ⊥

Tactic:
@hnot_symmDiff_self αᵒᵈ _ _

Premises used: hnot_symmDiff_self, bihimp, OrderDual
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
⊢ a ⇔ aᶜ = ⊥

Tactic:
@symmDiff_hnot_self αᵒᵈ _ _

Premises used: bihimp, symmDiff_hnot_self, OrderDual
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
h : IsCompl a b
rw : bᶜ ⇔ b = ⊥
rw₁ rw₂ : Eq.{u_2 + 1} (α := α) ⊥ ⊥
⊢ a ⇔ b = ⊥

Tactic:
rw [h.eq_compl, compl_bihimp_self]

Premises used: compl_bihimp_self, IsCompl.eq_compl
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw rw₁ : (a ⊔ b) \ (a ⊓ b) = (a ⊔ b) \ (a ⊓ b)
⊢ (a ⊔ b) \ (a ⊓ b) = a ∆ b

Tactic:
rw [symmDiff_eq_sup_sdiff_inf]

Premises used: symmDiff_eq_sup_sdiff_inf
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw : Disjoint ((a ⊔ b) \ (a ⊓ b)) (a ⊓ b)
⊢ Disjoint (a ∆ b) (a ⊓ b)

Tactic:
rw [symmDiff_eq_sup_sdiff_inf]

Premises used: symmDiff_eq_sup_sdiff_inf
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) (a ⊓ b)

Tactic:
disjoint_sdiff_self_left

Premises used: disjoint_sdiff_self_left
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) (a ⊓ b)

Tactic:
exact disjoint_sdiff_self_left

Premises used: disjoint_sdiff_self_left
-- Module: Mathlib.Order.SymmDiff
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)
rw₄ rw₅ : (a ⊓ b ⊔ a ⊓ c) \ (a ⊓ b ⊓ (a ⊓ c)) = (a ⊓ b ⊔ a ⊓ c) \ (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]

Premises used: inf_inf_distrib_left, symmDiff_eq_sup_sdiff_inf, inf_sup_left, inf_sdiff_distrib_left
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
simp_rw : c ⊓ a ∆ b = (c ⊓ a) ∆ (c ⊓ b)
⊢ a ∆ b ⊓ c = (a ⊓ c) ∆ (b ⊓ c)

Tactic:
simp_rw [inf_comm _ c, inf_symmDiff_distrib_left]

Premises used: inf_comm, inf_symmDiff_distrib_left
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
⊢ c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b

Tactic:
simp only [(· ∆ ·), sdiff_sdiff_sup_sdiff']

Premises used: sdiff_sdiff_sup_sdiff', symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
rw : c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)
rw₁ rw₂ : c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b = c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b
⊢ c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)

Tactic:
rw [sdiff_symmDiff, sdiff_sup]

Premises used: sdiff_symmDiff, sdiff_sup
-- Module: Mathlib.Order.SymmDiff
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
rw₄ rw₅ : b \ a = b \ a
⊢ a ∆ b \ a = b \ a

Tactic:
rw [symmDiff_def, sup_sdiff, sdiff_idem, sdiff_sdiff_self, bot_sup_eq]

Premises used: symmDiff_def, bot_sup_eq, sdiff_sdiff_self, sup_sdiff, sdiff_idem
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw : b ∆ a \ b = a \ b
rw₁ rw₂ : a \ b = a \ b
⊢ a ∆ b \ b = a \ b

Tactic:
rw [symmDiff_comm, symmDiff_sdiff_left]

Premises used: symmDiff_comm, symmDiff_sdiff_left
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ a \ a ∆ b = a ⊓ b

Tactic:
simp [sdiff_symmDiff]

Premises used: sdiff_symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw : b \ b ∆ a = a ⊓ b
rw₁ : b \ b ∆ a = b ⊓ a
rw₂ rw₃ : b ⊓ a = b ⊓ a
⊢ b \ a ∆ b = a ⊓ b

Tactic:
rw [symmDiff_comm, inf_comm, sdiff_symmDiff_left]

Premises used: symmDiff_comm, inf_comm, sdiff_symmDiff_left
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ b = a ⊔ b ↔ Disjoint a b

Tactic:
⟨fun h => ?_, Disjoint.symmDiff_eq_sup⟩

Premises used: Disjoint.symmDiff_eq_sup, Iff.intro
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
refine : ∀ (h : a ∆ b = a ⊔ b), Disjoint a b
⊢ a ∆ b = a ⊔ b ↔ Disjoint a b

Tactic:
refine ⟨fun h => ?_, Disjoint.symmDiff_eq_sup⟩
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
h : a ∆ b = a ⊔ b
⊢ Disjoint (a ⊓ b) (a ⊔ b)

Tactic:
rw [symmDiff_eq_sup_sdiff_inf, sdiff_eq_self_iff_disjoint] at h

Premises used: symmDiff_eq_sup_sdiff_inf, sdiff_eq_self_iff_disjoint
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
h : Disjoint (a ⊓ b) (a ⊔ b)
⊢ Disjoint a b

Tactic:
h.of_disjoint_inf_of_le le_sup_left

Premises used: le_sup_left, Disjoint.of_disjoint_inf_of_le
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
h : Disjoint (a ⊓ b) (a ⊔ b)
⊢ Disjoint a b

Tactic:
exact h.of_disjoint_inf_of_le le_sup_left

Premises used: le_sup_left, Disjoint.of_disjoint_inf_of_le
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ a ≤ a ∆ b ↔ Disjoint a b

Tactic:
⟨fun h => ?_, fun h => h.symmDiff_eq_sup.symm ▸ le_sup_left⟩

Premises used: le_sup_left, Eq.rec, Disjoint.symmDiff_eq_sup, Iff.intro, Eq.symm
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
refine : ∀ (h : a ≤ a ∆ b), Disjoint a b
⊢ a ≤ a ∆ b ↔ Disjoint a b

Tactic:
refine ⟨fun h => ?_, fun h => h.symmDiff_eq_sup.symm ▸ le_sup_left⟩
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
h : a ≤ a ∆ b
⊢ a ≤ (a ⊔ b) \ (a ⊓ b)

Tactic:
rw [symmDiff_eq_sup_sdiff_inf] at h

Premises used: symmDiff_eq_sup_sdiff_inf
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
h : a ≤ (a ⊔ b) \ (a ⊓ b)
⊢ Disjoint a b

Tactic:
disjoint_iff_inf_le.mpr (le_sdiff_right.1 <| inf_le_of_left_le h).le

Premises used: Iff.mpr, le_sdiff_right, inf_le_of_left_le, Eq.le, Iff.mp, disjoint_iff_inf_le
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
h : a ≤ (a ⊔ b) \ (a ⊓ b)
⊢ Disjoint a b

Tactic:
exact disjoint_iff_inf_le.mpr (le_sdiff_right.1 <| inf_le_of_left_le h).le

Premises used: Iff.mpr, le_sdiff_right, inf_le_of_left_le, Eq.le, Iff.mp, disjoint_iff_inf_le
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw : b ≤ b ∆ a ↔ Disjoint a b
rw₁ : Disjoint b a ↔ Disjoint a b
rw₂ rw₃ : Disjoint a b ↔ Disjoint a b
⊢ b ≤ a ∆ b ↔ Disjoint a b

Tactic:
rw [symmDiff_comm, le_symmDiff_iff_left, disjoint_comm]

Premises used: symmDiff_comm, disjoint_comm, le_symmDiff_iff_left
-- Module: Mathlib.Order.SymmDiff
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)
rw₂ 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)
⊢ a ∆ b \ c ⊔ 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]

Premises used: sdiff_symmDiff', sup_comm, symmDiff_sdiff, Min.min
-- Module: Mathlib.Order.SymmDiff
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)
rw₂ 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)
⊢ a ∆ b \ c ⊔ 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] }

Premises used: sdiff_symmDiff', sup_comm, symmDiff_sdiff, Min.min
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c

Tactic:
ac_rfl
-- Module: Mathlib.Order.SymmDiff
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))
rw₂ 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 \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))

Tactic:
rw [sdiff_symmDiff', sup_comm (a ⊓ b ⊓ c), symmDiff_sdiff]

Premises used: sdiff_symmDiff', sup_comm, symmDiff_sdiff, Min.min
-- Module: Mathlib.Order.SymmDiff
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))
rw₂ 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 \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))

Tactic:
{ rw [sdiff_symmDiff', sup_comm (a ⊓ b ⊓ c), symmDiff_sdiff] }

Premises used: sdiff_symmDiff', sup_comm, symmDiff_sdiff, Min.min
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a)) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c

Tactic:
ac_rfl
-- Module: Mathlib.Order.SymmDiff
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)
rw₁ 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
⊢ a ∆ b ∆ c = a ∆ (b ∆ c)

Tactic:
rw [symmDiff_symmDiff_left, symmDiff_symmDiff_right]

Premises used: symmDiff_symmDiff_right, symmDiff_symmDiff_left
-- Module: Mathlib.Order.SymmDiff
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : GeneralizedBooleanAlgebra α
a b c d : α
⊢ Std.Associative fun (x1 x2 : α) ↦ x1 ∆ x2

Tactic:
⟨symmDiff_assoc⟩

Premises used: symmDiff_assoc, Std.Associative.mk
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
simp_rw : a ∆ b ∆ c = b ∆ a ∆ c
⊢ a ∆ (b ∆ c) = b ∆ (a ∆ c)

Tactic:
simp_rw [← symmDiff_assoc, symmDiff_comm]

Premises used: symmDiff_assoc, symmDiff_comm
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
simp_rw : a ∆ (b ∆ c) = a ∆ (c ∆ b)
⊢ a ∆ b ∆ c = a ∆ c ∆ b

Tactic:
simp_rw [symmDiff_assoc, symmDiff_comm]

Premises used: symmDiff_assoc, symmDiff_comm
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c d : α
simp_rw : a ∆ (b ∆ (c ∆ d)) = a ∆ (c ∆ (b ∆ d))
⊢ a ∆ b ∆ (c ∆ d) = a ∆ c ∆ (b ∆ d)

Tactic:
simp_rw [symmDiff_assoc, symmDiff_left_comm]

Premises used: symmDiff_assoc, symmDiff_left_comm
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ (a ∆ b) = b

Tactic:
simp [← symmDiff_assoc]

Premises used: symmDiff_assoc
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ b ∆ a ∆ a = b

Tactic:
simp [symmDiff_assoc]

Premises used: symmDiff_assoc
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw : a ∆ (a ∆ b) = b
rw₁ rw₂ : b = b
⊢ a ∆ b ∆ a = b

Tactic:
rw [symmDiff_comm, symmDiff_symmDiff_cancel_left]

Premises used: symmDiff_comm, symmDiff_symmDiff_cancel_left
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a : α
⊢ Involutive fun (x : α) ↦ x ∆ a

Tactic:
symmDiff_symmDiff_cancel_right _

Premises used: Function.Involutive, symmDiff_symmDiff_cancel_right
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a : α
⊢ Involutive fun (x : α) ↦ a ∆ x

Tactic:
symmDiff_symmDiff_cancel_left _

Premises used: symmDiff_symmDiff_cancel_left, Function.Involutive
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a : α
⊢ Injective (β := α) fun (x : α) ↦ x ∆ a

Tactic:
Function.Involutive.injective (symmDiff_left_involutive a)

Premises used: symmDiff_left_involutive, Function.Involutive.injective
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a : α
⊢ Injective (β := α) fun (x : α) ↦ a ∆ x

Tactic:
Function.Involutive.injective (symmDiff_right_involutive _)

Premises used: Function.Involutive.injective, symmDiff_right_involutive
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a : α
⊢ Surjective (β := α) fun (x : α) ↦ x ∆ a

Tactic:
Function.Involutive.surjective (symmDiff_left_involutive _)

Premises used: symmDiff_left_involutive, Function.Involutive.surjective
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a : α
⊢ Surjective (β := α) fun (x : α) ↦ a ∆ x

Tactic:
Function.Involutive.surjective (symmDiff_right_involutive _)

Premises used: Function.Involutive.surjective, symmDiff_right_involutive
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b = c ∆ b ↔ a = c

Tactic:
(symmDiff_left_injective _).eq_iff

Premises used: Function.Injective.eq_iff, symmDiff_left_injective
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b = a ∆ c ↔ b = c

Tactic:
(symmDiff_right_injective _).eq_iff

Premises used: Function.Injective.eq_iff, symmDiff_right_injective
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw rw₁ : a ∆ b = a ↔ a ∆ b = a
⊢ a ∆ b = a ↔ a ∆ b = a ∆ ⊥

Tactic:
rw [symmDiff_bot]

Premises used: symmDiff_bot
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw rw₁ : b = ⊥ ↔ b = ⊥
⊢ a ∆ b = a ∆ ⊥ ↔ b = ⊥

Tactic:
rw [symmDiff_right_inj]

Premises used: symmDiff_right_inj
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b : α
rw : b ∆ a = b ↔ a = ⊥
rw₁ rw₂ : a = ⊥ ↔ a = ⊥
⊢ a ∆ b = b ↔ a = ⊥

Tactic:
rw [symmDiff_comm, symmDiff_eq_left]

Premises used: symmDiff_comm, symmDiff_eq_left
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
ha : Disjoint a c
hb : Disjoint b c
rw : Disjoint ((a ⊔ b) \ (a ⊓ b)) c
⊢ Disjoint (a ∆ b) c

Tactic:
rw [symmDiff_eq_sup_sdiff_inf]

Premises used: symmDiff_eq_sup_sdiff_inf
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
ha : Disjoint a c
hb : Disjoint b c
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) c

Tactic:
(ha.sup_left hb).disjoint_sdiff_left

Premises used: Disjoint.disjoint_sdiff_left, Disjoint.sup_left
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
ha : Disjoint a c
hb : Disjoint b c
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) c

Tactic:
exact (ha.sup_left hb).disjoint_sdiff_left

Premises used: Disjoint.disjoint_sdiff_left, Disjoint.sup_left
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
ha : Disjoint a b
hb : Disjoint a c
⊢ Disjoint a (b ∆ c)

Tactic:
(ha.symm.symmDiff_left hb.symm).symm

Premises used: Disjoint.symm, Disjoint.symmDiff_left
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
ha : a ≤ c
rw : a ∆ b = c ↔ a ∆ c = b
⊢ a ∆ b = c ↔ c \ a = b

Tactic:
rw [← symmDiff_of_le ha]

Premises used: symmDiff_of_le
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
ha : a ≤ c
⊢ a ∆ b = c ↔ a ∆ c = b

Tactic:
((symmDiff_right_involutive a).toPerm _).apply_eq_iff_eq_symm_apply.trans eq_comm

Premises used: Function.Involutive.toPerm, eq_comm, Iff.trans, symmDiff_right_involutive, symmDiff, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : GeneralizedBooleanAlgebra α
a b c : α
ha : a ≤ c
⊢ a ∆ b = c ↔ a ∆ c = b

Tactic:
exact ((symmDiff_right_involutive a).toPerm _).apply_eq_iff_eq_symm_apply.trans eq_comm

Premises used: Function.Involutive.toPerm, eq_comm, Iff.trans, symmDiff_right_involutive, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ a ⇔ b ⇨ a ⊓ b = a ⊔ b

Tactic:
@sup_sdiff_symmDiff αᵒᵈ _ _ _

Premises used: bihimp, OrderDual, symmDiff, sup_sdiff_symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ Codisjoint (a ⇔ b) (a ⊔ b)

Tactic:
@disjoint_symmDiff_inf αᵒᵈ _ _ _

Premises used: Codisjoint, disjoint_symmDiff_inf, bihimp, OrderDual
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ a ⇨ a ⇔ b = a ⇨ b

Tactic:
@symmDiff_sdiff_left αᵒᵈ _ _ _

Premises used: symmDiff_sdiff_left, bihimp, OrderDual, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ b ⇨ a ⇔ b = b ⇨ a

Tactic:
@symmDiff_sdiff_right αᵒᵈ _ _ _

Premises used: symmDiff_sdiff_right, bihimp, OrderDual, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ a ⇔ b ⇨ a = a ⊔ b

Tactic:
@sdiff_symmDiff_left αᵒᵈ _ _ _

Premises used: bihimp, sdiff_symmDiff_left, OrderDual, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ a ⇔ b ⇨ b = a ⊔ b

Tactic:
@sdiff_symmDiff_right αᵒᵈ _ _ _

Premises used: bihimp, OrderDual, symmDiff, sdiff_symmDiff_right
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ a ⇔ b = a ⊓ b ↔ Codisjoint a b

Tactic:
@symmDiff_eq_sup αᵒᵈ _ _ _

Premises used: Codisjoint, bihimp, symmDiff_eq_sup, OrderDual
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ a ⇔ b ≤ a ↔ Codisjoint a b

Tactic:
@le_symmDiff_iff_left αᵒᵈ _ _ _

Premises used: Codisjoint, bihimp, le_symmDiff_iff_left, OrderDual