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

Goal state before:
pp: α : Type u_1
motive : Lists' α true → Sort u_2
ofList : (l : List (Lists α)) → motive (Lists'.ofList l)
l : Lists' α true
⊢ motive (Lists'.ofList l.toList) = motive l

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
a y : Lists α
l : Lists' α true
⊢ a ∈ cons y l ↔ a ~ y ∨ a ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ lfpApprox f x a = ⨆ b, lfpApprox f x ↑b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
⊢ cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l₁ l₂ : List (Lists α)
h : l₁ ⊆ l₂
⊢ ofList l₁ ⊆ ofList l₂

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → x.1 ≤ log b o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l : Lists' α true
⊢ l ⊆ l

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b 0 → 0 < x.2

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
⊢ Monotone lfpApprox

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l : Lists' α true
⊢ l ⊆ nil → l = nil

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
a : Lists α
x✝ : Lists' α true
h : a ∈ nil.toList
⊢ a ∈ x✝

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
a : Lists α
b✝ : Bool
a0 : Lists' α b✝
l0 l₂ : Lists' α true
s : a0.cons' l0 ⊆ l₂
h : a ∈ (a0.cons' l0).toList
⊢ a ∈ l₂

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ (a : Lists α), a ∈ l₁.toList → a ∈ l₂
⊢ l₁ ⊆ l₂

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ Monotone (lfpApprox f)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l : Lists' α true
x✝ : IsList ⟨true, l⟩
⊢ ofList (toList ⟨true, l⟩) = ⟨true, l⟩

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
this :
  {b : Bool} →
    (l : Lists' α b) →
      C ⟨b, l⟩ ×'
        match b, l with
        | true, l => D l
        | false, x => PUnit
⊢ ((l : Lists α) → C l) ×' ((l : Lists' α true) → D l)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → 0 < x.2

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
⊢ ((l : Lists α) → C l) ×' ((l : Lists' α true) → D l)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l₁ l₂ : Lists' α true
⊢ of' l₁ ~ of' l₂ ↔ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
a : α
l : Lists α
h : atom a ~ l
⊢ atom a = l

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l₁ l₂ : Lists α
h : l₁ ~ l₂
⊢ l₂ ~ l₁

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
this : (∀ (l₁ : Lists α), trans l₁) ×' ∀ (l : Lists' α true) (l' : Lists α), l' ∈ l.toList → trans l'
⊢ ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → x.2 < b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
hab : a ≤ b
hf : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ lfpApprox f x b = lfpApprox f x a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : f x = x
o : Ordinal.{u}
⊢ lfpApprox f x 0 ∈ fixedPoints ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
⊢ (∀ (o : Ordinal.{u}), lfpApprox f x o = x) ↔ f x = x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
hx : x ≤ f x
hab : a < b
hac : a ≤ c
hf : lfpApprox f x a = lfpApprox f x b
⊢ lfpApprox f x a ∈ fixedPoints ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
hx : x ≤ f x
hab : a < b
hac : a ≤ c
hf : lfpApprox f x a = lfpApprox f x b
⊢ lfpApprox f x c ∈ fixedPoints ⇑f

Tactic:
have H : lfpApprox f x a ∈ fixedPoints f := by
    rw [mem_fixedPoints_iff, ← lfpApprox_add_one f hx]
    exact (lfpApprox_mono_right f).eq_of_ge_of_le
      hf (lt_add_one a).le (add_one_le_of_lt hab)

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
hx : x ≤ f x
hab : a < b
hac : a ≤ c
hf : lfpApprox f x a = lfpApprox f x b
H : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ lfpApprox f x c ∈ fixedPoints ⇑f
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
hx : x ≤ f x
hab : a < b
hac : a ≤ c
hf : lfpApprox f x a = lfpApprox f x b
⊢ lfpApprox f x c ∈ fixedPoints ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : lfpApprox f x o = x
ho : o ≠ 0
hpos : 0 < o
hmem : lfpApprox f x 0 ∈ fixedPoints ⇑f
⊢ x ∈ fixedPoints ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
⊢ lfpApprox f x o = x ↔ f x = x ∨ o = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ (map Prod.fst (CNF b o)).SortedGT

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ (map Prod.toSigma (CNF b o)).NodupKeys

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ ∀ a ∈ { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.entries, decide (a.snd ≠ 0) = true

Tactic:
simp_rw [mem_map]

Goal state after:
b o : Ordinal.{u_1}
⊢ ∀ (a : (_ : Ordinal.{u_1}) × Ordinal.{u_1}), (∃ a_1 ∈ CNF b o, a_1.toSigma = a) → decide (a.snd ≠ 0) = true
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ (coeff b o).support = (map Prod.fst (CNF b o)).toFinset

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
⊢ ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
b : Bool
l : Lists' α b
⊢ 0 < sizeOf l

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
b : Bool
a : Lists' α b
l : Lists' α true
⊢ sizeOf ⟨b, a⟩ < sizeOf (a.cons' l)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o e c : Ordinal.{u_1}
h : (e, c) ∈ CNF b o
⊢ (coeff b o) e = c

Tactic:
rw [coeff, lookupFinsupp_apply, mem_lookup_iff.2, Option.getD_some]
  simpa

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o e c : Ordinal.{u_1}
h : (e, c) ∈ CNF b o
⊢ (coeff b o) e = c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o e : Ordinal.{u_1}
h : e ∉ map Prod.fst (CNF b o)
⊢ (coeff b o) e = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
⊢ lfpApprox f x (succ #α).ord ∈ fixedPoints ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α false
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ : Lists' α false
l₂ : Lists' α true
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ : Lists' α true
l₂ : Lists' α false
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α true
⊢ sizeOf l₁ + sizeOf l₂ < sizeOf ⟨true, l₁⟩ + sizeOf ⟨true, l₂⟩

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α true
this : Decidable (l₁ ⊆ l₂)
⊢ sizeOf l₂ + sizeOf l₁ < sizeOf ⟨true, l₁⟩ + sizeOf ⟨true, l₂⟩

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α true
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
⊢ sizeOf ⟨b, a⟩ < 1 + 1 + sizeOf a + sizeOf l₁

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
this : Decidable (⟨b, a⟩ ∈ l₂)
⊢ sizeOf l₁ + sizeOf l₂ < sizeOf (a.cons' l₁) + sizeOf l₂

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
⊢ Decidable (a.cons' l₁ ⊆ l₂)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : Lists α
⊢ ¬a ∈ Lists'.nil

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
⊢ sizeOf ⟨b✝, b⟩ < 1 + 1 + sizeOf b + sizeOf l₂

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o e : Ordinal.{u_1}
h : o < b ^ e
⊢ (coeff b o) e = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b e : Ordinal.{u_1}
⊢ (coeff b 0) e = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ sizeOf a + sizeOf l₂ < sizeOf a + sizeOf (b.cons' l₂)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b : Ordinal.{u_1}
⊢ coeff b 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

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

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ ∃ y, lfp f = ↑y

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
⊢ Decidable (a ∈ b.cons' l₂)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ ∃ y, lfpApprox f ⊥ (succ #α).ord = ↑y

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfpApprox f ⊥ (succ #α).ord = lfp f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfp f ∈ Set.range (lfpApprox f ⊥)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b : Ordinal.{u_1}
hb : b ≤ 1
o : Ordinal.{u_1}
⊢ coeff b o = single 0 o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
hf : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ ⨆ i, lfpApprox f x i = lfpApprox f x a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
⊢ ↑(f.nextFixed x hx) = ⨆ a, lfpApprox f x a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
⊢ gfpApprox f x 0 = x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
⊢ Monotone gfpApprox

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: α : 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
⊢ Continuous f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
⊢ StrictMono f ∧ Continuous f → IsNormal f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: 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) = single e x + coeff b y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : SuccOrder α
ha : ¬IsSuccPrelimit a
⊢ IsOpen[inst✝²] {a}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

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

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

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

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b : Ordinal.{u_1}
⊢ eval b 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

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

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: 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
⊢ e ∉ f.support

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

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

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
h : IsMin a
⊢ 𝓝 a = pure a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
s : Set α
⊢ IsOpen[inst✝³] s ↔ ∀ o ∈ s, IsSuccLimit o → ∃ a < o, Ioo a o ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
⊢ AccPt a (𝓟 s) ↔ ¬IsMin a ∧ ∀ b < a, (s ∩ Ioo b a).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
h : AccPt a (𝓟 s)
⊢ IsSuccLimit a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
ha : a ∈ frontier s
⊢ IsSuccLimit a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

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

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b e x : Ordinal.{u_1}
⊢ eval b (single e x) = b ^ e * x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: 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)
⊢ e' ∈ (single e' y + f).support

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: a : Ordinal.{u}
s : Set Ordinal.{u}
⊢ a ∈ closure s → a ∈ closure (s ∩ Iic a)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: 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✝
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: n : ℕ
⊢ (↑n).repr = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
⊢ ω ^ e.repr ≤ (e.oadd n a).repr

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).cmp 0 = Ordering.eq
⊢ e.oadd n a = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
h : cmp 0 (e.oadd n a) = Ordering.eq
⊢ 0 = e.oadd n a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

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

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a → ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a
⊢ (∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a) → ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h : (e₁.oadd n₁ a₁).cmp (e₂.oadd n₂ a₂) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: ⊢ 0 < 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
h : (e.oadd n a).NFBelow b
⊢ e.NF

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
h : (e.oadd n a).NFBelow b
⊢ a.NFBelow e.repr

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
h : (e.oadd n a).NFBelow b
⊢ e.repr < b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : e = 0
⊢ a = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a → ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a) → ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a
⊢ (∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a) → a ∈ closure s

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b : Ordinal.{u_1}
f₁ f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁
⊢ eval b (f₁ + f₂) = eval b f₁ + eval b f₂

Tactic:
induction f₁ using Finsupp.induction_on_max with

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b : Ordinal.{u_1}
f₁ f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁
⊢ eval b (f₁ + f₂) = eval b f₁ + eval b f₂

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
b : Ordinal.{0}
h : o.NFBelow b
⊢ o.repr < ω ^ b

Tactic:
by

Goal state after: