mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ egauge 𝕜 (ball 0 ↑r) x ≤ ‖c‖ₑ * ‖x‖ₑ / ↑r

Tactic:
have hx' : ‖x‖ₑ = 0 := by simpa [enorm, ← coe_nnnorm, NNReal.coe_eq_zero] using hx
      simp only [hx', mul_zero, ENNReal.zero_div, nonpos_iff_eq_zero, egauge_eq_zero_iff]
      refine (frequently_iff_neBot.2 (inferInstance : NeBot (𝓝[≠] (0 : 𝕜)))).mono fun c hc ↦ ?_
      simp [mem_smul_set_iff_inv_smul_mem₀ hc, norm_smul, hx, hr]

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

Goal state before:
pp: a b : ℝ
hab : ¬a < b
⊢ UniqueDiffOn ℝ (Ico a b)

Tactic:
simp only [Ico_eq_empty hab, uniqueDiffOn_empty]

Goal state after:
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
L : Filter (E × E)
⊢ Tendsto (fun x ↦ ‖f x.1 - f x.2 - f' (x.1 - x.2)‖ / ‖x.1 - x.2‖) L (𝓝 0) ↔
    Tendsto (fun p ↦ ‖p.1 - p.2‖⁻¹ * ‖f p.1 - f p.2 - f' (p.1 - p.2)‖) L (𝓝 0)

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
L : Filter (E × E)
⊢ ∀ (x : E × E), ‖x.1 - x.2‖ = 0 → ‖f x.1 - f x.2 - f' (x.1 - x.2)‖ = 0

Tactic:
· simp [div_eq_inv_mul]

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
L : Filter (E × E)
⊢ ∀ (x : E × E), ‖x.1 - x.2‖ = 0 → ‖f x.1 - f x.2 - f' (x.1 - x.2)‖ = 0
Module: Mathlib.Analysis.Analytic.ChangeOrigin

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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
x y : E
⊢ ‖((p.changeOriginSeriesTerm k l s hs) fun x_1 ↦ x) fun x ↦ y‖₊ ≤ ‖p (k + l)‖₊ * ‖x‖₊ ^ l * ‖y‖₊ ^ k

Tactic:
rw [← p.nnnorm_changeOriginSeriesTerm k l s hs, ← Fin.prod_const, ← Fin.prod_const]
  apply ContinuousMultilinearMap.le_of_opNNNorm_le
  apply ContinuousMultilinearMap.le_opNNNorm

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

Goal state before:
pp: case inl
𝕜 : 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 →ₗᵢ[𝕜] F
h : Subsingleton E
⊢ p.radius ≤ (p.compContinuousLinearMap u.toContinuousLinearMap).radius

pp: case inr
𝕜 : 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 →ₗᵢ[𝕜] F
h : Nontrivial E
⊢ p.radius ≤ (p.compContinuousLinearMap u.toContinuousLinearMap).radius

Tactic:
· simp [Subsingleton.elim u.toContinuousLinearMap 0]

Goal state after:
case inr
𝕜 : 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 →ₗᵢ[𝕜] F
h : Nontrivial E
⊢ p.radius ≤ (p.compContinuousLinearMap u.toContinuousLinearMap).radius
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ : ℕ → 𝕜
⊢ ∀ ⦃a₂ : ℕ → 𝕜⦄, ofScalars E a₁✝ = ofScalars E a₂ → a₁✝ = a₂

Tactic:
_

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
⊢ ofScalars E a₁✝ = ofScalars E a₂✝ → a₁✝ = a₂✝
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
c : ℕ → 𝕜
r r' : ℝ≥0
hr' : r' ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
⊢ Tendsto (fun n ↦ ‖c (n + 1)‖ / ‖c n‖ * ↑r') atTop (𝓝 ↑(r' * r))

Tactic:
exact mul_comm r' r ▸ hc.mul tendsto_const_nhds

Goal state after:
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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
h' : g =ᶠ[𝓝[s] x] f
h'' : g x = f x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
ε : ℝ≥0∞
εpos : ε > 0
hε : Metric.eball x ε ∩ s ⊆ {y | g y = f y}
r' : ℝ≥0∞ := min r ε
⊢ HasFPowerSeriesWithinOnBall g p s x r'

Tactic:
have := hr.of_le (r' := r') (by simp [r', εpos, hr.r_pos]) (min_le_left _ _)

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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
h' : g =ᶠ[𝓝[s] x] f
h'' : g x = f x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
ε : ℝ≥0∞
εpos : ε > 0
hε : Metric.eball x ε ∩ s ⊆ {y | g y = f y}
r' : ℝ≥0∞ := min r ε
this : HasFPowerSeriesWithinOnBall f p s x r'
⊢ HasFPowerSeriesWithinOnBall g p s x r'
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case 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
x : E
n : ℕ
b : Composition n
⊢ b ∈ Finset.univ → b ≠ Composition.ones n → p.compAlongComposition (id 𝕜 E x) b = 0

Tactic:
_

Goal state after:
case 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
x : E
n : ℕ
b : Composition n
a✝ : b ∈ Finset.univ
⊢ b ≠ Composition.ones n → p.compAlongComposition (id 𝕜 E x) b = 0
Module: Mathlib.Analysis.Analytic.CPolynomial

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em F
y : (i : ι) → Em i
x✝ : y ∈ Metric.eball 0 ∞
m : ℕ
⊢ m ∈ Finset.range (Fintype.card ι + 1) → m ≠ Fintype.card ι → ((f.toFormalMultilinearSeries m) fun x ↦ y) = 0

Tactic:
_

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em F
y : (i : ι) → Em i
x✝ : y ∈ Metric.eball 0 ∞
m : ℕ
a✝ : m ∈ Finset.range (Fintype.card ι + 1)
⊢ m ≠ Fintype.card ι → ((f.toFormalMultilinearSeries m) fun x ↦ y) = 0
Module: Mathlib.Analysis.Analytic.CPolynomial

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
y : G × ((i : ι) → Em i)
⊢ y ∈ Metric.eball 0 ∞ →
    (∑ i ∈ Finset.range (Fintype.card (Option ι) + 1), (f.toFormalMultilinearSeriesOfMultilinear i) fun x ↦ y) =
      (f (0 + y).1) (0 + y).2

Tactic:
_

Goal state after:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
y : G × ((i : ι) → Em i)
a✝ : y ∈ Metric.eball 0 ∞
⊢ (∑ i ∈ Finset.range (Fintype.card (Option ι) + 1), (f.toFormalMultilinearSeriesOfMultilinear i) fun x ↦ y) =
    (f (0 + y).1) (0 + y).2
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 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 : Composition n
⊢ b ∈ Finset.univ → b ≠ Composition.single n n_pos → (id 𝕜 F ((p 0) v0)).compAlongComposition p b = 0

Tactic:
_

Goal state after:
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 : Composition n
a✝ : b ∈ Finset.univ
⊢ b ≠ Composition.single n n_pos → (id 𝕜 F ((p 0) v0)).compAlongComposition p b = 0
Module: Mathlib.Analysis.Analytic.CPolynomial

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
y : G × ((i : ι) → Em i)
a✝ : y ∈ Metric.eball 0 ∞
m : ℕ
⊢ m ∈ Finset.range (Fintype.card (Option ι) + 1) →
    m ≠ Fintype.card (Option ι) → ((f.toFormalMultilinearSeriesOfMultilinear m) fun x ↦ y) = 0

Tactic:
_

Goal state after:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
y : G × ((i : ι) → Em i)
a✝¹ : y ∈ Metric.eball 0 ∞
m : ℕ
a✝ : m ∈ Finset.range (Fintype.card (Option ι) + 1)
⊢ m ≠ Fintype.card (Option ι) → ((f.toFormalMultilinearSeriesOfMultilinear m) fun x ↦ y) = 0
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case refine_2
m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
⊢ compChangeOfVariables m M N ⟨c.length, c.blocksFun⟩ ⋯ = ⟨n, c⟩

Tactic:
· dsimp [compChangeOfVariables]
    rw [Composition.sigma_eq_iff_blocks_eq]
    simp only [Composition.blocksFun]
    conv_rhs => rw [← List.ofFn_get c.blocks]

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

Goal state before:
pp: case hf
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
x : (i : ℕ) × Composition i
⊢ x ∈ compPartialSumTarget 2 (n + 1) n →
    (x ∉ (Ico 2 (n + 1)).sigma fun k ↦ {c | 1 < c.length}.toFinset) →
      0 ≤ ∏ j, r * (a ^ x.snd.blocksFun j * p (x.snd.blocksFun j))

Tactic:
_

Goal state after:
case hf
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
x : (i : ℕ) × Composition i
a✝ : x ∈ compPartialSumTarget 2 (n + 1) n
⊢ (x ∉ (Ico 2 (n + 1)).sigma fun k ↦ {c | 1 < c.length}.toFinset) →
    0 ≤ ∏ j, r * (a ^ x.snd.blocksFun j * p (x.snd.blocksFun j))
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: case hf
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
x : (i : ℕ) × Composition i
a✝ : x ∈ compPartialSumTarget 2 (n + 1) n
⊢ (x ∉ (Ico 2 (n + 1)).sigma fun k ↦ {c | 1 < c.length}.toFinset) →
    0 ≤ ∏ j, r * (a ^ x.snd.blocksFun j * p (x.snd.blocksFun j))

Tactic:
_

Goal state after:
case hf
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
x : (i : ℕ) × Composition i
a✝¹ : x ∈ compPartialSumTarget 2 (n + 1) n
a✝ : x ∉ (Ico 2 (n + 1)).sigma fun k ↦ {c | 1 < c.length}.toFinset
⊢ 0 ≤ ∏ j, r * (a ^ x.snd.blocksFun j * p (x.snd.blocksFun j))
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case h
⊢ Monotone fun p ↦ compPartialSumTarget 0 p.1 p.2

pp: case h'
⊢ ∀ (x : (n : ℕ) × Composition n), ∃ n, x ∈ compPartialSumTarget 0 n.1 n.2

Tactic:
· intro m n hmn a ha
    have : ∀ i, i < m.1 → i < n.1 := fun i hi => lt_of_lt_of_le hi hmn.1
    have : ∀ i, i < m.2 → i < n.2 := fun i hi => lt_of_lt_of_le hi hmn.2
    simp_all

Goal state after:
case h'
⊢ ∀ (x : (n : ℕ) × Composition n), ∃ n, x ∈ compPartialSumTarget 0 n.1 n.2
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: ⊢ Tendsto (fun p ↦ compPartialSumTarget 0 p.1 p.2) atTop atTop

Tactic:
apply Monotone.tendsto_atTop_finset
  · intro m n hmn a ha
    have : ∀ i, i < m.1 → i < n.1 := fun i hi => lt_of_lt_of_le hi hmn.1
    have : ∀ i, i < m.2 → i < n.2 := fun i hi => lt_of_lt_of_le hi hmn.2
    simp_all
  · rintro ⟨n, c⟩
    simp only [mem_compPartialSumTarget_iff]
    obtain ⟨n, hn⟩ : BddAbove ((Finset.univ.image fun i : Fin c.length => c.blocksFun i) : Set ℕ) :=
      Finset.bddAbove _
    refine
      ⟨max n c.length + 1, bot_le, lt_of_le_of_lt (le_max_right n c.length) (lt_add_one _), fun j =>
        lt_of_le_of_lt (le_trans ?_ (le_max_left _ _)) (lt_add_one _)⟩
    apply hn
    simp only [Finset.mem_image_of_mem, Finset.mem_coe, Finset.mem_univ]

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

Goal state before:
pp: case hdb
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ⋯
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := ⋯
n : ℕ
one_le_n : 1 ≤ n
hn : S n ≤ (I + 1) * a
In : 2 ≤ n + 1
rSn : r * S n ≤ 1 / 2
⊢ 1 / 2 ≤ 1 - r * S n

Tactic:
linarith only [rSn]

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

Goal state before:
pp: 𝕜 : 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
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
t : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p t e r
hg : HasFPowerSeriesWithinOnBall g q t e s
⊢ min r s ≤ (p.prod q).radius

Tactic:
rw [p.radius_prod_eq_min]
    exact min_le_min hf.r_le hg.r_le

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

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
this✝ : ∀ᶠ (y : E) in 𝓝 0, f (x + y) - f x ∈ Metric.eball 0 q.radius
y : E
hy : Tendsto (fun a ↦ q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x ↦ 0)) atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun n ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : f (x + y) - f x ∈ Metric.eball 0 q.radius
u : Set G
hu : u ∈ 𝓝 (g (f (x + y)))
u_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
v : Set G
vu : v ⊆ u
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
hv : g (f (x + y)) ∈ v
a₀ b₀ : ℕ
hab : ∀ (a b : ℕ), a₀ ≤ a → b₀ ≤ b → q.partialSum a (p.partialSum b y - (p 0) fun x ↦ 0) ∈ v
a : ℕ
ha : a₀ ≤ a
this : ContinuousAt (q.partialSum a) (f (x + y) - f x)
⊢ Tendsto (fun b ↦ q.partialSum a (p.partialSum b y - (p 0) fun x ↦ 0)) atTop (𝓝 (q.partialSum a (f (x + y) - f x)))

Tactic:
apply this.tendsto.comp

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
this✝ : ∀ᶠ (y : E) in 𝓝 0, f (x + y) - f x ∈ Metric.eball 0 q.radius
y : E
hy : Tendsto (fun a ↦ q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x ↦ 0)) atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun n ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : f (x + y) - f x ∈ Metric.eball 0 q.radius
u : Set G
hu : u ∈ 𝓝 (g (f (x + y)))
u_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
v : Set G
vu : v ⊆ u
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
hv : g (f (x + y)) ∈ v
a₀ b₀ : ℕ
hab : ∀ (a b : ℕ), a₀ ≤ a → b₀ ≤ b → q.partialSum a (p.partialSum b y - (p 0) fun x ↦ 0) ∈ v
a : ℕ
ha : a₀ ≤ a
this : ContinuousAt (q.partialSum a) (f (x + y) - f x)
⊢ Tendsto (fun b ↦ p.partialSum b y - (p 0) fun x ↦ 0) atTop (𝓝 (f (x + y) - f x))
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case zero
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_7
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
⊢ AnalyticWithinAt 𝕜 (f ^ 0) s z

Tactic:
simp only [pow_zero]
    apply analyticWithinAt_const

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

Goal state before:
pp: case insert
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
c : E
s : Set E
a : α
B : Finset α
aB : a ∉ B
hB : (∀ n ∈ B, AnalyticWithinAt 𝕜 (f n) s c) → AnalyticWithinAt 𝕜 (∑ n ∈ B, f n) s c
h : ∀ n ∈ insert a B, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt 𝕜 (f a + ∑ n ∈ B, f n) s c

Tactic:
simp only [Finset.mem_insert] at h

Goal state after:
case insert
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
c : E
s : Set E
a : α
B : Finset α
aB : a ∉ B
hB : (∀ n ∈ B, AnalyticWithinAt 𝕜 (f n) s c) → AnalyticWithinAt 𝕜 (∑ n ∈ B, f n) s c
h : ∀ (n : α), n = a ∨ n ∈ B → AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt 𝕜 (f a + ∑ n ∈ B, f n) s c
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case insert
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_9
inst✝¹ : NormedCommRing A
inst✝ : NormedAlgebra 𝕜 A
f : α → E → A
c : E
s : Set E
a : α
B : Finset α
aB : a ∉ B
hB : (∀ n ∈ B, AnalyticWithinAt 𝕜 (f n) s c) → AnalyticWithinAt 𝕜 (fun z ↦ ∏ n ∈ B, f n z) s c
h : ∀ n ∈ insert a B, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt 𝕜 (fun z ↦ f a z * ∏ n ∈ B, f n z) s c

Tactic:
simp only [Finset.mem_insert] at h

Goal state after:
case insert
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_9
inst✝¹ : NormedCommRing A
inst✝ : NormedAlgebra 𝕜 A
f : α → E → A
c : E
s : Set E
a : α
B : Finset α
aB : a ∉ B
hB : (∀ n ∈ B, AnalyticWithinAt 𝕜 (f n) s c) → AnalyticWithinAt 𝕜 (fun z ↦ ∏ n ∈ B, f n z) s c
h : ∀ (n : α), n = a ∨ n ∈ B → AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt 𝕜 (fun z ↦ f a z * ∏ n ∈ B, f n z) s c
Module: Mathlib.Analysis.Calculus.FDeriv.Add

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
R : Type u_4
inst✝⁴ : Monoid R
inst✝³ : DistribMulAction R F
inst✝² : SMulCommClass 𝕜 R F
inst✝¹ : ContinuousConstSMul R F
c : R
inst✝ : Invertible c
⊢ DifferentiableAt 𝕜 (c • f) x ↔ DifferentiableAt 𝕜 f x

Tactic:
by
  rw [← differentiableWithinAt_univ, differentiableWithinAt_smul_iff, differentiableWithinAt_univ]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Finite ι
⊢ Continuous compContinuousLinearMapCLM

Tactic:
rcases nonempty_fintype ι

Goal state after:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Finite ι
val✝ : Fintype ι
⊢ Continuous compContinuousLinearMapCLM
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case fderivWithin
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
k : ℕ
H : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k)) f p s
m : ℕ
⊢ ↑m < N → ∀ x ∈ s, HasFDerivWithinAt (fun x ↦ p x m) (p x m.succ).curryLeft s x

Tactic:
_

Goal state after:
case fderivWithin
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
k : ℕ
H : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k)) f p s
m : ℕ
a✝ : ↑m < N
⊢ ∀ x ∈ s, HasFDerivWithinAt (fun x ↦ p x m) (p x m.succ).curryLeft s x
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case mpr.cont
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
k : ℕ
H : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k)) f p s
m : ℕ
⊢ ↑m ≤ N → ContinuousOn (fun x ↦ p x m) s

Tactic:
_

Goal state after:
case mpr.cont
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
k : ℕ
H : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k)) f p s
m : ℕ
a✝ : ↑m ≤ N
⊢ ContinuousOn (fun x ↦ p x m) s