awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : yᶜ = x ↔ y = xᶜ
rw₁ : IsCompl y x ↔ y = xᶜ
rw₂ rw₃ : IsCompl y x ↔ IsCompl y x
⊢ x = yᶜ ↔ y = xᶜ

Tactic:
rw [eq_comm, compl_eq_iff_isCompl, eq_compl_iff_isCompl]

Premises used: eq_comm, eq_compl_iff_isCompl, compl_eq_iff_isCompl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
inst : BooleanAlgebra α
x : α
⊢ xᶜᶜ = x

Tactic:
(@isCompl_compl _ x _).symm.compl_eq

Premises used: IsCompl.compl_eq, isCompl_compl, IsCompl.symm
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
inst : BooleanAlgebra α
⊢ Eq.{u + 1} (α := α → α) (compl ∘ compl) id

Tactic:
funext compl_compl

Premises used: compl_compl, funext
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
inst : BooleanAlgebra α
⊢ Function.Involutive.{u + 1} (α := α) compl

Tactic:
compl_compl

Premises used: compl_compl, Function.Involutive
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
inst : BooleanAlgebra α
⊢ Function.Bijective.{u + 1, u + 1} (α := α) compl

Tactic:
compl_involutive.bijective

Premises used: compl_involutive, Function.Involutive.bijective
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
inst : BooleanAlgebra α
⊢ Function.Surjective.{u + 1, u + 1} (α := α) compl

Tactic:
compl_involutive.surjective

Premises used: Function.Involutive.surjective, compl_involutive
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
inst : BooleanAlgebra α
⊢ Function.Injective.{u + 1, u + 1} (α := α) compl

Tactic:
compl_involutive.injective

Premises used: Function.Involutive.injective, compl_involutive
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ xᶜ = yᶜ ↔ x = y

Tactic:
compl_injective.eq_iff

Premises used: Function.Injective.eq_iff, compl_injective
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : BooleanAlgebra α
h : IsCompl x y
⊢ zᶜ = y ↔ z = x

Tactic:
h.compl_eq ▸ compl_inj_iff

Premises used: Eq.rec, IsCompl.compl_eq, compl_inj_iff
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x : α
inst : BooleanAlgebra α
⊢ xᶜ = ⊤ ↔ x = ⊥

Tactic:
isCompl_bot_top.compl_eq_iff

Premises used: IsCompl.compl_eq_iff, isCompl_bot_top
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x : α
inst : BooleanAlgebra α
⊢ xᶜ = ⊥ ↔ x = ⊤

Tactic:
isCompl_top_bot.compl_eq_iff

Premises used: IsCompl.compl_eq_iff, isCompl_top_bot
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ (x ⊓ y)ᶜ = xᶜ ⊔ yᶜ

Tactic:
hnot_inf_distrib _ _

Premises used: hnot_inf_distrib
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
h : yᶜ ≤ xᶜ
⊢ xᶜᶜ ≤ yᶜᶜ

Tactic:
have h := compl_le_compl h
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
h_1 : yᶜ ≤ xᶜ
h : xᶜᶜ ≤ yᶜᶜ
⊢ x ≤ y

Tactic:
simpa using h
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ yᶜ < xᶜ ↔ x < y

Tactic:
lt_iff_lt_of_le_iff_le' compl_le_compl_iff_le compl_le_compl_iff_le

Premises used: lt_iff_lt_of_le_iff_le', compl_le_compl_iff_le
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
h : yᶜ ≤ x
⊢ xᶜ ≤ y

Tactic:
simpa only [compl_compl] using compl_le_compl h

Premises used: compl_compl, compl_le_compl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ xᶜ ≤ y ↔ yᶜ ≤ x

Tactic:
⟨compl_le_of_compl_le, compl_le_of_compl_le⟩

Premises used: compl_le_of_compl_le, Iff.intro
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x : α
inst : BooleanAlgebra α
⊢ xᶜ ≤ x ↔ x = ⊤

Tactic:
simpa using le_compl_self (a := xᶜ)

Premises used: le_compl_self
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x : α
inst : BooleanAlgebra α
inst_1 : Nontrivial α
⊢ xᶜ < x ↔ x = ⊤

Tactic:
simpa using lt_compl_self (a := xᶜ)

Premises used: lt_compl_self
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : x ⊓ yᶜᶜ = x ⊓ y
rw₁ rw₂ : x ⊓ y = x ⊓ y
⊢ x \ yᶜ = x ⊓ y

Tactic:
rw [sdiff_eq, compl_compl]

Premises used: compl_compl, sdiff_eq
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : x ⊓ y ⊔ x \ y = x
rw₁ rw₂ : x = x
⊢ x ⊓ y ⊔ x ⊓ yᶜ = x

Tactic:
rw [← sdiff_eq, sup_inf_sdiff _ _]

Premises used: sdiff_eq, sup_inf_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : (x ⊓ yᶜ)ᶜ = x ⇨ y
rw₁ : (x ⊓ yᶜ)ᶜ = y ⊔ xᶜ
rw₂ : xᶜ ⊔ yᶜᶜ = y ⊔ xᶜ
rw₃ : xᶜ ⊔ y = y ⊔ xᶜ
rw₄ rw₅ : y ⊔ xᶜ = y ⊔ xᶜ
⊢ (x \ y)ᶜ = x ⇨ y

Tactic:
rw [sdiff_eq, himp_eq, compl_inf, compl_compl, sup_comm]

Premises used: compl_inf, compl_compl, himp_eq, sdiff_eq, sup_comm
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ (x ⇨ y)ᶜ = x \ y

Tactic:
@compl_sdiff αᵒᵈ _ _ _

Premises used: compl_sdiff, OrderDual
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : xᶜ ⊓ y = y \ x
rw₁ : xᶜ ⊓ y = y ⊓ xᶜ
rw₂ rw₃ : y ⊓ xᶜ = y ⊓ xᶜ
⊢ xᶜ \ yᶜ = y \ x

Tactic:
rw [sdiff_compl, sdiff_eq, inf_comm]

Premises used: sdiff_eq, inf_comm, sdiff_compl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ xᶜ ⇨ yᶜ = y ⇨ x

Tactic:
@compl_sdiff_compl αᵒᵈ _ _ _

Premises used: compl_sdiff_compl, OrderDual
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : y ≤ xᶜᶜ ↔ y ≤ x
rw₁ rw₂ : y ≤ x ↔ y ≤ x
⊢ Disjoint xᶜ y ↔ y ≤ x

Tactic:
rw [← le_compl_iff_disjoint_left, compl_compl]

Premises used: compl_compl, le_compl_iff_disjoint_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : x ≤ yᶜᶜ ↔ x ≤ y
rw₁ rw₂ : x ≤ y ↔ x ≤ y
⊢ Disjoint x yᶜ ↔ x ≤ y

Tactic:
rw [← le_compl_iff_disjoint_right, compl_compl]

Premises used: compl_compl, le_compl_iff_disjoint_right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ Codisjoint (x ⇨ y) x

Tactic:
@disjoint_sdiff_self_left αᵒᵈ _ _ _

Premises used: Codisjoint, OrderDual, disjoint_sdiff_self_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ Codisjoint x (x ⇨ y)

Tactic:
@disjoint_sdiff_self_right αᵒᵈ _ _ _

Premises used: disjoint_sdiff_self_right, Codisjoint, OrderDual
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : BooleanAlgebra α
rw : y ≤ z → (xᶜ ≤ z ↔ Codisjoint x z)
⊢ x ⇨ y ≤ z ↔ y ≤ z ∧ Codisjoint x z

Tactic:
rw [himp_eq, sup_le_iff, and_congr_right_iff]

Premises used: himp_eq, and_congr_right_iff, sup_le_iff
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : BooleanAlgebra α
⊢ y ≤ z → (xᶜ ≤ z ↔ Codisjoint x z)

Tactic:
fun _ => hnot_le_iff_codisjoint_right

Premises used: hnot_le_iff_codisjoint_right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : BooleanAlgebra α
⊢ y ≤ z → (xᶜ ≤ z ↔ Codisjoint x z)

Tactic:
exact fun _ => hnot_le_iff_codisjoint_right

Premises used: hnot_le_iff_codisjoint_right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ x ⇨ y ≤ x ↔ x = ⊤

Tactic:
⟨fun h ↦ codisjoint_self.1 <| codisjoint_himp_self_right.mono_right h, fun h ↦ le_top.trans h.ge⟩

Premises used: Eq.ge, codisjoint_self, le_top, Iff.intro, Iff.mp, Codisjoint.mono_right, LE.le.trans, codisjoint_himp_self_right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : x ⇨ y = ⊤ ∧ x = ⊤ ↔ x = ⊤ ∧ y = ⊤
⊢ x ⇨ y = x ↔ x = ⊤ ∧ y = ⊤

Tactic:
rw [codisjoint_himp_self_left.eq_iff]

Premises used: Codisjoint.eq_iff, codisjoint_himp_self_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ x ⇨ y = ⊤ ∧ x = ⊤ ↔ x = ⊤ ∧ y = ⊤

Tactic:
aesop
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ x ⇨ y ≠ x ↔ x ≠ ⊤ ∨ y ≠ ⊤

Tactic:
himp_eq_left.not.trans not_and_or

Premises used: Iff.not, himp_eq_left, not_and_or, Iff.trans
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ Codisjoint x y ↔ yᶜ ≤ x

Tactic:
hnot_le_iff_codisjoint_left.symm

Premises used: hnot_le_iff_codisjoint_left, Iff.symm
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ Codisjoint x y ↔ xᶜ ≤ y

Tactic:
hnot_le_iff_codisjoint_right.symm

Premises used: Iff.symm, hnot_le_iff_codisjoint_right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x_1 y z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x : α × β
left : (x ⊓ xᶜ).fst ≤ fst.{u, u_1} (β := β) ⊥
right : (x ⊓ xᶜ).snd ≤ snd.{u, u_1} (α := α) ⊥
⊢ x ⊓ xᶜ ≤ ⊥

Tactic:
constructor
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x_1 y z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x : α × β
⊢ (x ⊓ xᶜ).fst ≤ fst.{u, u_1} (β := β) ⊥

Tactic:
simp
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x_1 y z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x : α × β
⊢ (x ⊓ xᶜ).snd ≤ snd.{u, u_1} (α := α) ⊥

Tactic:
simp
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x_1 y z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x : α × β
left : fst.{u, u_1} (β := β) ⊤ ≤ (x ⊔ xᶜ).fst
right : snd.{u, u_1} (α := α) ⊤ ≤ (x ⊔ xᶜ).snd
⊢ ⊤ ≤ x ⊔ xᶜ

Tactic:
constructor
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x_1 y z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x : α × β
⊢ fst.{u, u_1} (β := β) ⊤ ≤ (x ⊔ xᶜ).fst

Tactic:
simp
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x_1 y z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x : α × β
⊢ snd.{u, u_1} (α := α) ⊤ ≤ (x ⊔ xᶜ).snd

Tactic:
simp
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x_1 y_1 z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x y : α × β
fst : (x \ y).fst = (x ⊓ yᶜ).fst
snd : (x \ y).snd = (x ⊓ yᶜ).snd
⊢ x \ y = x ⊓ yᶜ

Tactic:
ext
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x_1 y_1 z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x y : α × β
⊢ (x \ y).fst = (x ⊓ yᶜ).fst

Tactic:
simp [sdiff_eq]

Premises used: sdiff_eq
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x_1 y_1 z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x y : α × β
⊢ (x \ y).snd = (x ⊓ yᶜ).snd

Tactic:
simp [sdiff_eq]

Premises used: sdiff_eq
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x_1 y_1 z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x y : α × β
fst : (x ⇨ y).fst = (y ⊔ xᶜ).fst
snd : (x ⇨ y).snd = (y ⊔ xᶜ).snd
⊢ x ⇨ y = y ⊔ xᶜ

Tactic:
ext
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x_1 y_1 z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x y : α × β
⊢ (x ⇨ y).fst = (y ⊔ xᶜ).fst

Tactic:
simp [himp_eq]

Premises used: himp_eq
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x_1 y_1 z : α
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
x y : α × β
⊢ (x ⇨ y).snd = (y ⊔ xᶜ).snd

Tactic:
simp [himp_eq]

Premises used: himp_eq
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b : α
rw : f (a ⊓ b) ⊔ f (a \ b) = f a
rw₁ : f (a ⊓ b) ⊔ f a \ f b = f a
rw₂ : f a ⊓ f b ⊔ f a \ f b = f a
rw₃ rw₄ : f a = f a
⊢ f (a ⊓ b ⊔ a \ b) = f a

Tactic:
rw [map_sup, map_sdiff, map_inf, sup_inf_sdiff]

Premises used: sup_inf_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b : α
rw : f (a ⊓ b) ⊓ f (a \ b) = f ⊥
rw₁ : f (a ⊓ b) ⊓ f a \ f b = f ⊥
rw₂ : f a ⊓ f b ⊓ f a \ f b = f ⊥
rw₃ : ⊥ = f ⊥
rw₄ rw₅ : Eq.{u_1 + 1} (α := β) ⊥ ⊥
⊢ f (a ⊓ b ⊓ a \ b) = f ⊥

Tactic:
rw [map_inf, map_sdiff, map_inf, inf_inf_sdiff, map_bot]

Premises used: inf_inf_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : SDiff α
inst_8 : HImp α
inst_9 : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
rw : f a ⊓ (f a)ᶜ = f ⊥
rw₁ : ⊥ = f ⊥
rw₂ rw₃ : Eq.{u_1 + 1} (α := β) ⊥ ⊥
⊢ f a ⊓ f aᶜ = f ⊥

Tactic:
rw [map_compl, inf_compl_eq_bot, map_bot]

Premises used: inf_compl_eq_bot
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : SDiff α
inst_8 : HImp α
inst_9 : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
rw : f a ⊔ (f a)ᶜ = f ⊤
rw₁ : ⊤ = f ⊤
rw₂ rw₃ : Eq.{u_1 + 1} (α := β) ⊤ ⊤
⊢ f a ⊔ f aᶜ = f ⊤

Tactic:
rw [map_compl, sup_compl_eq_top, map_top]

Premises used: sup_compl_eq_top
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : SDiff α
inst_8 : HImp α
inst_9 : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b : α
rw : f a ⊓ (f b)ᶜ = f a ⊓ f bᶜ
rw₁ rw₂ : f a ⊓ (f b)ᶜ = f a ⊓ (f b)ᶜ
⊢ f a ⊓ (f b)ᶜ = f (a ⊓ bᶜ)

Tactic:
rw [map_inf, map_compl]
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : SDiff α
inst_8 : HImp α
inst_9 : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b : α
rw : f b ⊔ (f a)ᶜ = f b ⊔ f aᶜ
rw₁ rw₂ : f b ⊔ (f a)ᶜ = f b ⊔ (f a)ᶜ
⊢ f b ⊔ (f a)ᶜ = f (b ⊔ aᶜ)

Tactic:
rw [map_sup, map_compl]
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
le : ∀ {x y : α}, LE.le.{u_1} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_1} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_bot : Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_sdiff :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)
⊢ GeneralizedBooleanAlgebra α

Tactic:
apply e.injective.generalizedBooleanAlgebra

Premises used: Function.Injective.generalizedBooleanAlgebra, Equiv.injective
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
x_1 y_1 : α
⊢ LE.le.{u_1} (α := β) ((e : (a : α) → β) x_1 : β) ((e : (a : α) → β) y_1 : β) ↔ x_1 ≤ y_1

Tactic:
rfl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
x_1 y_1 : α
⊢ LE.le.{u_1} (α := β) ((e : (a : α) → β) x_1 : β) ((e : (a : α) → β) y_1 : β) ↔ x_1 ≤ y_1

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
x_1 y_1 : α
⊢ LT.lt.{u_1} (α := β) ((e : (a : α) → β) x_1 : β) ((e : (a : α) → β) y_1 : β) ↔ x_1 < y_1

Tactic:
rfl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
x_1 y_1 : α
⊢ LT.lt.{u_1} (α := β) ((e : (a : α) → β) x_1 : β) ((e : (a : α) → β) y_1 : β) ↔ x_1 < y_1

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
a b : α
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
a b : α
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
a b : α
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
a b : α
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
a b : α
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
a b : α
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
a b : α
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
a b : α
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
a b : α
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply