mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder

Tactic:
by_cases! h : f = 0 ∨ g = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f = 0 ∨ g = 0
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: case neg
σ : 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✝⁶ : IsTopologicalSemiring R
inst✝⁵ : IsUniformAddGroup R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : CompleteSpace S
inst✝² : T2Space S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁹.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑φ
ha : HasEval a
f : MvPowerSeries σ R
h : ¬∃ p, ↑p = f
⊢ ⋯.extend (MvPolynomial.eval₂ φ a) f = ⋯.extend (MvPolynomial.eval₂ φ a) f

Tactic:
rw [← eval₂Hom_eq_extend hφ ha]

Goal state after:
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✝¹³ : IsTopologicalSemiring R
inst✝¹² : IsUniformAddGroup R
inst✝¹¹ : IsUniformAddGroup S
inst✝¹⁰ : CompleteSpace S
inst✝⁹ : T2Space S
inst✝⁸ : IsTopologicalRing S
inst✝⁷ : IsLinearTopology S S
hφ : Continuous[inst✝¹⁶.toTopologicalSpace, inst✝¹⁴.toTopologicalSpace] ⇑φ
ha : HasEval a
T : Type u_4
inst✝⁶ : UniformSpace T
inst✝⁵ : CompleteSpace T
inst✝⁴ : T2Space T
inst✝³ : CommRing T
inst✝² : IsTopologicalRing T
inst✝¹ : IsLinearTopology T T
inst✝ : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst✝¹⁴.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑ε
⊢ ⇑ε ∘ eval₂ φ a = eval₂ (ε.comp φ) (⇑ε ∘ a)

Tactic:
apply eval₂_unique _ (ha.map hε)
  · exact Continuous.comp hε (continuous_eval₂ hφ ha)
  · intro p
    simp only [Function.comp_apply, eval₂_coe]
    rw [← MvPolynomial.coe_eval₂Hom, ← comp_apply, MvPolynomial.comp_eval₂Hom,
      MvPolynomial.coe_eval₂Hom]
  · simp only [coe_comp, Continuous.comp hε hφ]

Goal state after:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case e'_3
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
this : c / (1 - c) < 1
⊢ cantorFunction c f_max = c / (1 - c)

Tactic:
rw [cantorFunction_succ _ (le_of_lt h1) h3, div_eq_mul_inv, ←
        tsum_geometric_of_lt_one (le_of_lt h1) h3]

Goal state after:
case e'_3
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
this : c / (1 - c) < 1
⊢ ((bif f_max 0 then 1 else 0) + c * cantorFunction c fun n ↦ f_max (n + 1)) = c * ∑' (n : ℕ), c ^ n
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: ⊢ #ℝ = 𝔠

Tactic:
mk_real

Goal state after:
⊢ 𝔠 = 𝔠
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ℵ₀ < #ℝ

Tactic:
mk_real

Goal state after:
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ℵ₀ < 𝔠
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
i j : ℕ
hab : i + j = k ∧ q ^ k ≠ 0
h :
  ∀ (x : ℕ × ℕ),
    ¬(x ∈ Finset.antidiagonal k ∧
        ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) x = (q ^ i, q ^ j))
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (q ^ i, q ^ j).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (q ^ i, q ^ j).2 =
    0

Tactic:
not_and,

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
i j : ℕ
hab : i + j = k ∧ q ^ k ≠ 0
h :
  ∀ x ∈ Finset.antidiagonal k,
    ¬({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) x = (q ^ i, q ^ j)
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (q ^ i, q ^ j).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (q ^ i, q ^ j).2 =
    0
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
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
⊢ ⨅ d, ⨅ (_ : (coeff d) f ≠ 0), (Finsupp.weight (weightedOrder w ∘ a)) d ≤ weightedOrder w (subst a f)

Tactic:
apply MvPowerSeries.le_weightedOrder

Goal state after:
σ : 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
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
⊢ ∀ (d : τ →₀ ℕ),
    ↑((Finsupp.weight w) d) < ⨅ d, ⨅ (_ : (coeff d) f ≠ 0), (Finsupp.weight (weightedOrder w ∘ a)) d →
      (coeff d) (subst a f) = 0
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
f : R⟦X⟧
e : τ →₀ ℕ
⊢ (⇑(Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv ⁻¹'
      Function.support fun d ↦ (coeff d) f • (MvPowerSeries.coeff e) (a ^ d)) =
    Function.support fun d ↦ (MvPowerSeries.coeff d) f • (MvPowerSeries.coeff e) (d.prod fun s e ↦ a ^ e)

Tactic:
← Function.support_comp_eq_preimage

Goal state after:
R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
f : R⟦X⟧
e : τ →₀ ℕ
⊢ Function.support
      ((fun d ↦ (coeff d) f • (MvPowerSeries.coeff e) (a ^ d)) ∘ ⇑(Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv) =
    Function.support fun d ↦ (MvPowerSeries.coeff d) f • (MvPowerSeries.coeff e) (d.prod fun s e ↦ a ^ e)
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
⊢ ((ofPowerSeries (q ^ k)) f) (q ^ i) = (PowerSeries.coeff i) (PowerSeries.subst (PowerSeries.X ^ k) f)

Tactic:
PowerSeries.coeff_subst_X_pow hk

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
⊢ ((ofPowerSeries (q ^ k)) f) (q ^ i) = if k ∣ i then (algebraMap R R) ((PowerSeries.coeff (i / k)) f) else 0
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: case pos.a
σ : 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
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
d : τ →₀ ℕ
hd : Finsupp.degree d < k
h1 : Function.HasFiniteSupport fun d_1 ↦ (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
h2 :
  Function.HasFiniteSupport fun d_1 ↦
    (coeff d_1) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
this : Set.Finite.toFinset h2 ⊆ Set.Finite.toFinset h1
aux : ∀ {n : σ →₀ ℕ}, (coeff d) (n.prod fun s e ↦ a s ^ e) ≠ 0 → Finsupp.degree n ≤ Finsupp.degree d
n : σ →₀ ℕ
hn : n ∈ Set.Finite.toFinset h2
⊢ (coeff n) f = (coeff n) (∑ i ∈ range k, (homogeneousComponent i) f)

Tactic:
simp only [map_sum, coeff_homogeneousComponent, sum_ite_eq, mem_range, left_eq_ite_iff,
        not_lt]

Goal state after:
case pos.a
σ : 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
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
d : τ →₀ ℕ
hd : Finsupp.degree d < k
h1 : Function.HasFiniteSupport fun d_1 ↦ (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
h2 :
  Function.HasFiniteSupport fun d_1 ↦
    (coeff d_1) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
this : Set.Finite.toFinset h2 ⊆ Set.Finite.toFinset h1
aux : ∀ {n : σ →₀ ℕ}, (coeff d) (n.prod fun s e ↦ a s ^ e) ≠ 0 → Finsupp.degree n ≤ Finsupp.degree d
n : σ →₀ ℕ
hn : n ∈ Set.Finite.toFinset h2
⊢ k ≤ Finsupp.degree n → (coeff n) f = 0
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
ha : MvPowerSeries.constantCoeff a = 0
f : R⟦X⟧
hf : constantCoeff f = 0
⊢ MvPowerSeries.constantCoeff (subst a f) = 0

Tactic:
have := MvPowerSeries.constantCoeff_subst_eq_zero
    (hasSubst_iff.mp <| HasSubst.of_constantCoeff_zero ha) (fun _ ↦ ha) hf
  simpa [hasSubst_iff]

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

Goal state before:
pp: case refine_2
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∃ᶠ (n : α) in l, x + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
⊢ ∀ᶠ (n : α) in l ⊓ 𝓟 {y | x + d y ∈ s}, d n ∈ (fun x_1 ↦ x + x_1) ⁻¹' s

Tactic:
simp [eventually_inf_principal]

Goal state after:
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: case inr.inl
𝕜 : 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
hx' : ‖x‖ₑ = 0
⊢ egauge 𝕜 (ball 0 ↑r) x ≤ ‖c‖ₑ * ‖x‖ₑ / ↑r

Tactic:
simp only [hx', mul_zero, ENNReal.zero_div, nonpos_iff_eq_zero, egauge_eq_zero_iff]

Goal state after:
case inr.inl
𝕜 : 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
hx' : ‖x‖ₑ = 0
⊢ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ c • ball 0 ↑r
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =o[𝕜; l] k
⊢ f =o[𝕜; l] k

Tactic:
refine ⟨fun U hU₀ ↦ ?_⟩
  obtain ⟨V, hV₀, hV⟩ := hfg.1 U hU₀
  obtain ⟨W, hW₀, hW⟩ := hgk.1 V hV₀
  refine ⟨W, hW₀, fun ε hε ↦ ?_⟩
  filter_upwards [hV, hW ε hε] with x hx₁ hx₂ using hx₁.trans hx₂

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

Goal state before:
pp: case refine_1
α : 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 : α → F
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : (𝓝 0).HasBasis pE sE
hF : (𝓝 0).HasBasis pF sF
⊢ ∀ ⦃s t : Set E⦄,
    s ⊆ t →
      (∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 s (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)) →
        ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 t (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)

Tactic:
rintro s t hsub ⟨V, hV₀, hV⟩
    exact ⟨V, hV₀, fun ε hε ↦ (hV ε hε).mono fun x ↦ le_trans <| egauge_anti _ hsub _⟩

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

Goal state before:
pp: case empty
𝕜 : 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 : Set E
inst✝ : T1Space E
⊢ HasFDerivWithinAt f f' ∅ x

Tactic:
exact .empty

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

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
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen[inst✝³] u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)
x : E
⊢ x ∈ s → DifferentiableWithinAt 𝕜 f s x

Tactic:
xs

Goal state after:
𝕜 : 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
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen[inst✝³] u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)
x : E
xs : x ∈ s
⊢ DifferentiableWithinAt 𝕜 f s 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
⊢ HasFDerivAt f f' x ↔ (fun h ↦ f (x + h) - f x - f' h) =o[𝓝 0] fun h ↦ h

Tactic:
rw [hasFDerivAt_iff_isLittleO, ← map_add_left_nhds_zero x, isLittleO_map]
  simp [Function.comp_def]

Goal state after:
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : AddCommMonoid F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : ContinuousAdd E
inst✝² : ContinuousAdd F
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ Continuous[inst✝⁵, inst✝⁴] (p.partialSum n)

Tactic:
by
  unfold partialSum
  fun_prop

Goal state after:
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h₀ : r ≠ 0
a : ℝ
ha : a ∈ Ioo (-1) 1
hp : (fun n ↦ ‖p n‖ * ↑r ^ n) =O[atTop] fun x ↦ a ^ x
⊢ ↑r < p.radius

Tactic:
by
  have := ((TFAE_exists_lt_isLittleO_pow (fun n => ‖p n‖ * (r : ℝ) ^ n) 1).out 2 5)
  rcases this.mp ⟨a, ha, hp⟩ with ⟨a, ha, C, hC, hp⟩
  rw [← pos_iff_ne_zero, ← NNReal.coe_pos] at h₀
  lift a to ℝ≥0 using ha.1.le
  have : (r : ℝ) < r / a := by
    simpa only [div_one] using (div_lt_div_iff_of_pos_left h₀ zero_lt_one ha.1).2 ha.2
  norm_cast at this
  rw [← ENNReal.coe_lt_coe] at this
  refine this.trans_le (p.le_radius_of_bound C fun n => ?_)
  rw [NNReal.coe_div, div_pow, ← mul_div_assoc, div_le_iff₀ (pow_pos ha.1 n)]
  exact (le_abs_self _).trans (hp n)

Goal state after:
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
r : ℝ≥0
hr : ↑r < p.radius
C : ℝ
hC_pos : C > 0
hC : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ ‖p.compContinuousLinearMap u n‖ * ↑(r / ‖u‖₊) ^ n ≤ ‖p n‖ * ‖u‖ ^ n * ↑(r / ‖u‖₊) ^ n

Tactic:
gcongr
      exact nnnorm_compContinuousLinearMap_le p u n

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei i.castSucc [×n]→L[𝕜] Ei (last n) →L[𝕜] G
m : (i : Fin n.succ) → Ei i
⊢ ‖(f (init m)) (m (last n))‖ ≤ (‖f‖ * ∏ i, ‖m i.castSucc‖) * ‖m (last n)‖

Tactic:
exact (f (init m)).le_of_opNorm_le (f.le_opNorm _) _

Goal state after:
Module: Mathlib.Analysis.Analytic.ChangeOrigin

Goal state before:
pp: case h'y
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
this : insert (x + y) s ⊆ insert (x + y) (insert x s)
⊢ x + (y + z) ∈ insert x s

Tactic:
rw [insert_eq_of_mem hy] at this

Goal state after:
case h'y
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
this : insert (x + y) s ⊆ insert x s
⊢ x + (y + z) ∈ insert x s
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : NontriviallyNormedField 𝕜
p : ℕ → 𝕜
n : ℕ
⊢ (ofScalars 𝕜 p).coeff n = p n

Tactic:
by
  simp [FormalMultilinearSeries.coeff, FormalMultilinearSeries.ofScalars, List.prod_ofFn]

Goal state after:
Module: Mathlib.Analysis.Analytic.CPolynomialDef

Goal state before:
pp: case ht
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
s : (k : ℕ) × (l : ℕ) × { s // s.card = l }
hs : s ∉ ⇑changeOriginIndexEquiv ⁻¹' Sigma.fst ⁻¹' {m | m < n}
⊢ f s = 0

Tactic:
simp only [preimage_ofPred_eq, changeOriginIndexEquiv_apply_fst, mem_ofPred, not_lt] at hs

Goal state after:
case ht
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
s : (k : ℕ) × (l : ℕ) × { s // s.card = l }
hs : n ≤ s.fst + s.snd.fst
⊢ f s = 0
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
⊢ ∑ c, (id 𝕜 F ((p 0) v0)).compAlongComposition p c = p n

Tactic:
Finset.sum_eq_single (Composition.single n n_pos)

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
⊢ (id 𝕜 F ((p 0) v0)).compAlongComposition p (Composition.single n n_pos) = p n

case inr.h₀
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
⊢ ∀ b ∈ Finset.univ, b ≠ Composition.single n n_pos → (id 𝕜 F ((p 0) v0)).compAlongComposition p b = 0

case inr.h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
⊢ Composition.single n n_pos ∉ Finset.univ → (id 𝕜 F ((p 0) v0)).compAlongComposition p (Composition.single n n_pos) = 0
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : ↑r' < r
hr'0 : 0 < r'
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n
L : E × E → ℝ := fun y ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))
y : E × E
hy' : ‖y - (x, x)‖₊ < r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F := fun n ↦ ((p n) fun x_1 ↦ y.1 - x) - (p n) fun x_1 ↦ y.2 - x
hA : HasSum (fun n ↦ A (n + 2)) (f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2)
⊢ ‖f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2‖ ≤ L y

Tactic:
set B : ℕ → ℝ := fun n => C * (a / r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * ((n + 2) * a ^ n)

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : ↑r' < r
hr'0 : 0 < r'
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n
L : E × E → ℝ := fun y ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))
y : E × E
hy' : ‖y - (x, x)‖₊ < r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F := fun n ↦ ((p n) fun x_1 ↦ y.1 - x) - (p n) fun x_1 ↦ y.2 - x
hA : HasSum (fun n ↦ A (n + 2)) (f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2)
B : ℕ → ℝ := fun n ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * ((↑n + 2) * a ^ n)
⊢ ‖f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2‖ ≤ L y
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case a
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
⊢ min p.radius q.radius ≤ (p.prod q).radius

Tactic:
· refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_
    rw [lt_min_iff] at hr
    have := ((p.isLittleO_one_of_lt_radius hr.1).add
      (q.isLittleO_one_of_lt_radius hr.2)).isBigO
    refine (p.prod q).le_radius_of_isBigO ((isBigO_of_le _ fun n ↦ ?_).trans this)
    rw [norm_mul, norm_norm, ← add_mul, norm_mul]
    refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
    rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]
    refine (max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)).trans ?_
    apply Real.le_norm_self

Goal state after: