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
r : R
⊢ (valuation K v) ↑r ≤ 1

Tactic:
exact valuation_le_one v r

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

Goal state before:
pp: case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
⊢ ∀ (i : ℕ), ↑i = φ.order → (coeff i) (φ + ψ) ≠ 0

Tactic:
intro i

Goal state after:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
i : ℕ
⊢ ↑i = φ.order → (coeff i) (φ + ψ) ≠ 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case right
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
⊢ ∀ (i : ℕ), ↑i < φ.order → (coeff i) (φ + ψ) = 0

Tactic:
intro i

Goal state after:
case right
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
i : ℕ
⊢ ↑i < φ.order → (coeff i) (φ + ψ) = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg.left
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (i : ℕ), ↑i = ↑n → (coeff i) ((monomial n) a) ≠ 0

Tactic:
intro i

Goal state after:
case neg.left
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
⊢ ↑i = ↑n → (coeff i) ((monomial n) a) ≠ 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg.right
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (i : ℕ), ↑i < ↑n → (coeff i) ((monomial n) a) = 0

Tactic:
intro i

Goal state after:
case neg.right
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
⊢ ↑i < ↑n → (coeff i) ((monomial n) a) = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
x : ℕ × ℕ
hx : x.1 + x.2 = n
⊢ ↑x.2 ≤ ↑n

Tactic:
norm_cast

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
x : ℕ × ℕ
hx : x.1 + x.2 = n
⊢ x.2 ≤ n
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : ¬m < n
⊢ 0 = (coeff m) ↑f

Tactic:
rw [not_lt] at h

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : n ≤ m
⊢ 0 = (coeff m) ↑f
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
a✝ : Nontrivial R
n m : ℕ
hm : n ≤ m
⊢ ↑n < ↑(m + 1)

Tactic:
norm_cast

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
a✝ : Nontrivial R
n m : ℕ
hm : n ≤ m
⊢ n < m + 1
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case succ
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
n✝ : ℕ
hn : f (n✝ + 1) = true
⊢ f_max (n✝ + 1) = true

Tactic:
simp [f_max]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ (algebraMap R S) ((coeff e) f) = ∑ᶠ (d : σ →₀ ℕ), (coeff d) f • (coeff e) (d.prod fun s e ↦ X s ^ e)

Tactic:
finsum_eq_single _ e

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ (algebraMap R S) ((coeff e) f) = (coeff e) f • (coeff e) (e.prod fun s e ↦ X s ^ e)

σ : Type u_1
R : Type u_3
inst✝² : CommRing R
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ ∀ (x : σ →₀ ℕ), x ≠ e → (coeff x) f • (coeff e) (x.prod fun s e ↦ X s ^ e) = 0
Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional

Goal state before:
pp: ⊢ Module.rank ℚ ℂ = 𝔠

Tactic:
by
  refine (Free.rank_eq_mk_of_infinite_lt ℚ ℂ ?_).trans Cardinal.mk_complex
  simpa using aleph0_lt_continuum

Goal state after:
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
ha : HasSubst a
f : MvPowerSeries σ R
⊢ ∀ (i : σ →₀ ℕ), ¬(coeff i) f = 0 → (⨅ i, (a i).order) * f.order ≤ (Finsupp.weight ((weightedOrder fun x ↦ 1) ∘ a)) i

Tactic:
intro i

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
ha : HasSubst a
f : MvPowerSeries σ R
i : σ →₀ ℕ
⊢ ¬(coeff i) f = 0 → (⨅ i, (a i).order) * f.order ≤ (Finsupp.weight ((weightedOrder fun x ↦ 1) ∘ a)) i
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f : PowerSeries R
hq : 1 < q
⊢ ((ofPowerSeries q) f) (q ^ 0) = PowerSeries.constantCoeff f

Tactic:
ofPowerSeries_apply_pow hq,

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f : PowerSeries R
hq : 1 < q
⊢ (PowerSeries.coeff 0) f = PowerSeries.constantCoeff f
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) = ((ofPowerSeries q) (PowerSeries.subst (PowerSeries.X ^ k) f)) (q ^ i)

Tactic:
ofPowerSeries_apply_pow hq,

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) = (PowerSeries.coeff i) (PowerSeries.subst (PowerSeries.X ^ k) f)
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
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
⊢ ∀ (i : Unit →₀ ℕ),
    ¬(MvPowerSeries.coeff i) f = 0 →
      f.order * MvPowerSeries.weightedOrder w a ≤
        (Finsupp.weight (Function.const Unit (MvPowerSeries.weightedOrder w a))) i

Tactic:
intro i

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
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
⊢ ¬(MvPowerSeries.coeff i) f = 0 →
    f.order * MvPowerSeries.weightedOrder w a ≤
      (Finsupp.weight (Function.const Unit (MvPowerSeries.weightedOrder w a))) i
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hu : t ⊆ u
hv : t ⊆ v
⊢ ∀ i ∈ u \ t, i ∈ s

Tactic:
intro i

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hu : t ⊆ u
hv : t ⊆ v
i : ι
⊢ i ∈ u \ t → i ∈ s
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hv : t ⊆ v
hu : ∀ i ∈ u \ t, i ∈ s
⊢ ∀ i ∈ v \ t, i ∈ s

Tactic:
intro i

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hv : t ⊆ v
hu : ∀ i ∈ u \ t, i ∈ s
i : ι
⊢ i ∈ v \ t → i ∈ s
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
c : ι → 𝕜
hc : ∀ i ∈ I, x i ∈ c i • U i
hcr : ∀ i ∈ I, ‖c i‖ₑ < r
c₀ : 𝕜
hc₀ : c₀ ≠ 0 ∨ I = univ
hc₀I : ∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖
hc₀r : ‖c₀‖ₑ < r
⊢ x ∈ I.pi (c₀ • U)

Tactic:
intro i

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
c : ι → 𝕜
hc : ∀ i ∈ I, x i ∈ c i • U i
hcr : ∀ i ∈ I, ‖c i‖ₑ < r
c₀ : 𝕜
hc₀ : c₀ ≠ 0 ∨ I = univ
hc₀I : ∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖
hc₀r : ‖c₀‖ₑ < r
i : ι
⊢ i ∈ I → x i ∈ (c₀ • U) i
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:
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.Asymptotics.TVS

Goal state before:
pp: α : 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
inst✝ : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : (𝓝 0).HasBasis p U
h : ∀ (i : ι), p i → ∃ C, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
⊢ ∀ (i : ι), p i → ∃ j ∈ 𝓝 0, ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id j) (g x)

Tactic:
intro i

Goal state after:
α : 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
inst✝ : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : (𝓝 0).HasBasis p U
h : ∀ (i : ι), p i → ∃ C, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
i : ι
⊢ p i → ∃ j ∈ 𝓝 0, ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id j) (g x)
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f' : F
hf' : f' ≠ 0
⊢ AntilipschitzWith ‖f'‖₊⁻¹ ⇑(toSpanSingleton 𝕜 f')

Tactic:
simp [antilipschitzWith_iff_le_mul_dist, dist_eq_norm, ← sub_smul, norm_smul, field]

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ (fderivWithin 𝕜 f₁ s x) 1 = (fderivWithin 𝕜 f s x) 1

Tactic:
hs.fderivWithin_eq hx

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ (fderivWithin 𝕜 f s x) 1 = (fderivWithin 𝕜 f s x) 1
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
inst✝ : Nontrivial F
p : FormalMultilinearSeries 𝕜 F G
u : E ≃L[𝕜] F
⊢ (p.compContinuousLinearMap ↑u).radius ≤ ‖↑u.symm‖ₑ * p.radius

Tactic:
by
  have := (p.compContinuousLinearMap u.toContinuousLinearMap).div_le_radius_compContinuousLinearMap
    u.symm.toContinuousLinearMap
  simp only [compContinuousLinearMap_comp, ContinuousLinearEquiv.coe_comp_coe_symm,
    compContinuousLinearMap_id] at this
  rwa [ENNReal.div_le_iff' (by simpa [DFunLike.ext_iff] using exists_ne 0) (by simp)] at this

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
i : Fin (n + 1)
f : Ei i →L[𝕜] Ei (i.succAbove j) [×n]→L[𝕜] G
m : (i : Fin n.succ) → Ei i
⊢ ‖(f (m i)) (i.removeNth m)‖ ≤ ‖f‖ * ‖m i‖ * ∏ i_1, ‖m (i.succAbove i_1)‖

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

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) → Ei i.castSucc
x : Ei (last n)
⊢ (f (init (snoc m x))) (snoc m x (last n)) = (f m) x

Tactic:
snoc_last,

Goal state after:
𝕜 : 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) → Ei i.castSucc
x : Ei (last n)
⊢ (f (init (snoc m x))) x = (f m) x
Module: Mathlib.Analysis.Analytic.CPolynomialDef

Goal state before:
pp: case refine_2
𝕜 : 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
x : E
r : ℝ≥0∞
hf : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
y : E
hy : y ∈ Metric.eball 0 r
⊢ HasSum (fun n ↦ (p n) fun x ↦ y) 0

Tactic:
convert! hasSum_zero

Goal state after:
case e'_5
𝕜 : 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
x : E
r : ℝ≥0∞
hf : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
y : E
hy : y ∈ Metric.eball 0 r
x✝ : ℕ
⊢ ((p x✝) fun x ↦ y) = 0
Module: Mathlib.Analysis.Analytic.Basic

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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
hy : x ≠ y
⊢ HasFPowerSeriesWithinAt f p (insert y s) x ↔ HasFPowerSeriesWithinAt f p s x

Tactic:
refine ⟨fun h ↦ h.mono (subset_insert _ _), fun h ↦ ?_⟩
    apply HasFPowerSeriesWithinAt.mono_of_mem_nhdsWithin h
    rw [nhdsWithin_insert_of_ne hy]
    exact self_mem_nhdsWithin

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 : E → F
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
v : Fin 0 → E
v_eq : v = fun i ↦ 0
zero_mem : 0 ∈ Metric.eball 0 r
⊢ ∀ (i : ℕ), i ≠ 0 → ((pf i) fun x ↦ 0) = 0

Tactic:
intro i

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
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
v : Fin 0 → E
v_eq : v = fun i ↦ 0
zero_mem : 0 ∈ Metric.eball 0 r
i : ℕ
⊢ i ≠ 0 → ((pf i) fun x ↦ 0) = 0
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousConstSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
⊢ p.applyComposition c (Function.update v j z) =
    Function.update (p.applyComposition c v) (c.index j)
      ((p (c.blocksFun (c.index j))) (Function.update (v ∘ ⇑(c.embedding (c.index j))) (c.invEmbedding j) z))

Tactic:
by
  ext k
  by_cases h : k = c.index j
  · rw [h]
    let r : Fin (c.blocksFun (c.index j)) → Fin n := c.embedding (c.index j)
    simp only [Function.update_self]
    change p (c.blocksFun (c.index j)) (Function.update v j z ∘ r) = _
    let j' := c.invEmbedding j
    suffices B : Function.update v j z ∘ r = Function.update (v ∘ r) j' z by rw [B]
    suffices C : Function.update v (r j') z ∘ r = Function.update (v ∘ r) j' z by
      convert! C; exact (c.embedding_comp_inv j).symm
    exact Function.update_comp_eq_of_injective _ (c.embedding _).injective _ _
  · simp only [h, Function.update_of_ne, Ne, not_false_iff]
    let r : Fin (c.blocksFun k) → Fin n := c.embedding k
    change p (c.blocksFun k) (Function.update v j z ∘ r) = p (c.blocksFun k) (v ∘ r)
    suffices B : Function.update v j z ∘ r = v ∘ r by rw [B]
    apply Function.update_comp_eq_of_notMem_range
    rwa [c.mem_range_embedding_iff']

Goal state after:
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
⊢ (id 𝕜 F ((p 0) v0)).compAlongComposition p (Composition.single n n_pos) = p n

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

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
⊢ Composition.single n n_pos ∉ Finset.univ → (id 𝕜 F ((p 0) v0)).compAlongComposition p (Composition.single n n_pos) = 0

Tactic:
· show compAlongComposition (id 𝕜 F (p 0 v0)) p (Composition.single n n_pos) = p n
      ext v
      rw [compAlongComposition_apply, id_apply_one' _ _ _ (Composition.single_length n_pos)]
      dsimp [applyComposition]
      refine p.congr rfl fun i him hin => congr_arg v <| ?_
      ext; simp

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 ∈ 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.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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n : ℕ
v : Fin 0 → F
⊢ (p.comp (p.rightInv i x) 0) v = (id 𝕜 F ((p 0) 0) 0) v

Tactic:
simp only [comp_coeff_zero', Matrix.zero_empty, id_apply_zero]

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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n : ℕ
v : Fin 0 → F
⊢ ((p 0) fun _i ↦ 0) = (p 0) ![]
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case i_surj
α : Type u_6
inst✝ : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
⊢ ∀ b ∈ compPartialSumTarget m M N, ∃ a, ∃ (ha : a ∈ compPartialSumSource m M N), compChangeOfVariables m M N a ha = b

Tactic:
intro i

Goal state after:
case i_surj
α : Type u_6
inst✝ : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
i : (n : ℕ) × Composition n
⊢ i ∈ compPartialSumTarget m M N → ∃ a, ∃ (ha : a ∈ compPartialSumSource m M N), compChangeOfVariables m M N a ha = i
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' ↑r
y : E
h'y : x + y ∈ insert x s
hy : y ∈ Metric.eball 0 (min rf' ↑r)
y_mem : y ∈ Metric.eball 0 rf
this : y ∈ Metric.eball 0 δ
⊢ x + y ∈ insert x s ∩ Metric.eball x δ

Tactic:
simpa [-Set.mem_insert_iff, edist_eq_enorm_sub, h'y]

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

Goal state before:
pp: case mp.refine_1.refine_2.refine_3
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
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 : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
e0 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (p.sum (y - x))
e1 : HasSum (fun n ↦ (p n) fun x_1 ↦ y - x) (f y)
⊢ f y = (fun y ↦ p.sum (y - x)) y

Tactic:
exact e1.unique e0

Goal state after: