mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
hRS : uR • S ⊆ S
hR'S : uR' • S ⊆ S
A : AddSubgroup M := AddSubgroup.closure S
r : R
i : M
hi : i ∈ A
⊢ r • 0 ∈ A

Tactic:
simp_rw [smul_zero]

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
hRS : uR • S ⊆ S
hR'S : uR' • S ⊆ S
A : AddSubgroup M := AddSubgroup.closure S
r : R
i : M
hi : i ∈ A
⊢ 0 ∈ A
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
x y : R
⊢ v.intAdicAbvDef hb (x + y) ≤ max (v.intAdicAbvDef hb x) (v.intAdicAbvDef hb y)

Tactic:
simp only [intAdicAbvDef]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
x y : R
⊢ (toNNReal ⋯) (v.intValuation (x + y)) ≤ max ((toNNReal ⋯) (v.intValuation x)) ((toNNReal ⋯) (v.intValuation y))
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
hRS : uR • S ⊆ S
hR'S : uR' • S ⊆ S
A : AddSubgroup M := AddSubgroup.closure S
hRA : ∀ (r : R), ∀ i ∈ A, r • i ∈ A
r' : R'
i : M
hi : i ∈ A
⊢ r' • 0 ∈ A

Tactic:
simp_rw [smul_zero]

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
hRS : uR • S ⊆ S
hR'S : uR' • S ⊆ S
A : AddSubgroup M := AddSubgroup.closure S
hRA : ∀ (r : R), ∀ i ∈ A, r • i ∈ A
r' : R'
i : M
hi : i ∈ A
⊢ 0 ∈ A
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
φ : ι → R⟦X⟧
s : Finset ι
⊢ ∑ i ∈ s, (φ i).order ≤ (∏ i ∈ s, φ i).order

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ih => grw [Finset.sum_cons ha, Finset.prod_cons ha, ih, le_order_mul]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ 1 ≤ φ.order → constantCoeff φ = 0

pp: case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ constantCoeff φ = 0 → 1 ≤ φ.order

Tactic:
· intro h
    rw [← coeff_zero_eq_constantCoeff]
    apply coeff_of_lt_order
    simpa using Order.one_le_iff_pos.mp h

Goal state after:
case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ constantCoeff φ = 0 → 1 ≤ φ.order
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
h : ∀ (d : ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a
⊢ ∃ a, ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)

Tactic:
choose a h using h

Goal state after:
case mpr
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
a : ℕ → R
h : ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) (a d)
⊢ ∃ a, ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
⊢ (φ * ψ).order ≤ φ.order + ψ.order

Tactic:
by_cases! h : φ = 0 ∨ ψ = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ = 0 ∨ ψ = 0
⊢ (φ * ψ).order ≤ φ.order + ψ.order

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ (φ * ψ).order ≤ φ.order + ψ.order
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
⊢ (𝓝 0).HasBasis (fun Id ↦ ↑Id.1 ∈ 𝓝 0) fun Id ↦ ↑(basis σ R Id)

Tactic:
rw [nhds_pi]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
⊢ (Filter.pi fun i ↦ 𝓝 (0 i)).HasBasis (fun Id ↦ ↑Id.1 ∈ 𝓝 0) fun Id ↦ ↑(basis σ R Id)
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : UniformSpace R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : IsUniformAddGroup R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : CompleteSpace S
inst✝² : T2Space S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁹.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑φ
ha : HasEval a
f : MvPowerSeries σ R
⊢ (eval₂Hom hφ ha) f = eval₂ φ a f

Tactic:
simp only [eval₂Hom_eq_extend, eval₂]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : UniformSpace R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : IsUniformAddGroup R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : CompleteSpace S
inst✝² : T2Space S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁹.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑φ
ha : HasEval a
f : MvPowerSeries σ R
⊢ ⋯.extend (MvPolynomial.eval₂ φ a) f =
    if H : ∃ p, ↑p = f then MvPolynomial.eval₂ φ a H.choose else ⋯.extend (MvPolynomial.eval₂ φ a) f
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
⊢ (substAlgHom ha) f = subst a f

Tactic:
rw [coe_substAlgHom]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q n : ℕ
hq : 1 < q
hn : ¬∃ k, q ^ k = n
⊢ { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) 1) 0, map_zero' := ⋯ } n = 1 n

Tactic:
· simp [hn, one_apply_ne (fun H ↦ hn ⟨0, H.symm⟩)]

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

Goal state before:
pp: case false
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ k < n, f k = g k
fn : f n = false
⊢ ¬cantorFunction c f = cantorFunction c g

Tactic:
apply _root_.ne_of_lt
      refine increasing_cantorFunction h1 h2 hn fn ?_
      apply Bool.eq_true_of_not_eq_false
      rw [← fn]
      apply Ne.symm
      exact Nat.find_spec this

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
⊢ (if hq : 1 < q then
      { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) (f * g)) 0, map_zero' := ⋯ }
    else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff (f * g))) =
    (if hq : 1 < q then { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0, map_zero' := ⋯ }
      else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff f)) *
      if hq : 1 < q then
        { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0, map_zero' := ⋯ }
      else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff g)

Tactic:
ext n
    split_ifs with hq
    · simp_rw [mul_apply, coe_mk]
      by_cases hn : ∃ a, q ^ a = n
      · obtain ⟨k, rfl⟩ := hn
        rw [(Nat.pow_right_injective hq).extend_apply]
        have hs : (Finset.antidiagonal k).map (.prodMap ⟨fun k ↦ q ^ k, Nat.pow_right_injective hq⟩
            ⟨fun k ↦ q ^ k, Nat.pow_right_injective hq⟩) ⊆ (q ^ k).divisorsAntidiagonal :=
          Nat.antidiagonal_map_subset_divisorsAntidiagonal_pow hq k
        rw [PowerSeries.coeff_mul k f g, ← Finset.sum_subset hs]
        · simp [(Nat.pow_right_injective hq).extend_apply]
        · intro (a, b) hab h
          by_cases ha : ∃ i, q ^ i = a
          · by_cases hb : ∃ j, q ^ j = b
            · obtain ⟨i, rfl⟩ := ha
              obtain ⟨j, rfl⟩ := hb
              rw [Nat.mem_divisorsAntidiagonal, ← pow_add, Nat.pow_right_inj hq] at hab
              simp_rw [Finset.mem_map, not_exists, not_and, Finset.mem_antidiagonal] at h
              simpa using h (i, j) hab.1
            · rwa [mul_comm, Function.extend_apply', Pi.zero_apply, zero_mul]
          · rwa [Function.extend_apply', Pi.zero_apply, zero_mul]
      · rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply, Finset.sum_eq_zero]
        intro (a, b) hk
        obtain ⟨hab, -⟩ := Nat.mem_divisorsAntidiagonal.mp hk
        by_cases ha : ∃ i, q ^ i = a
        · by_cases hb : ∃ j, q ^ j = b
          · obtain ⟨i, rfl⟩ := ha
            obtain ⟨j, rfl⟩ := hb
            rw [← pow_add] at hab
            exact (hn ⟨i + j, hab⟩).elim
          · rwa [mul_comm, Function.extend_apply', Pi.zero_apply, zero_mul]
        · rwa [Function.extend_apply', Pi.zero_apply, zero_mul]
    · simp

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg.hb
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
hn : ¬k ∣ i
⊢ ¬k ∣ i

Tactic:
exact hn

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Finsupp.degree d = 1
f : R⟦X⟧
hp : HasSubst p
n✝ : σ →₀ ℕ
⊢ (MvPowerSeries.coeff n✝) (subst (subst p (a • X)) f) =
    (MvPowerSeries.coeff n✝)
      (MvPowerSeries.subst (fun s ↦ MvPowerSeries.subst (Function.const σ a • MvPowerSeries.X) p) f)

Tactic:
rw [subst_smul hp, ← Polynomial.coe_X, subst_coe hp, Polynomial.aeval_X,
    ← MvPowerSeries.rescale_eq_subst, MvPowerSeries.rescale_homogeneous_eq_smul hp_lin,
    subst, pow_one]

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

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x : E
inst✝ : (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
c : 𝕜
hc : x ∈ c • s
hc₀ : c ≠ 0
⊢ r ≤ ‖c‖ₑ

Tactic:
exact h c hc₀ hc

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_9
inst✝ : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, Finsupp.degree d = n
e : σ →₀ ℕ
he : e ∈ Function.support f
⊢ (r ^ ∑ i ∈ e.support, e i) * (coeff e) f = r ^ n * (coeff e) f

Tactic:
← hf e he,

Goal state after:
case pos
σ : Type u_1
R : Type u_9
inst✝ : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, Finsupp.degree d = n
e : σ →₀ ℕ
he : e ∈ Function.support f
⊢ (r ^ ∑ i ∈ e.support, e i) * (coeff e) f = r ^ Finsupp.degree e * (coeff e) f
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a : σ → R
f : MvPowerSeries σ R
n b : σ →₀ ℕ
hb : b ∈ ⋯.toFinset
hbn : b ≠ n
⊢ (coeff b) f * (coeff n) (b.prod fun s e ↦ (a s • X s) ^ e) = 0

Tactic:
← monomial_eq,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a : σ → R
f : MvPowerSeries σ R
n b : σ →₀ ℕ
hb : b ∈ ⋯.toFinset
hbn : b ≠ n
⊢ (coeff b) f * (coeff n) ((monomial b) (b.prod fun s n ↦ a s ^ n)) = 0
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: case inr
𝕜 : 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
hr₀ : 0 < r
hIne : I.Nonempty
⊢ ∃ c₀, (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r

Tactic:
· obtain ⟨i₀, hi₀I, hc_max⟩ : ∃ i₀ ∈ I, IsMaxOn (‖c ·‖ₑ) I i₀ :=
        exists_max_image _ (‖c ·‖ₑ) hI hIne
      by_cases! H : c i₀ ≠ 0 ∨ I = univ
      · exact ⟨c i₀, H, fun i hi ↦ by simpa [enorm] using! hc_max hi, hcr _ hi₀I⟩
      · have hc0 (i : ι) (hi : i ∈ I) : c i = 0 := by simpa [H] using hc_max hi
        have heg0 (i : ι) (hi : i ∈ I) : x i = 0 :=
          zero_smul_set_subset (α := 𝕜) (U i) (hc0 i hi ▸ hc i hi)
        have : (𝓝[≠] (0 : 𝕜)).NeBot := (hI₀.resolve_left H.2).resolve_left (by simpa)
        rcases exists_enorm_lt 𝕜 hr₀.ne' with ⟨c₁, hc₁, hc₁r⟩
        refine ⟨c₁, .inl hc₁, fun i hi ↦ ?_, hc₁r⟩
        simp [hc0 i hi]

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
h : (tangentConeAt 𝕜 s x).Nonempty
⊢ x ∈ closure[inst✝¹] s

Tactic:
by
  rcases h with ⟨y, hy⟩
  rcases exists_fun_of_mem_tangentConeAt hy with ⟨ι, l, hl, -, d, hd, hds, -⟩
  refine mem_closure_of_tendsto ?_ hds
  simpa using tendsto_const_nhds.add hd

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' : F
x : 𝕜
inst✝ : PartialOrder 𝕜
⊢ HasDerivWithinAt f f' (Ioi x) x ↔ HasDerivWithinAt f f' (Ici x) x

Tactic:
rw [← Ici_sdiff_left, hasDerivWithinAt_sdiff_singleton]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x : E
s : Set E
h : ¬AccPt x (𝓟 s)
⊢ (if HasFDerivWithinAt f 0 s x then 0 else if h : DifferentiableWithinAt 𝕜 f s x then Classical.choose h else 0) = 0

Tactic:
if_pos (.of_not_accPt h)

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x : E
s : Set E
h : ¬AccPt x (𝓟 s)
⊢ 0 = 0
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
hf : HasFDerivAtFilter f f' L
hf' : IsInducing ⇑f'
⊢ ((fun p ↦ f p.1 - f p.2) - fun p ↦ f' (p.1 - p.2)) =o[L] fun p ↦ f' (p.1 - p.2)

Tactic:
← isLittleOTVS_iff_isLittleO (𝕜 := 𝕜)

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
hf : HasFDerivAtFilter f f' L
hf' : IsInducing ⇑f'
⊢ ((fun p ↦ f p.1 - f p.2) - fun p ↦ f' (p.1 - p.2)) =o[𝕜; L] fun p ↦ f' (p.1 - p.2)
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: case h.inl
𝕜 : 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
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
hr : r = 0
⊢ ‖p (n + 1)‖ * ↑r ^ n ≤ ‖p 1‖ ∨ ‖p (n + 1)‖ * ↑r ^ n ≤ C / ↑r

Tactic:
hr

Goal state after:
case h.inl
𝕜 : 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
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
hr : r = 0
⊢ ‖p (n + 1)‖ * ↑0 ^ n ≤ ‖p 1‖ ∨ ‖p (n + 1)‖ * ↑0 ^ n ≤ C / ↑0
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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
r : ℝ≥0∞
finite : ∀ (m : ℕ), n ≤ m → p m = 0
pos : 0 < r
sum_eq : ∀ y ∈ Metric.eball 0 r, (∑ i ∈ Finset.range n, (p i) fun x ↦ y) = f (x + y)
y✝ : E
hy : y✝ ∈ Metric.eball 0 r
m : ℕ
hm : m ∉ Finset.range n
⊢ ((p m) fun x ↦ y✝) = 0

Tactic:
rw [Finset.mem_range, not_lt] at hm; rw [finite m hm]; rfl

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
f : F →L[𝕜] G
r : ℝ≥0
hr : ↑r < p.radius
⊢ IsBigOWith ‖f‖ atTop (fun n ↦ ‖f.compFormalMultilinearSeries p n‖) fun n ↦ ‖p n‖

Tactic:
refine IsBigOWith.of_bound (Eventually.of_forall fun n => ?_)

Goal state after:
𝕜 : 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 𝕜 E F
f : F →L[𝕜] G
r : ℝ≥0
hr : ↑r < p.radius
n : ℕ
⊢ ‖‖f.compFormalMultilinearSeries p n‖‖ ≤ ‖f‖ * ‖‖p n‖‖
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
x : E
hg : f =ᶠ[𝓝 x] g
r₁ : ℝ≥0∞
h₁ : HasFPowerSeriesOnBall f p x r₁
⊢ HasFPowerSeriesAt g p x

Tactic:
rcases EMetric.mem_nhds_iff.mp hg with ⟨r₂, h₂pos, h₂⟩

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
x : E
hg : f =ᶠ[𝓝 x] g
r₁ : ℝ≥0∞
h₁ : HasFPowerSeriesOnBall f p x r₁
r₂ : ℝ≥0∞
h₂pos : r₂ > 0
h₂ : Metric.eball x r₂ ⊆ {x | (fun x ↦ f x = g x) x}
⊢ HasFPowerSeriesAt g p x
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)
n : ℕ
⊢ HasSum (fun c ↦ (f ∘ ⇑changeOriginIndexEquiv.symm) ⟨n, c⟩) ((p n) fun x_1 ↦ x + y)

Tactic:
rw [← Pi.add_def, (p n).map_add_univ (fun _ ↦ x) fun _ ↦ y]

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⟩) (∑ s, (p n) (s.piecewise (fun x_1 ↦ x) fun x ↦ y))
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : y ∈ Metric.eball 0 r
h'y : x + y ∈ insert x s
A : Tendsto (fun z ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : ↑r' < r
yr'_2 : ‖y‖ < ↑r'
S : Summable fun n ↦ ‖p n‖ * ↑r' ^ n
⊢ ∃ k, ∑' (n : ℕ), ‖p (n + k)‖ * ↑r' ^ (n + k) < ε / 4

Tactic:
have : Tendsto (fun k ↦ ∑' n, ‖p (n + k)‖ * ↑r' ^ (n + k)) atTop (𝓝 0) := by
      apply _root_.tendsto_sum_nat_add (f := fun n ↦ ‖p n‖ * ↑r' ^ n)

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : y ∈ Metric.eball 0 r
h'y : x + y ∈ insert x s
A : Tendsto (fun z ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : ↑r' < r
yr'_2 : ‖y‖ < ↑r'
S : Summable fun n ↦ ‖p n‖ * ↑r' ^ n
this : Tendsto (fun k ↦ ∑' (n : ℕ), ‖p (n + k)‖ * ↑r' ^ (n + k)) atTop (𝓝 0)
⊢ ∃ k, ∑' (n : ℕ), ‖p (n + k)‖ * ↑r' ^ (n + k) < ε / 4
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 : ℕ
v : Fin n → E
i : Fin (Composition.ones n).length
j : ℕ
hjn : j < (Composition.ones n).blocksFun i
⊢ j < 1 → (v ∘ ⇑((Composition.ones n).embedding i)) ⟨j, hjn⟩ = v (Fin.castLE ⋯ i)

Tactic:
hj1

Goal state after:
𝕜 : 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 : ℕ
v : Fin n → E
i : Fin (Composition.ones n).length
j : ℕ
hjn : j < (Composition.ones n).blocksFun i
hj1 : j < 1
⊢ (v ∘ ⇑((Composition.ones n).embedding i)) ⟨j, hjn⟩ = v (Fin.castLE ⋯ i)