awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
map_himp :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)
map_hnot : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)
map_sdiff :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)
⊢ CompletelyDistribLattice α

Tactic:
apply e.injective.completelyDistribLattice

Premises used: Function.Injective.completelyDistribLattice, Equiv.injective
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
x y : α
⊢ LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
rfl
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
x y : α
⊢ LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
x y : α
⊢ LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
rfl
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
x y : α
⊢ LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a b : α
⊢ Eq.{v + 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.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a b : α
⊢ Eq.{v + 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.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a b : α
⊢ Eq.{v + 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.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a b : α
⊢ Eq.{v + 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.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a b : α
⊢ Eq.{v + 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.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a b : α
⊢ Eq.{v + 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.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
s : Set α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
s : Set α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
s : Set α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
s : Set α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
s : Set α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
s : Set α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a b : α
⊢ Eq.{v + 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.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a b : α
⊢ Eq.{v + 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.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a b : α
⊢ Eq.{v + 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.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a b : α
⊢ Eq.{v + 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.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a b : α
⊢ Eq.{v + 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.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a b : α
⊢ Eq.{v + 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.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
map_himp :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)
map_sdiff :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)
⊢ CompleteBooleanAlgebra α

Tactic:
apply e.injective.completeBooleanAlgebra

Premises used: Function.Injective.completeBooleanAlgebra, Equiv.injective
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
x y : α
⊢ LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
rfl
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
x y : α
⊢ LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
x y : α
⊢ LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
rfl
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
x y : α
⊢ LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
a b : α
⊢ Eq.{v + 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.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
a b : α
⊢ Eq.{v + 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.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
a b : α
⊢ Eq.{v + 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.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
a b : α
⊢ Eq.{v + 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.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
a b : α
⊢ Eq.{v + 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.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
a b : α
⊢ Eq.{v + 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.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
s : Set α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
s : Set α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
s : Set α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
s : Set α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
s : Set α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
s : Set α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply