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

Goal state before:
pp: case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
ha : a ∈ fixedPoints ⇑f
hxa : x ≤ a
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ a
⊢ x ⊔ ⨆ b, ⨆ (_ : b < i), f (lfpApprox f x b) ≤ a

Tactic:
apply sup_le hxa

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
ha : a ∈ fixedPoints ⇑f
hxa : x ≤ a
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ a
⊢ ⨆ b, ⨆ (_ : b < i), f (lfpApprox f x b) ≤ 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
⊢ lfpApprox f x o ≤ ↑(f.nextFixed x hx)

Tactic:
· exact lfpApprox_le_of_mem_fixedPoints f (f.nextFixed x hx).2 (f.le_nextFixed hx) o

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

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

Tactic:
intro f g h
  have : g.dual ≤ f.dual := h
  exact lfpApprox_mono_left this

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

Goal state before:
pp: e o₁ o₂ : ONote
n₁ n₂ : ℕ+
h₁ : (e.oadd n₁ o₁).NF
h : ↑n₁ < ↑n₂
⊢ e.oadd n₁ o₁ < e.oadd n₂ o₂

Tactic:
simp only [lt_def, repr]

Goal state after:
e o₁ o₂ : ONote
n₁ n₂ : ℕ+
h₁ : (e.oadd n₁ o₁).NF
h : ↑n₁ < ↑n₂
⊢ ω ^ e.repr * ↑↑n₁ + o₁.repr < ω ^ e.repr * ↑↑n₂ + o₂.repr
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: case refine_2
x y z : ZFSet.{u_1}
⊢ x = z ∧ y = z → {x, y} = {z}

Tactic:
rintro ⟨rfl, rfl⟩

Goal state after:
case refine_2
y : ZFSet.{u_1}
⊢ {y, y} = {y}
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)

Tactic:
let ⟨b, hb⟩ := αβ a
    induction ea : A a with | _ γ Γ
    induction eb : B b with | _ δ Δ
    rw [ea, eb] at hb
    obtain ⟨γδ, δγ⟩ := hb
    let c : (A a).Type := c
    let ⟨d, hd⟩ := γδ (by rwa [ea] at c)
    use ⟨b, Eq.ndrec d (Eq.symm eb)⟩
    change PSet.Equiv ((A a).Func c) ((B b).Func (Eq.ndrec d eb.symm))
    match A a, B b, ea, eb, c, d, hd with
    | _, _, rfl, rfl, _, _, hd => exact hd

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

Goal state before:
pp: a x : Ordinal.{u}
⊢ x.invVeblen₂ = a ↔ ω ^ x = veblen x.invVeblen₁ a

Tactic:
rw [← veblen_inj (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]

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

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

Tactic:
rintro (rfl | h)

Goal state after:
case mpr.inl
x : ZFSet.{u}
hx hy : x.IsOrdinal
⊢ x ⊆ x

case mpr.inr
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x ∈ y
⊢ x ⊆ y
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case a
o : Ordinal.{u_1}
a✝ : PSet.{u_1}
x✝ : Ordinal.{u_1}
⊢ a✝.Equiv x✝.toPSet ↔ x✝.toZFSet = mk a✝

Tactic:
rw [toZFSet, eq, PSet.Equiv.comm]

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

Goal state before:
pp: case pos
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h✝ : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
h : m = 0
⊢ R' = ω0 ^ ↑k * (α' * ↑m) + R

pp: case neg
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h✝ : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
h : ¬m = 0
⊢ R' = ω0 ^ ↑k * (α' * ↑m) + R

Tactic:
· simp only [R, R', h, ONote.ofNat, Nat.cast_zero, ONote.repr_zero,
        mul_zero, ONote.opowAux, add_zero]

Goal state after:
case neg
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h✝ : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
h : ¬m = 0
⊢ R' = ω0 ^ ↑k * (α' * ↑m) + R
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: b : ℝ → ℝ
h_tendsto : Tendsto b atTop atTop
c : ℝ
⊢ Majorized (fun x ↦ c) b 0

Tactic:
intro exp h_exp

Goal state after:
b : ℝ → ℝ
h_tendsto : Tendsto b atTop atTop
c exp : ℝ
h_exp : exp > 0
⊢ (fun x ↦ c) =o[atTop] (b ^ exp)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
⊢ ∀ exp' > f_exp + g_exp, (f * g) =o[atTop] (b ^ exp')

Tactic:
intro exp h_exp

Goal state after:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
⊢ (f * g) =o[atTop] (b ^ exp)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
⊢ (ω0 ^ ↑k * α' + R) * α' + (ω0 ^ ↑k * α' + R) * ↑m = (α' + ↑m) ^ succ ↑k.succ

Tactic:
rw [← mul_add, opow_succ, Nat.cast_add_one, IH.2, succ_eq_add_one]

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

Goal state before:
pp: f g basis_hd : ℝ → ℝ
exp : ℝ
hf : Majorized f basis_hd exp
hg : g =O[atTop] fun x ↦ 1
⊢ Majorized (f * g) basis_hd exp

Tactic:
intro exp h_exp

Goal state after:
f g basis_hd : ℝ → ℝ
exp✝ : ℝ
hf : Majorized f basis_hd exp✝
hg : g =O[atTop] fun x ↦ 1
exp : ℝ
h_exp : exp > exp✝
⊢ (f * g) =o[atTop] (basis_hd ^ exp)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
⊢ CompleteSpace (Stream'.Seq α)

Tactic:
by
  suffices IsClosed (X := Stream' (Option α)) {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none} by
    exact this.completeSpace_coe
  rw [isClosed_iff_clusterPt]
  intro s hs n hn
  rw [clusterPt_principal_iff] at hs
  obtain ⟨t, hts, ht⟩ := hs (Metric.ball s ((1 / 2 : ℝ) ^ (n + 1)))
    (Metric.ball_mem_nhds _ (by positivity))
  simp only [Metric.ball, Set.mem_ofPred_eq] at hts
  rw [← PiNat.apply_eq_of_dist_lt hts (by simp)] at hn
  rw [← PiNat.apply_eq_of_dist_lt hts (by rfl)]
  exact ht hn

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

Goal state before:
pp: basis : Basis
f : ℝ → ℝ
h : WellFormedBasis basis
h_comp : ∀ (g : ℝ → ℝ), List.head? basis = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ ∀ g ∈ basis, (Real.log ∘ g) =o[atTop] (Real.log ∘ f)

Tactic:
intro g hg
  cases basis with
  | nil => simp at hg
  | cons basis_hd basis_tl =>
    specialize h_comp basis_hd (by simp)
    simp only [List.mem_cons] at hg
    rcases hg with hg | hg
    · simpa [hg]
    · simp only [WellFormedBasis, List.pairwise_cons, List.mem_cons, forall_eq_or_imp] at h
      exact .trans (by grind) h_comp

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

Goal state before:
pp: hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r : ℝ
⊢ Majorized (f ^ r) hd 0

Tactic:
intro exp h_exp

Goal state after:
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ (f ^ r) =o[atTop] (hd ^ exp)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg.a1
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ 1 < ↑m + 1

Tactic:
simpa [Nat.one_le_iff_ne_zero]

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
h : ms.destruct = none
⊢ Seq.destruct ms = none

Tactic:
simpa [destruct] using h

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

Goal state before:
pp: case oadd.inl.none.inl.none.zero
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
e' : m.natPred = 0
⊢ (a.oadd m b).repr = succ zero.repr ∧ ((a.oadd m b).NF → zero.NF)

Tactic:
(try rw [show m = 1 by
            have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm])

Goal state after:
case oadd.inl.none.inl.none.zero
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
e' : m.natPred = 0
⊢ (a.oadd 1 b).repr = succ zero.repr ∧ ((a.oadd 1 b).NF → zero.NF)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inl.none.succ
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
m' : ℕ
e' : m.natPred = m' + 1
⊢ (a.oadd m b).repr = succ (zero.oadd m'.succPNat zero).repr ∧ ((a.oadd m b).NF → (zero.oadd m'.succPNat zero).NF)

Tactic:
(try rw [show m = 1 by
            have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm])

Goal state after:
case oadd.inl.none.inl.none.succ
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
m' : ℕ
e' : m.natPred = m' + 1
⊢ (a.oadd m b).repr = succ (zero.oadd m'.succPNat zero).repr ∧ ((a.oadd m b).NF → (zero.oadd m'.succPNat zero).NF)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inl.some.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
e' : m.natPred = 0
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a'.oadd i.succPNat zero < a'.oadd (i + 1).succPNat zero ∧
          a'.oadd i.succPNat zero < a.oadd m b ∧ ((a.oadd m b).NF → (a'.oadd i.succPNat zero).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a'.oadd i.succPNat zero).repr

Tactic:
(try rw [show m = 1 by
            have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm])

Goal state after:
case oadd.inl.none.inl.some.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
e' : m.natPred = 0
⊢ IsSuccLimit (a.oadd 1 b).repr ∧
    (∀ (i : ℕ),
        a'.oadd i.succPNat zero < a'.oadd (i + 1).succPNat zero ∧
          a'.oadd i.succPNat zero < a.oadd 1 b ∧ ((a.oadd 1 b).NF → (a'.oadd i.succPNat zero).NF)) ∧
      ∀ a_1 < (a.oadd 1 b).repr, ∃ i, a_1 < (a'.oadd i.succPNat zero).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inl.some.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m'.succPNat (a'.oadd i.succPNat zero) < a.oadd m'.succPNat (a'.oadd (i + 1).succPNat zero) ∧
          a.oadd m'.succPNat (a'.oadd i.succPNat zero) < a.oadd m b ∧
            ((a.oadd m b).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).repr

Tactic:
(try rw [show m = 1 by
            have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm])

Goal state after:
case oadd.inl.none.inl.some.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m'.succPNat (a'.oadd i.succPNat zero) < a.oadd m'.succPNat (a'.oadd (i + 1).succPNat zero) ∧
          a.oadd m'.succPNat (a'.oadd i.succPNat zero) < a.oadd m b ∧
            ((a.oadd m b).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inr.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        (f i).oadd 1 zero < (f (i + 1)).oadd 1 zero ∧
          (f i).oadd 1 zero < a.oadd m b ∧ ((a.oadd m b).NF → ((f i).oadd 1 zero).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < ((f i).oadd 1 zero).repr

Tactic:
(try rw [show m = 1 by
            have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm])

Goal state after:
case oadd.inl.none.inr.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
⊢ IsSuccLimit (a.oadd 1 b).repr ∧
    (∀ (i : ℕ),
        (f i).oadd 1 zero < (f (i + 1)).oadd 1 zero ∧
          (f i).oadd 1 zero < a.oadd 1 b ∧ ((a.oadd 1 b).NF → ((f i).oadd 1 zero).NF)) ∧
      ∀ a_1 < (a.oadd 1 b).repr, ∃ i, a_1 < ((f i).oadd 1 zero).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inr.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m'.succPNat ((f i).oadd 1 zero) < a.oadd m'.succPNat ((f (i + 1)).oadd 1 zero) ∧
          a.oadd m'.succPNat ((f i).oadd 1 zero) < a.oadd m b ∧
            ((a.oadd m b).NF → (a.oadd m'.succPNat ((f i).oadd 1 zero)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a.oadd m'.succPNat ((f i).oadd 1 zero)).repr

Tactic:
(try rw [show m = 1 by
            have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm])

Goal state after:
case oadd.inl.none.inr.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m'.succPNat ((f i).oadd 1 zero) < a.oadd m'.succPNat ((f (i + 1)).oadd 1 zero) ∧
          a.oadd m'.succPNat ((f i).oadd 1 zero) < a.oadd m b ∧
            ((a.oadd m b).NF → (a.oadd m'.succPNat ((f i).oadd 1 zero)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a.oadd m'.succPNat ((f i).oadd 1 zero)).repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: case nil
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
f✝ : ℝ → ℝ
⊢ (mk Multiseries.nil f✝).seq = Multiseries.nil

Tactic:
mk_seq

Goal state after:
case nil
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
f✝ : ℝ → ℝ
⊢ Multiseries.nil = Multiseries.nil
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case succ
α : Type u_1
γ : Type u_3
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
n : ℕ
ih : ∀ {s t : Stream'.Seq α}, motive s t → dist s t ≤ 2⁻¹ ^ n
s t : Stream'.Seq α
base : motive s t
⊢ dist s t ≤ 2⁻¹ ^ (n + 1)

Tactic:
obtain step | ⟨hd, u, v, c, rfl, rfl, h_next⟩ := step s t base
    · simp [step]
    simp only [dist_cons_cons]
    specialize ih h_next
    calc
      _ ≤ 2⁻¹ * dist u v := by
        gcongr
        exact (FriendlyOperationClass.friend _).dist_le
      _ ≤ _ := by
        grw [ih, pow_succ']

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

Goal state before:
pp: case oadd.inl.some.refine_2
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
H : (a.oadd m b).NF
⊢ b'.repr < ω ^ a.repr

Tactic:
have := H.snd'.repr_lt

Goal state after:
case oadd.inl.some.refine_2
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
H : (a.oadd m b).NF
this : b.repr < ω ^ a.repr
⊢ b'.repr < ω ^ a.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
C : NONote → Sort u_1
H0 : C 0
H1 : (e : NONote) → (n : ℕ+) → (a : NONote) → (h : a.below e) → C e → C a → C (e.oadd n a h)
h : ONote.zero.NF
⊢ C ⟨ONote.zero, h⟩

Tactic:
exact H0

Goal state after:
Module: Mathlib.Tactic.ModCases

Goal state before:
pp: p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ 0 ≤ (a % ↑n).toNat ∧ (a % ↑n).toNat < n ∧ a ≡ ↑(a % ↑n).toNat [ZMOD ↑n]

Tactic:
refine ⟨Nat.zero_le _, ?_, ?_⟩

Goal state after:
case refine_1
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ (a % ↑n).toNat < n

case refine_2
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ a ≡ ↑(a % ↑n).toNat [ZMOD ↑n]
Module: Mathlib.Tactic.ModCases

Goal state before:
pp: p : Sort ?u.2
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ 0 ≤ a % n ∧ a % n < n ∧ a ≡ a % n [MOD n]

Tactic:
refine ⟨Nat.zero_le _, ?_, ?_⟩

Goal state after:
case refine_1
p : Sort ?u.2
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ a % n < n

case refine_2
p : Sort ?u.2
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ a ≡ a % n [MOD n]
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: n k p q : ℕ
hq : 0 < q
h_coprime : p.Coprime q
h_left : k ^ q < n
h_right : n < (k + 1) ^ q
m : ℕ
⊢ n ^ p ≠ m ^ q

Tactic:
apply not_power_nat_pow h_coprime hq

Goal state after:
n k p q : ℕ
hq : 0 < q
h_coprime : p.Coprime q
h_left : k ^ q < n
h_right : n < (k + 1) ^ q
m : ℕ
⊢ ∀ (m : ℕ), n ≠ m ^ q
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : ⟨a, od⟩ ∈ A.dedupKeys
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a A.dedupKeys
⊢ ¬(some od).getD 0 = 0

Tactic:
simpa using hod

Goal state after:
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝³ : Monoid A
inst✝² : Monoid B
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
⊢ Set.range toContinuousMap = {f | f 1 = 1 ∧ ∀ (x y : A), f (x * y) = f x * f y}

Tactic:
by
  refine Set.Subset.antisymm (Set.range_subset_iff.2 fun f ↦ ⟨map_one f, map_mul f⟩) ?_
  rintro f ⟨h1, hmul⟩
  exact ⟨{ f with map_one' := h1, map_mul' := hmul }, rfl⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
this✝ : Nonempty X
this : Encodable ↑s
n : ℕ
g : G
hg : g ∈ s
⊢ IsCompact (K n ∩ g • V)

Tactic:
exact (isCompact_compactCovering G n).inter_right (V_closed.smul g)

Goal state after:
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝¹ : DivInvMonoid G
inst✝ : TopologicalSpace G
x y : G
⊢ ClusterPt x (map (fun x ↦ y ^ x) (map Nat.cast atTop)) ↔ ClusterPt x (map (fun x ↦ y ^ x) atTop)

Tactic:
map_map,

Goal state after:
G : Type u_1
inst✝¹ : DivInvMonoid G
inst✝ : TopologicalSpace G
x y : G
⊢ ClusterPt x (map ((fun x ↦ y ^ x) ∘ Nat.cast) atTop) ↔ ClusterPt x (map (fun x ↦ y ^ x) atTop)
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ IsInducing (Subtype.val ∘ ⇑(Equiv.Set.image DFunLike.coe S ⋯))

Tactic:
← EquicontinuousOn.isInducing_uniformOnFun_iff_pi

Goal state after:
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ IsInducing (⇑(UniformOnFun.ofFun ?m.83) ∘ Subtype.val ∘ ⇑(Equiv.Set.image DFunLike.coe S ⋯))

case 𝔖_covers
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ ⋃₀ ?m.83 = univ

case 𝔖_compact
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ ∀ K ∈ ?m.83, IsCompact K

case F_eqcont
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ ∀ K ∈ ?m.83, EquicontinuousOn (Subtype.val ∘ ⇑(Equiv.Set.image DFunLike.coe S ⋯)) K

X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ Set (Set X)
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ ⊓ 𝓟 V = 𝓕₂ ⊓ 𝓟 V
⊢ 𝓕₁ = 𝓕₂ ⊓ 𝓟 V

Tactic:
simpa [← H]

Goal state after: