mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: case h
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
hx : x ∈ f.ker ⊓ I • ⊤
y : TensorProduct R (↥I) M
hy : (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) y = x
inj : Function.Injective ⇑(↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I))
comm1 :
  (↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I)) ∘ₗ lTensor (↥I) f =
    f ∘ₗ ↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)
eq0 : (lTensor (↥I) f) y = 0
z : TensorProduct R ↥I ↥f.ker
hz : (lTensor (↥I) f.ker.subtype) z = y
comm2 :
  (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) ∘ₗ lTensor (↥I) f.ker.subtype =
    f.ker.subtype ∘ₗ ↑(TensorProduct.lid R ↥f.ker) ∘ₗ rTensor (↥f.ker) (Submodule.subtype I)
⊢ f.ker.subtype ((↑(TensorProduct.lid R ↥f.ker) ∘ₗ rTensor (↥f.ker) (Submodule.subtype I)) z) = f.ker.subtype ⟨x, ⋯⟩

Tactic:
← LinearMap.comp_apply,

Goal state after:
case h
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
hx : x ∈ f.ker ⊓ I • ⊤
y : TensorProduct R (↥I) M
hy : (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) y = x
inj : Function.Injective ⇑(↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I))
comm1 :
  (↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I)) ∘ₗ lTensor (↥I) f =
    f ∘ₗ ↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)
eq0 : (lTensor (↥I) f) y = 0
z : TensorProduct R ↥I ↥f.ker
hz : (lTensor (↥I) f.ker.subtype) z = y
comm2 :
  (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) ∘ₗ lTensor (↥I) f.ker.subtype =
    f.ker.subtype ∘ₗ ↑(TensorProduct.lid R ↥f.ker) ∘ₗ rTensor (↥f.ker) (Submodule.subtype I)
⊢ (f.ker.subtype ∘ₗ ↑(TensorProduct.lid R ↥f.ker) ∘ₗ rTensor (↥f.ker) (Submodule.subtype I)) z = f.ker.subtype ⟨x, ⋯⟩
Module: Mathlib.RingTheory.Valuation.Extension

Goal state before:
pp: K : Type u_5
L : Type u_6
Γ₀ : Type u_7
Γ₁ : Type u_8
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₁
vK : Valuation K Γ₀
vL : Valuation L Γ₁
inst✝ : vK.HasExtension vL
x : ↥K₀
⊢ vL ((algebraMap K L) ↑x) ≤ vL ((algebraMap K L) 1)

Tactic:
val_map_le_iff (vR := vK),

Goal state after:
K : Type u_5
L : Type u_6
Γ₀ : Type u_7
Γ₁ : Type u_8
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₁
vK : Valuation K Γ₀
vL : Valuation L Γ₁
inst✝ : vK.HasExtension vL
x : ↥K₀
⊢ vK ↑x ≤ vK 1
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
this : Nontrivial R
⊢ ¬1 = 0

Tactic:
exact one_ne_zero

Goal state after:
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ (toPadicInt p).comp (fromPadicInt p) = RingHom.id ℤ_[p]

Tactic:
by
  rw [← PadicInt.toZModPow_eq_iff_ext]
  intro n
  rw [← RingHom.comp_assoc, toPadicInt, PadicInt.lift_spec]
  simp only [fromPadicInt, toZModPow, RingHom.comp_id]
  rw [RingHom.comp_assoc, truncate_comp_lift, ← RingHom.comp_assoc]
  simp only [RingEquiv.symm_toRingHom_comp_toRingHom, RingHom.id_comp]

Goal state after:
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
⊢ ∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b

Tactic:
obtain ⟨m, c, hc, hcm⟩ := WittVector.verschiebung_nonzero ha
  obtain ⟨b, rfl⟩ := (frobenius_bijective p k).surjective.iterate m c
  rw [WittVector.iterate_frobenius_coeff] at hc
  have := congr_fun (WittVector.verschiebung_frobenius_comm.comp_iterate m) b
  simp only [Function.comp_apply] at this
  rw [← this] at hcm
  refine ⟨m, b, ?_, ?_⟩
  · contrapose hc
    simp [hc, zero_pow <| pow_ne_zero _ hp.out.ne_zero]
  · simp_rw [← mul_left_iterate (p : 𝕎 k) m]
    convert! hcm using 2
    ext1 x
    rw [mul_comm, ← WittVector.verschiebung_frobenius x]; rfl

Goal state after:
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| (∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ↑p ^ (n + 1) * X (0, n + 1)) *
    ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))

Tactic:
arg 2
    rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    ↑p ^ (n + 1) * X (1, n + 1)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
⊢ IsClub (Function.fixedPoints f)

Tactic:
refine ⟨fun s hs hs₀ _ a ha ↦ (hf.map_isLUB ha hs₀).unique ?_, fun a ↦ ?_⟩

Goal state after:
case inr.refine_1
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
s : Set α
hs : s ⊆ Function.fixedPoints f
hs₀ : s.Nonempty
x✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
⊢ IsLUB (f '' s) a

case inr.refine_2
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
a : α
⊢ ∃ y ∈ Function.fixedPoints f, a ≤ y
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case right
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ ∀ (i : Ordinal.{u}), ⨆ (_ : i < a), f (lfpApprox f x i) ≤ ⨆ b, lfpApprox f x ↑b

Tactic:
· exact fun b => iSup_mono' fun hab => ⟨⟨b + 1, ha.succ_lt hab⟩, (by
    simpa using apply_lfpApprox_le_lfpApprox_of_lt f (lt_add_one b))⟩

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
⊢ f (lfpApprox f x a) = lfpApprox f x a

Tactic:
← lfpApprox_add_one f hx

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
⊢ lfpApprox f x (a + 1) = lfpApprox f x a
Module: Mathlib.SetTheory.Ordinal.Topology

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

Tactic:
by
  tfae_have 1 → 2 := by
    simpa only [mem_closure_iff_nhdsWithin_neBot, inter_comm s, nhdsWithin_inter',
      SuccOrder.nhdsLE_eq_nhds] using! id
  tfae_have 2 → 3
  | h => by
    rcases (s ∩ Iic a).eq_empty_or_nonempty with he | hne
    · simp [he] at h
    · refine ⟨hne, (isLUB_of_mem_closure ?_ h).csSup_eq hne⟩
      exact fun x hx => hx.2
  tfae_have 3 → 4
  | h => ⟨_, inter_subset_left, h.1, bddAbove_Iic.mono inter_subset_right, h.2⟩
  tfae_have 4 → 5 := by
    rintro ⟨t, ht, ht₀, ht₁, rfl⟩
    rw [bddAbove_iff_small] at ht₁
    refine ⟨Shrink t, ?_, Subtype.val ∘ (equivShrink _).symm, ?_, ?_⟩
    · have := ht₀.to_subtype
      exact (equivShrink _).symm.nonempty
    · simpa [← (equivShrink t).forall_congr_left (p := (·.1 ∈ s))]
    · simp [(equivShrink t).symm.iSup_comp, ← sSup_eq_iSup']
  tfae_have 5 → 1 := by
    rintro ⟨ι, hne, f, hfs, rfl⟩
    exact closure_mono (range_subset_iff.2 hfs) <| csSup_mem_closure (range_nonempty f)
      bddAbove_of_small
  tfae_finish

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

Goal state before:
pp: case refine_2.refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this✝ : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
this : sSup (enumOrd s '' Set.Iio a) ∈ s
⊢ enumOrd s a ≤ o

Tactic:
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.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
R' : Type u_3
S' : Type u_4
inst✝¹ : CommRing R'
inst✝ : CommRing S'
f : R →+* S
flat : f.Flat
qR : R →+* R'
qS : S →+* S'
g : R' →+* S'
surjR : Function.Surjective ⇑qR
surjS : Function.Surjective ⇑qS
comm : qS.comp f = g.comp qR
sq0 : ker qR ^ 2 = ⊥
eqmap : ker qS = Ideal.map f (ker qR)
smoothq : g.FormallySmooth
⊢ f.FormallySmooth

Tactic:
algebraize [f, qR, qS, g, qS.comp f]
  let _ : IsScalarTower R R' S' := IsScalarTower.of_algebraMap_eq' comm
  exact Algebra.FormallySmooth.of_surjective_of_ker_eq_map_of_flat surjR surjS eqmap sq0 ‹_›

Goal state after:
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 : β
γ : Type u
Γ : γ → PSet.{u}
A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, (Γ a).Equiv (Δ b)
δγ : ∀ (b : δ), ∃ a, (Γ a).Equiv (Δ b)
c : (A a).Type := c✝
⊢ γ

Tactic:
ea

Goal state after:
α β : 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 : β
γ : Type u
Γ : γ → PSet.{u}
A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, (Γ a).Equiv (Δ b)
δγ : ∀ (b : δ), ∃ a, (Γ a).Equiv (Δ b)
c : (PSet.mk γ Γ).Type
⊢ γ
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u_1}
mem : ∀ z ∈ x, y ∈ z
s : ZFSet.{u_1}
h : s ∈ ↑x
⊢ ∃ z ∈ x, y ∈ z

Tactic:
exact ⟨_, h, mem _ h⟩

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

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

Tactic:
· simpa [(lt_veblen_invVeblen₁ a).trans_le (veblen_left_monotone _ h)]

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

Goal state before:
pp: case pos
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : ↑n₁ - ↑n₂ = 0
en : n₁ = n₂
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

pp: case neg
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : ↑n₁ - ↑n₂ = 0
en : ¬n₁ = n₂
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
· simpa [en]

Goal state after:
case neg
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : ↑n₁ - ↑n₂ = 0
en : ¬n₁ = n₂
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case limit.refine_1
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ ℵ₀ ≤ #↑(Set.Iio o)

Tactic:
rw [mk_Iio_ordinal, ← lift_aleph0.{u + 1, u}, lift_le, Ordinal.aleph0_le_card]
      exact Ordinal.omega0_le_of_isSuccLimit ho

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

Goal state before:
pp: x✝¹ x✝ : Ordinal.{u_1}
h : x✝¹ < x✝
⊢ x✝¹.toZFSet ⊂ x✝.toZFSet

Tactic:
rw [ssubset_iff_subset_not_subset]; simp [h, h.le]

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

Goal state before:
pp: x : ZFSet.{u}
⊢ x.IsOrdinal ↔ x ∈ Set.range toZFSet

Tactic:
by
  refine ⟨fun h ↦ ?_, ?_⟩
  · rw [← h.toZFSet_rank_eq]
    exact Set.mem_range_self _
  · rintro ⟨a, rfl⟩
    exact isOrdinal_toZFSet a

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

Goal state before:
pp: case succ.refine_1
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)
x✝ : k + 1 ≠ 0
⊢ R' < (ω ^ a0.repr) ^ succ ↑(k + 1)

Tactic:
RR,

Goal state after:
case succ.refine_1
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)
x✝ : k + 1 ≠ 0
⊢ ω0 ^ ↑k * (α' * ↑m) + R < (ω ^ a0.repr) ^ succ ↑(k + 1)
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 + 1) * α' + R' = ω0 ^ succ ↑k * α' + (ω0 ^ ↑k * α' * ↑m + R)

Tactic:
RR,

Goal state after:
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 + 1) * α' + (ω0 ^ ↑k * (α' * ↑m) + R) = ω0 ^ succ ↑k * α' + (ω0 ^ ↑k * α' * ↑m + R)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case pos
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h_if : some x :: ↑s = some x :: ↑t
h' : True
⊢ Seq.cons x s = Seq.cons x t

Tactic:
apply_fun Subtype.val using Subtype.val_injective

Goal state after:
case pos
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h_if : some x :: ↑s = some x :: ↑t
h' : True
⊢ ↑(Seq.cons x s) = ↑(Seq.cons x t)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case succ.refine_2.e_a
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 ^ succ ↑k * α' = (ω0 ^ ↑k * α' + R) * α'

Tactic:
have αd : ω ∣ α' :=
      dvd_add (dvd_mul_of_dvd_left (by simpa using opow_dvd_opow ω (one_le_iff_ne_zero.2 e0)) _) d
    have α0 : ¬IsMin α' := by
      rw [isMin_iff_eq_bot]
      exact α0.ne'
    rw [mul_add (ω0 ^ (k : Ordinal)), add_assoc, ← mul_assoc, ← opow_succ,
      add_mul_of_isSuccLimit _ ⟨α0, isSuccPrelimit_iff_omega0_dvd.2 αd⟩, mul_assoc,
      @mul_omega0_dvd n (Nat.cast_pos'.2 n.pos) (natCast_lt_omega0 _) _ αd]
    apply @add_of_omega0_opow_le _ (repr a0 * succ ↑k)
    · refine isPrincipal_add_omega0_opow _ ?_ Rl
      rw [opow_mul, opow_succ]
      gcongr
      exact No.snd'.repr_lt
    · have := mul_le_mul_right (one_le_iff_pos.2 <| Nat.cast_pos'.2 n.pos) (ω0 ^ succ (k : Ordinal))
      rw [opow_mul]
      simpa

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

Goal state before:
pp: case succ.some
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, op') => (hd, ↑op' s.tail))
              (T s.head)
n : ℕ
ih :
  ∀ {op : Stream'.Seq α → Stream'.Seq α},
    motive op → ∀ (s t : Stream'.Seq α), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n
op : Stream'.Seq α → Stream'.Seq α
h_base : motive op
s t : Stream'.Seq α
hn : dist s t ≤ 2⁻¹ ^ (n + 1)
T : Option α → Option (α × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, op') => (hd, ↑op' s.tail))
        (T s.head)
h_head : s.head = t.head
hs :
  (op s).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' s.tail))
      (T s.head)
ht :
  (op t).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' t.tail))
      (T t.head)
v : α × Subtype motive
hT_head : T s.head = some v
⊢ dist (op s) (op t) ≤ 2⁻¹ ^ (n + 1)

Tactic:
obtain ⟨hd, op', h_next⟩ := v
      simp only [hT_head, Option.map_some, ← h_head] at hs ht
      simp only [destruct_eq_cons hs, destruct_eq_cons ht, dist_cons_cons, pow_succ', inv_pos,
        Nat.ofNat_pos, mul_le_mul_iff_right₀, ge_iff_le]
      apply ih h_next
      simpa [dist_eq_half_of_head h_head, pow_succ'] using hn

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

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

Tactic:
rcases e' : m.natPred with - | m'

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

case oadd.inl.none.inl.none.succ
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
m' : ℕ
e' : m.natPred = m' + 1
⊢ match
    match Sum.inl none, m' + 1 with
    | Sum.inl none, 0 => Sum.inl (some zero)
    | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
    | Sum.inl (some a'), 0 => Sum.inr fun i ↦ a'.oadd i.succPNat zero
    | Sum.inl (some a'), m.succ => Sum.inr fun i ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
    | Sum.inr f, 0 => Sum.inr fun i ↦ (f i).oadd 1 zero
    | Sum.inr f, m.succ => Sum.inr fun i ↦ a.oadd m.succPNat ((f i).oadd 1 zero) with
  | Sum.inl none => a.oadd m b = 0
  | Sum.inl (some a_1) => (a.oadd m b).repr = succ a_1.repr ∧ ((a.oadd m b).NF → a_1.NF)
  | Sum.inr f =>
    IsSuccLimit (a.oadd m b).repr ∧
      (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a.oadd m b ∧ ((a.oadd m b).NF → (f i).NF)) ∧
        ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (f i).repr