mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case inr.succ.inr
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
⊢ constantCoeff φ ^ n' * (coeff 1) φ + constantCoeff φ ^ (n' - 1) * constantCoeff φ ^ 1 * ↑n' * (coeff 1) φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'

Tactic:
← pow_add (a := constantCoeff φ)

Goal state after:
case inr.succ.inr
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
⊢ constantCoeff φ ^ n' * (coeff 1) φ + constantCoeff φ ^ (n' - 1 + 1) * ↑n' * (coeff 1) φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
⊢ ↑(C a) = PowerSeries.C a

Tactic:
by
  have := coe_monomial 0 a
  rwa [PowerSeries.monomial_zero_eq_C_apply] at this

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : weightedOrder w f = ↑n
⊢ ↑(weightedOrder w f).toNat = weightedOrder w f

Tactic:
by simp only [h, toNat_natCast]

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
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
⊢ weightedOrder w (f + g) = weightedOrder w f

Tactic:
← hn,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
⊢ weightedOrder w (f + g) = ↑n
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case left
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
⊢ (coeff d) (f + g) ≠ 0

Tactic:
← hn,

Goal state after:
case left
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
n : ℕ
H : ↑n < weightedOrder w g
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
⊢ (coeff d) (f + g) ≠ 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case right
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ ↑((weight w) b) < weightedOrder w f

Tactic:
← hn,

Goal state after:
case right
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ ↑((weight w) b) < ↑n
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
hd : (weight w) d = p + q
⊢ (coeff d) (f * g) = (coeff d) ((weightedHomogeneousComponent w p) f * (weightedHomogeneousComponent w q) g)

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
hd : ¬(weight w) d = p + q
⊢ 0 = (coeff d) ((weightedHomogeneousComponent w p) f * (weightedHomogeneousComponent w q) g)

Tactic:
· apply Finset.sum_congr rfl
    intro x hx
    rw [Finset.mem_antidiagonal] at hx
    rw [← hx, map_add] at hd
    simp only [coeff_weightedHomogeneousComponent]
    rcases trichotomy_of_add_eq_add hd with h | h | h
    · rw [if_pos h.1, if_pos h.2]
    · rw [if_neg (ne_of_lt h), zero_mul]
      rw [← ENat.natCast_lt_natCast] at h
      rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hf), zero_mul]
    · rw [if_neg (ne_of_lt h), mul_zero]
      rw [← ENat.natCast_lt_natCast] at h
      rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hg), mul_zero]

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
hd : ¬(weight w) d = p + q
⊢ 0 = (coeff d) ((weightedHomogeneousComponent w p) f * (weightedHomogeneousComponent w q) g)
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
n : (WithZero (Multiplicative ℤ))ˣ
x✝ : ∃ a, ¬Valued.v a = 0 ∧ ∃ x, Valued.v a * ↑n = Valued.v x
a : adicCompletion K v
ha0 : ¬Valued.v a = 0
x : adicCompletion K v
hx : Valued.v a * ↑n = Valued.v x
b : K
hb : (valuation K v) b = Valued.v a
y : K
hy : (valuation K v) y = Valued.v x
⊢ (valuation K v) b * ↑n = (valuation K v) y

Tactic:
rw [hb, hy]

Goal state after:
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
n : (WithZero (Multiplicative ℤ))ˣ
x✝ : ∃ a, ¬Valued.v a = 0 ∧ ∃ x, Valued.v a * ↑n = Valued.v x
a : adicCompletion K v
ha0 : ¬Valued.v a = 0
x : adicCompletion K v
hx : Valued.v a * ↑n = Valued.v x
b : K
hb : (valuation K v) b = Valued.v a
y : K
hy : (valuation K v) y = Valued.v x
⊢ Valued.v a * ↑n = Valued.v x
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
g : MvPowerSeries σ R
⊢ HasSum f g ↔ ∀ (d : σ →₀ ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) g)

Tactic:
simp_rw [HasSum, ← map_sum]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
g : MvPowerSeries σ R
⊢ Tendsto (fun s ↦ ∑ b ∈ s, f b) (SummationFilter.unconditional ι).filter (𝓝 g) ↔
    ∀ (d : σ →₀ ℕ),
      Tendsto (fun s ↦ (coeff d) (∑ b ∈ s, f b)) (SummationFilter.unconditional ι).filter (𝓝 ((coeff d) g))
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ∞
h : ∀ (i : ℕ), ↑i < n → (coeff i) φ = 0
⊢ n ≤ φ.order

Tactic:
by
  cases n with
  | top => simpa using ext (by simpa using h)
  | coe n =>
    convert! nat_le_order φ n _
    simpa using h

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ∞
⊢ φ.order = n ↔ (∀ (i : ℕ), ↑i = n → (coeff i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < n → (coeff i) φ = 0

Tactic:
by
  cases n with
  | top => simp
  | coe n => simp [order_eq_nat]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : φ.order ≤ ↑i
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) ψ = 0

Tactic:
by_cases! hj : ↑j < order ψ

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : φ.order ≤ ↑i
hj : ↑j < ψ.order
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) ψ = 0

case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : φ.order ≤ ↑i
hj : ψ.order ≤ ↑j
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) ψ = 0
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
h_mono : Monotone ⇑(toNNReal ⋯)
⊢ (toNNReal ⋯) (v.intValuation (x + y)) ≤ max ((toNNReal ⋯) (v.intValuation x)) ((toNNReal ⋯) (v.intValuation y))

Tactic:
← h_mono.map_max

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
x y : R
h_mono : Monotone ⇑(toNNReal ⋯)
⊢ (toNNReal ⋯) (v.intValuation (x + y)) ≤ (toNNReal ⋯) (max (v.intValuation x) (v.intValuation y))
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
b : ℝ≥0
hb : 1 < b
x y : K
h_mono : Monotone ⇑(toNNReal ⋯)
⊢ (toNNReal ⋯) ((valuation K v) (x + y)) ≤ max ((toNNReal ⋯) ((valuation K v) x)) ((toNNReal ⋯) ((valuation K v) y))

Tactic:
← h_mono.map_max

Goal state after:
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
b : ℝ≥0
hb : 1 < b
x y : K
h_mono : Monotone ⇑(toNNReal ⋯)
⊢ (toNNReal ⋯) ((valuation K v) (x + y)) ≤ (toNNReal ⋯) (max ((valuation K v) x) ((valuation K v) y))
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
f : R⟦X⟧
⊢ f = (X ^ n * mk fun i ↦ (coeff (i + n)) f) + ↑((trunc n) f)

Tactic:
← (commute_X_pow _ n).eq,

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
f : R⟦X⟧
⊢ f = (mk fun i ↦ (coeff (i + n)) f) * X ^ n + ↑((trunc n) f)
Module: Mathlib.RingTheory.PowerSeries.Trunc

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

Tactic:
rw [← Polynomial.coe_inj]
  ext m
  rw [coeff_coe, coeff_trunc]
  split
  case isTrue h => rfl
  case isFalse h =>
    rw [not_lt] at h
    rw [coeff_coe]; symm
    exact coeff_eq_zero_of_natDegree_lt <| lt_of_lt_of_le hn h

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

Goal state before:
pp: case inr.coe
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
⊢ ↑n = emultiplicity X φ

Tactic:
← hn,

Goal state after:
case inr.coe
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
⊢ ↑φ.order.toNat = emultiplicity X φ
Module: Mathlib.RingTheory.PowerSeries.PiTopology

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

Tactic:
simp_rw [HasSum, ← map_sum]

Goal state after:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
g : R⟦X⟧
⊢ Tendsto (fun s ↦ ∑ b ∈ s, f b) (SummationFilter.unconditional ι).filter (𝓝 g) ↔
    ∀ (d : ℕ), Tendsto (fun s ↦ (coeff d) (∑ b ∈ s, f b)) (SummationFilter.unconditional ι).filter (𝓝 ((coeff d) g))
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : ¬1 = 0
⊢ ↑n < ↑(φ.order.toNat + 1)

Tactic:
← hn,

Goal state after:
case neg
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : ¬1 = 0
⊢ ↑φ.order.toNat < ↑(φ.order.toNat + 1)
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), (coeff n) p ∈ T
d : ℕ
hd : ↑d < (p.toSubring T hp).order
⊢ (coeff d) p = 0

Tactic:
simp [coeff_of_lt_order d hd, ← coeff_toSubring p T hp]

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

Goal state before:
pp: c : ℝ
f : ℕ → Bool
⊢ (fun n ↦ cantorFunctionAux c f (n + 1)) = fun n ↦ c * cantorFunctionAux c (fun n ↦ f (n + 1)) n

Tactic:
by
  ext n
  cases h : f (n + 1) <;> simp [h, _root_.pow_succ']

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

Goal state before:
pp: a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑Set.univ < 𝔠

Tactic:
rw [← hu]

Goal state after:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑(Iio a ∪ {a} ∪ Ioi a) < 𝔠
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
T : Type u_6
inst✝¹³ : CommRing T
inst✝¹² : UniformSpace T
inst✝¹¹ : T2Space T
inst✝¹⁰ : CompleteSpace T
inst✝⁹ : IsUniformAddGroup T
inst✝⁸ : IsTopologicalRing T
inst✝⁷ : IsLinearTopology T T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
b : τ → T
hb : HasEval b
f : MvPowerSeries σ R
⊢ eval₂ (algebraMap S T) b (subst a f) = eval₂ (algebraMap R T) (fun s ↦ eval₂ (algebraMap S T) b (a s)) f

Tactic:
let ε : MvPowerSeries τ S →ₐ[R] T := (aeval hb).restrictScalars R

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
T : Type u_6
inst✝¹³ : CommRing T
inst✝¹² : UniformSpace T
inst✝¹¹ : T2Space T
inst✝¹⁰ : CompleteSpace T
inst✝⁹ : IsUniformAddGroup T
inst✝⁸ : IsTopologicalRing T
inst✝⁷ : IsLinearTopology T T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
b : τ → T
hb : HasEval b
f : MvPowerSeries σ R
ε : MvPowerSeries τ S →ₐ[R] T := AlgHom.restrictScalars R (aeval hb)
⊢ eval₂ (algebraMap S T) b (subst a f) = eval₂ (algebraMap R T) (fun s ↦ eval₂ (algebraMap S T) b (a s)) 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
ha : HasSubst a
p : Polynomial R
⊢ (substAlgHom ha) ↑p = (Polynomial.aeval a) p

Tactic:
by
  rw [p.toPowerSeries_toMvPowerSeries, substAlgHom, MvPowerSeries.coe_substAlgHom,
    MvPowerSeries.subst_coe, ← AlgHom.comp_apply]
  apply AlgHom.congr_fun
  apply Polynomial.algHom_ext
  simp

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

Goal state before:
pp: case hg
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ Function.HasFiniteSupport fun d ↦ (coeff d) P * if d = 1 then k else 0

Tactic:
· exact .subset (Set.finite_singleton 1) (fun _ ↦ by simp +contextual)

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
this : Invertible ((coeff 1) P.substInv)
Q : R⟦X⟧ := P.substInv.substInv
hQ : HasSubst Q
eq_aux : subst Q P.substInv = X
h : Q = P
⊢ subst Q P.substInv = X

Tactic:
eq_aux

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : DivisionSemiring 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalSpace E
inst✝² : ContinuousSMul 𝕜 E
s : Set E
x : E
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : ContinuousAdd E
h : s ∈ 𝓝 x
⊢ tangentConeAt 𝕜 s x = univ

Tactic:
rw [← s.univ_inter, tangentConeAt_inter_nhds h, tangentConeAt_univ]

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
⊢ DifferentiableWithinAt 𝕜 f univ x ↔ DifferentiableAt 𝕜 f x

Tactic:
simp only [DifferentiableWithinAt, hasFDerivWithinAt_univ, DifferentiableAt]

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
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hst : s ∪ t = univ
hs : IsOpen[inst✝³] s
ht : IsOpen[inst✝³] t
⊢ DifferentiableOn 𝕜 f (s ∪ t)

Tactic:
exact hf.union_of_isOpen hf' hs ht

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
hf : ¬DifferentiableAt 𝕜 f x₀
⊢ ‖fderiv 𝕜 f x₀‖ ≤ C

Tactic:
rw [fderiv_zero_of_not_differentiableAt hf]

Goal state after:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
hf : ¬DifferentiableAt 𝕜 f x₀
⊢ ‖0‖ ≤ C
Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries

Goal state before:
pp: 𝕜 : Type u
E : Type v
F : Type w
G : Type x
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
⊢ p.compContinuousLinearMap 0 = constFormalMultilinearSeries 𝕜 E ((p 0) 0)

Tactic:
ext n v
  cases n with
  | zero =>
    simp only [FormalMultilinearSeries.compContinuousLinearMap_apply, Matrix.zero_empty,
      constFormalMultilinearSeries_apply_zero, ContinuousMultilinearMap.uncurry0_apply]
    congr
    apply Subsingleton.allEq
  | succ =>
    simp [FunLike.coe_zero]

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

Goal state before:
pp: case refine_1
𝕜 : 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
⊢ r ≤ p.radius

Tactic:
rw [p.radius_eq_top_of_forall_image_add_eq_zero 0 (fun n ↦ by rw [add_zero]; exact hp n)]
    exact le_top

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 : E
hy : y ∈ Metric.eball x r
⊢ pf.partialSum 1 (y - x) = pf.partialSum 1 (x - x)

Tactic:
simp only [FormalMultilinearSeries.partialSum, Finset.range_one, Finset.sum_singleton]

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
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 1 r
y : E
hy : y ∈ Metric.eball x r
⊢ ((pf 0) fun x_1 ↦ y - x) = (pf 0) fun x_1 ↦ x - x
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ 2 * (↑r ^ n / ↑r ^ (n + 1)) ≤ ‖c (n + 1)‖ / ‖c n‖

Tactic:
convert! hc

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ ↑r ^ n / ↑r ^ (n + 1) = ↑r⁻¹
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun n ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
⊢ (ofScalars E c).radius = r⁻¹

Tactic:
by
  rcases ENNReal.trichotomy r with (hr | hr | hr)
  · simp_rw [hr, inv_zero] at hc' ⊢
    by_cases h : (∀ᶠ (n : ℕ) in atTop, c n ≠ 0)
    · apply ofScalars_radius_eq_top_of_tendsto E c h ?_
      refine Tendsto.congr' ?_ <| (tendsto_toReal zero_ne_top).comp hc'
      filter_upwards [h]
      simp
    · apply (ofScalars E c).radius_eq_top_of_eventually_eq_zero
      simp only [eventually_atTop, not_exists, not_forall, not_not] at h ⊢
      obtain ⟨ti, hti⟩ := eventually_atTop.mp (hc'.eventually_ne zero_ne_top)
      obtain ⟨zi, hzi, z⟩ := h ti
      refine ⟨zi, Nat.le_induction (ofScalars_eq_zero_of_scalar_zero E z) fun n hmn a ↦ ?_⟩
      nontriviality E
      simp only [ofScalars_eq_zero] at a ⊢
      contrapose! hti
      exact ⟨n, hzi.trans hmn, ENNReal.div_eq_top.mpr (by simp [a, hti])⟩
  · simp_rw [hr, inv_top] at hc' ⊢
    apply ofScalars_radius_eq_zero_of_tendsto E c ((tendsto_add_atTop_iff_nat 1).mp ?_)
    refine tendsto_ofReal_nhds_top.mp (Tendsto.congr' ?_ ((tendsto_add_atTop_iff_nat 1).mpr hc'))
    filter_upwards [hc'.eventually_ne top_ne_zero] with n hn
    apply (ofReal_div_of_pos (Ne.lt_of_le (Ne.symm ?_) (norm_nonneg _))).symm
    simp_all
  · have hr' := toReal_ne_zero.mp hr.ne.symm
    have hr'' := toNNReal_ne_zero.mpr hr' -- this result could go in ENNReal
    convert! ofScalars_radius_eq_inv_of_tendsto E c hr'' ?_
    · simp [ENNReal.coe_inv hr'', ENNReal.coe_toNNReal (toReal_ne_zero.mp hr.ne.symm).2]
    · simp_rw [ENNReal.coe_toNNReal_eq_toReal]
      refine Tendsto.congr' ?_ <| (tendsto_toReal hr'.2).comp hc'
      filter_upwards [hc'.eventually_ne hr'.1, hc'.eventually_ne hr'.2]
      simp

Goal state after: