mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
⊢ a.toOption.elim b f = if h : a.Dom then f (a.get h) else b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_4
⊢ (↑Option.none).Dom ↔ Option.none.isSome = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_4
a : α
⊢ (↑(Option.some a)).Dom ↔ (Option.some a).isSome = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_4
o : Option α
h₁ : (↑o).Dom
h₂ : { Dom := o.isSome = true, get := o.get }.Dom
⊢ (↑o).get h₁ = { Dom := o.isSome = true, get := o.get }.get h₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
o : Option α
⊢ (↑o).toOption = o

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
this : (p : Prop) → Decidable p
o : Option α
⊢ (fun o ↦ o.toOption) ↑o = (↑o).toOption

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a : Part α), none ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ f '' Ici x ⊆ Ici x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
⊢ x ≤ y ∨ y ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a : β
⊢ ¬a ∈ map f none

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
p : Prop
f : p → Part α
h : p
⊢ assert p f = f h

Tactic:
by

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ ∀ (c : NonemptyChain α), ↑c ⊆ Ici x → cSup c ∈ Ici x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
p : Prop
f : p → Part α
h : ¬p
⊢ assert p f = none

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
b : β
x : Part α
f : α → Part β
⊢ x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b

Tactic:
by

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsLeast (bot x f) x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
⊢ o.bind f = f (o.get h)

Tactic:
by

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ f '' bot x f ⊆ bot x f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → Part β
a : β
⊢ ¬a ∈ none.bind f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → Part β
⊢ ∀ (a_1 : β), a_1 ∈ (some a).bind f ↔ a_1 ∈ f a

Tactic:
by

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ ∀ (c : NonemptyChain α), ↑c ⊆ bot x f → cSup c ∈ bot x f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
o : Part α
a : α
h : a ∈ o
f : α → Part β
⊢ o.bind f = f a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
x : Part α
⊢ ∀ (a : β), (a ∈ x.bind fun y ↦ some (f y)) ↔ a ∈ map f x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun a ↦ (f a).toOption

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_4
f : Part α
g : α → Part β
k : β → Part γ
a : γ
⊢ a ∈ (f.bind g).bind k ↔ a ∈ f.bind fun x ↦ (g x).bind k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_4
f : α → β
x : Part α
g : β → Part γ
⊢ (map f x).bind g = x.bind fun y ↦ g (f y)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
⊢ map g (x.bind f) = x.bind fun y ↦ map g (f y)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
o : Part α
⊢ map g (map f o) = map (g ∘ f) o

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ {α β : Type u_4}, Functor.mapConst = Functor.map ∘ const β

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
α✝ : Type u_4
f : Part α✝
⊢ id <$> f = f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
α✝ β✝ : Type u_4
x : Part α✝
y : Part β✝
⊢ (x <* y).Dom ↔ (const β✝ <$> x <*> y).Dom

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
α✝ β✝ : Type u_4
x : Part α✝
y : Part β✝
⊢ (x *> y).Dom ↔ (const α✝ id <$> x <*> y).Dom

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
α✝ β✝ : Type u_4
x : α✝ → β✝
y : Part α✝
⊢ (pure x <*> y).Dom ↔ (x <$> y).Dom

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
α✝ β✝ : Type u_4
x : Part (α✝ → β✝)
y : Part α✝
⊢ (do
        let x ← x
        x <$> y).Dom ↔
    (x <*> y).Dom

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map f o = o

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
⊢ Function.Injective fun c ↦ ⇑c.toOrderHom

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
x : Part α
⊢ x.bind some = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
c : Chain α
f : α →o β
b : β
h : ∃ a ∈ c, f a = b
⊢ b ∈ c.map f

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
c : Chain α
⊢ c.map OrderHom.id = c

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g : β →o γ
a b : α
hab : a ≤ b
x✝² x✝¹ : ℕ
x✝ : x✝² ≤ x✝¹
⊢ (fun x ↦
        match x with
        | 0 => a
        | x => b)
      x✝² ≤
    (fun x ↦
        match x with
        | 0 => a
        | x => b)
      x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a b : α
hab : a ≤ b
x✝ : α
⊢ ((pair a b hab) 0 = x✝ ∨ ∃ n, (pair a b hab) (n + 1) = x✝) ↔ x✝ ∈ {a, b}

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a b : α
hab : a ≤ b
⊢ Set.range ⇑(pair a b hab) = {a, b}

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ (pair a₁ a₂ ha).zip (pair b₁ b₂ hb) = pair (a₁, b₁) (a₂, b₂) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: β α : Type u_2
x : Part α
f : α → Part β
y : Part β
⊢ x >>= f ≤ y ↔ ∀ (a : α), a ∈ x → f a ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), f x ≤ f y → x ≤ y
h' : ∀ (c : Chain β), f (ωSup₀ c) = ωSup (c.map f)
c : Chain β
i : ℕ
⊢ f (c i) ≤ f (ωSup₀ c)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ a ∈ restrict p o h ↔ p ∧ a ∈ o

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ (a * b).get ⋯ = ma * mb

Tactic:
by

Goal state after:
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ lfp f → p (f a)
hSup : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sSup s)
⊢ p (lfp f)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
a b : α
⊢ some a * some b = some (a * b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), f x ≤ f y → x ≤ y
h' : ∀ (c : Chain β), f (ωSup₀ c) = ωSup (c.map f)
c : Chain β
x : β
hx : ∀ (i : ℕ), c i ≤ x
⊢ f (ωSup₀ c) ≤ f x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Inv α
a : Part α
ma : α
ha : ma ∈ a
⊢ ma⁻¹ ∈ a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
h : ∀ (i : ℕ), c i ≤ x ∨ x ≤ c i
this : ¬∀ (i : ℕ), c i ≤ x
⊢ ∃ i, ¬c i ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
h : α →o α →o α
⊢ lfp (lfp.comp h) = lfp h.onDiag

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Div α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma / mb ∈ a / b

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c₀ c₁ : Chain α
h : c₀ ≤ c₁
i : ℕ
⊢ c₀ i ≤ ωSup c₁

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Div α
a b : Part α
hab : (a / b).Dom
⊢ (a / b).get hab = a.get ⋯ / b.get ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Div α
a b : α
⊢ some a / some b = some (a / b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
⊢ ωSup c ≤ x ↔ ∀ (i : ℕ), c i ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Mod α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma % mb ∈ a % b

Tactic:
by

Goal state after:
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ lfp f = ⨆ n, (⇑f)^[n] ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Mod α
a b : Part α
hab : (a % b).Dom
⊢ (a % b).get hab = a.get ⋯ % b.get ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Mod α
a b : α
⊢ some a % some b = some (a % b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ IsLUB (Set.range ⇑c) (ωSup c)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Append α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ++ mb ∈ a ++ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ChainClosure r ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₁ : ChainClosure r c₁
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ c₁ ∨ c₁ ⊆ c₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Append α
a b : Part α
hab : (a ++ b).Dom
⊢ (a ++ b).get hab = a.get ⋯ ++ b.get ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Append α
a b : α
⊢ some a ++ some b = some (a ++ b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Inter α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ∩ mb ∈ a ∩ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Inter α
a b : Part α
hab : (a ∩ b).Dom
⊢ (a ∩ b).get hab = a.get ⋯ ∩ b.get ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : IsLUB (Set.range ⇑c) a
⊢ a = ωSup c

Tactic:
by

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} = bot x f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Inter α
a b : α
⊢ some a ∩ some b = some (a ∩ b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
h : ωScottContinuous f
a b : α
hab : a ≤ b
⊢ {a, b} ∈ Set.range fun c ↦ Set.range ⇑c

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
c : Chain α
hf : ωScottContinuous f
⊢ Set.range ⇑c ∈ Set.range fun c ↦ Set.range ⇑c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Union α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ∪ mb ∈ a ∪ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
c : Chain α
hf : ωScottContinuous f
⊢ IsLUB (Set.range ⇑(c.map { toFun := f, monotone' := ⋯ })) (f (ωSup c))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Union α
a b : Part α
hab : (a ∪ b).Dom
⊢ (a ∪ b).get hab = a.get ⋯ ∪ b.get ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Union α
a b : α
⊢ some a ∪ some b = some (a ∪ b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : SDiff α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma \ mb ∈ a \ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : SDiff α
a b : Part α
hab : (a \ b).Dom
⊢ (a \ b).get hab = a.get ⋯ \ b.get ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : SDiff α
a b : α
⊢ some a \ some b = some (a \ b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: α : Type u_1
r : α → α → Prop
h : ∀ (c : Set α), IsChain r c → ∃ ub, ∀ a ∈ c, r a ub
trans : ∀ {a b c : α}, r a b → r b c → r a c
this✝ : ∃ ub, ∀ a ∈ maxChain r, r a ub
ub : α
hub : ∀ a ∈ maxChain r, r a ub
a : α
ha : r ub a
this : IsChain r (insert a (maxChain r))
⊢ a ∈ maxChain r

Tactic:
by

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
c : Set ↑s
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
⊢ IsChain (fun x1 x2 ↦ x1 ≤ x2) (Subtype.val '' c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
⊢ ∃ m, x ≤ m ∧ Maximal (fun x ↦ x ∈ s) m

Tactic:
by

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
⊢ ∃ m, x ≤ m ∧ IsMax m

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
⊢ ωScottContinuous f ↔ ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₁ : ChainClosure r c₁
hc₂ : ChainClosure r c₂
h : c₁ ⊆ c₂
⊢ c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α →o β
⊢ ωScottContinuous ⇑f ↔ ∀ (c : Chain α), f (ωSup c) = ωSup (c.map f)

Tactic:
by

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
⊢ ∃ z ∈ c, ¬f z ≤ y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₁ : ChainClosure r c₁
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
⊢ c₁ ⊆ c₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β
g : β → γ
hg : ωScottContinuous g
hf : ωScottContinuous f
⊢ ∀ (c : Chain α), (g ∘ f) (ωSup c) = ωSup (c.map { toFun := g ∘ f, monotone' := ⋯ })

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
c : Set α
hc : ChainClosure r c
⊢ IsChain r c

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
c : Chain (Part α)
a b : α
ha : some a ∈ c
hb : some b ∈ c
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
z : α
hz : z ∈ c
hzy : ¬f z ≤ y
⊢ y ≤ z

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
c : Chain (Part α)
a : α
h : a ∈ Part.ωSup c
⊢ some a ∈ c

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
⊢ c i ≤ Part.ωSup c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
⊢ ∃ M, IsMaxChain r M ∧ c ⊆ M

Tactic:
by

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
hab : a ≤ b
⊢ ∃ s, a ∈ s ∧ b ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
⊢ ∀ (c : Chain (Part α)) (x : Part α), (∀ (i : ℕ), c i ≤ x) → Part.ωSup c ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
x : α
c : Chain (Part α)
⊢ x ∈ ωSup c ↔ some x ∈ c

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
β : α → Type u_6
inst✝ : (a : α) → OmegaCompletePartialOrder (β a)
x✝¹ : Chain ((a : α) → β a)
x✝ : (a : α) → β a
hf : ∀ (i : ℕ), x✝¹ i ≤ x✝
a : α
⊢ ∀ (i : ℕ), (x✝¹.map (Pi.evalOrderHom a)) i ≤ x✝ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
γ : Type u_4
β : α → Type u_6
inst✝¹ : (x : α) → OmegaCompletePartialOrder (β x)
inst✝ : OmegaCompletePartialOrder γ
f : γ → (x : α) → β x
hf : ∀ (a : α), ωScottContinuous fun x ↦ f x a
c : Chain γ
⊢ f (ωSup c) = ωSup (c.map { toFun := f, monotone' := ⋯ })

Tactic:
by

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsAdmissible x f {y | IsExtremePt x f y}

Tactic:
by

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ {y | IsExtremePt x f y} = bot x f

Tactic:
by

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
⊢ y ∈ bot x f ↔ IsExtremePt x f y

Tactic:
by

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β
inst✝¹ : OmegaCompletePartialOrder γ
inst✝ : OmegaCompletePartialOrder δ
⊢ Function.Injective fun f ↦ f.toFun

Tactic:
by

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
a✝ : y ≠ z
left✝ : z ∈ bot x f
hz : z ≤ y
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z ∨ (fun x1 x2 ↦ x1 ≤ x2) z y

Tactic:
right; exact hz

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsChain (fun x1 x2 ↦ x1 ≤ x2) (bot x f)

Tactic:
by

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝¹ : ChainCompletePartialOrder α
f : α → α
inst✝ : Nonempty α
le_map : ∀ (x : α), x ≤ f x
⊢ (fixedPoints f).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), ωScottContinuous (f i)
⊢ ωScottContinuous (⨆ i, f i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α → β)
hs : ∀ f ∈ s, ωScottContinuous f
⊢ ωScottContinuous (SupSet.sSup s)

Tactic:
by

Goal state after: