mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n✝ : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
w✝⁴ : Type v
w✝³ : AddCommGroup w✝⁴
w✝² : Module R w✝⁴
w✝¹ : Free R w✝⁴
w✝ : Module.Finite R w✝⁴
f : w✝⁴ →ₗ[R] ↑M
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := f.shortComplexKer
hS : S.ShortExact
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1))) → HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1 + 1))
this : ∀ (L : ModuleCat R), Subsingleton (Ext S.X₁ L (n + 1)) ↔ Subsingleton (Ext M L (n + 2))
⊢ HasProjectiveDimensionLT S.X₁ (n + 1)

Tactic:
apply hn S.X₁

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n✝ : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
w✝⁴ : Type v
w✝³ : AddCommGroup w✝⁴
w✝² : Module R w✝⁴
w✝¹ : Free R w✝⁴
w✝ : Module.Finite R w✝⁴
f : w✝⁴ →ₗ[R] ↑M
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := ⋯
hS : S.ShortExact
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1))) → HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1 + 1))
this : ∀ (L : ModuleCat R), Subsingleton (Ext S.X₁ L (n + 1)) ↔ Subsingleton (Ext M L (n + 2))
⊢ ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext S.X₁ L (n + 1))
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
r : R
f : M →ₚₗ[R] N
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ toFun S (r • f) = r • toFun S f

Tactic:
ext t
  obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
  simp only [toFun_eq_rTensor_φ_toFun' _ ha, smul_def, Pi.smul_apply, map_smul]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case neg
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsLocalRing A
f g : A⟦X⟧
inst✝¹ : IsPrecomplete (IsLocalRing.maximalIdeal A) A
hg : ¬(map (IsLocalRing.residue A)) g ≠ 0
inst✝ : Nontrivial A
⊢ ⊥ < ↑((map (IsLocalRing.residue A)) g).order.toNat

Tactic:
exact WithBot.bot_lt_coe _

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst✝⁹ : CommSemiring R₀
inst✝⁸ : Ring R
inst✝⁷ : Algebra R₀ R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R S
inst✝ : IsSemisimpleModule R S
m : Submodule R M
x✝ : m ∈ {m | Nonempty (↥m ≃ₗ[R] S)}
e : ↥m ≃ₗ[R] S
⊢ IsSemisimpleModule R ↥m

Tactic:
have := IsSemisimpleModule.congr e

Goal state after:
R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst✝⁹ : CommSemiring R₀
inst✝⁸ : Ring R
inst✝⁷ : Algebra R₀ R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R S
inst✝ : IsSemisimpleModule R S
m : Submodule R M
x✝ : m ∈ {m | Nonempty (↥m ≃ₗ[R] S)}
e : ↥m ≃ₗ[R] S
this : IsSemisimpleModule R ↥m
⊢ IsSemisimpleModule R ↥m
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ (List.map f l).sum ∈ I

Tactic:
rw [mem_iff, ← List.sum_map_zero]

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ I.ringCon (List.map f l).sum (List.map (fun x ↦ 0) ?m.26).sum

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ Type ?u.29

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ List ?m.23
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
s : S
n : ℕ
hn : n > 0
r : R
hr : f r = s ^ n
⊢ ↑(basicOpen s) = comap f ⁻¹' ↑(basicOpen r)

Tactic:
rw [← basicOpen_pow _ n hn, ← hr]; rfl

Goal state after:
Module: Mathlib.RingTheory.Valuation.Extension

Goal state before:
pp: case hx
R : Type u_1
inst✝⁶ : CommRing R
ΓR : Type u_6
inst✝⁵ : LinearOrderedCommGroupWithZero ΓR
vR : Valuation R ΓR
S : Type u_9
ΓS : Type u_10
inst✝⁴ : CommRing S
inst✝³ : LinearOrderedCommGroupWithZero ΓS
inst✝² : Algebra R S
inst✝¹ : IsLocalHom (algebraMap R S)
vS : Valuation S ΓS
inst✝ : vR.HasExtension vS
r : ↥vR.integer
hr : IsUnit ((algebraMap ↥vR.integer ↥vS.integer) r)
⊢ IsUnit ((algebraMap (↥vR.integer) R) r)

Tactic:
exact (isUnit_map_iff (algebraMap R S) _).mp (hr.map (algebraMap _ S))

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ (zmodEquivTrunc p m).symm.toRingHom.comp ((TruncatedWittVector.truncate h).comp (truncate n)) =
    (zmodEquivTrunc p m).symm.toRingHom.comp (truncate m)

Tactic:
truncate_comp_wittVector_truncate

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ (zmodEquivTrunc p m).symm.toRingHom.comp (truncate m) = (zmodEquivTrunc p m).symm.toRingHom.comp (truncate m)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ wittPolyProdRemainder p n + ↑p ^ n * wittMul p n =
    ∑ x ∈ range n, ↑p ^ x * wittMul p x ^ p ^ (n - x) + ↑p ^ n * wittMul p n ^ p ^ 0

Tactic:
pow_zero,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ wittPolyProdRemainder p n + ↑p ^ n * wittMul p n =
    ∑ x ∈ range n, ↑p ^ x * wittMul p x ^ p ^ (n - x) + ↑p ^ n * wittMul p n ^ 1
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)) +
    (rename (Prod.mk 0)) (C (↑p ^ (n + 1)) * X (n + 1) ^ p ^ 0)

Tactic:
pow_zero,

Goal state after:
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)) +
    (rename (Prod.mk 0)) (C (↑p ^ (n + 1)) * X (n + 1) ^ 1)
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 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    (rename (Prod.mk 1)) (C (↑p ^ (n + 1)) * X (n + 1) ^ p ^ 0)

Tactic:
pow_zero,

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)) +
    (rename (Prod.mk 1)) (C (↑p ^ (n + 1)) * X (n + 1) ^ 1)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
⊢ TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k

Tactic:
intro x y
    apply f₀
    rintro ⟨a, ha⟩
    apply Function.uncurry ![x, y]
    let S : Set (Fin 2 × ℕ) := { a | a.2 = n ∨ a.2 < n }
    have ha' : a ∈ S := by grind
    refine ⟨a.fst, ⟨a.snd, ?_⟩⟩
    obtain ⟨ha, ha⟩ := ha' <;> lia

Goal state after:
Module: Mathlib.SetTheory.Lists

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

Tactic:
cases a
    cases h'

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

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

Tactic:
obtain (ha | ha) := not_isSuccLimit_iff.mp ha
    · convert! isOpen_Iio (a := Order.succ a) using 1
      simp [ha.Iic_eq]
    · exact isOpen_singleton_of_not_isSuccPrelimit ha

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}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ x + f e' = x

Tactic:
notMem_support_iff.1,

Goal state after:
b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ x + 0 = x

b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ e' ∉ f.support
Module: Mathlib.SetTheory.Ordinal.Topology

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

Tactic:
rw [← mem_closure_iff_bsup, hs.closure_eq]

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

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ foldr (fun p r ↦ b ^ p * (coeff b o) p + r) 0 ((map Prod.fst (CNF b o)).toFinset.sort fun x1 x2 ↦ x1 ≥ x2) =
    foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o)

Tactic:
(toFinset_sort _ _).2,

Goal state after:
b o : Ordinal.{u_1}
⊢ foldr (fun p r ↦ b ^ p * (coeff b o) p + r) 0 (map Prod.fst (CNF b o)) =
    foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o)

b o : Ordinal.{u_1}
⊢ List.Pairwise (fun x1 x2 ↦ x1 ≥ x2) (map Prod.fst (CNF b o))

b o : Ordinal.{u_1}
⊢ (map Prod.fst (CNF b o)).Nodup
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case single_add.hxb
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : (∀ (e : Ordinal.{u_1}), f e < b) → coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ x + f e = x

Tactic:
notMem_support_iff.1,

Goal state after:
case single_add.hxb
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : (∀ (e : Ordinal.{u_1}), f e < b) → coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ x + 0 = x

case single_add.hxb
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : (∀ (e : Ordinal.{u_1}), f e < b) → coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ e ∉ f.support
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
⊢ StrictMono fun x ↦ veblenWith f x 0

Tactic:
by
  intro o₁ o₂ h
  dsimp only
  rw [← veblenWith_veblenWith_of_lt hf h, veblenWith_lt_veblenWith_iff_right hf]
  exact veblenWith_pos hf hp

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o₁ a ≤ veblenWith f o₂ b ↔
    o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a ≤ b

Tactic:
by
  rw [← not_lt, ← cmp_eq_gt_iff, cmp_veblenWith hf]
  aesop (add simp [not_lt_of_ge, lt_asymm])

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

Goal state before:
pp: x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝.rank < x.rank

Tactic:
trans <;> apply rank_lt_of_mem

Goal state after:
case a
x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝ ∈ ?x✝

case x
x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ PSet.{u_1}

x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ ?x✝ ∈ x
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝.rank < x.rank

Tactic:
trans <;> apply rank_lt_of_mem

Goal state after:
case a
x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝ ∈ ?x✝

case x
x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ ZFSet.{u_1}

x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ ?x✝ ∈ x
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ x ∈ o.toPSet ↔ ∃ a < o, x.Equiv a.toPSet

Tactic:
by
  rw [toPSet, PSet.mem_def]
  simpa using ((@ToType.mk o).exists_congr_left (p := fun y ↦ x.Equiv y.1.toPSet)).symm

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:
by rw [ssubset_iff_subset_not_subset]; simp [h, h.le]

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

Goal state before:
pp: case refine_1
o : Ordinal.{u_1}
y : ZFSet.{u_1}
a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
hy : y ∈ a.toZFSet
⊢ y ∈ o.toZFSet

Tactic:
obtain ⟨b, hb, rfl⟩ := mem_toZFSet_iff.1 hy

Goal state after:
case refine_1
o a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
b : Ordinal.{u_1}
hb : b < a
hy : b.toZFSet ∈ a.toZFSet
⊢ b.toZFSet ∈ o.toZFSet
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case refine_2
o : Ordinal.{u_1}
z y : ZFSet.{u_1}
hz : z ∈ y
a : Ordinal.{u_1}
ha : a < o
hy : y ∈ a.toZFSet
hx : a.toZFSet ∈ o.toZFSet
⊢ z ∈ a.toZFSet

Tactic:
obtain ⟨b, hb, rfl⟩ := mem_toZFSet_iff.1 hy

Goal state after:
case refine_2
o : Ordinal.{u_1}
z : ZFSet.{u_1}
a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
b : Ordinal.{u_1}
hb : b < a
hz : z ∈ b.toZFSet
hy : b.toZFSet ∈ a.toZFSet
⊢ z ∈ a.toZFSet
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
⊢ (o₁ ^ o₂).NF

Tactic:
· by_cases h : m = 0
      · simp only [(· ^ ·), Pow.pow, opow, opowAux2, OfNat.ofNat, Zero.zero, One.one, *]
        decide
      · simp only [(· ^ ·), Pow.pow, opow, opowAux2, OfNat.ofNat, Zero.zero, *]
        change NF (oadd _ _ 0)
        infer_instance

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

Goal state before:
pp: o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
⊢ (o₁ ^ o₂).NF

Tactic:
by
  rcases e₁ : split o₁ with ⟨a, m⟩
  have na := (nf_repr_split e₁).1
  rcases e₂ : split' o₂ with ⟨b', k⟩
  have := (nf_repr_split' e₂).1
  obtain - | ⟨a0, n, a'⟩ := a
  #adaptation_note /-- Proof repaired after leanprover/lean4#13363.
  The next branch was previously
  ```
  · rcases m with - | m
    · by_cases o₂ = 0 <;> simp only [(· ^ ·), Pow.pow, opow, opowAux2, *] <;> decide
    · by_cases m = 0
      · simp only [(· ^ ·), Pow.pow, opow, opowAux2, *, zero_def]
        decide
      · simp only [(· ^ ·), Pow.pow, opow, opowAux2, *]
        infer_instance
  ```
  The replacement proof is a short-term fix, and we request that the authors/maintainers of
  this file review the proof, and either approve it by removing this note, revise
  the proof or the prerequisites appropriately, or minimize a problem in lean4 that still
  needs addressing. -/
  · rcases m with - | m
    · by_cases h : o₂ = 0
      · subst h
        simp only [(· ^ ·), Pow.pow, opow, opowAux2, e₁, OfNat.ofNat, Zero.zero, One.one]
        decide
      · have h' : o₂ ≠ zero := fun he => h (he ▸ zero_def ▸ rfl)
        simp only [(· ^ ·), Pow.pow, opow, opowAux2, e₁, OfNat.ofNat, Zero.zero, One.one,
          h', ite_false]
        exact NF.zero
    · by_cases h : m = 0
      · simp only [(· ^ ·), Pow.pow, opow, opowAux2, OfNat.ofNat, Zero.zero, One.one, *]
        decide
      · simp only [(· ^ ·), Pow.pow, opow, opowAux2, OfNat.ofNat, Zero.zero, *]
        change NF (oadd _ _ 0)
        infer_instance
  · simp only [(· ^ ·), Pow.pow, opow, opowAux2, e₁, split_eq_scale_split' e₂, mulNat_eq_mul]
    have := na.fst
    rcases k with - | k
    · infer_instance
    · cases k <;> cases m <;> infer_instance

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

Goal state before:
pp: case hf_comp
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ ∀ (g : ℝ → ℝ),
    (basis_hd :: basis_tl).getLast? = some g →
      (Real.log ∘ Real.log ∘ (basis_hd :: basis_tl).getLast ⋯) =o[atTop] (Real.log ∘ g)

Tactic:
intro g hg
    simpa [List.getLast_of_getLast?_eq_some hg] using Real.isLittleO_log_id_atTop.comp_tendsto <|
      Real.tendsto_log_atTop.comp <| h_basis.tendsto_atTop <| List.mem_of_getLast? hg

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

Goal state before:
pp: case inl
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹
hx : op (Seq.cons hd x) = nil
hy : op (Seq.cons hd y) = nil
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head

Tactic:
simp [hx, hy]

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

Goal state before:
pp: case inr
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹
w✝² : α
w✝¹ w✝ : Stream'.Seq α
hx : op (Seq.cons hd x) = Seq.cons w✝² w✝¹
hy : op (Seq.cons hd y) = Seq.cons w✝² w✝
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head

Tactic:
simp [hx, hy]

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

Goal state before:
pp: case oadd
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
obtain ⟨a00, ad⟩ := N₁.of_dvd_omega0 (split_dvd e₁)

Goal state after:
case oadd
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: basis : Basis
n : Fin (List.length basis)
r : ℝ
h_basis : WellFormedBasis basis
⊢ (monomialRpow basis (↑n) r).Approximates

Tactic:
cases basis with
  | nil => simp
  | cons basis_hd basis_tl =>
    simp only [List.length_cons, monomialRpow, Fin.is_lt, getElem!_pos]
    cases n using Fin.cases with
    | zero =>
      simp only [Fin.coe_ofNat_eq_mod, Nat.zero_mod, Multiseries.monomialRpow,
        List.getElem_cons_zero]
      apply (one_approximates h_basis.tail).cons _ (by simp)
      exact Majorized.self <| h_basis.tendsto_atTop (by simp)
    | succ m =>
      simp only [Fin.val_succ, Multiseries.monomialRpow, List.getElem_cons_succ]
      apply (monomialRpow_approximates h_basis.tail).cons _ (by simp)
      apply h_basis.tail_pow_majorized_head (by simp)

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

Goal state before:
pp: exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : exps_hd ≠ 0
⊢ exps_hd • log ∘ basis_hd + exps_tl.toLogFun basis_tl ~[atTop] exps_hd • log ∘ basis_hd

Tactic:
apply IsEquivalent.refl.add_isLittleO

Goal state after:
exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : exps_hd ≠ 0
⊢ exps_tl.toLogFun basis_tl =o[atTop] (exps_hd • log ∘ basis_hd)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case h.cons
α : Type u_1
op✝ : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_base : motive op✝
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = opf ∘ op' ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
s : Stream'.Seq α
s_hd : α
s_tl : Stream'.Seq α
hT :
  (Seq.cons s_hd s_tl).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
      (T s.head)
⊢ (opf (Seq.cons s_hd s_tl)).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match T s.head with
      | none => Option.map (fun x ↦ (x.1, ⟨(fun x_1 ↦ ↑x.2 nil) ∘ op, ⋯⟩)) (h_opf.unfold none)
      | some (hd, opf', op') => Option.map (fun x ↦ (x.1, ⟨(↑x.2 ∘ ↑opf') ∘ ↑op', ⋯⟩)) (h_opf.unfold (some hd)))

Tactic:
simp only [destruct_cons] at hT

Goal state after:
case h.cons
α : Type u_1
op✝ : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_base : motive op✝
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = opf ∘ op' ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
s : Stream'.Seq α
s_hd : α
s_tl : Stream'.Seq α
hT : some (s_hd, s_tl) = Option.map (fun x ↦ (x.1, ↑x.2.1 (↑x.2.2 s.tail))) (T s.head)
⊢ (opf (Seq.cons s_hd s_tl)).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match T s.head with
      | none => Option.map (fun x ↦ (x.1, ⟨(fun x_1 ↦ ↑x.2 nil) ∘ op, ⋯⟩)) (h_opf.unfold none)
      | some (hd, opf', op') => Option.map (fun x ↦ (x.1, ⟨(↑x.2 ∘ ↑opf') ∘ ↑op', ⋯⟩)) (h_opf.unfold (some hd)))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl
h_trimmed : coef✝.Trimmed
h_ne_zero : ¬coef✝.IsZero
tl✝ : Multiseries basis_hd basis_tl
h_ms : Multiseries.cons exp coef tl = Multiseries.cons exp✝ coef✝ tl✝
⊢ coef.Trimmed ∧ ¬coef.IsZero

Tactic:
simp at h_ms
    grind

Goal state after:
Module: Mathlib.Tactic.NormNum.NatLog

Goal state before:
pp: b m n : ℕ
hb : 1 < b
h₁ : (b ^ m).blt n = true
h₂ : n.ble (b ^ (m + 1)) = true
⊢ Nat.clog b n = m + 1

Tactic:
rw [Nat.blt_eq, ← Nat.lt_clog_iff_pow_lt hb] at h₁

Goal state after:
b m n : ℕ
hb : 1 < b
h₁ : m < Nat.clog b n
h₂ : n.ble (b ^ (m + 1)) = true
⊢ Nat.clog b n = m + 1
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a m k : ℕ
hm : m * m = k
hk₁ : k.blt a = true
hk₂ : a.ble (k + 2 * m) = true
⊢ ¬IsSquare a

Tactic:
subst k

Goal state after:
a m : ℕ
hk₁ : (m * m).blt a = true
hk₂ : a.ble (m * m + 2 * m) = true
⊢ ¬IsSquare a