mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case pos
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
hf : lfpApprox f x a ∈ fixedPoints ⇑f
i : Ordinal.{u}
h : i ≤ a
⊢ lfpApprox f x i ≤ lfpApprox f x a

pp: case neg
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
hf : lfpApprox f x a ∈ fixedPoints ⇑f
i : Ordinal.{u}
h : ¬i ≤ a
⊢ lfpApprox f x i ≤ lfpApprox f x a

Tactic:
·

Goal state after:
case pos
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
hf : lfpApprox f x a ∈ fixedPoints ⇑f
i : Ordinal.{u}
h : i ≤ a
⊢ lfpApprox f x i ≤ lfpApprox f x a
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case neg
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
hf : lfpApprox f x a ∈ fixedPoints ⇑f
i : Ordinal.{u}
h : ¬i ≤ a
⊢ lfpApprox f x i ≤ lfpApprox f x a

Tactic:
·

Goal state after:
case neg
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
hf : lfpApprox f x a ∈ fixedPoints ⇑f
i : Ordinal.{u}
h : ¬i ≤ a
⊢ lfpApprox f x i ≤ lfpApprox f x a
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u} := ⋯
hfix : lfpApprox f x o ∈ fixedPoints ⇑f
⊢ ↑(f.nextFixed x hx) ≤ lfpApprox f x o

pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u} := ⋯
hfix : lfpApprox f x o ∈ fixedPoints ⇑f
⊢ lfpApprox f x o ≤ ↑(f.nextFixed x hx)

Tactic:
·

Goal state after:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u} := ⋯
hfix : lfpApprox f x o ∈ fixedPoints ⇑f
⊢ ↑(f.nextFixed x hx) ≤ lfpApprox f x o
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u} := ⋯
hfix : lfpApprox f x o ∈ fixedPoints ⇑f
⊢ lfpApprox f x o ≤ ↑(f.nextFixed x hx)

Tactic:
·

Goal state after:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u} := ⋯
hfix : lfpApprox f x o ∈ fixedPoints ⇑f
⊢ lfpApprox f x o ≤ ↑(f.nextFixed x hx)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inl
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ (coeff b (b ^ e * x + y)) e = (single e x) e + (coeff b y) e

pp: case inr
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
⊢ (coeff b (b ^ e * x + y)) e' = (single e x) e' + (coeff b y) e'

Tactic:
·

Goal state after:
case inl
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ (coeff b (b ^ e * x + y)) e = (single e x) e + (coeff b y) e
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inr
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
⊢ (coeff b (b ^ e * x + y)) e' = (single e x) e' + (coeff b y) e'

Tactic:
·

Goal state after:
case inr
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
⊢ (coeff b (b ^ e * x + y)) e' = (single e x) e' + (coeff b y) e'
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case pos
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
h : e' ∈ map Prod.fst (CNF b y)
⊢ (coeff b (b ^ e * x + y)) e' = (coeff b y) e'

pp: case neg
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
h : e' ∉ map Prod.fst (CNF b y)
⊢ (coeff b (b ^ e * x + y)) e' = (coeff b y) e'

Tactic:
·

Goal state after:
case pos
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
h : e' ∈ map Prod.fst (CNF b y)
⊢ (coeff b (b ^ e * x + y)) e' = (coeff b y) e'
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
ha : f ⁻¹' Iic b = univ
⊢ IsClosed (f ⁻¹' Iic b)

pp: case inr
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
⊢ IsClosed (f ⁻¹' Iic b)

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
ha : f ⁻¹' Iic b = univ
⊢ IsClosed (f ⁻¹' Iic b)
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
⊢ IsClosed (f ⁻¹' Iic b)

Tactic:
·

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
⊢ IsClosed (f ⁻¹' Iic b)
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : f ⁻¹' Iic b = ∅
⊢ IsClosed (f ⁻¹' Iic b)

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
⊢ IsClosed (f ⁻¹' Iic b)

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : f ⁻¹' Iic b = ∅
⊢ IsClosed (f ⁻¹' Iic b)
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
⊢ IsClosed (f ⁻¹' Iic b)

Tactic:
·

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
⊢ IsClosed (f ⁻¹' Iic b)
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
a : α
ha : IsSuccLimit a
⊢ f a ∈ upperBounds (f '' Iio a)

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
a : α
ha : IsSuccLimit a
⊢ f a ∈ closure (f '' Iio a)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
a : α
ha : IsSuccLimit a
⊢ f a ∈ upperBounds (f '' Iio a)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case neg
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
h : e' ∉ map Prod.fst (CNF b y)
⊢ (coeff b (b ^ e * x + y)) e' = (coeff b y) e'

Tactic:
·

Goal state after:
case neg
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
h : e' ∉ map Prod.fst (CNF b y)
⊢ (coeff b (b ^ e * x + y)) e' = (coeff b y) e'
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
a : α
ha : IsSuccLimit a
⊢ f a ∈ closure (f '' Iio a)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
a : α
ha : IsSuccLimit a
⊢ f a ∈ closure (f '' Iio a)
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : IsMax a
⊢ IsOpen[inst✝²] {a}

pp: case neg
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : ¬IsMax a
⊢ IsOpen[inst✝²] {a}

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : IsMax a
⊢ IsOpen[inst✝²] {a}
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : ¬IsMax a
⊢ IsOpen[inst✝²] {a}

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : ¬IsMax a
⊢ IsOpen[inst✝²] {a}
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
h : IsOpen[inst✝³] {a}
ha : IsSuccLimit a
⊢ False

pp: case refine_2
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha : ¬IsSuccLimit a
⊢ IsOpen[inst✝³] {a}

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
h : IsOpen[inst✝³] {a}
ha : IsSuccLimit a
⊢ False
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inl
b e : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
⊢ eval b (single e 0 + f) = b ^ e * 0 + eval b f

pp: case inr
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
⊢ eval b (single e x + f) = b ^ e * x + eval b f

Tactic:
·

Goal state after:
case inl
b e : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
⊢ eval b (single e 0 + f) = b ^ e * 0 + eval b f
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha : ¬IsSuccLimit a
⊢ IsOpen[inst✝³] {a}

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha : ¬IsSuccLimit a
⊢ IsOpen[inst✝³] {a}
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case refine_2.inl
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha✝ : ¬IsSuccLimit a
ha : IsMin a
⊢ IsOpen[inst✝³] {a}

pp: case refine_2.inr
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha✝ : ¬IsSuccLimit a
ha : ¬IsSuccPrelimit a
⊢ IsOpen[inst✝³] {a}

Tactic:
·

Goal state after:
case refine_2.inl
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha✝ : ¬IsSuccLimit a
ha : IsMin a
⊢ IsOpen[inst✝³] {a}
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha✝ : ¬IsSuccLimit a
ha : ¬IsSuccPrelimit a
⊢ IsOpen[inst✝³] {a}

Tactic:
·

Goal state after:
case refine_2.inr
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha✝ : ¬IsSuccLimit a
ha : ¬IsSuccPrelimit a
⊢ IsOpen[inst✝³] {a}
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inr
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
⊢ foldr (fun p r ↦ b ^ p * (single e x + f) p + r) 0 (e :: f.support.sort fun x1 x2 ↦ x1 ≥ x2) = b ^ e * x + eval b f

pp: case inr.h₁
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
⊢ ∀ b ∈ f.support, e ≥ b

Tactic:
·

Goal state after:
case inr
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
⊢ foldr (fun p r ↦ b ^ p * (single e x + f) p + r) 0 (e :: f.support.sort fun x1 x2 ↦ x1 ≥ x2) = b ^ e * x + eval b f
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case pos
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
s : Set α
o : α
ho : o ∈ s
ho' : IsSuccLimit o
⊢ s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Ioo a o ⊆ s

pp: case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
s : Set α
o : α
ho : o ∈ s
ho' : ¬IsSuccLimit o
⊢ s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Ioo a o ⊆ s

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
s : Set α
o : α
ho : o ∈ s
ho' : IsSuccLimit o
⊢ s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Ioo a o ⊆ s
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
s : Set α
o : α
ho : o ∈ s
ho' : ¬IsSuccLimit o
⊢ s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Ioo a o ⊆ s

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
s : Set α
o : α
ho : o ∈ s
ho' : ¬IsSuccLimit o
⊢ s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Ioo a o ⊆ s
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case pos
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
ha : IsMin a
⊢ (∃ᶠ (y : α) in 𝓝 a, y ≠ a ∧ y ∈ s) ↔ ¬IsMin a ∧ ∀ b < a, (s ∩ Ioo b a).Nonempty

pp: case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
ha : ¬IsMin a
⊢ (∃ᶠ (y : α) in 𝓝 a, y ≠ a ∧ y ∈ s) ↔ ¬IsMin a ∧ ∀ b < a, (s ∩ Ioo b a).Nonempty

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
ha : IsMin a
⊢ (∃ᶠ (y : α) in 𝓝 a, y ≠ a ∧ y ∈ s) ↔ ¬IsMin a ∧ ∀ b < a, (s ∩ Ioo b a).Nonempty
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
ha : ¬IsMin a
⊢ (∃ᶠ (y : α) in 𝓝 a, y ≠ a ∧ y ∈ s) ↔ ¬IsMin a ∧ ∀ b < a, (s ∩ Ioo b a).Nonempty

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
ha : ¬IsMin a
⊢ (∃ᶠ (y : α) in 𝓝 a, y ≠ a ∧ y ∈ s) ↔ ¬IsMin a ∧ ∀ b < a, (s ∩ Ioo b a).Nonempty
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inr.h₁
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
⊢ ∀ b ∈ f.support, e ≥ b

Tactic:
·

Goal state after:
case inr.h₁
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
⊢ ∀ b ∈ f.support, e ≥ b
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case inl
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
x✝ : a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a) := x✝
he : s ∩ Iic a = ∅
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a

pp: case inr
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
x✝ : a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a) := x✝
hne : (s ∩ Iic a).Nonempty
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a

Tactic:
·

Goal state after:
case inl
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
x✝ : a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a) := x✝
he : s ∩ Iic a = ∅
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case inr
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
x✝ : a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a) := x✝
hne : (s ∩ Iic a).Nonempty
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a

Tactic:
·

Goal state after:
case inr
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
x✝ : a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a) := x✝
hne : (s ∩ Iic a).Nonempty
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case single_add
b e x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ e
a✝ : single e' y + f = f → eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)
⊢ eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)

Tactic:
obtain rfl | he' := (h e' (by simp [hy])).eq_or_lt

Goal state after:
case single_add.inl
b x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ e'
a✝ : single e' y + f = f → eval b (single e' x + (single e' y + f)) = b ^ e' * x + eval b (single e' y + f)
⊢ eval b (single e' x + (single e' y + f)) = b ^ e' * x + eval b (single e' y + f)

case single_add.inr
b e x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ e
a✝ : single e' y + f = f → eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)
he' : e' < e
⊢ eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case single_add.inl
b x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ e'
a✝ : single e' y + f = f → eval b (single e' x + (single e' y + f)) = b ^ e' * x + eval b (single e' y + f)
⊢ eval b (single e' x + (single e' y + f)) = b ^ e' * x + eval b (single e' y + f)

pp: case single_add.inr
b e x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ e
a✝ : single e' y + f = f → eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)
he' : e' < e
⊢ eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)

Tactic:
·

Goal state after:
case single_add.inl
b x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ e'
a✝ : single e' y + f = f → eval b (single e' x + (single e' y + f)) = b ^ e' * x + eval b (single e' y + f)
⊢ eval b (single e' x + (single e' y + f)) = b ^ e' * x + eval b (single e' y + f)
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case refine_1
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : Small.{u, u + 1} ↑t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1 ⊆ s, t_1.Nonempty ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
⊢ Nonempty (Shrink.{u, u + 1} ↑t)

pp: case refine_2
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : Small.{u, u + 1} ↑t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1 ⊆ s, t_1.Nonempty ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
⊢ ∀ (i : Shrink.{u, u + 1} ↑t), (Subtype.val ∘ ⇑(equivShrink ↑t).symm) i ∈ s

pp: case refine_3
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : Small.{u, u + 1} ↑t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1 ⊆ s, t_1.Nonempty ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
⊢ ⨆ i, (Subtype.val ∘ ⇑(equivShrink ↑t).symm) i = sSup t

Tactic:
·

Goal state after:
case refine_1
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : Small.{u, u + 1} ↑t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1 ⊆ s, t_1.Nonempty ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
⊢ Nonempty (Shrink.{u, u + 1} ↑t)