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

Goal state before:
pp: case oadd'
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ (e✝.oadd n✝ a✝).NFBelow b₂

Tactic:
constructor

Goal state after:
case oadd'.a
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ e✝.NFBelow ?oadd'.eb

case oadd'.a
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ a✝.NFBelow e✝.repr

case oadd'.a
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ e✝.repr < b₂

case oadd'.eb
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ Ordinal.{0}
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ (∃ ι, ∃ (_ : Nonempty ι), ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a) ↔
    ∃ o, ∃ (_ : o ≠ 0), ∃ f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a

Tactic:
constructor

Goal state after:
case mp
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ (∃ ι, ∃ (_ : Nonempty ι), ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a) →
    ∃ o, ∃ (_ : o ≠ 0), ∃ f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a

case mpr
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ (∃ o, ∃ (_ : o ≠ 0), ∃ f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a) →
    ∃ ι, ∃ (_ : Nonempty ι), ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: s : Set Ordinal.{u}
hs : ¬BddAbove s
⊢ IsNormal (enumOrd s) ↔ IsClosed s

Tactic:
by
  have Hs := enumOrd_strictMono hs
  refine
    ⟨fun h => isClosed_iff_iSup.2 fun {ι} hι f hf => ?_, fun h =>
      isNormal_iff.2 ⟨Hs, fun a ha o H => ?_⟩⟩
  · let g : ι → Ordinal.{u} := fun i => (enumOrdOrderIso s hs).symm ⟨_, hf i⟩
    suffices enumOrd s (⨆ i, g i) = ⨆ i, f i by
      rw [← this]
      exact enumOrd_mem hs _
    rw [h.map_iSup bddAbove_of_small]
    congr
    ext x
    change (enumOrdOrderIso s hs _).val = f x
    rw [OrderIso.apply_symm_apply]
  · have := csSup_mem_closure (ha.nonempty_Iio.image (enumOrd s)) bddAbove_of_small
    have := h.closure_eq ▸ closure_mono (t := s) ?_ this
    · apply (Set.image_subset_range ..).trans_eq
      rw [range_enumOrd hs]
    · apply (enumOrd_le_of_forall_lt this _).trans
      · apply csSup_le'
        grind [upperBounds]
      · exact fun b hb ↦ (enumOrd_strictMono hs (lt_add_one b)).trans_le <|
          le_csSup bddAbove_of_small <| Set.mem_image_of_mem _ (ha.add_one_lt hb)

Goal state after:
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: x : PSet.{u}
⊢ (⋃₀ x).toSet = ⋃₀ (toSet '' x.toSet)

Tactic:
ext

Goal state after:
x x✝ : PSet.{u}
⊢ x✝ ∈ (⋃₀ x).toSet ↔ x✝ ∈ ⋃₀ (toSet '' x.toSet)
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: ⊢ ↑∅ = ∅

Tactic:
ext

Goal state after:
x✝ : ZFSet.{u}
⊢ x✝ ∈ ↑∅ ↔ x✝ ∈ ∅
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u_1}
⊢ ↑(insert x y) = insert x ↑y

Tactic:
ext

Goal state after:
x y x✝ : ZFSet.{u_1}
⊢ x✝ ∈ ↑(insert x y) ↔ x✝ ∈ insert x ↑y
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x : ZFSet.{u_1}
⊢ ↑{x} = {x}

Tactic:
ext

Goal state after:
x x✝ : ZFSet.{u_1}
⊢ x✝ ∈ ↑{x} ↔ x✝ ∈ {x}
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x : ZFSet.{u_1}
⊢ {x, x} = {x}

Tactic:
ext

Goal state after:
x z✝ : ZFSet.{u_1}
⊢ z✝ ∈ {x, x} ↔ z✝ ∈ {x}
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: a : ZFSet.{u_1}
p : ZFSet.{u_1} → Prop
⊢ ↑(ZFSet.sep p a) = {x | x ∈ a ∧ p x}

Tactic:
ext

Goal state after:
a : ZFSet.{u_1}
p : ZFSet.{u_1} → Prop
x✝ : ZFSet.{u_1}
⊢ x✝ ∈ ↑(ZFSet.sep p a) ↔ x✝ ∈ {x | x ∈ a ∧ p x}
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.eq
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
n' : ℕ+
a' : ONote
h' : (e.oadd n' a').NFBelow b
h : e.cmp e = Ordering.eq
⊢ (e.oadd (n + n') a').NFBelow b

Tactic:
exact NFBelow.oadd h'.fst h'.snd h'.lt

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a : Ordinal.{u}
⊢ Monotone fun x ↦ veblenWith f x a

Tactic:
monotone_iff_forall_lt

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a : Ordinal.{u}
⊢ ∀ ⦃a_1 b : Ordinal.{u}⦄, a_1 < b → veblenWith f a_1 a ≤ veblenWith f b a
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: ⊢ ⋃₀ ∅ = ∅

Tactic:
ext

Goal state after:
z✝ : ZFSet.{u}
⊢ z✝ ∈ ⋃₀ ∅ ↔ z✝ ∈ ∅
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x : ZFSet.{u}
⊢ ↑(⋃₀ x) = ⋃₀ (SetLike.coe '' ↑x)

Tactic:
ext

Goal state after:
x x✝ : ZFSet.{u}
⊢ x✝ ∈ ↑(⋃₀ x) ↔ x✝ ∈ ⋃₀ (SetLike.coe '' ↑x)
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x : ZFSet.{u}
h : x.Nonempty
⊢ ↑(⋂₀ x) = ⋂₀ (SetLike.coe '' ↑x)

Tactic:
ext

Goal state after:
x : ZFSet.{u}
h : x.Nonempty
x✝ : ZFSet.{u}
⊢ x✝ ∈ ↑(⋂₀ x) ↔ x✝ ∈ ⋂₀ (SetLike.coe '' ↑x)
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u}
⊢ ↑(x ∪ y) = ↑x ∪ ↑y

Tactic:
ext

Goal state after:
x y x✝ : ZFSet.{u}
⊢ x✝ ∈ ↑(x ∪ y) ↔ x✝ ∈ ↑x ∪ ↑y
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u}
⊢ ↑(x ∩ y) = ↑x ∩ ↑y

Tactic:
ext

Goal state after:
x y x✝ : ZFSet.{u}
⊢ x✝ ∈ ↑(x ∩ y) ↔ x✝ ∈ ↑x ∩ ↑y
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u}
⊢ ↑(x \ y) = ↑x \ ↑y

Tactic:
ext

Goal state after:
x y x✝ : ZFSet.{u}
⊢ x✝ ∈ ↑(x \ y) ↔ x✝ ∈ ↑x \ ↑y
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u}
hxy : x ⊆ y
⊢ x ∩ y = x

Tactic:
ext

Goal state after:
x y : ZFSet.{u}
hxy : x ⊆ y
z✝ : ZFSet.{u}
⊢ z✝ ∈ x ∩ y ↔ z✝ ∈ x
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u}
hyx : y ⊆ x
⊢ x ∩ y = y

Tactic:
ext

Goal state after:
x y : ZFSet.{u}
hyx : y ⊆ x
z✝ : ZFSet.{u}
⊢ z✝ ∈ x ∩ y ↔ z✝ ∈ y
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u_1}
⊢ insert x y = {x} ∪ y

Tactic:
ext

Goal state after:
x y z✝ : ZFSet.{u_1}
⊢ z✝ ∈ insert x y ↔ z✝ ∈ {x} ∪ y
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
⊢ (Set.range fun a ↦ succ (A✝¹ a).rank) = Set.range fun a ↦ succ (A✝ a).rank

Tactic:
ext

Goal state after:
α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
x✝ : Ordinal.{u_1}
⊢ (x✝ ∈ Set.range fun a ↦ succ (A✝¹ a).rank) ↔ x✝ ∈ Set.range fun a ↦ succ (A✝ a).rank
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: f : ZFSet.{u_1} → ZFSet.{u_1}
inst✝ : Definable₁ f
x : ZFSet.{u_1}
⊢ ↑(image f x) = f '' ↑x

Tactic:
ext

Goal state after:
f : ZFSet.{u_1} → ZFSet.{u_1}
inst✝ : Definable₁ f
x x✝ : ZFSet.{u_1}
⊢ x✝ ∈ ↑(image f x) ↔ x✝ ∈ f '' ↑x
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
x✝ : Ordinal.{u_1}
⊢ (x✝ ∈ Set.range fun a ↦ succ (A✝¹ a).rank) ↔ x✝ ∈ Set.range fun a ↦ succ (A✝ a).rank

Tactic:
constructor

Goal state after:
case mp
α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
x✝ : Ordinal.{u_1}
⊢ (x✝ ∈ Set.range fun a ↦ succ (A✝¹ a).rank) → x✝ ∈ Set.range fun a ↦ succ (A✝ a).rank

case mpr
α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
x✝ : Ordinal.{u_1}
⊢ (x✝ ∈ Set.range fun a ↦ succ (A✝ a).rank) → x✝ ∈ Set.range fun a ↦ succ (A✝¹ a).rank
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
⊢ ⟦y⟧ ∈ range f ↔ ∃ i, f i = ⟦y⟧

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
⊢ ⟦y⟧ ∈ range f → ∃ i, f i = ⟦y⟧

case mpr
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
⊢ (∃ i, f i = ⟦y⟧) → ⟦y⟧ ∈ range f
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ↑(range f) = Set.range f

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x✝ : ZFSet.{u}
⊢ x✝ ∈ ↑(range f) ↔ x✝ ∈ Set.range f
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ↑(⋃ (i : α), f i) = ⋃ i, ↑(f i)

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x✝ : ZFSet.{u}
⊢ x✝ ∈ ↑(⋃ (i : α), f i) ↔ x✝ ∈ ⋃ i, ↑(f i)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case a
o a : Ordinal.{u}
h : a < veblen o a
⊢ (veblen o a).invVeblen₁ ≤ o

pp: case a
o a : Ordinal.{u}
h : a < veblen o a
⊢ o ≤ (veblen o a).invVeblen₁

Tactic:
· rwa [← lt_veblen_iff_invVeblen₁_le, veblen_lt_veblen_iff_right]

Goal state after:
case a
o a : Ordinal.{u}
h : a < veblen o a
⊢ o ≤ (veblen o a).invVeblen₁
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case lt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
this : (e₁.cmp e₂).Compares e₁ e₂
h : e₁.cmp e₂ = Ordering.lt
⊢ (match Ordering.lt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (↑n₁).sub ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).NFBelow
    b

Tactic:
apply NFBelow.zero

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

Goal state before:
pp: o : Ordinal.{u}
h : ω ^ o ≤ o
⊢ ε_ 0 ≤ o

Tactic:
rw [epsilon_zero_eq_nfp]
  exact nfp_le_fp (fun _ _ ↦ (opow_le_opow_iff_right one_lt_omega0).2) zero_le h

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

Goal state before:
pp: o : Ordinal.{u}
⊢ o.invVeblen₁ = o ↔ o = 0 ∨ o ∈ range Γ_

Tactic:
constructor

Goal state after:
case mp
o : Ordinal.{u}
⊢ o.invVeblen₁ = o → o = 0 ∨ o ∈ range Γ_

case mpr
o : Ordinal.{u}
⊢ o = 0 ∨ o ∈ range Γ_ → o.invVeblen₁ = o
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (⋃₀ x) y ↔ ∃ z, x z ∧ y ∈ z

Tactic:
constructor

Goal state after:
case mp
x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (⋃₀ x) y → ∃ z, x z ∧ y ∈ z

case mpr
x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (∃ z, x z ∧ y ∈ z) → (⋃₀ x) y
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: x y : Class.{u}
⊢ y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z

Tactic:
constructor

Goal state after:
case mp
x y : Class.{u}
⊢ y ∈ ⋃₀ x → ∃ z ∈ x, y ∈ z

case mpr
x y : Class.{u}
⊢ (∃ z ∈ x, y ∈ z) → y ∈ ⋃₀ x
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: ⊢ ⋃₀ ∅ = ∅

Tactic:
ext

Goal state after:
z✝ : ZFSet.{u}
⊢ (⋃₀ ∅) z✝ ↔ ∅ z✝
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
w : ZFSet.{u}
hw : w ∈ x
hw' : y ∈ w
⊢ z ∈ ⋃₀ x

Tactic:
exact mem_sUnion_of_mem hz (h.mem_trans hw' hw)

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

Goal state before:
pp: x : ZFSet.{u}
⊢ x.IsTransitive ↔ ⋃₀ x ⊆ x

Tactic:
constructor

Goal state after:
case mp
x : ZFSet.{u}
⊢ x.IsTransitive → ⋃₀ x ⊆ x

case mpr
x : ZFSet.{u}
⊢ ⋃₀ x ⊆ x → x.IsTransitive
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ⊆ y ↔ x = y ∨ x ∈ y

Tactic:
constructor

Goal state after:
case mp
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ⊆ y → x = y ∨ x ∈ y

case mpr
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x = y ∨ x ∈ y → x ⊆ y
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ x ⊆ V_ o ↔ ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o

Tactic:
constructor

Goal state after:
case mp
o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ x ⊆ V_ o → ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o

case mpr
o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ (∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o) → x ⊆ V_ o
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ↑o.toZFSet = toZFSet '' Iio o

Tactic:
ext

Goal state after:
o : Ordinal.{u_1}
x✝ : ZFSet.{u_1}
⊢ x✝ ∈ ↑o.toZFSet ↔ x✝ ∈ toZFSet '' Iio o
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: ⊢ toZFSet 0 = ∅

Tactic:
ext

Goal state after:
z✝ : ZFSet.{u_1}
⊢ z✝ ∈ toZFSet 0 ↔ z✝ ∈ ∅
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: n : ℕ
R : Type u_3
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : n.AtLeastTwo
a : A
⊢ OfNat.ofNat n • a = OfNat.ofNat n * a

Tactic:
simp_rw [← nat_rawCast_2]
  simp [Nat.cast_smul_eq_nsmul]

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

Goal state before:
pp: o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (e.oadd n a, m)
h₁ : (e.oadd n a).NF
h₂ : o.repr = (e.oadd n a).repr + ↑m
e0 : e.repr ≠ 0
d : ω ∣ a.repr
⊢ ω ≤ ω ^ e.repr

Tactic:
simpa using opow_le_opow_right omega0_pos (one_le_iff_ne_zero.2 e0)

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
this : (fun t ↦ f t ^ exp / f t ^ exp') =ᶠ[atTop] fun t ↦ f t ^ (exp - exp')
⊢ (fun t ↦ f t ^ (exp - exp')) = (fun t ↦ t ^ (-(exp' - exp))) ∘ f

Tactic:
ext

Goal state after:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
this : (fun t ↦ f t ^ exp / f t ^ exp') =ᶠ[atTop] fun t ↦ f t ^ (exp - exp')
x✝ : ℝ
⊢ f x✝ ^ (exp - exp') = ((fun t ↦ t ^ (-(exp' - exp))) ∘ f) x✝
Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h : Tendsto (fun x ↦ f (c - x⁻¹)) atTop l
⊢ (fun x ↦ f (c - x⁻¹)) = f ∘ (fun x ↦ c + x) ∘ Neg.neg ∘ Inv.inv

Tactic:
ext

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h : Tendsto (fun x ↦ f (c - x⁻¹)) atTop l
x✝ : 𝕜
⊢ f (c - x✝⁻¹) = (f ∘ (fun x ↦ c + x) ∘ Neg.neg ∘ Inv.inv) x✝
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: left right : Basis
h_left : List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) left ∧ ∀ f ∈ left, Tendsto f atTop atTop
h_right : List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) right ∧ ∀ f ∈ right, Tendsto f atTop atTop
h : ∀ f ∈ left, ∀ g ∈ right, (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) (left ++ right) ∧
    ∀ f ∈ left ++ right, Tendsto f atTop atTop

Tactic:
constructor

Goal state after:
case left
left right : Basis
h_left : List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) left ∧ ∀ f ∈ left, Tendsto f atTop atTop
h_right : List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) right ∧ ∀ f ∈ right, Tendsto f atTop atTop
h : ∀ f ∈ left, ∀ g ∈ right, (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) (left ++ right)

case right
left right : Basis
h_left : List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) left ∧ ∀ f ∈ left, Tendsto f atTop atTop
h_right : List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) right ∧ ∀ f ∈ right, Tendsto f atTop atTop
h : ∀ f ∈ left, ∀ g ∈ right, (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ ∀ f ∈ left ++ right, Tendsto f atTop atTop
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
β : Type u_2
F : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α
h : LipschitzWith 2⁻¹ F
⊢ ContractingWith 2⁻¹ F

Tactic:
constructor

Goal state after:
case left
α : Type u_1
β : Type u_2
F : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α
h : LipschitzWith 2⁻¹ F
⊢ 2⁻¹ < 1

case right
α : Type u_1
β : Type u_2
F : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α
h : LipschitzWith 2⁻¹ F
⊢ LipschitzWith 2⁻¹ F
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
γ : Type u_1
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
h : ∀ (c : γ), FriendlyOperation (op c)
this : Seq.FriendlyOperationClass op
⊢ FriendlyOperationClass op

Tactic:
constructor

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: case nil
c : ℝ
⊢ (const [] c).Sorted

Tactic:
constructor

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: case nil
⊢ Sorted 0

Tactic:
constructor

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: case nil
n : ℕ
r : ℝ
⊢ (monomialRpow [] n r).Sorted

Tactic:
constructor

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
m : Fin basis_tl.length
⊢ Majorized (basis_tl[↑m] ^ r) basis_hd 0

Tactic:
apply h_basis.tail_pow_majorized_head (by simp)

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates

Goal state before:
pp: n : ℕ
⊢ AllZero (List.replicate n 0)

Tactic:
by
  induction n <;> grind [AllZero, sign]

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
h : FriendlyOperation op
ms : Multiseries basis_hd basis_tl
⊢ (op ms).destruct =
    Option.map
      (fun x ↦
        match x with
        | (exp, coef, op') => (exp, coef, ↑op' ms.tail))
      (h.unfold ms.head)

Tactic:
unfold Multiseries.destruct
  simp [Seq.FriendlyOperation.destruct_apply_eq_unfold h, FriendlyOperation.unfold, head]
  cases Seq.FriendlyOperation.unfold h (Seq.head ms) <;> rfl

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
γ : Type u_1
γ' : Type u_2
g : γ' → γ
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
h : FriendlyOperationClass op
this : Seq.FriendlyOperationClass fun c ↦ op (g c)
⊢ FriendlyOperationClass fun c ↦ op (g c)

Tactic:
constructor

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case seq
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_coef : ∀ x ∈ ms.seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) ms.seq
⊢ ms.seq.Sorted

Tactic:
constructor

Goal state after:
case seq.h_coef
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_coef : ∀ x ∈ ms.seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) ms.seq
⊢ ∀ x ∈ (mk ms.seq 0).seq, x.2.Sorted

case seq.h_Pairwise
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_coef : ∀ x ∈ ms.seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) ms.seq
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk ms.seq 0).seq
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case seq
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_coef : ∀ x ∈ (mk ms.seq 0).seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk ms.seq 0).seq
⊢ ms.Sorted

Tactic:
constructor

Goal state after:
case seq.h_coef
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_coef : ∀ x ∈ (mk ms.seq 0).seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk ms.seq 0).seq
⊢ ∀ x ∈ ms.seq, x.2.Sorted

case seq.h_Pairwise
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_coef : ∀ x ∈ (mk ms.seq 0).seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk ms.seq 0).seq
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) ms.seq
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ Multiseries.nil.Sorted

Tactic:
constructor

Goal state after:
case h_coef
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ ∀ x ∈ (mk Multiseries.nil 0).seq, x.2.Sorted

case h_Pairwise
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk Multiseries.nil 0).seq
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
⊢ (cons exp coef Multiseries.nil).Sorted

Tactic:
constructor

Goal state after:
case h_coef
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
⊢ ∀ x ∈ (mk (cons exp coef Multiseries.nil) 0).seq, x.2.Sorted

case h_Pairwise
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (cons exp coef Multiseries.nil) 0).seq
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case seq
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : coef.Sorted
h_comp : tl.leadingExp < ↑exp
h_tl_coef : ∀ x ∈ (mk tl 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk tl 0).seq
⊢ (Multiseries.cons exp coef tl).Sorted

Tactic:
constructor

Goal state after:
case seq.h_coef
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : coef.Sorted
h_comp : tl.leadingExp < ↑exp
h_tl_coef : ∀ x ∈ (mk tl 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk tl 0).seq
⊢ ∀ x ∈ (mk (Multiseries.cons exp coef tl) 0).seq, x.2.Sorted

case seq.h_Pairwise
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : coef.Sorted
h_comp : tl.leadingExp < ↑exp
h_tl_coef : ∀ x ∈ (mk tl 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk tl 0).seq
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef tl) 0).seq