Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case le
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

pp: case lt
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

pp: case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

pp: case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

pp: case map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ ∀ (s : Set α), e (sSup s) = ⨆ a ∈ s, e a

pp: case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ ∀ (s : Set α), e (sInf s) = ⨅ a ∈ s, e a

pp: case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ e ⊤ = ⊤

pp: case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ e ⊥ = ⊥

pp: case map_compl
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ ∀ (a : α), e aᶜ = (e a)ᶜ

pp: case map_himp
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⇨ b) = e a ⇨ e b

Tactic:
<;>

Goal state after:
case le
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

case map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ ∀ (s : Set α), e (sSup s) = ⨆ a ∈ s, e a

case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ ∀ (s : Set α), e (sInf s) = ⨅ a ∈ s, e a

case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ e ⊤ = ⊤

case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ e ⊥ = ⊥

case map_compl
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ ∀ (a : α), e aᶜ = (e a)ᶜ

case map_himp
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⇨ b) = e a ⇨ e b