awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ a ⇔ b ≤ b ↔ Codisjoint a b

Tactic:
@le_symmDiff_iff_right αᵒᵈ _ _ _

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

Tactic:
@symmDiff_assoc αᵒᵈ _ _ _ _

Premises used: symmDiff_assoc, bihimp, OrderDual, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : BooleanAlgebra α
a b c d : α
⊢ Std.Associative fun (x1 x2 : α) ↦ x1 ⇔ x2

Tactic:
⟨bihimp_assoc⟩

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

Tactic:
simp_rw [← bihimp_assoc, bihimp_comm]

Premises used: bihimp_comm, bihimp_assoc
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
simp_rw : a ⇔ (b ⇔ c) = a ⇔ (c ⇔ b)
⊢ a ⇔ b ⇔ c = a ⇔ c ⇔ b

Tactic:
simp_rw [bihimp_assoc, bihimp_comm]

Premises used: bihimp_comm, bihimp_assoc
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
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 [bihimp_assoc, bihimp_left_comm]

Premises used: bihimp_left_comm, bihimp_assoc
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ a ⇔ (a ⇔ b) = b

Tactic:
simp [← bihimp_assoc]

Premises used: bihimp_assoc
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ b ⇔ a ⇔ a = b

Tactic:
simp [bihimp_assoc]

Premises used: bihimp_assoc
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
rw : a ⇔ (a ⇔ b) = b
rw₁ rw₂ : b = b
⊢ a ⇔ b ⇔ a = b

Tactic:
rw [bihimp_comm, bihimp_bihimp_cancel_left]

Premises used: bihimp_comm, bihimp_bihimp_cancel_left
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a : α
⊢ Involutive fun (x : α) ↦ x ⇔ a

Tactic:
bihimp_bihimp_cancel_right _

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

Tactic:
bihimp_bihimp_cancel_left _

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

Tactic:
@symmDiff_left_injective αᵒᵈ _ _

Premises used: bihimp, symmDiff_left_injective, OrderDual
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a : α
⊢ Injective (β := α) fun (x : α) ↦ a ⇔ x

Tactic:
@symmDiff_right_injective αᵒᵈ _ _

Premises used: bihimp, symmDiff_right_injective, OrderDual
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a : α
⊢ Surjective (β := α) fun (x : α) ↦ x ⇔ a

Tactic:
@symmDiff_left_surjective αᵒᵈ _ _

Premises used: symmDiff_left_surjective, bihimp, OrderDual
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a : α
⊢ Surjective (β := α) fun (x : α) ↦ a ⇔ x

Tactic:
@symmDiff_right_surjective αᵒᵈ _ _

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

Tactic:
(bihimp_left_injective _).eq_iff

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

Tactic:
(bihimp_right_injective _).eq_iff

Premises used: Function.Injective.eq_iff, bihimp_right_injective
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ a ⇔ b = a ↔ b = ⊤

Tactic:
@symmDiff_eq_left αᵒᵈ _ _ _

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

Tactic:
@symmDiff_eq_right αᵒᵈ _ _ _

Premises used: symmDiff_eq_right, bihimp, OrderDual
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
ha : Codisjoint a c
hb : Codisjoint b c
⊢ Codisjoint (a ⇔ b) c

Tactic:
(ha.inf_left hb).mono_left inf_le_bihimp

Premises used: Codisjoint.mono_left, inf_le_bihimp, Codisjoint.inf_left
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
ha : Codisjoint a b
hb : Codisjoint a c
⊢ Codisjoint a (b ⇔ c)

Tactic:
(ha.inf_right hb).mono_right inf_le_bihimp

Premises used: Codisjoint.inf_right, inf_le_bihimp, Codisjoint.mono_right
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ a ∆ b = a ⊓ bᶜ ⊔ b ⊓ aᶜ

Tactic:
simp only [(· ∆ ·), sdiff_eq]

Premises used: sdiff_eq, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ a ⇔ b = (a ⊔ bᶜ) ⊓ (b ⊔ aᶜ)

Tactic:
simp only [(· ⇔ ·), himp_eq]

Premises used: himp_eq, bihimp
-- Module: Mathlib.Order.SymmDiff
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ᶜ)
rw₂ rw₃ : (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ) = (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ)
⊢ a ∆ b = (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ)

Tactic:
rw [symmDiff_eq_sup_sdiff_inf, sdiff_eq, compl_inf]

Premises used: compl_inf, sdiff_eq, symmDiff_eq_sup_sdiff_inf
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ a ⇔ b = a ⊓ b ⊔ aᶜ ⊓ bᶜ

Tactic:
@symmDiff_eq' αᵒᵈ _ _ _

Premises used: symmDiff_eq', bihimp, OrderDual
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a : α
⊢ a ∆ ⊤ = aᶜ

Tactic:
symmDiff_top' _

Premises used: symmDiff_top'
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a : α
⊢ ⊤ ∆ a = aᶜ

Tactic:
top_symmDiff' _

Premises used: top_symmDiff'
-- Module: Mathlib.Order.SymmDiff
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
simp_rw₃ : (a ⇨ b) ⊓ (b ⇨ a) = (b ⇨ a) ⊓ (a ⇨ b)
⊢ (a ∆ b)ᶜ = a ⇔ b

Tactic:
simp_rw [symmDiff, compl_sup_distrib, compl_sdiff, bihimp, inf_comm]

Premises used: compl_sdiff, inf_comm, bihimp, compl_sup_distrib, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ (a ⇔ b)ᶜ = a ∆ b

Tactic:
@compl_symmDiff αᵒᵈ _ _ _

Premises used: compl_symmDiff, bihimp, OrderDual, symmDiff
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
simp_rw : a \ b ⊔ b \ a = a ∆ b
simp_rw₁ : a ⊓ bᶜ ⊔ b ⊓ aᶜ = a ∆ b
⊢ bᶜ \ aᶜ ⊔ aᶜ \ bᶜ = a ∆ b

Tactic:
simp_rw [compl_sdiff_compl, sdiff_eq, symmDiff_eq]

Premises used: compl_sdiff_compl, sdiff_eq, symmDiff_eq
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b : α
⊢ aᶜ ⇔ bᶜ = a ⇔ b

Tactic:
@compl_symmDiff_compl αᵒᵈ _ _ _

Premises used: bihimp, compl_symmDiff_compl, OrderDual
-- Module: Mathlib.Order.SymmDiff
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 = ⊤
rw₇ rw₈ : a ⊓ b = ⊥ ∧ a ⊔ b = ⊤ ↔ a ⊓ b = ⊥ ∧ 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]

Premises used: symmDiff_eq', compl_inf, codisjoint_iff, disjoint_iff, isCompl_iff, and_comm, inf_eq_top_iff, compl_eq_top
-- Module: Mathlib.Order.SymmDiff
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₆ rw₇ : a ⊓ b = ⊥ ∧ a ⊔ b = ⊤ ↔ a ⊓ b = ⊥ ∧ 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]

Premises used: codisjoint_iff, disjoint_iff, isCompl_iff, sup_eq_bot_iff, compl_sup, compl_eq_bot, bihimp_eq'
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a : α
⊢ aᶜ ∆ a = ⊤

Tactic:
hnot_symmDiff_self _

Premises used: hnot_symmDiff_self
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a : α
⊢ a ∆ aᶜ = ⊤

Tactic:
symmDiff_hnot_self _

Premises used: symmDiff_hnot_self
-- Module: Mathlib.Order.SymmDiff
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ᶜ
rw₃ rw₄ : a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
⊢ a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ

Tactic:
rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq]

Premises used: compl_symmDiff, symmDiff_eq, bihimp_eq'
-- Module: Mathlib.Order.SymmDiff
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ᶜ
rw₃ rw₄ : a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
⊢ a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ

Tactic:
{ rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq] }

Premises used: compl_symmDiff, symmDiff_eq, bihimp_eq'
-- Module: Mathlib.Order.SymmDiff
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ᶜ
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ᶜ) ⊔ (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]

Premises used: sup_assoc, inf_sup_right, inf_sup_left, inf_assoc
-- Module: Mathlib.Order.SymmDiff
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ᶜ
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ᶜ) ⊔ (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] }

Premises used: sup_assoc, inf_sup_right, inf_sup_left, inf_assoc
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
e_a : a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ
e_a₁ : c ⊓ bᶜ ⊓ aᶜ = aᶜ ⊓ bᶜ ⊓ c
⊢ a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c

Tactic:
congr 1
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
e_a : b ⊓ cᶜ ⊓ aᶜ = aᶜ ⊓ b ⊓ cᶜ
⊢ a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ

Tactic:
congr 1
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
e_a : aᶜ ⊓ (b ⊓ cᶜ) = aᶜ ⊓ b ⊓ cᶜ
e_a₁ e_a₂ : aᶜ ⊓ (b ⊓ cᶜ) = aᶜ ⊓ (b ⊓ cᶜ)
⊢ b ⊓ cᶜ ⊓ aᶜ = aᶜ ⊓ b ⊓ cᶜ

Tactic:
rw [inf_comm, inf_assoc]

Premises used: inf_comm, inf_assoc
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
⊢ c ⊓ bᶜ ⊓ aᶜ = aᶜ ⊓ bᶜ ⊓ c

Tactic:
apply inf_left_right_swap

Premises used: inf_left_right_swap
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
h : Disjoint a b
trans : c ≤ c \ (a ⊓ b)
trans₁ : c \ (a ⊓ b) ≤ a ∆ c ⊔ b ∆ c
⊢ c ≤ a ∆ c ⊔ b ∆ c

Tactic:
trans c \ (a ⊓ b)

Premises used: Min.min
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
h : Disjoint a b
rw : c ≤ c \ ⊥
rw₁ rw₂ : c ≤ c
⊢ c ≤ c \ (a ⊓ b)

Tactic:
rw [h.eq_bot, sdiff_bot]

Premises used: sdiff_bot, Disjoint.eq_bot
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
h : Disjoint a b
rw : c \ a ⊔ c \ b ≤ a ∆ c ⊔ b ∆ c
⊢ c \ (a ⊓ b) ≤ a ∆ c ⊔ b ∆ c

Tactic:
rw [sdiff_inf]

Premises used: sdiff_inf
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c \ a ⊔ c \ b ≤ a ∆ c ⊔ b ∆ c

Tactic:
sup_le_sup le_sup_right le_sup_right

Premises used: sup_le_sup, le_sup_right
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c \ a ⊔ c \ b ≤ a ∆ c ⊔ b ∆ c

Tactic:
exact sup_le_sup le_sup_right le_sup_right

Premises used: sup_le_sup, le_sup_right
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
h : Disjoint b c
simp_rw : a ≤ b ∆ a ⊔ c ∆ a
⊢ a ≤ a ∆ b ⊔ a ∆ c

Tactic:
simp_rw [symmDiff_comm a]

Premises used: symmDiff_comm
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
h : Disjoint b c
⊢ a ≤ b ∆ a ⊔ c ∆ a

Tactic:
h.le_symmDiff_sup_symmDiff_left

Premises used: Disjoint.le_symmDiff_sup_symmDiff_left
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
h : Disjoint b c
⊢ a ≤ b ∆ a ⊔ c ∆ a

Tactic:
exact h.le_symmDiff_sup_symmDiff_left

Premises used: Disjoint.le_symmDiff_sup_symmDiff_left
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
h : Codisjoint a b
⊢ a ⇔ c ⊓ b ⇔ c ≤ c

Tactic:
h.dual.le_symmDiff_sup_symmDiff_left

Premises used: Codisjoint.dual, Disjoint.le_symmDiff_sup_symmDiff_left, bihimp
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
h : Codisjoint b c
⊢ a ⇔ b ⊓ a ⇔ c ≤ a

Tactic:
h.dual.le_symmDiff_sup_symmDiff_right

Premises used: Codisjoint.dual, Disjoint.le_symmDiff_sup_symmDiff_right, bihimp
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
β : Type u_3
inst : GeneralizedCoheytingAlgebra α
inst_1 : GeneralizedCoheytingAlgebra β
a b : α × β
⊢ (a ∆ b).fst = a.fst ∆ b.fst

Tactic:
rfl

Premises used: symmDiff, rfl
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
β : Type u_3
inst : GeneralizedCoheytingAlgebra α
inst_1 : GeneralizedCoheytingAlgebra β
a b : α × β
⊢ (a ∆ b).snd = a.snd ∆ b.snd

Tactic:
rfl

Premises used: symmDiff, rfl
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
β : Type u_3
inst : GeneralizedHeytingAlgebra α
inst_1 : GeneralizedHeytingAlgebra β
a b : α × β
⊢ (a ⇔ b).fst = a.fst ⇔ b.fst

Tactic:
rfl

Premises used: bihimp, rfl
-- Module: Mathlib.Order.SymmDiff
Goal:
α : Type u_2
β : Type u_3
inst : GeneralizedHeytingAlgebra α
inst_1 : GeneralizedHeytingAlgebra β
a b : α × β
⊢ (a ⇔ b).snd = a.snd ⇔ b.snd

Tactic:
rfl

Premises used: bihimp, rfl
-- Module: Mathlib.Order.SymmDiff
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → GeneralizedCoheytingAlgebra (π i)
a b : (i : ι) → π i
⊢ a ∆ b = fun (i : ι) ↦ a i ∆ b i

Tactic:
rfl

Premises used: symmDiff, rfl
-- Module: Mathlib.Order.SymmDiff
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → GeneralizedHeytingAlgebra (π i)
a b : (i : ι) → π i
⊢ a ⇔ b = fun (i : ι) ↦ a i ⇔ b i

Tactic:
rfl

Premises used: bihimp, rfl
-- Module: Mathlib.Order.SymmDiff
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → GeneralizedCoheytingAlgebra (π i)
a b : (i : ι) → π i
i : ι
⊢ (a ∆ b) i = a i ∆ b i

Tactic:
rfl

Premises used: symmDiff, rfl
-- Module: Mathlib.Order.SymmDiff
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → GeneralizedHeytingAlgebra (π i)
a b : (i : ι) → π i
i : ι
⊢ (a ⇔ b) i = a i ⇔ b i

Tactic:
rfl

Premises used: bihimp, rfl
-- Module: Mathlib.Order.TeichmullerTukey
Goal:
α : Type u_1
F : Set (Set α)
hF : IsOfFiniteCharacter F
x : Set α
xF : x ∈ F
⊢ ∃ (m : Set α), x ⊆ m ∧ Maximal (fun (x : Set α) ↦ x ∈ F) m

Tactic:
zorn_subset_nonempty F (fun c cF cch cne ↦
    ⟨sUnion c, ?_, fun s sc ↦ subset_sUnion_of_mem sc⟩) x xF

Premises used: Set.sUnion, zorn_subset_nonempty, And.intro, Exists.intro, Set.subset_sUnion_of_mem
-- Module: Mathlib.Order.TeichmullerTukey
Goal:
α : Type u_1
F : Set (Set α)
hF : IsOfFiniteCharacter F
x : Set α
xF : x ∈ F
refine : ∀ (c : Set (Set α)) (cF : c ⊆ F) (cch : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c) (cne : c.Nonempty), ⋃₀ c ∈ F
⊢ ∃ (m : Set α), x ⊆ m ∧ Maximal (fun (x : Set α) ↦ x ∈ F) m

Tactic:
refine zorn_subset_nonempty F (fun c cF cch cne ↦
    ⟨sUnion c, ?_, fun s sc ↦ subset_sUnion_of_mem sc⟩) x xF

Premises used: Set.sUnion, zorn_subset_nonempty, And.intro, Exists.intro, Set.subset_sUnion_of_mem
-- Module: Mathlib.Order.TeichmullerTukey
Goal:
α : Type u_1
F : Set (Set α)
hF : IsOfFiniteCharacter F
x : Set α
xF : x ∈ F
c : Set (Set α)
cF : c ⊆ F
cch : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
cne : c.Nonempty
⊢ ⋃₀ c ∈ F

Tactic:
(hF (sUnion c)).mpr fun s sc sfin ↦ ?_

Premises used: Iff.mpr, Set.sUnion
-- Module: Mathlib.Order.TeichmullerTukey
Goal:
α : Type u_1
F : Set (Set α)
hF : IsOfFiniteCharacter F
x : Set α
xF : x ∈ F
c : Set (Set α)
cF : c ⊆ F
cch : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
cne : c.Nonempty
refine : ∀ (s : Set α) (sc : s ⊆ ⋃₀ c) (sfin : s.Finite), s ∈ F
⊢ ⋃₀ c ∈ F

Tactic:
refine (hF (sUnion c)).mpr fun s sc sfin ↦ ?_

Premises used: Iff.mpr, Set.sUnion
-- Module: Mathlib.Order.TeichmullerTukey
Goal:
α : Type u_1
F : Set (Set α)
hF : IsOfFiniteCharacter F
x : Set α
xF : x ∈ F
c : Set (Set α)
cF : c ⊆ F
cch : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
cne : c.Nonempty
s : Set α
sc : s ⊆ ⋃₀ c
sfin : s.Finite
obtain : ∀ (t : Set α) (tc : t ∈ c) (st : s ⊆ t), s ∈ F
⊢ s ∈ F

Tactic:
obtain ⟨t, tc, st⟩ := cch.directedOn.exists_mem_subset_of_finite_of_subset_sUnion cne sfin sc

Premises used: IsChain.directedOn, DirectedOn.exists_mem_subset_of_finite_of_subset_sUnion
-- Module: Mathlib.Order.TeichmullerTukey
Goal:
α : Type u_1
F : Set (Set α)
hF : IsOfFiniteCharacter F
x : Set α
xF : x ∈ F
c : Set (Set α)
cF : c ⊆ F
cch : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
cne : c.Nonempty
s : Set α
sc : s ⊆ ⋃₀ c
sfin : s.Finite
t : Set α
tc : t ∈ c
st : s ⊆ t
⊢ s ∈ F

Tactic:
(hF t).mp (cF tc) s st sfin

Premises used: Iff.mp
-- Module: Mathlib.Order.TeichmullerTukey
Goal:
α : Type u_1
F : Set (Set α)
hF : IsOfFiniteCharacter F
x : Set α
xF : x ∈ F
c : Set (Set α)
cF : c ⊆ F
cch : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
cne : c.Nonempty
s : Set α
sc : s ⊆ ⋃₀ c
sfin : s.Finite
t : Set α
tc : t ∈ c
st : s ⊆ t
⊢ s ∈ F

Tactic:
exact (hF t).mp (cF tc) s st sfin

Premises used: Iff.mp
-- Module: Mathlib.Order.TransfiniteIteration
Goal:
I : Type u
inst : SupSet I
φ : I → I
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : WellFoundedLT J
inst_4 : OrderBot J
i₀ : I
dsimp :
  SuccOrder.limitRecOn ⊥ (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
      (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
      (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
        ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) ⋯)
      i₀ =
    i₀
⊢ transfiniteIterate.{w, u} φ (J := J) ⊥ i₀ = i₀

Tactic:
dsimp [transfiniteIterate]

Premises used: transfiniteIterate
-- Module: Mathlib.Order.TransfiniteIteration
Goal:
I : Type u
inst : SupSet I
φ : I → I
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : WellFoundedLT J
inst_4 : OrderBot J
i₀ : I
⊢ SuccOrder.limitRecOn ⊥ (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
      (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
      (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
        ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) ⋯)
      i₀ =
    i₀

Tactic:
simp only [isMin_iff_eq_bot, SuccOrder.limitRecOn_isMin, id_eq]

Premises used: isMin_iff_eq_bot, id_eq, SuccOrder.limitRecOn_isMin
-- Module: Mathlib.Order.TransfiniteIteration
Goal:
I : Type u
inst : SupSet I
φ : I → I
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : WellFoundedLT J
i₀ : I
j : J
hj : ¬IsMax j
dsimp :
  SuccOrder.limitRecOn (Order.succ j) (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
      (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
      (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
        ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) ⋯)
      i₀ =
    φ
      (SuccOrder.limitRecOn j (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
        (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
        (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
          ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) ⋯)
        i₀)
⊢ transfiniteIterate φ (Order.succ j) i₀ = φ (transfiniteIterate φ j i₀)

Tactic:
dsimp [transfiniteIterate]

Premises used: transfiniteIterate
-- Module: Mathlib.Order.TransfiniteIteration
Goal:
I : Type u
inst : SupSet I
φ : I → I
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : WellFoundedLT J
i₀ : I
j : J
hj : ¬IsMax j
rw :
  (φ ∘
        SuccOrder.limitRecOn j (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
          (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
          fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
          ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) ⋯)
      i₀ =
    φ
      (SuccOrder.limitRecOn j (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
        (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
        (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
          ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) ⋯)
        i₀)
⊢ SuccOrder.limitRecOn (Order.succ j) (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
      (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
      (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
        ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) ⋯)
      i₀ =
    φ
      (SuccOrder.limitRecOn j (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
        (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
        (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
          ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) ⋯)
        i₀)

Tactic:
rw [SuccOrder.limitRecOn_succ_of_not_isMax _ _ _ hj]

Premises used: SuccOrder.limitRecOn_succ_of_not_isMax
-- Module: Mathlib.Order.TransfiniteIteration
Goal:
I : Type u
inst : SupSet I
φ : I → I
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : WellFoundedLT J
i₀ : I
j : J
hj : ¬IsMax j
⊢ (φ ∘
        SuccOrder.limitRecOn j (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
          (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
          fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
          ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) ⋯)
      i₀ =
    φ
      (SuccOrder.limitRecOn j (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
        (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
        (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
          ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) ⋯)
        i₀)

Tactic:
rfl