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

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
this : (p : Prop) → Decidable p
o : Option α
⊢ (↑o).toOption = (↑o).toOption
Module: Mathlib.Data.Part

Goal state before:
pp: case inr
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ y ≤ x

Tactic:
;

Goal state after:
case inr
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ y ≤ x
Module: Mathlib.Data.Part

Goal state before:
pp: case inr
α : Type u_1
x y z : Part α
hx✝ : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx : b ∈ z
⊢ b' ∈ x

Tactic:
;

Goal state after:
case inr
α : Type u_1
x y z : Part α
hx✝ : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx : b ∈ z
⊢ b' ∈ x
Module: Mathlib.Data.Part

Goal state before:
pp: case inr
α : Type u_1
x y z : Part α
hx✝¹ : x ≤ z
hy✝ : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx✝ : b ∈ z
hy : b' ∈ z
hx : b = b'
⊢ b' ∈ x

Tactic:
;

Goal state after:
case inr
α : Type u_1
x y z : Part α
hx✝¹ : x ≤ z
hy✝ : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx✝ : b ∈ z
hy : b' ∈ z
hx : b = b'
⊢ b' ∈ x
Module: Mathlib.Order.BourbakiWitt

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

Tactic:
intro y hy
      exact hy (Ici x) (ici_isAdmissible le_map)

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 γ
⊢ (x.bind fun x ↦ (some (f x)).bind g) = x.bind fun y ↦ g (f y)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_4
f : α → β
x : Part α
g : β → Part γ
⊢ (x.bind fun x ↦ (some (f x)).bind g) = x.bind fun y ↦ g (f y)
Module: Mathlib.Data.Part

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
⊢ (x.bind fun x ↦ (f x).bind fun y ↦ some (g y)) = x.bind fun y ↦ map g (f y)
Module: Mathlib.Data.Part

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
γ : Type u_3
α✝ : Type u_4
Dom✝ : Prop
get✝ : Dom✝ → α✝
⊢ id <$> { Dom := Dom✝, get := get✝ } = { Dom := Dom✝, get := get✝ }

Tactic:
;

Goal state after:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
α✝ : Type u_4
Dom✝ : Prop
get✝ : Dom✝ → α✝
⊢ id <$> { Dom := Dom✝, get := get✝ } = { Dom := Dom✝, get := get✝ }
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 γ
f : ℕ → α
hf : Monotone f
⊢ ∀ ⦃a₂ : Chain α⦄,
    (fun c ↦ ⇑c.toOrderHom) { toFun := f, monotone' := hf } = (fun c ↦ ⇑c.toOrderHom) a₂ →
      { toFun := f, monotone' := hf } = a₂

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : ℕ → α
hf : Monotone f
⊢ ∀ ⦃a₂ : Chain α⦄,
    (fun c ↦ ⇑c.toOrderHom) { toFun := f, monotone' := hf } = (fun c ↦ ⇑c.toOrderHom) a₂ →
      { toFun := f, monotone' := hf } = a₂
Module: Mathlib.Data.Part

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

Tactic:
;

Goal state after:
α : Type u_1
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map id o = o
Module: Mathlib.Order.OmegaCompletePartialOrder

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

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : Preorder α
c : Chain α
x✝ : ℕ
⊢ (c.map OrderHom.id) x✝ = c x✝
Module: Mathlib.Order.OmegaCompletePartialOrder

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

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : Preorder α
a b : α
hab : a ≤ b
x✝ : α
⊢ x✝ ∈ Set.range ⇑(pair a b hab) ↔ x✝ ∈ {a, b}
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inl.inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hzy✝ : z ≤ y
hzy : z < y
⊢ f z ≤ y

Tactic:
;

Goal state after:
case image_self_subset_self.inl.inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hzy✝ : z ≤ y
hzy : z < y
⊢ f z ≤ y
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₂
n : ℕ
⊢ ((pair a₁ a₂ ha).zip (pair b₁ b₂ hb)) n = (pair (a₁, b₁) (a₂, b₂) ⋯) n

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
n : ℕ
⊢ ((pair a₁ a₂ ha).zip (pair b₁ b₂ hb)) n = (pair (a₁, b₁) (a₂, b₂) ⋯) n
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inl.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
z : α
hz : z ∈ bot x f
hy : IsExtremePt x f z
hzy : z ≤ z
⊢ f z ≤ f z

Tactic:
;

Goal state after:
case image_self_subset_self.inl.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
z : α
hz : z ∈ bot x f
hy : IsExtremePt x f z
hzy : z ≤ z
⊢ f z ≤ f z
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ h_1, o.get ⋯ = a) ↔ p ∧ ∃ h, o.get h = a

Tactic:
;

Goal state after:
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ h_1, o.get ⋯ = a) ↔ p ∧ ∃ h, o.get h = a
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) ≤ ωSup (c.map f)

Tactic:
;

Goal state after:
ι : 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) ≤ ωSup (c.map f)
Module: Mathlib.Data.Part

Goal state before:
pp: case mpr
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
w✝ : o.Dom
h₂ : o.get w✝ = a
⊢ ∃ h_1, o.get ⋯ = a

Tactic:
;

Goal state after:
case mpr
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
w✝ : o.Dom
h₂ : o.get w✝ = a
⊢ ∃ h_1, o.get ⋯ = a
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
⊢ ωSup (c.map f) ≤ f x

Tactic:
;

Goal state after:
ι : 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
⊢ ωSup (c.map f) ≤ f x
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hyz : f y ≤ z
⊢ f y ≤ f z

Tactic:
;

Goal state after:
case image_self_subset_self.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hyz : f y ≤ z
⊢ f y ≤ f z
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
⊢ ∀ (i : ℕ), (c.map f) i ≤ f x

Tactic:
;

Goal state after:
ι : 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
⊢ ∀ (i : ℕ), (c.map f) i ≤ f x
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 ⋯ = a.get ⋯ * b.get ⋯

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ (a * b).get ⋯ = a.get ⋯ * b.get ⋯
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
i : ℕ
⊢ (c.map f) i ≤ f x

Tactic:
;

Goal state after:
ι : 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
i : ℕ
⊢ (c.map f) i ≤ f x
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Inv α
a : Part α
ma : α
ha : ma ∈ a
⊢ ∃ a_1, a_1 ∈ a ∧ a_1⁻¹ = ma⁻¹

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Inv α
a : Part α
ma : α
ha : ma ∈ a
⊢ ∃ a_1, a_1 ∈ a ∧ a_1⁻¹ = ma⁻¹
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 : ∃ x_1, ¬c x_1 ≤ x
⊢ ∃ i, ¬c i ≤ x

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
h : ∀ (i : ℕ), c i ≤ x ∨ x ≤ c i
this : ∃ x_1, ¬c x_1 ≤ x
⊢ ∃ i, ¬c i ≤ x
Module: Mathlib.Data.Part

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Div α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 / a = ma / mb
Module: Mathlib.Data.Part

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Div α
a b : Part α
hab : (a / b).Dom
⊢ (a.bind fun y ↦ map (fun x ↦ y / x) b).get ⋯ = a.get ⋯ / b.get ⋯
Module: Mathlib.Data.Part

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Mod α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 % a = ma % mb
Module: Mathlib.Data.Part

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Mod α
a b : Part α
hab : (a % b).Dom
⊢ (a.bind fun y ↦ map (fun x ↦ y % x) b).get ⋯ = a.get ⋯ % b.get ⋯
Module: Mathlib.Data.Part

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Append α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 ++ a = ma ++ mb
Module: Mathlib.Order.BourbakiWitt

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

Tactic:
;

Goal state after:
case pos
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
h : ∀ z ∈ c, z ≤ y
⊢ cSup c ≤ y
Module: Mathlib.Data.Part

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Append α
a b : Part α
hab : (a ++ b).Dom
⊢ (a.bind fun y ↦ map (fun x ↦ y ++ x) b).get ⋯ = a.get ⋯ ++ b.get ⋯
Module: Mathlib.Data.Part

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Inter α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 ∩ a = ma ∩ mb
Module: Mathlib.Data.Part

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Inter α
a b : Part α
hab : (a ∩ b).Dom
⊢ (a.bind fun y ↦ map (fun x ↦ y ∩ x) b).get ⋯ = a.get ⋯ ∩ b.get ⋯
Module: Mathlib.Order.OmegaCompletePartialOrder

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

Tactic:
;

Goal state after:
case h
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
h : ωScottContinuous f
a b : α
hab : a ≤ b
⊢ (fun c ↦ Set.range ⇑c) (pair a b hab) = {a, b}
Module: Mathlib.Data.Part

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Union α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 ∪ a = ma ∪ mb
Module: Mathlib.Data.Part

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Union α
a b : Part α
hab : (a ∪ b).Dom
⊢ (a.bind fun y ↦ map (fun x ↦ y ∪ x) b).get ⋯ = a.get ⋯ ∪ b.get ⋯
Module: Mathlib.Data.Part

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : SDiff α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 \ a = ma \ mb
Module: Mathlib.Data.Part

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : SDiff α
a b : Part α
hab : (a \ b).Dom
⊢ (a.bind fun y ↦ map (fun x ↦ y \ x) b).get ⋯ = a.get ⋯ \ b.get ⋯
Module: Mathlib.Order.OmegaCompletePartialOrder

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

Tactic:
;

Goal state after:
α : Type u_2
c : Chain (Part α)
a b : α
hb : some b ∈ c
i : ℕ
ha : some a = c i
⊢ a = b
Module: Mathlib.Order.OmegaCompletePartialOrder

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

Tactic:
;

Goal state after:
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : c i = some a
j : ℕ
hb : some b = c j
⊢ a = b
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case inl
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hij : i ≤ j
this : a ∈ c.toOrderHom j
⊢ a = b

Tactic:
;

Goal state after:
case inl
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hij : i ≤ j
this : a ∈ c.toOrderHom j
⊢ a = b
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case inr
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hji : j ≤ i
this : b ∈ c.toOrderHom i
⊢ a = b

Tactic:
;

Goal state after:
case inr
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hji : j ≤ i
this : b ∈ c.toOrderHom i
⊢ a = b
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case inr
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hji : j ≤ i
this : b ∈ c.toOrderHom i
⊢ b = a

Tactic:
;

Goal state after:
case inr
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hji : j ≤ i
this : b ∈ c.toOrderHom i
⊢ b = a
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
c : Chain (Part α)
a : α
h : a ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none
⊢ some a ∈ c

Tactic:
;

Goal state after:
α : Type u_2
c : Chain (Part α)
a : α
h : a ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none
⊢ some a ∈ c
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 γ
a : α
⊢ f (ωSup c) a = ωSup (c.map { toFun := f, monotone' := ⋯ }) a

Tactic:
;

Goal state after:
α : 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 γ
a : α
⊢ f (ωSup c) a = ωSup (c.map { toFun := f, monotone' := ⋯ }) a
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 δ
toOrderHom✝¹ : α →o β
map_ωSup'✝¹ : ∀ (c : Chain α), toOrderHom✝¹.toFun (ωSup c) = ωSup (c.map toOrderHom✝¹)
toOrderHom✝ : α →o β
map_ωSup'✝ : ∀ (c : Chain α), toOrderHom✝.toFun (ωSup c) = ωSup (c.map toOrderHom✝)
h :
  (fun f ↦ f.toFun) { toOrderHom := toOrderHom✝¹, map_ωSup' := map_ωSup'✝¹ } =
    (fun f ↦ f.toFun) { toOrderHom := toOrderHom✝, map_ωSup' := map_ωSup'✝ }
⊢ { toOrderHom := toOrderHom✝¹, map_ωSup' := map_ωSup'✝¹ } = { toOrderHom := toOrderHom✝, map_ωSup' := map_ωSup'✝ }

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β
inst✝¹ : OmegaCompletePartialOrder γ
inst✝ : OmegaCompletePartialOrder δ
toOrderHom✝¹ : α →o β
map_ωSup'✝¹ : ∀ (c : Chain α), toOrderHom✝¹.toFun (ωSup c) = ωSup (c.map toOrderHom✝¹)
toOrderHom✝ : α →o β
map_ωSup'✝ : ∀ (c : Chain α), toOrderHom✝.toFun (ωSup c) = ωSup (c.map toOrderHom✝)
h :
  (fun f ↦ f.toFun) { toOrderHom := toOrderHom✝¹, map_ωSup' := map_ωSup'✝¹ } =
    (fun f ↦ f.toFun) { toOrderHom := toOrderHom✝, map_ωSup' := map_ωSup'✝ }
⊢ { toOrderHom := toOrderHom✝¹, map_ωSup' := map_ωSup'✝¹ } = { toOrderHom := toOrderHom✝, map_ωSup' := map_ωSup'✝ }
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 δ
toOrderHom✝¹ : α →o β
map_ωSup'✝¹ : ∀ (c : Chain α), toOrderHom✝¹.toFun (ωSup c) = ωSup (c.map toOrderHom✝¹)
toOrderHom✝ : α →o β
map_ωSup'✝ : ∀ (c : Chain α), toOrderHom✝.toFun (ωSup c) = ωSup (c.map toOrderHom✝)
h :
  (fun f ↦ f.toFun) { toOrderHom := toOrderHom✝¹, map_ωSup' := map_ωSup'✝¹ } =
    (fun f ↦ f.toFun) { toOrderHom := toOrderHom✝, map_ωSup' := map_ωSup'✝ }
⊢ toOrderHom✝¹ = toOrderHom✝

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β
inst✝¹ : OmegaCompletePartialOrder γ
inst✝ : OmegaCompletePartialOrder δ
toOrderHom✝¹ : α →o β
map_ωSup'✝¹ : ∀ (c : Chain α), toOrderHom✝¹.toFun (ωSup c) = ωSup (c.map toOrderHom✝¹)
toOrderHom✝ : α →o β
map_ωSup'✝ : ∀ (c : Chain α), toOrderHom✝.toFun (ωSup c) = ωSup (c.map toOrderHom✝)
h :
  (fun f ↦ f.toFun) { toOrderHom := toOrderHom✝¹, map_ωSup' := map_ωSup'✝¹ } =
    (fun f ↦ f.toFun) { toOrderHom := toOrderHom✝, map_ωSup' := map_ωSup'✝ }
⊢ toOrderHom✝¹ = toOrderHom✝
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 δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
map_ωSup'✝¹ :
  ∀ (c : Chain α),
    { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun (ωSup c) =
      ωSup (c.map { toFun := toFun✝¹, monotone' := monotone'✝¹ })
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
map_ωSup'✝ :
  ∀ (c : Chain α),
    { toFun := toFun✝, monotone' := monotone'✝ }.toFun (ωSup c) =
      ωSup (c.map { toFun := toFun✝, monotone' := monotone'✝ })
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, monotone' := monotone'✝¹, map_ωSup' := map_ωSup'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, monotone' := monotone'✝, map_ωSup' := map_ωSup'✝ }
⊢ { toFun := toFun✝¹, monotone' := monotone'✝¹, map_ωSup' := map_ωSup'✝¹ } =
    { toFun := toFun✝, monotone' := monotone'✝, map_ωSup' := map_ωSup'✝ }

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β
inst✝¹ : OmegaCompletePartialOrder γ
inst✝ : OmegaCompletePartialOrder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
map_ωSup'✝¹ :
  ∀ (c : Chain α),
    { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun (ωSup c) =
      ωSup (c.map { toFun := toFun✝¹, monotone' := monotone'✝¹ })
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
map_ωSup'✝ :
  ∀ (c : Chain α),
    { toFun := toFun✝, monotone' := monotone'✝ }.toFun (ωSup c) =
      ωSup (c.map { toFun := toFun✝, monotone' := monotone'✝ })
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, monotone' := monotone'✝¹, map_ωSup' := map_ωSup'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, monotone' := monotone'✝, map_ωSup' := map_ωSup'✝ }
⊢ { toFun := toFun✝¹, monotone' := monotone'✝¹, map_ωSup' := map_ωSup'✝¹ } =
    { toFun := toFun✝, monotone' := monotone'✝, map_ωSup' := map_ωSup'✝ }
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) z y

Tactic:
;

Goal state after:
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) z y
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case inr
α : 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 : f y ≤ z
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z

Tactic:
;

Goal state after:
case inr
α : 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 : f y ≤ z
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z