mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hv : b ∈ v.asIdeal
ha₀ : a ≠ 0
hva : (valuation K v) ↑a ≠ 0
⊢ ↑b ≠ 0

Tactic:
by simp [hb]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x✝ : ∃ i, {x | embedding (extension x) < embedding ↑i} ⊆ s
γ : (ofClass v).ValueGroup₀ˣ
h : {x | embedding (extension x) < embedding ↑γ} ⊆ s
⊢ ∃ γ, {x | extensionValuation.restrict x < ↑γ} ⊆ s

Tactic:
use Units.map valueGroup₀_equiv_extensionValuation.toMonoidHom γ
        convert! h
        apply this

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n d : R
hd : d ∈ nonZeroDivisors R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K n ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K n ⟨d, hd⟩ * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hn0 : n ≠ 0
hd0 : d ≠ 0
ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥
v : Ideal R
hv hv' : Irreducible (Associates.mk v)
⊢ Multiset.count ⟨Associates.mk v, hv⟩ (Associates.factors' (Ideal.span {d})) ≤
    Multiset.count ⟨Associates.mk v, hv⟩ (Associates.factors' (Ideal.span {n}))

Tactic:
rw [Associates.irreducible_mk, irreducible_iff_prime] at hv

Goal state after:
case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n d : R
hd : d ∈ nonZeroDivisors R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K n ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K n ⟨d, hd⟩ * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hn0 : n ≠ 0
hd0 : d ≠ 0
ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥
v : Ideal R
hv✝ : Irreducible (Associates.mk v)
hv : Prime v
hv' : Irreducible (Associates.mk v)
⊢ Multiset.count ⟨Associates.mk v, hv✝⟩ (Associates.factors' (Ideal.span {d})) ≤
    Multiset.count ⟨Associates.mk v, hv✝⟩ (Associates.factors' (Ideal.span {n}))
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case mp
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Function.Surjective ⇑v → Function.Surjective ⇑v

Tactic:
intro h γ

Goal state after:
case mp
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
⊢ ∃ a, v a = γ
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case mpr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Function.Surjective ⇑v → Function.Surjective ⇑v

Tactic:
intro h γ

Goal state after:
case mpr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
⊢ ∃ a, v a = γ
Module: Mathlib.Data.Finset.Finsupp

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∈ s
⊢ f i ∈ t i

pp: case neg
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∉ s
⊢ f i ∈ t i

Tactic:
· exact h.2 hi

Goal state after:
case neg
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∉ s
⊢ f i ∈ t i
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R✝ : Type u_2
S : Type u_3
inst✝¹ : CommSemiring R✝
s✝ : Finset (σ →₀ ℕ)
R : Type u_4
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
x✝¹ x✝ : MvPowerSeries σ R
⊢ ∑ x ∈ s, (MvPolynomial.monomial x) ((coeff x) (x✝¹ + x✝)) =
    ∑ x ∈ s, (MvPolynomial.monomial x) ((coeff x) x✝¹) + ∑ x ∈ s, (MvPolynomial.monomial x) ((coeff x) x✝)

Tactic:
by simp [sum_add_distrib]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case cons
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∑ i ∈ s, weightedOrder w (f i) ≤ weightedOrder w (∏ i ∈ s, f i)
⊢ ∑ i ∈ Finset.cons a s ha, weightedOrder w (f i) ≤ weightedOrder w (∏ i ∈ Finset.cons a s ha, f i)

Tactic:
Finset.sum_cons ha,

Goal state after:
case cons
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∑ i ∈ s, weightedOrder w (f i) ≤ weightedOrder w (∏ i ∈ s, f i)
⊢ weightedOrder w (f a) + ∑ x ∈ s, weightedOrder w (f x) ≤ weightedOrder w (∏ i ∈ Finset.cons a s ha, f i)
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: a✝ b : ℕ∞
h : a✝ ≠ ⊤ ∨ b ≠ ⊤
a : ℕ
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 - x2) (↑a, ⊤)

Tactic:
suffices ∀ᶠ b in 𝓝 ⊤, (a - b : ℕ∞) = 0 by
      simpa [ContinuousAt, nhds_prod_eq, tsub_eq_zero_of_le]

Goal state after:
a✝ b : ℕ∞
h : a✝ ≠ ⊤ ∨ b ≠ ⊤
a : ℕ
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ ∀ᶠ (b : ℕ∞) in 𝓝 ⊤, ↑a - b = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
s : Set (adicCompletion K v)
⊢ s ∈ 𝓝 0 ↔ ∃ γ, {x | (valuation K v).restrict x < ↑γ} ⊆ s

Tactic:
(isUniformInducing_toCompletion K v).isInducing.nhds_eq_comap 0,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
s : Set (adicCompletion K v)
⊢ s ∈ Filter.comap toCompletion (𝓝 (toCompletion 0)) ↔ ∃ γ, {x | (valuation K v).restrict x < ↑γ} ⊆ s
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = p
⊢ (coeff d) f = (coeff d) 0

Tactic:
rw [coeff_zero]

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = p
⊢ (coeff d) f = 0
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
h : constantCoeff f = 0
⊢ Tendsto (fun i ↦ (f ^ i).order) atTop (𝓝 ⊤)

Tactic:
simp_rw [ENat.tendsto_nhds_top_iff_natCast_lt, Filter.eventually_atTop]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
h : constantCoeff f = 0
⊢ ∀ (n : ℕ), ∃ a, ∀ (b : ℕ), a ≤ b → ↑n < (f ^ b).order
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
ha : a ∉ adicCompletionIntegers K v
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Tactic:
notMem_adicCompletionIntegers

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : adicCompletion K v
ha : 1 < Valued.v a
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
φ : R⟦X⟧
⊢ (truncAux n φ).coeff m = if m < n then (coeff m) φ else 0

Tactic:
simp [truncAux, Polynomial.coeff_monomial]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
t : R
φ : R⟦X⟧
n✝ : ℕ
⊢ (truncAux n (t • φ)).coeff n✝ = ((RingHom.id R) t • truncAux n φ).coeff n✝

Tactic:
simp [truncAux, Polynomial.coeff_monomial]

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

Goal state before:
pp: case cons
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
φ : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : ∑ i ∈ s, (φ i).order ≤ (∏ i ∈ s, φ i).order
⊢ ∑ i ∈ Finset.cons a s ha, (φ i).order ≤ (∏ i ∈ Finset.cons a s ha, φ i).order

Tactic:
Finset.sum_cons ha,

Goal state after:
case cons
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
φ : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : ∑ i ∈ s, (φ i).order ≤ (∏ i ∈ s, φ i).order
⊢ (φ a).order + ∑ x ∈ s, (φ x).order ≤ (∏ i ∈ Finset.cons a s ha, φ i).order
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
h : f = 0
⊢ constantCoeff f.divXPowOrder = 0 ↔ f = 0

pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
h : ¬f = 0
⊢ constantCoeff f.divXPowOrder = 0 ↔ f = 0

Tactic:
· simp [h]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
h : ¬f = 0
⊢ constantCoeff f.divXPowOrder = 0 ↔ f = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
h : f.order.toNat ≤ n
⊢ (coeff (n - f.order.toNat)) f.divXPowOrder = (coeff n) f

pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
h : ¬f.order.toNat ≤ n
⊢ 0 = (coeff n) f

Tactic:
· simp [h]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
h : ¬f.order.toNat ≤ n
⊢ 0 = (coeff n) f
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : UniformSpace R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
I : Ideal S
hI : ↑I ∈ 𝓝 0
n : σ → ℕ := fun s ↦ sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this : ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, φ (MvPolynomial.coeff i x) ∈ I
p : MvPolynomial σ R
⊢ (∀ i ∈ D, φ (MvPolynomial.coeff i p) ∈ I) → (eval₂Hom φ a) p ∈ ↑I

Tactic:
hp

Goal state after:
σ : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : UniformSpace R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
I : Ideal S
hI : ↑I ∈ 𝓝 0
n : σ → ℕ := fun s ↦ sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this : ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, φ (MvPolynomial.coeff i x) ∈ I
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (MvPolynomial.coeff i p) ∈ I
⊢ (eval₂Hom φ a) p ∈ ↑I
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case zero
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := ⋯
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := ⋯
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ cantorFunction c f_max < cantorFunction c g

Tactic:
refine lt_of_lt_of_le ?_ (cantorFunction_le (le_of_lt h1) h3 hg_min)

Goal state after:
case zero
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ cantorFunction c f_max < cantorFunction c g_min
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹⁴ : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
a : σ → MvPowerSeries τ S
T : Type u_6
inst✝¹¹ : CommRing T
inst✝¹⁰ : UniformSpace T
inst✝⁹ : T2Space T
inst✝⁸ : CompleteSpace T
inst✝⁷ : IsUniformAddGroup T
inst✝⁶ : IsTopologicalRing T
inst✝⁵ : IsLinearTopology T T
inst✝⁴ : Algebra R T
ε : MvPowerSeries τ S →ₐ[R] T
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
hε : Continuous ⇑ε
f : MvPowerSeries σ R
⊢ (⇑ε ∘ ⇑(aeval ⋯)) f = (aeval ⋯) f

Tactic:
exact DFunLike.congr_fun (comp_aeval ha.hasEval hε) f

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re

Tactic:
replace h := h.norm

Goal state after:
f : ℕ → ℂ
s : ℂ
h : Summable fun x ↦ ‖term f s x‖
⊢ ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
h : ¬∃ a, q ^ a = n
⊢ { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) (f + g)) 0, map_zero' := ⋯ } n =
    ({ toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0, map_zero' := ⋯ } +
        { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0, map_zero' := ⋯ })
      n

Tactic:
· simp [h]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : f =O[atTop] fun n ↦ ↑n ^ (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖
C' : ℝ := max C ((insert 0 (image (fun n ↦ ‖f n‖ / ↑n ^ (x - 1)) (range m))).max' ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : n < m
⊢ ‖f n‖ ≤ C' * ↑n ^ (x - 1)

Tactic:
· have hn' : 0 < n := Nat.pos_of_ne_zero hn₀
    refine (div_le_iff₀ <| rpow_pos_of_pos (cast_pos.mpr hn') _).mp ?_
    refine (le_max' _ _ <| mem_insert_of_mem ?_).trans <| le_max_right ..
    exact mem_image.mpr ⟨n, mem_range.mpr hn, rfl⟩

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ (∑ᶠ (i : ℕ), (coeff i) P * (coeff (n + 1 + 1)) (B ^ i) - ∑ᶠ (i : ℕ), (coeff i) P * if i = 1 then k else 0) = 0

Tactic:
simp only [mul_ite, mul_zero]

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ (∑ᶠ (i : ℕ), (coeff i) P * (coeff (n + 1 + 1)) (B ^ i) - ∑ᶠ (i : ℕ), if i = 1 then (coeff i) P * k else 0) = 0
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ (∑ᶠ (i : ℕ), (coeff i) P * (coeff (n + 1 + 1)) (B ^ i) - if 1 = 1 then (coeff 1) P * k else 0) = 0

pp: case ha
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ ∀ (x : ℕ), x ≠ 1 → (if x = 1 then (coeff x) P * k else 0) = 0

Tactic:
· simp only [↓reduceIte, ← hk, mul_invOf_cancel_left', sub_eq_zero]
            rw [coeff_subst']
            · rfl
            · simp [HasSubst, ← PowerSeries.constantCoeff.eq_def, hB']

Goal state after:
case ha
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ ∀ (x : ℕ), x ≠ 1 → (if x = 1 then (coeff x) P * k else 0) = 0
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝², non_trivial := ⋯ }
hr : 0 < r
hx : ‖x‖ ≠ 0
a : 𝕜
ha₀ : a ≠ 0
har : ‖a • x‖ < ↑r
hainv : ‖a‖⁻¹ ≤ (↑r)⁻¹ * ‖c‖ * ‖x‖
⊢ ↑‖a‖₊⁻¹ ≤ ↑(‖c‖₊ * ‖x‖₊ / r)

Tactic:
by rwa [ENNReal.coe_le_coe, div_eq_inv_mul, ← mul_assoc]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Congr

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s t : Set E
inst✝ : T1Space E
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x

Tactic:
by
  rcases eq_or_ne x y with rfl | hne
  · exact hasFDerivWithinAt_congr_set_nhdsNE h
  · rw [hne.nhdsWithin_compl_singleton] at h
    exact hasFDerivWithinAt_congr_set h

Goal state after:
Module: Mathlib.Analysis.Calculus.TangentCone.Real

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul ℝ E
s : Set E
x : E
inst✝ : IsTopologicalAddGroup E
conv : Convex ℝ s
hs : (interior s).Nonempty
hx : x ∈ closure[inst✝²] s
⊢ Submodule.span ℝ (tangentConeAt ℝ s x) = ⊤

Tactic:
by
  rcases hs with ⟨y, hy⟩
  suffices y - x ∈ interior (tangentConeAt ℝ s x) by
    apply (Submodule.span ℝ (tangentConeAt ℝ s x)).eq_top_of_nonempty_interior'
    exact ⟨y - x, interior_mono Submodule.subset_span this⟩
  rw [mem_interior_iff_mem_nhds]
  replace hy : interior s ∈ 𝓝 y := IsOpen.mem_nhds isOpen_interior hy
  apply mem_of_superset ((isOpenMap_sub_right x).image_mem_nhds hy)
  rintro _ ⟨z, zs, rfl⟩
  refine mem_tangentConeAt_of_openSegment_subset (Subset.trans ?_ interior_subset)
  exact conv.openSegment_closure_interior_subset_interior hx zs

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: case right
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : E →ₗ[𝕜] F
hg : comap (⇑g) (𝓝 0) ≤ 𝓝 0
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV : V ∈ 𝓝 0
hgV : ⇑g ⁻¹' V ⊆ U
a : α
c : 𝕜
hc₀ : c ≠ 0
hc : (⇑g ∘ f) a ∈ c • V
⊢ f a ∈ c • U

Tactic:
grw [← hgV, ← (IsUnit.mk0 _ hc₀).preimage_smul_set]

Goal state after:
case right
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : E →ₗ[𝕜] F
hg : comap (⇑g) (𝓝 0) ≤ 𝓝 0
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV : V ∈ 𝓝 0
hgV : ⇑g ⁻¹' V ⊆ U
a : α
c : 𝕜
hc₀ : c ≠ 0
hc : (⇑g ∘ f) a ∈ c • V
⊢ f a ∈ ⇑g ⁻¹' (c • V)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst✝³ : (i : ι) → AddCommGroup (E i)
inst✝² : (i : ι) → Module 𝕜 (E i)
inst✝¹ : (i : ι) → TopologicalSpace (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =o[𝕜; l] g
⊢ (fun x i ↦ f i x) =o[𝕜; l] g

Tactic:
have := hasBasis_pi fun i ↦ nhds_basis_balanced 𝕜 (E i)

Goal state after:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst✝³ : (i : ι) → AddCommGroup (E i)
inst✝² : (i : ι) → Module 𝕜 (E i)
inst✝¹ : (i : ι) → TopologicalSpace (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =o[𝕜; l] g
this :
  (Filter.pi fun i ↦ 𝓝 0).HasBasis (fun If ↦ If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 0 ∧ Balanced 𝕜 (If.2 i)) fun If ↦
    If.1.pi fun i ↦ id (If.2 i)
⊢ (fun x i ↦ f i x) =o[𝕜; l] g
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst✝³ : (i : ι) → AddCommGroup (E i)
inst✝² : (i : ι) → Module 𝕜 (E i)
inst✝¹ : (i : ι) → TopologicalSpace (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =O[𝕜; l] g
⊢ (fun x i ↦ f i x) =O[𝕜; l] g

Tactic:
have := hasBasis_pi fun i ↦ nhds_basis_balanced 𝕜 (E i)

Goal state after:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst✝³ : (i : ι) → AddCommGroup (E i)
inst✝² : (i : ι) → Module 𝕜 (E i)
inst✝¹ : (i : ι) → TopologicalSpace (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =O[𝕜; l] g
this :
  (Filter.pi fun i ↦ 𝓝 0).HasBasis (fun If ↦ If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 0 ∧ Balanced 𝕜 (If.2 i)) fun If ↦
    If.1.pi fun i ↦ id (If.2 i)
⊢ (fun x i ↦ f i x) =O[𝕜; l] g
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
s : Set E
n : ℕ
h : f =O[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : 1 < n
⊢ (fun x' ↦ f x' - 0 - 0 (x' - x₀)) =o[𝓝[s] x₀] fun x' ↦ x' - x₀

Tactic:
zero_apply,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
s : Set E
n : ℕ
h : f =O[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : 1 < n
⊢ (fun x' ↦ f x' - 0 - 0) =o[𝓝[s] x₀] fun x' ↦ x' - x₀
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖f'‖ ≤ ↑C

Tactic:
refine hf.le_of_lip' C.coe_nonneg ?_

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ ↑C * ‖x - x₀‖