mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
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

Tactic:
intros

Goal state after:
case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
s✝ : Set α
⊢ e (sInf s✝) = ⨅ a ∈ s✝, e a
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
intros

Goal state after:
case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ e ⊤ = ⊤
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
intros

Goal state after:
case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := ⋯
heytingAlgebra : HeytingAlgebra α := ⋯
⊢ e ⊥ = ⊥
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
intros

Goal state after:
case map_compl
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
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:
intros

Goal state after:
case map_himp
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
intros

Goal state after:
case le
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case lt
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

Tactic:
intros

Goal state after:
case lt
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

Tactic:
intros

Goal state after:
case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

Tactic:
intros

Goal state after:
case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ (s : Set α), e (sSup s) = ⨆ a ∈ s, e a

Tactic:
intros

Goal state after:
case map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
s✝ : Set α
⊢ e (sSup s✝) = ⨆ a ∈ s✝, e a
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ (s : Set α), e (sInf s) = ⨅ a ∈ s, e a

Tactic:
intros

Goal state after:
case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
s✝ : Set α
⊢ e (sInf s✝) = ⨅ a ∈ s✝, e a
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ e ⊤ = ⊤

Tactic:
intros

Goal state after:
case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ e ⊤ = ⊤
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ e ⊥ = ⊥

Tactic:
intros

Goal state after:
case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ e ⊥ = ⊥
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_hnot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ (a : α), e (￢a) = ￢e a

Tactic:
intros

Goal state after:
case map_hnot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ : α
⊢ e (￢a✝) = ￢e a✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sdiff
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a \ b) = e a \ e b

Tactic:
intros

Goal state after:
case map_sdiff
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h✝ : a < b ∨ c < d
h : Ico a b = Ico c d
⊢ a = c ∧ b = d

Tactic:
have : c ≤ a ∧ b ≤ d := (Ico_subset_Ico_iff (show a < b by grind [Set.nonempty_Ico])).1 h.subset

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h✝ : a < b ∨ c < d
h : Ico a b = Ico c d
this : c ≤ a ∧ b ≤ d
⊢ a = c ∧ b = d
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
intros

Goal state after:
case le
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := e.completeLattice
biheytingAlgebra : BiheytingAlgebra α := e.biheytingAlgebra
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case lt
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := ⋯
biheytingAlgebra : BiheytingAlgebra α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

Tactic:
intros

Goal state after:
case lt
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := e.completeLattice
biheytingAlgebra : BiheytingAlgebra α := e.biheytingAlgebra
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := ⋯
biheytingAlgebra : BiheytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

Tactic:
intros

Goal state after:
case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := e.completeLattice
biheytingAlgebra : BiheytingAlgebra α := e.biheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := ⋯
biheytingAlgebra : BiheytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

Tactic:
intros

Goal state after:
case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := e.completeLattice
biheytingAlgebra : BiheytingAlgebra α := e.biheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := ⋯
biheytingAlgebra : BiheytingAlgebra α := ⋯
⊢ ∀ (s : Set α), e (sSup s) = ⨆ a ∈ s, e a

Tactic:
intros

Goal state after:
case map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := e.completeLattice
biheytingAlgebra : BiheytingAlgebra α := e.biheytingAlgebra
s✝ : Set α
⊢ e (sSup s✝) = ⨆ a ∈ s✝, e a
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := ⋯
biheytingAlgebra : BiheytingAlgebra α := ⋯
⊢ ∀ (s : Set α), e (sInf s) = ⨅ a ∈ s, e a

Tactic:
intros

Goal state after:
case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := e.completeLattice
biheytingAlgebra : BiheytingAlgebra α := e.biheytingAlgebra
s✝ : Set α
⊢ e (sInf s✝) = ⨅ a ∈ s✝, e a
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := ⋯
biheytingAlgebra : BiheytingAlgebra α := ⋯
⊢ e ⊤ = ⊤

Tactic:
intros

Goal state after:
case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := ⋯
biheytingAlgebra : BiheytingAlgebra α := ⋯
⊢ e ⊤ = ⊤
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := ⋯
biheytingAlgebra : BiheytingAlgebra α := ⋯
⊢ e ⊥ = ⊥

Tactic:
intros

Goal state after:
case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := ⋯
biheytingAlgebra : BiheytingAlgebra α := ⋯
⊢ e ⊥ = ⊥
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_compl
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := ⋯
biheytingAlgebra : BiheytingAlgebra α := ⋯
⊢ ∀ (a : α), e aᶜ = (e a)ᶜ

Tactic:
intros

Goal state after:
case map_compl
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := e.completeLattice
biheytingAlgebra : BiheytingAlgebra α := e.biheytingAlgebra
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_himp
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := ⋯
biheytingAlgebra : BiheytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⇨ b) = e a ⇨ e b

Tactic:
intros

Goal state after:
case map_himp
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := e.completeLattice
biheytingAlgebra : BiheytingAlgebra α := e.biheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_hnot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := ⋯
biheytingAlgebra : BiheytingAlgebra α := ⋯
⊢ ∀ (a : α), e (￢a) = ￢e a

Tactic:
intros

Goal state after:
case map_hnot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := e.completeLattice
biheytingAlgebra : BiheytingAlgebra α := e.biheytingAlgebra
a✝ : α
⊢ e (￢a✝) = ￢e a✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sdiff
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := ⋯
biheytingAlgebra : BiheytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a \ b) = e a \ e b

Tactic:
intros

Goal state after:
case map_sdiff
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := e.completeLattice
biheytingAlgebra : BiheytingAlgebra α := e.biheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
intros

Goal state after:
case le
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case lt
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

Tactic:
intros

Goal state after:
case lt
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

Tactic:
intros

Goal state after:
case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

Tactic:
intros

Goal state after:
case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ (s : Set α), e (sSup s) = ⨆ a ∈ s, e a

Tactic:
intros

Goal state after:
case map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
s✝ : Set α
⊢ e (sSup s✝) = ⨆ a ∈ s✝, e a
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ (s : Set α), e (sInf s) = ⨅ a ∈ s, e a

Tactic:
intros

Goal state after:
case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
s✝ : Set α
⊢ e (sInf s✝) = ⨅ a ∈ s✝, e a
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ e ⊤ = ⊤

Tactic:
intros

Goal state after:
case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ e ⊤ = ⊤
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ e ⊥ = ⊥

Tactic:
intros

Goal state after:
case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ e ⊥ = ⊥
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_compl
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ (a : α), e aᶜ = (e a)ᶜ

Tactic:
intros

Goal state after:
case map_compl
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_himp
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ (a b : α), e (a ⇨ b) = e a ⇨ e b

Tactic:
intros

Goal state after:
case map_himp
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_hnot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ (a : α), e (￢a) = ￢e a

Tactic:
intros

Goal state after:
case map_hnot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a✝ : α
⊢ e (￢a✝) = ￢e a✝
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₂ : β
a₁ : α
hne : e a₁ ≠ b₂
⊢ (Disjoint on extend e f ⊥) (e a₁) b₂

Tactic:
rcases em (∃ a₂, e a₂ = b₂) with ⟨a₂, rfl⟩ | hb₂
    · simpa only [onFun, he.extend_apply] using! hf (ne_of_apply_ne e hne)
    · simpa only [onFun, extend_apply' _ _ _ hb₂] using! disjoint_bot_right

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sdiff
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := ⋯
⊢ ∀ (a b : α), e (a \ b) = e a \ e b

Tactic:
intros

Goal state after:
case map_sdiff
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
intros

Goal state after:
case le
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case lt
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := ⋯
booleanAlgebra : BooleanAlgebra α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

Tactic:
intros

Goal state after:
case lt
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := ⋯
booleanAlgebra : BooleanAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

Tactic:
intros

Goal state after:
case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := ⋯
booleanAlgebra : BooleanAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

Tactic:
intros

Goal state after:
case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
completeLattice : CompleteLattice α := e.completeLattice
booleanAlgebra : BooleanAlgebra α := e.booleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝