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
v : HeightOneSpectrum R
r : R
⊢ v.intValuation r < 1 ↔ v.asIdeal ∣ Ideal.span {r}

Tactic:
by_cases hr : r = 0
  · simp [hr]
  · rw [v.intValuation_if_neg hr, ← exp_zero, exp_lt_exp,
      neg_lt_zero, ← Int.ofNat_zero, Int.ofNat_lt, zero_lt_iff]
    have h : (Ideal.span {r} : Ideal R) ≠ 0 := by
      rw [Ne, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]
      exact hr
    exact Associates.count_ne_zero_iff_dvd h v.irreducible

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
⊢ X s ^ n ∣ φ ↔ ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0

Tactic:
classical
  constructor
  · rintro ⟨φ, rfl⟩ m h
    rw [coeff_mul, Finset.sum_eq_zero]
    rintro ⟨i, j⟩ hij
    rw [coeff_X_pow, if_neg, zero_mul]
    contrapose! h
    dsimp at h
    subst i
    rw [mem_antidiagonal] at hij
    rw [← hij, Finsupp.add_apply, Finsupp.single_eq_same]
    exact Nat.le_add_right n _
  · intro h
    refine ⟨fun m => coeff (m + single s n) φ, ?_⟩
    ext m
    by_cases H : m - single s n + single s n = m
    · rw [coeff_mul, Finset.sum_eq_single (single s n, m - single s n)]
      · rw [coeff_X_pow, if_pos rfl, one_mul]
        simpa using! congr_arg (fun m : σ →₀ ℕ => coeff m φ) H.symm
      · rintro ⟨i, j⟩ hij hne
        rw [mem_antidiagonal] at hij
        rw [coeff_X_pow]
        split_ifs with hi
        · exfalso
          apply hne
          rw [← hij, ← hi, Prod.mk_inj]
          refine ⟨rfl, ?_⟩
          ext t
          simp only [add_tsub_cancel_left]
        · exact zero_mul _
      · intro hni
        exfalso
        apply hni
        rwa [mem_antidiagonal, add_comm]
    · rw [h, coeff_mul, Finset.sum_eq_zero]
      · rintro ⟨i, j⟩ hij
        rw [mem_antidiagonal] at hij
        rw [coeff_X_pow]
        split_ifs with hi
        · exfalso
          apply H
          rw [← hij, hi]
          ext
          rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm]
        · exact zero_mul _
      · contrapose! H
        ext t
        by_cases hst : s = t
        · subst t
          simpa using! tsub_add_cancel_of_le H
        · simp [hst]

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

Goal state before:
pp: case h
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : (ofClass extensionValuation).ValueGroup₀
k' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hk' : (restrict₀ (ofClass extensionValuation)) k' = x
⊢ valueGroup₀_hom_extensionValuation (extension k') = x

Tactic:
have := (restrict₀_surjective (.ofClass hv.v) (extension k')).choose_spec

Goal state after:
case h
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : (ofClass extensionValuation).ValueGroup₀
k' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hk' : (restrict₀ (ofClass extensionValuation)) k' = x
this : (restrict₀ (ofClass v)) ⋯.choose = extension k'
⊢ valueGroup₀_hom_extensionValuation (extension k') = x
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ exp (-↑n) ≤ v.intValuation r ↔ exp (-↑n) * (exp 1)⁻¹ < v.intValuation r

Tactic:
mul_inv_lt_iff₀ (by simp)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ exp (-↑n) ≤ v.intValuation r ↔ exp (-↑n) < v.intValuation r * exp 1
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
f g : ι →₀ α
⊢ #(Ico f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 1

Tactic:
card_Ico_eq_card_Icc_sub_one,

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
f g : ι →₀ α
⊢ #(Icc f g) - 1 = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 1
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : (ofClass (valuation K v)).ValueGroup₀
⊢ (map' ↑(valueGroupEquiv K v).symm) ((map' ↑(valueGroupEquiv K v)) x) = x

Tactic:
match x with | 0 => simp | .coe a => simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
hd : ¬(weight w) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = d
⊢ ¬((weight w) x.1 = p ∧ (weight w) x.2 = q)

Tactic:
rintro ⟨hp, hq⟩

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
hd : ¬(weight w) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = d
hp : (weight w) x.1 = p
hq : (weight w) x.2 = q
⊢ False
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
⊢ ((trunc (n + 1)) (C a)).coeff m = (Polynomial.C a).coeff m

Tactic:
by
    rw [coeff_trunc, coeff_C, Polynomial.coeff_C]
    split_ifs with H <;> first | rfl | try simp_all

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

Goal state before:
pp: x y : ℝ
h : x < y
⊢ ℵ₀ < 𝔠

Tactic:
exact Cardinal.aleph0_lt_continuum

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional

Goal state before:
pp: ⊢ Module.rank ℝ ℂ = 2

Tactic:
simp [← finrank_eq_rank, finrank_real_complex]

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun x ↦ a • x) y = c • x
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ↑(‖c‖₊⁻¹ * ‖a‖₊)

Tactic:
← nnnorm_inv,

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun x ↦ a • x) y = c • x
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ↑(‖c⁻¹‖₊ * ‖a‖₊)
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (n : ℕ), ∀ᶠ (i : ι) in cofinite, (f i) n = 1 n
⊢ ∀ (n : ℕ), ∀ᶠ (s : Finset ι) in atTop, (∏ i ∈ s, f i) n = (eulerProduct f) n

Tactic:
by
  let : UniformSpace R := ⊥
  have : IsUniformInducing ((↑) : ArithmeticFunction R → (ℕ → R)) := ⟨rfl⟩
  classical
  suffices Multipliable f from tendsto_iff.mp this.hasProd
  simp_rw [multipliable_iff_cauchySeq_finset, CauchySeq, ← this.cauchy_map_iff,
    Filter.map_map, cauchy_map_iff', Pi.uniformity, DiscreteUniformity.eq_principal_setRelId,
    tendsto_iInf, tendsto_comap_iff, tendsto_principal, Function.comp_apply, prod_atTop_atTop_eq,
    eventually_atTop_prod_self, SetRel.mem_id]
  intro n
  replace hf : ∀ k ∈ Set.Iic n, ∀ᶠ (x : ι) in cofinite, (f x) k = (1 : ArithmeticFunction R) k :=
    fun k hk ↦ hf k
  rw [← eventually_all_finite (Set.finite_Iic n), eventually_iff_exists_mem] at hf
  obtain ⟨s, hs, hs'⟩ := hf
  let t := (mem_cofinite.mp hs).toFinset
  refine ⟨t, fun u v hu hv ↦ ?_⟩
  rw [← Finset.prod_sdiff hu, ← Finset.prod_sdiff hv]
  replace hu : ∀ i ∈ u \ t, i ∈ s := by
    intro i hi
    rw [Finset.mem_sdiff, Set.Finite.mem_toFinset, Set.notMem_compl_iff] at hi
    exact hi.2
  replace hv : ∀ i ∈ v \ t, i ∈ s := by
    intro i hi
    rw [Finset.mem_sdiff, Set.Finite.mem_toFinset, Set.notMem_compl_iff] at hi
    exact hi.2
  suffices ∀ k ≤ n, (∏ x ∈ u \ t, f x) k = (∏ x ∈ v \ t, f x) k by
    rw [mul_apply, mul_apply]
    refine Finset.sum_congr rfl fun k hk ↦ ?_
    rw [this k.1 (Nat.divisor_le (Nat.fst_mem_divisors_of_mem_antidiagonal hk))]
  suffices ∀ w, (∀ i ∈ w, i ∈ s) → ∀ k ≤ n, (∏ x ∈ w, f x) k = (1 : ArithmeticFunction R) k by
    intro k hk
    rw [this (u \ t) hu k hk, this (v \ t) hv k hk]
  intro w hw
  induction w using Finset.induction_on
  case empty => simp
  case insert i w hi hw' =>
    intro k hk
    rw [← one_mul (1 : ArithmeticFunction R), Finset.prod_insert hi, mul_apply, mul_apply]
    refine Finset.sum_congr rfl fun j hj ↦ ?_
    have h1 := hs' i (hw i (Finset.mem_insert_self i w)) j.1
      ((Nat.divisor_le (Nat.fst_mem_divisors_of_mem_antidiagonal hj)).trans hk)
    have h2 := hw' (fun i hi ↦ hw i (Finset.mem_insert_of_mem hi)) j.2
      ((Nat.divisor_le (Nat.snd_mem_divisors_of_mem_antidiagonal hj)).trans hk)
    rw [h1, h2]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
x : E
⊢ egauge 𝕜 (ball 0 1) x ≤ ‖c‖ₑ * ‖x‖ₑ

Tactic:
simpa using egauge_ball_le_of_one_lt_norm hc (.inl one_ne_zero)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : SMul 𝕜 E
inst✝² : TopologicalSpace E
s : Set E
x : E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousConstSMul 𝕜 E
⊢ tangentConeAt 𝕜 (closure[inst✝²] s) x = tangentConeAt 𝕜 s x

Tactic:
refine Subset.antisymm ?_ (tangentConeAt_mono subset_closure)
  simp only [(nhds_basis_opens _).tangentConeAt_eq_biInter_closure]
  refine iInter₂_mono fun U hU ↦ closure_minimal ?_ isClosed_closure
  grw [(isOpenMap_add_left x).preimage_closure_subset_closure_preimage, hU.2.inter_closure,
    set_smul_closure_subset]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Semiring 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
s t : Set E
x : E
h : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure[inst✝] s
st : s ⊆ t
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t x)) ∧ x ∈ closure[inst✝] t

Tactic:
← st

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Semiring 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
s t : Set E
x : E
h : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure[inst✝] s
st : s ⊆ t
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure[inst✝] s
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: case refine_2
𝕜 : 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
inst✝³ : ContinuousAdd E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousSMul 𝕜 F
hf : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto (fun n ↦ ‖c n‖) l atTop
⊢ ∀ᶠ (x' : α) in l, c x' • (c x')⁻¹ • v = v

Tactic:
refine (eventually_ne_of_tendsto_norm_atTop hc (0 : 𝕜)).mono fun y hy => ?_

Goal state after:
case refine_2
𝕜 : 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
inst✝³ : ContinuousAdd E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousSMul 𝕜 F
hf : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto (fun n ↦ ‖c n‖) l atTop
y : α
hy : c y ≠ 0
⊢ c y • (c y)⁻¹ • v = v
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
f : α → E
inst✝ : ContinuousSMul 𝕜 E
hf :
  ∀ i ∈ 𝓝 0, ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (1 x)
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
r : ℝ≥0
hr : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ≥0
hε₀ : 0 < ε
hε : ↑ε * ↑‖c‖₊ / ↑r < 1
x : α
hx : egauge 𝕜 (id U) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x)
⊢ ↑ε * egauge 𝕜 (ball 0 ↑r) 1 ≤ ↑ε * ↑‖c‖₊ / ↑r

Tactic:
rw [mul_div_assoc]

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
f : α → E
inst✝ : ContinuousSMul 𝕜 E
hf :
  ∀ i ∈ 𝓝 0, ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (1 x)
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
r : ℝ≥0
hr : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ≥0
hε₀ : 0 < ε
hε : ↑ε * ↑‖c‖₊ / ↑r < 1
x : α
hx : egauge 𝕜 (id U) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x)
⊢ ↑ε * egauge 𝕜 (ball 0 ↑r) 1 ≤ ↑ε * (↑‖c‖₊ / ↑r)
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)
⊢ HasFDerivAtFilter f f' L ↔ Tendsto (fun p ↦ ‖p.1 - p.2‖⁻¹ * ‖f p.1 - f p.2 - f' (p.1 - p.2)‖) L (𝓝 0)

Tactic:
hasFDerivAtFilter_iff_isLittleO,

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)
⊢ ((fun p ↦ f p.1 - f p.2 - f' (p.1 - p.2)) =o[L] fun p ↦ p.1 - p.2) ↔
    Tendsto (fun p ↦ ‖p.1 - p.2‖⁻¹ * ‖f p.1 - f p.2 - f' (p.1 - p.2)‖) L (𝓝 0)
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✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ : ∀ (ε_1 : ℝ≥0), ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 ↑ε) (f x) ≤ ↑ε_1 * egauge 𝕜 (ball 0 ↑δ) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 ↑ε) (f x) ≤ ↑(δ / ‖c‖₊) * egauge 𝕜 (ball 0 ↑δ) (g x)
this : ↑‖f x‖₊ / ↑ε ≤ ↑‖g x‖₊
⊢ ‖f x‖ ≤ ↑ε * ‖g x‖

Tactic:
← ENNReal.coe_div hε.ne'

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ : ∀ (ε_1 : ℝ≥0), ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 ↑ε) (f x) ≤ ↑ε_1 * egauge 𝕜 (ball 0 ↑δ) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 ↑ε) (f x) ≤ ↑(δ / ‖c‖₊) * egauge 𝕜 (ball 0 ↑δ) (g x)
this : ↑(‖f x‖₊ / ε) ≤ ↑‖g x‖₊
⊢ ‖f x‖ ≤ ↑ε * ‖g x‖
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: case mpr
𝕜 : 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), Summable fun n ↦ ‖p n‖ * ↑r ^ n) → p.radius = ∞

Tactic:
· exact p.radius_eq_top_of_summable_norm

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

Goal state before:
pp: 𝕜 : 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 : ContinuousMultilinearMap 𝕜 (fun x ↦ G) G'
⊢ f.currySum.uncurrySum = f

Tactic:
ext m
        exact congr_arg f (Sum.elim_comp_inl_inr m)

Goal state after:
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
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 : z ∈ Metric.eball 0 (r - ‖y‖ₑ)
⊢ HasSum (fun n ↦ (p.changeOrigin y n) fun x ↦ z) (f (x + y + z))

Tactic:
by
    have : f (x + y + z) =
        FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z := by
      rw [mem_eball_zero_iff, lt_tsub_iff_right, add_comm] at hz
      rw [p.changeOrigin_eval (hz.trans_le hf.r_le), add_assoc, hf.sum]
      · have : insert (x + y) s ⊆ insert (x + y) (insert x s) := by
          apply insert_subset_insert (subset_insert _ _)
        rw [insert_eq_of_mem hy] at this
        apply this
        simpa [add_assoc] using h'z
      exact mem_eball_zero_iff.2 (lt_of_le_of_lt (enorm_add_le _ _) hz)
    rw [this]
    apply (p.changeOrigin y).hasSum
    refine Metric.eball_subset_eball (le_trans ?_ p.changeOrigin_radius) hz
    exact tsub_le_tsub hf.r_le le_rfl

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
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 1 r
⊢ ∀ y ∈ Metric.eball x r, f y = f x

Tactic:
by
  intro y hy
  rw [hf.eq_partialSum' y hy 1 le_rfl, hf.eq_partialSum' x
    (by rw [Metric.mem_eball, edist_self]; exact hf.r_pos) 1 le_rfl]
  simp only [FormalMultilinearSeries.partialSum, Finset.range_one, Finset.sum_singleton]
  congr
  apply funext
  simp only [IsEmpty.forall_iff]

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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p (insert x s) x r
y : E
⊢ x + y ∈ insert x s → y ∈ Metric.eball 0 r → HasSum (fun n ↦ (p n) fun x ↦ y) (f (x + y))

Tactic:
by simpa only [insert_idem] using h.hasSum (y := y)

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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
⊢ x + y ∈ insert x (insert x s) → y ∈ Metric.eball 0 r → HasSum (fun n ↦ (p n) fun x ↦ y) (f (x + y))

Tactic:
by simpa only [insert_idem] using h.hasSum (y := y)

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

Goal state before:
pp: case pos
𝕜 : 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
k : Fin c.length
h : k = c.index j
⊢ p.applyComposition c (Function.update v j z) k =
    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)) k

Tactic:
rw [h]

Goal state after:
case pos
𝕜 : 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
k : Fin c.length
h : k = c.index j
⊢ p.applyComposition c (Function.update v j z) (c.index j) =
    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))
      (c.index j)
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
n : ℕ
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
f : F [×c.length]→L[𝕜] G
v : Fin n → E
⊢ ‖f‖ * ∏ i, ‖p.applyComposition c v i‖ ≤ ‖f‖ * ∏ i, ‖p (c.blocksFun i)‖ * ∏ j, ‖(v ∘ ⇑(c.embedding i)) j‖

Tactic:
gcongr with i

Goal state after:
case h1
𝕜 : 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
n : ℕ
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
f : F [×c.length]→L[𝕜] G
v : Fin n → E
i : Fin c.length
a✝ : i ∈ Finset.univ
⊢ ‖p.applyComposition c v i‖ ≤ ‖p (c.blocksFun i)‖ * ∏ j, ‖(v ∘ ⇑(c.embedding i)) j‖