awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
a : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
a : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
a : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
a b : α
⊢ Eq.{u_3 + 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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
a b : α
⊢ Eq.{u_3 + 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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
a b : α
⊢ Eq.{u_3 + 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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_top : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_hnot : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)
map_sdiff :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)
⊢ CoheytingAlgebra α

Tactic:
apply e.injective.coheytingAlgebra

Premises used: Function.Injective.coheytingAlgebra, Equiv.injective
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
x y : α
⊢ LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
x y : α
⊢ LE.le.{u_3} (α := β) ((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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
x y : α
⊢ LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
x y : α
⊢ LT.lt.{u_3} (α := β) ((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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
a b : α
⊢ Eq.{u_3 + 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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
a b : α
⊢ Eq.{u_3 + 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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
a b : α
⊢ Eq.{u_3 + 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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
a b : α
⊢ Eq.{u_3 + 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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
a b : α
⊢ Eq.{u_3 + 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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
a b : α
⊢ Eq.{u_3 + 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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
a : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
a : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
a : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
a b : α
⊢ Eq.{u_3 + 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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
a b : α
⊢ Eq.{u_3 + 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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : CoheytingAlgebra β
generalizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α := e.generalizedCoheytingAlgebra
top : Top α := e.top
hnot : HNot α := e.hnot
a b : α
⊢ Eq.{u_3 + 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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_top : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
map_hnot : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)
map_himp :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)
map_sdiff :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)
⊢ BiheytingAlgebra α

Tactic:
apply e.injective.biheytingAlgebra

Premises used: Function.Injective.biheytingAlgebra, Equiv.injective
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
x y : α
⊢ LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
x y : α
⊢ LE.le.{u_3} (α := β) ((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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
x y : α
⊢ LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
x y : α
⊢ LT.lt.{u_3} (α := β) ((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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a b : α
⊢ Eq.{u_3 + 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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a b : α
⊢ Eq.{u_3 + 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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a b : α
⊢ Eq.{u_3 + 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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a b : α
⊢ Eq.{u_3 + 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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a b : α
⊢ Eq.{u_3 + 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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a b : α
⊢ Eq.{u_3 + 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.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply