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

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ {x y : α}, e y ≤ e x ↔ y ≤ x

pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ {x y : α}, e y < e x ↔ y < x

pp: case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

Tactic:
<;>

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ {x y : α}, e y ≤ e x ↔ y ≤ x

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ {x y : α}, e y < e x ↔ y < x

case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e y✝ ≤ e x✝ ↔ y✝ ≤ x✝

pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e y✝ < e x✝ ↔ y✝ < x✝

pp: case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
<;>

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e y✝ ≤ e x✝ ↔ y✝ ≤ x✝

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e y✝ < e x✝ ↔ y✝ < x✝

case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := ⋯
semilatticeInf : SemilatticeInf α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := ⋯
semilatticeInf : SemilatticeInf α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

pp: case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := ⋯
semilatticeInf : SemilatticeInf α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

pp: case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := ⋯
semilatticeInf : SemilatticeInf α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

Tactic:
<;>

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := ⋯
semilatticeInf : SemilatticeInf α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := ⋯
semilatticeInf : SemilatticeInf α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := ⋯
semilatticeInf : SemilatticeInf α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := ⋯
semilatticeInf : SemilatticeInf α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

pp: case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

pp: case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
<;>

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

pp: case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

pp: case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

Tactic:
<;>

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := e.lattice
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := e.lattice
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

pp: case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := e.lattice
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

pp: case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := e.lattice
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
<;>

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := e.lattice
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := e.lattice
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := e.lattice
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := e.lattice
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNoneAux x)) = none
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

pp: case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNoneAux x)) = none
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case none.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNoneAux x)) = none
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

Tactic:
removeNoneAux_some _ ⟨_, h2⟩

Goal state after:
case none.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (e (some x)) = none
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ e.symm (some (e.removeNoneAux x)) = some x

Tactic:
removeNoneAux_some _ ⟨_, h2⟩

Goal state after:
case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ e.symm (e (some x)) = some x
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
b : α
hbt : ¬b ∈ t
⊢ b ∈ insert b (s \ t)

pp: case inr
α : Type u_1
s t : Set α
a b : α
hbt : ¬b ∈ t
hbs : b ∈ s
⊢ b ∈ insert a (s \ t)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
s t : Set α
b : α
hbt : ¬b ∈ t
⊢ b ∈ insert b (s \ t)

case inr
α : Type u_1
s t : Set α
a b : α
hbt : ¬b ∈ t
hbs : b ∈ s
⊢ b ∈ insert a (s \ t)
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : β
h : b = x
⊢ (fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e)) ((fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩)) b) = b

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : β
h : ¬b = x
⊢ (fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e)) ((fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩)) b) = b

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : β
h : b = x
⊢ (fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e)) ((fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩)) b) = b

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : β
h : ¬b = x
⊢ (fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e)) ((fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩)) b) = b
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: case pos
α : Type u_1
t s s' u : Set α
x : α
hx : x ∈ t
⊢ x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')

pp: case neg
α : Type u_1
t s s' u : Set α
x : α
hx : ¬x ∈ t
⊢ x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
t s s' u : Set α
x : α
hx : x ∈ t
⊢ x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')

case neg
α : Type u_1
t s s' u : Set α
x : α
hx : ¬x ∈ t
⊢ x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: case pos
α : Type u_1
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
x : α
hx : x ∈ t
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t

pp: case neg
α : Type u_1
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
x : α
hx : ¬x ∈ t
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
x : α
hx : x ∈ t
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t

case neg
α : Type u_1
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
x : α
hx : ¬x ∈ t
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: case pos
α : Type u_1
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
x : α
hx : x ∈ t
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂

pp: case neg
α : Type u_1
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
x : α
hx : ¬x ∈ t
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
x : α
hx : x ∈ t
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂

case neg
α : Type u_1
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
x : α
hx : ¬x ∈ t
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

pp: case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

pp: case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

pp: case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

pp: case map_top
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ e ⊤ = ⊤

pp: case map_himp
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ ∀ (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✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

case map_top
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ e ⊤ = ⊤

case map_himp
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ ∀ (a b : α), e (a ⇨ b) = e a ⇨ e b
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case none
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
a b : α✝
α : Type w
⊢ (fun s ↦ Sum.elim some (fun x ↦ none) s) ((fun o ↦ o.elim (inr PUnit.unit) inl) none) = none

pp: case some
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
a b : α✝
α : Type w
val✝ : α
⊢ (fun s ↦ Sum.elim some (fun x ↦ none) s) ((fun o ↦ o.elim (inr PUnit.unit) inl) (some val✝)) = some val✝

Tactic:
<;>

Goal state after:
case none
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
a b : α✝
α : Type w
⊢ (fun s ↦ Sum.elim some (fun x ↦ none) s) ((fun o ↦ o.elim (inr PUnit.unit) inl) none) = none

case some
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
a b : α✝
α : Type w
val✝ : α
⊢ (fun s ↦ Sum.elim some (fun x ↦ none) s) ((fun o ↦ o.elim (inr PUnit.unit) inl) (some val✝)) = some val✝
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
a b : α✝
α : Type w
val✝ : α
⊢ (fun o ↦ o.elim (inr PUnit.unit) inl) ((fun s ↦ Sum.elim some (fun x ↦ none) s) (inl val✝)) = inl val✝

pp: case inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
a b : α✝
α : Type w
⊢ (fun o ↦ o.elim (inr PUnit.unit) inl) ((fun s ↦ Sum.elim some (fun x ↦ none) s) (inr PUnit.unit)) = inr PUnit.unit

Tactic:
<;>

Goal state after:
case inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
a b : α✝
α : Type w
val✝ : α
⊢ (fun o ↦ o.elim (inr PUnit.unit) inl) ((fun s ↦ Sum.elim some (fun x ↦ none) s) (inl val✝)) = inl val✝

case inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
a b : α✝
α : Type w
⊢ (fun o ↦ o.elim (inr PUnit.unit) inl) ((fun s ↦ Sum.elim some (fun x ↦ none) s) (inr PUnit.unit)) = inr PUnit.unit
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

pp: case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

pp: case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

pp: case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

pp: case map_top
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ e ⊤ = ⊤

pp: case map_himp
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
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✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

case map_top
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ e ⊤ = ⊤

case map_himp
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

pp: case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

pp: case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

pp: case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

pp: case map_bot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ e ⊥ = ⊥

pp: case map_sdiff
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ ∀ (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✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

case map_bot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ e ⊥ = ⊥

case map_sdiff
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ ∀ (a b : α), e (a \ b) = e a \ e b
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

pp: case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

pp: case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

pp: case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

pp: case map_bot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ e ⊥ = ⊥

pp: case map_sdiff
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
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✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

case map_bot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ e ⊥ = ⊥

case map_sdiff
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝