Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

pp: case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

pp: case map_sup
ι : 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✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

pp: case map_inf
ι : 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✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

pp: case map_top
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := ⋯
bot : Bot α := ⋯
compl : Compl α := ⋯
⊢ e ⊤ = ⊤

pp: case map_bot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := ⋯
bot : Bot α := ⋯
compl : Compl α := ⋯
⊢ e ⊥ = ⊥

pp: case map_compl
ι : 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✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ

pp: case map_himp
ι : 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✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝

Tactic:
<;>

Goal state after:
case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

case map_sup
ι : 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✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

case map_inf
ι : 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✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

case map_top
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := ⋯
bot : Bot α := ⋯
compl : Compl α := ⋯
⊢ e ⊤ = ⊤

case map_bot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := ⋯
bot : Bot α := ⋯
compl : Compl α := ⋯
⊢ e ⊥ = ⊥

case map_compl
ι : 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✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ

case map_himp
ι : 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✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝