mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: case h₁
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G✝ : Type wG
G' : Type wG'
inst✝¹⁴ : Fintype ι
inst✝¹³ : Fintype ι'
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁹ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝⁸ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝⁷ : NormedAddCommGroup G✝
inst✝⁶ : NormedSpace 𝕜 G✝
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : Option ι → G × ((i : ι) → E i)
⊢ ‖B (b none).1‖ ≤ ‖B‖ * ‖b none‖

pp: case h1
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G✝ : Type wG
G' : Type wG'
inst✝¹⁴ : Fintype ι
inst✝¹³ : Fintype ι'
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁹ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝⁸ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝⁷ : NormedAddCommGroup G✝
inst✝⁶ : NormedSpace 𝕜 G✝
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : Option ι → G × ((i : ι) → E i)
i : ι
a✝ : i ∈ univ
⊢ ‖(b (some i)).2 i‖ ≤ ‖b (some i)‖

Tactic:
· apply (B.le_opNorm _).trans
    gcongr
    exact norm_fst_le _

Goal state after:
case h1
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G✝ : Type wG
G' : Type wG'
inst✝¹⁴ : Fintype ι
inst✝¹³ : Fintype ι'
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁹ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝⁸ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝⁷ : NormedAddCommGroup G✝
inst✝⁶ : NormedSpace 𝕜 G✝
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : Option ι → G × ((i : ι) → E i)
i : ι
a✝ : i ∈ univ
⊢ ‖(b (some i)).2 i‖ ≤ ‖b (some i)‖
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
x : E
hf : AnalyticAt 𝕜 f x
y : E
⊢ AnalyticAt 𝕜 (fun z ↦ f (z - y)) (x + y)

Tactic:
by
  obtain ⟨p, hf⟩ := hf
  exact ⟨p, hf.comp_sub _⟩

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
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
y : E
⊢ AnalyticWithinAt 𝕜 (fun z ↦ f (z - y)) (s + {y}) (x + y)

Tactic:
by
  obtain ⟨p, hf⟩ := hf
  exact ⟨p, hf.comp_sub _⟩

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

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
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
finsupp : (Function.support f).Finite
hfkl : ∀ (k l : ℕ), HasSum (fun x ↦ f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 ↦ x) fun x ↦ y)
hfk : ∀ (k : ℕ), HasSum (fun x ↦ f ⟨k, x⟩) ((p.changeOrigin x k) fun x ↦ y)
hf : HasSum f ((p.changeOrigin x).sum y)
⊢ HasSum (f ∘ ⇑changeOriginIndexEquiv.symm) (p.sum (x + y))

Tactic:
refine (p.hasSum_of_finite hn (x + y)).sigma_of_hasSum (fun n ↦ ?_)
    (changeOriginIndexEquiv.symm.summable_iff.2 hf.summable)

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
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
finsupp : (Function.support f).Finite
hfkl : ∀ (k l : ℕ), HasSum (fun x ↦ f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 ↦ x) fun x ↦ y)
hfk : ∀ (k : ℕ), HasSum (fun x ↦ f ⟨k, x⟩) ((p.changeOrigin x k) fun x ↦ y)
hf : HasSum f ((p.changeOrigin x).sum y)
n : ℕ
⊢ HasSum (fun c ↦ (f ∘ ⇑changeOriginIndexEquiv.symm) ⟨n, c⟩) ((p n) fun x_1 ↦ x + y)
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✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 1 → E
this : {Composition.ones 1} = Finset.univ
i : ℕ
hi1 : i < (Composition.ones 1).length
hi2 : i < 1
⊢ p.applyComposition (Composition.ones 1) v ⟨i, hi1⟩ = (p 1) v

Tactic:
simp only [applyComposition_ones]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 1 → E
this : {Composition.ones 1} = Finset.univ
i : ℕ
hi1 : i < (Composition.ones 1).length
hi2 : i < 1
⊢ ((p 1) fun x ↦ v (Fin.castLE ⋯ ⟨i, hi1⟩)) = (p 1) v
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: α : 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)
⊢ ∑ e ∈ compPartialSumSource m M N, f e = ∑ e ∈ compPartialSumTarget m M N, g e

Tactic:
apply Finset.sum_bij (compChangeOfVariables m M N)
  -- We should show that the correspondence we have set up is indeed a bijection
  -- between the index sets of the two sums.
  -- 1 - show that the image belongs to `compPartialSumTarget m N N`
  · rintro ⟨k, blocks_fun⟩ H
    rw [mem_compPartialSumSource_iff] at H
    simp only [mem_compPartialSumTarget_iff, Composition.length, H.left,
      length_ofFn, true_and, compChangeOfVariables]
    intro j
    simp only [Composition.blocksFun, (H.right _).right, List.get_ofFn]
  -- 2 - show that the map is injective
  · rintro ⟨k, blocks_fun⟩ H ⟨k', blocks_fun'⟩ H' heq
    obtain rfl : k = k' := by
      have := (compChangeOfVariables_length m M N H).symm
      rwa [heq, compChangeOfVariables_length] at this
    congr
    funext i
    calc
      blocks_fun i = (compChangeOfVariables m M N _ H).2.blocksFun _ :=
        (compChangeOfVariables_blocksFun m M N H i).symm
      _ = (compChangeOfVariables m M N _ H').2.blocksFun _ := by
        grind
      _ = blocks_fun' i := compChangeOfVariables_blocksFun m M N H' i
  -- 3 - show that the map is surjective
  · intro i hi
    apply compPartialSumTargetSet_image_compPartialSumSource m M N i
    simpa [compPartialSumTarget] using hi
  -- 4 - show that the composition gives the `compAlongComposition` application
  · assumption

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

Goal state before:
pp: case h
m n : ℕ × ℕ
⊢ m ≤ n → (fun p ↦ compPartialSumTarget 0 p.1 p.2) m ⊆ (fun p ↦ compPartialSumTarget 0 p.1 p.2) n

Tactic:
hmn

Goal state after:
case h
m n : ℕ × ℕ
hmn : m ≤ n
⊢ (fun p ↦ compPartialSumTarget 0 p.1 p.2) m ⊆ (fun p ↦ compPartialSumTarget 0 p.1 p.2) n
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case refine_2
𝕜 : 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
s : Set E
x : E
g : E → F
hf : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
⊢ ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x

Tactic:
exact ⟨g, by filter_upwards [self_mem_nhdsWithin] using hf, hg⟩

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
⊢ AnalyticOnNhd 𝕜 (fun z ↦ z⁻¹) {z | z ≠ 0}

Tactic:
by
  intro z m; exact analyticAt_inv m

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

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
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
H : DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x
this : DifferentiableWithinAt 𝕜 (⇑iso.symm ∘ ⇑iso ∘ f) s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
rwa [← Function.comp_assoc iso.symm iso f, iso.symm_comp_self] at this

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

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
iso : E ≃L[𝕜] F
f : G → E
s : Set G
⊢ (∀ x ∈ s, DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x) ↔ ∀ x ∈ s, DifferentiableWithinAt 𝕜 f s x

Tactic:
simp only [iso.comp_differentiableWithinAt_iff]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Alternating.Topology

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : UniformSpace F
inst✝³ : IsUniformAddGroup F
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [inst : AddCommGroup F] [inst_1 : Module 𝕜 F] [inst_2 : UniformSpace F]
    [inst_3 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F],
    T2Space F → CompleteSpace (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
⊢ CompleteSpace (E [⋀^ι]→L[𝕜] F)

Tactic:
rw [(isUniformInducing_postcomp (SeparationQuotient.mkCLM _ _)
      SeparationQuotient.isUniformInducing_mk).completeSpace_congr]
    · exact this inferInstance
    · intro f
      use (SeparationQuotient.outCLM _ _).compContinuousAlternatingMap f
      ext
      simp

Goal state after:
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ ∀ (a b : α), dist (Completion.extension f ↑a) (Completion.extension f ↑b) ≤ ↑K * dist ↑a ↑b

Tactic:
by
      simpa only [extension_coe h.uniformContinuous, Completion.dist_eq] using h.dist_le_mul

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

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
n : ℕ
IH : AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 n f s) s
⊢ AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 (n + 1) f s) s

Tactic:
rw [iteratedFDerivWithin_succ_eq_comp_left]

Goal state after:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
n : ℕ
IH : AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 n f s) s
⊢ AnalyticOn 𝕜
    (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s) s
Module: Mathlib.Analysis.Calculus.Deriv.Pow

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedCommRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
f' : 𝔸
x : 𝕜
s : Set 𝕜
h : HasDerivWithinAt f f' s x
n : ℕ
⊢ HasDerivWithinAt (fun x ↦ f x ^ n) (↑n * f x ^ (n - 1) * f') s x

Tactic:
simpa using h.hasFDerivWithinAt.pow n |>.hasDerivWithinAt

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
hc : HasDerivAt c c' x
hd : HasDerivAt d d' x
⊢ HasDerivAt (fun y ↦ c y ∘SL d y) (c' ∘SL d x + c x ∘SL d') x

Tactic:
by
  rw [← hasDerivWithinAt_univ] at *
  exact hc.clm_comp hd

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

Goal state before:
pp: case succ
𝕜 : 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
y : E
c : ℝ
c_pos : c > 0
t : Set E
t_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
n : ℕ
p : E [×n + 1]→L[𝕜] F
ht : ∀ y ∈ t, ‖p fun x ↦ y‖ ≤ c * ‖‖y‖ ^ (n + 1 + 1)‖
hy : 0 < ‖y‖
ε : ℝ
ε_pos : 0 < ε
h₀ : 0 < c * ‖y‖ ^ (n.succ + 1)
k : 𝕜
k_pos : 0 < ‖k‖
k_norm : ‖k‖ < min (δ * ‖y‖⁻¹) (ε * (c * ‖y‖ ^ (n.succ + 1))⁻¹)
h₁ : ‖k • y‖ < δ
h₂ : ‖p fun x ↦ k • y‖ ≤ ‖k‖ ^ n.succ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1)))
⊢ ‖p fun x ↦ y‖ ≤ 0 + ε

Tactic:
have h₃ : ‖k‖ * (c * ‖y‖ ^ (n.succ + 1)) < ε :=
      inv_mul_cancel_right₀ h₀.ne.symm ε ▸
        mul_lt_mul_of_pos_right (lt_of_lt_of_le k_norm (min_le_right _ _)) h₀

Goal state after:
case succ
𝕜 : 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
y : E
c : ℝ
c_pos : c > 0
t : Set E
t_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
n : ℕ
p : E [×n + 1]→L[𝕜] F
ht : ∀ y ∈ t, ‖p fun x ↦ y‖ ≤ c * ‖‖y‖ ^ (n + 1 + 1)‖
hy : 0 < ‖y‖
ε : ℝ
ε_pos : 0 < ε
h₀ : 0 < c * ‖y‖ ^ (n.succ + 1)
k : 𝕜
k_pos : 0 < ‖k‖
k_norm : ‖k‖ < min (δ * ‖y‖⁻¹) (ε * (c * ‖y‖ ^ (n.succ + 1))⁻¹)
h₁ : ‖k • y‖ < δ
h₂ : ‖p fun x ↦ k • y‖ ≤ ‖k‖ ^ n.succ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1)))
h₃ : ‖k‖ * (c * ‖y‖ ^ (n.succ + 1)) < ε
⊢ ‖p fun x ↦ y‖ ≤ 0 + ε
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
e : Fin n.succ ↪ ι
k : ι
hke : k ∉ range ⇑e
⊢ k ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst

Tactic:
contrapose hke

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
e : Fin n.succ ↪ ι
k : ι
hke : k ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ k ∈ range ⇑e
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
e : Fin n.succ ↪ ι
k : ι
hke : k ∈ range (⇑e ∘ Fin.succ)
⊢ k ∈ range ⇑e

Tactic:
exact Set.range_comp_subset_range _ _ hke

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

Goal state before:
pp: case neg.h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
e : Fin n.succ ↪ ι
k : ι
hke : k ∉ range ⇑e
hkf : k ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ ⟨k, ⋯⟩ ≠ ((Equiv.embeddingFinSucc n ι) e).snd

Tactic:
contrapose hke

Goal state after:
case neg.h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
e : Fin n.succ ↪ ι
k : ι
hkf : k ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hke : ⟨k, ⋯⟩ = ((Equiv.embeddingFinSucc n ι) e).snd
⊢ k ∈ range ⇑e
Module: Mathlib.Analysis.Analytic.Uniqueness

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
inst✝ : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
has_series : HasFPowerSeriesOnBall f q y (r / 2)
M : Metric.eball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ Metric.eball y (r / 2)
A : HasSum (fun n ↦ (q n) fun x ↦ z - y) (f z)
⊢ HasSum (fun n ↦ (q n) fun x ↦ z - y) 0

Tactic:
have : HasFPowerSeriesAt 0 q y := has_series.hasFPowerSeriesAt.congr yu

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
inst✝ : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
has_series : HasFPowerSeriesOnBall f q y (r / 2)
M : Metric.eball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ Metric.eball y (r / 2)
A : HasSum (fun n ↦ (q n) fun x ↦ z - y) (f z)
this : HasFPowerSeriesAt 0 q y
⊢ HasSum (fun n ↦ (q n) fun x ↦ z - y) 0
Module: Mathlib.Analysis.Complex.ReImTopology

Goal state before:
pp: a : ℝ
⊢ closure {z | z.re < a} = {z | z.re ≤ a}

Tactic:
by
  simpa only [closure_Iio] using! closure_preimage_re (Iio a)

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' s' y
hh : HasDerivAt h h' x
hs : ∀ (x : 𝕜), h x ∈ s'
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
rw [hy] at hg

Goal state after:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' s' (h x)
hh : HasDerivAt h h' x
hs : ∀ (x : 𝕜), h x ∈ s'
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' t' y
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s t'
hy : y = h x
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Tactic:
rw [hy] at hg

Goal state after:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' t' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s t'
hy : y = h x
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' y
hh : HasDerivAt h h' x
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
rw [hy] at hg

Goal state after:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' (h x)
hh : HasDerivAt h h' x
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasStrictDerivAt g₁ g₁' y
hh : HasStrictDerivAt h h' x
hy : y = h x
⊢ HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
rw [hy] at hg

Goal state after:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasStrictDerivAt g₁ g₁' (h x)
hh : HasStrictDerivAt h h' x
hy : y = h x
⊢ HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x