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

Goal state before:
pp: α : Type u_8
β : α → Type u_9
ι : Sort u_10
inst✝ : (i : α) → SupSet (β i)
f : ι → (a : α) → β a
a : α
⊢ sSup (range ((fun f ↦ f a) ∘ f)) = sSup (range fun i ↦ f i a)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
π : α → Type u_12
α' : Type u_13
s : α' → Set α
t : (a : α) → Set (π a)
f : (i : α) → π i
⊢ (∀ (i : α) (x : α'), i ∈ s x → f i ∈ t i) ↔ ∀ (i : α'), ∀ i_1 ∈ s i, f i_1 ∈ t i_1

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ h₂ : b₁ ∈ t a₁
eq : sigmaToiUnion t ⟨a₁, ⟨b₁, h₁⟩⟩ = sigmaToiUnion t ⟨a₁, ⟨b₁, h₂⟩⟩
⊢ ↑(Eq.recOn ⋯ ⟨a₁, ⟨b₁, h₁⟩⟩.snd) = ↑⟨a₁, ⟨b₁, h₂⟩⟩.snd

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : (i : α) × ↑(t i)
⊢ ↑((unionEqSigmaOfDisjoint h).symm x) = ↑x.snd

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: case le
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: case lt
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: case map_sup
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
rfl

Goal state after:
case map_sup
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : ↑(⋃ i, t i)
⊢ ↑((unionEqSigmaOfDisjoint h) x).snd = ↑((unionEqSigmaOfDisjoint h).symm ((unionEqSigmaOfDisjoint h) x))

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: case map_inf
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
rfl

Goal state after:
case map_inf
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: case map_sSup
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
s✝ : Set α
⊢ e (sSup s✝) = ⨆ a ∈ s✝, e a

Tactic:
rfl

Goal state after:
case map_sSup
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
s✝ : Set α
⊢ e (sSup s✝) = ⨆ a ∈ s✝, e a
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: case map_sInf
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
s✝ : Set α
⊢ e (sInf s✝) = ⨅ a ∈ s✝, e a

Tactic:
rfl

Goal state after:
case map_sInf
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
s✝ : Set α
⊢ e (sInf s✝) = ⨅ a ∈ s✝, e a
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: case map_top
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := ⋯
bot : Bot α := ⋯
supSet : SupSet α := ⋯
infSet : InfSet α := ⋯
lattice : Lattice α := ⋯
⊢ e ⊤ = ⊤

Tactic:
rfl

Goal state after:
case map_top
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := ⋯
bot : Bot α := ⋯
supSet : SupSet α := ⋯
infSet : InfSet α := ⋯
lattice : Lattice α := ⋯
⊢ e ⊤ = ⊤
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: case map_bot
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := ⋯
bot : Bot α := ⋯
supSet : SupSet α := ⋯
infSet : InfSet α := ⋯
lattice : Lattice α := ⋯
⊢ e ⊥ = ⊥

Tactic:
rfl

Goal state after:
case map_bot
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := ⋯
bot : Bot α := ⋯
supSet : SupSet α := ⋯
infSet : InfSet α := ⋯
lattice : Lattice α := ⋯
⊢ e ⊥ = ⊥
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case lt
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sup
α : 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✝

Tactic:
rfl

Goal state after:
case map_sup
α : 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 map_inf
α : 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✝

Tactic:
rfl

Goal state after:
case map_inf
α : 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 map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
s✝ : Set α
⊢ e (sSup s✝) = ⨆ a ∈ s✝, e a

Tactic:
rfl

Goal state after:
case map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
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✝ : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
s✝ : Set α
⊢ e (sInf s✝) = ⨅ a ∈ s✝, e a

Tactic:
rfl

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:
rfl

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:
rfl

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 α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ

Tactic:
rfl

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 α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝

Tactic:
rfl

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.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ⊤ ∈ lowerBounds (upperBounds s)

Tactic:
· rintro (⟨⟩ | b) hb
      · exact le_rfl
      · exfalso
        apply h₂
        use b
        intro a ha
        exact coe_le_coe.1 (hb ha)

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ∈ lowerBounds s

Tactic:
· rintro (⟨⟩ | a) ha
      · exact le_top
      refine coe_le_coe.2 (csInf_le ?_ ha)
      rcases hs with ⟨⟨⟩ | b, hb⟩
      · exfalso
        apply h
        intro c hc
        rw [mem_singleton_iff, ← top_le_iff]
        exact hb hc
      use b
      intro c hc
      exact coe_le_coe.1 (hb hc)

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
rfl

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.Interval.Set.LinearOrder

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

Tactic:
grind

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
ht : BddBelow (f '' ∅)
hf : MonotoneOn f ∅
hst : ∅ ⊆ ∅
h : ∀ y ∈ ∅, ∃ x ∈ ∅, x ≤ y
⊢ sInf (f '' ∅) = sInf (f '' ∅)

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
rfl

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.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
this : c ≤ a ∧ b ≤ d
⊢ c < d

Tactic:
grind

Goal state after:
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
this✝ : c ≤ a ∧ b ≤ d
this : a ≤ c ∧ d ≤ b
⊢ a = c ∧ b = d

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

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

Tactic:
grind

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
rfl

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.Interval.Set.LinearOrder

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

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

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

Tactic:
grind

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
rfl

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:
rfl

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:
rfl

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.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc a b)
⊢ Icc a b = ⇑ofDual ⁻¹' Icc a b

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
rfl

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 α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝

Tactic:
rfl

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 : α
h : c < max a b
⊢ Ioo a b ∪ Ioi c = Ioi (min a c)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : c ≤ max a b
⊢ Ico a b ∪ Ici c = Ici (min a c)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : c ≤ max a b
⊢ Ioc a b ∪ Ioi c = Ioi (min a c)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : c ≤ max a b
⊢ Icc a b ∪ Ici c = Ici (min a c)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
b c d : α
h : min c d ≤ b
⊢ Iio b ∪ Ico c d = Iio (max b d)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
b c d : α
h : min c d < b
⊢ Iic b ∪ Ioc c d = Iic (max b d)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
b c d : α
h : min c d < b
⊢ Iio b ∪ Ioo c d = Iio (max b d)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
b c d : α
h : min c d ≤ b
⊢ Iic b ∪ Icc c d = Iic (max b d)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : c ≤ b
h₂ : a ≤ d
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : c < b
h₂ : a < d
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Ico a₁ b₁ ∩ Ico a₂ b₂ = Ico (max a₁ a₂) (min b₁ b₂)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Ioo a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (max a₁ a₂) (min b₁ b₂)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ioo a b ∩ Iio c = Ioo a (min b c)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Iio a ∩ Ioo b c = Ioo b (min a c)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : b₁ < b₂
⊢ Ioc a₁ b₁ ∩ Ioo a₂ b₂ = Ioc (max a₁ a₂) b₁

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : b₂ ≤ b₁
⊢ Ioc a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (max a₁ a₂) b₂

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : b₁ ≤ b₂
⊢ Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioo (max a₁ a₂) b₁

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : b₂ < b₁
⊢ Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (max a₁ a₂) b₂

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ico a b \ Iio c = Ico (max a c) b

Tactic:
grind

Goal state after: