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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x : R⟦X⟧
n : ℕ
⊢ (coeff n) ({ toFun := fun f ↦ mk fun n ↦ 0 ^ n * (coeff n) f, map_one' := ⋯, map_mul' := ⋯ } x) =
    if n = 0 then constantCoeff x else 0

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
x : R⟦X⟧
n : ℕ
h : n = 0
⊢ (coeff n) ({ toFun := fun f ↦ mk fun n ↦ 0 ^ n * (coeff n) f, map_one' := ⋯, map_mul' := ⋯ } x) = constantCoeff x

case neg
R : Type u_1
inst✝ : CommSemiring R
x : R⟦X⟧
n : ℕ
h : ¬n = 0
⊢ (coeff n) ({ toFun := fun f ↦ mk fun n ↦ 0 ^ n * (coeff n) f, map_one' := ⋯, map_mul' := ⋯ } x) = 0
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
x : K
h : ∀ (v : HeightOneSpectrum R), (valuation K v) x ≤ 1
⊢ x ∈ (algebraMap R K).range

Tactic:
obtain ⟨⟨n, d, hd⟩, hx⟩ := IsLocalization.surj (nonZeroDivisors R) x

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
x : K
h : ∀ (v : HeightOneSpectrum R), (valuation K v) x ≤ 1
n d : R
hd : d ∈ nonZeroDivisors R
hx : x * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
⊢ x ∈ (algebraMap R K).range
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case neg
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
⊢ ¬IsField A⟦X⟧

Tactic:
nontriviality A
    rw [Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top]
    use Ideal.span {X}
    constructor
    · rw [bot_lt_iff_ne_bot, Ne, Ideal.span_singleton_eq_bot]
      exact X_ne_zero
    · rw [lt_top_iff_ne_top, Ne, Ideal.eq_top_iff_one, Ideal.mem_span_singleton,
        X_dvd_iff, constantCoeff_one]
      exact one_ne_zero

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

Goal state before:
pp: A : Type u_2
inst✝ : CommRing A
a : A
n✝ : ℕ
⊢ (a ^ n✝ * if n✝ = 1 then 1 else 0) = a * if n✝ = 1 then 1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
A : Type u_2
inst✝ : CommRing A
a : A
n✝ : ℕ
h : n✝ = 1
⊢ a ^ n✝ * 1 = a * 1

case neg
A : Type u_2
inst✝ : CommRing A
a : A
n✝ : ℕ
h : ¬n✝ = 1
⊢ a ^ n✝ * 0 = a * 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ weightedOrder w ((monomial d) a) = if a = 0 then ⊤ else ↑((weight w) d)

Tactic:
split_ifs with h

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ weightedOrder w ((monomial d) a) = ⊤

case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ weightedOrder w ((monomial d) a) = ↑((weight w) d)
Module: Mathlib.Data.Finset.Finsupp

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : f i ∈ t i
hi : i ∈ f.support
H : t i = 0
⊢ f i = 0

Tactic:
H,

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : f i ∈ 0
hi : i ∈ f.support
H : t i = 0
⊢ f i = 0
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R✝ : Type u_2
S : Type u_3
inst✝¹ : CommSemiring R✝
s✝ : Finset (σ →₀ ℕ)
R : Type u_4
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
x✝¹ : R
x✝ : MvPowerSeries σ R
m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝ (∑ x ∈ s, (MvPolynomial.monomial x) ((coeff x) (x✝¹ • x✝))) =
    MvPolynomial.coeff m✝ ((RingHom.id R) x✝¹ • ∑ x ∈ s, (MvPolynomial.monomial x) ((coeff x) x✝))

Tactic:
simp [MvPolynomial.coeff, single, MvPolynomial.monomial]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv : v.intValuation b ≤ v.intValuation a
γ : Multiplicative ℤ
⊢ ∃ y, v.intValuation (b - y * a) < ↑γ

Tactic:
by_cases ha: a = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv : v.intValuation b ≤ v.intValuation a
γ : Multiplicative ℤ
ha : a = 0
⊢ ∃ y, v.intValuation (b - y * a) < ↑γ

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv : v.intValuation b ≤ v.intValuation a
γ : Multiplicative ℤ
ha : ¬a = 0
⊢ ∃ y, v.intValuation (b - y * a) < ↑γ
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), degree d < n → (coeff d) f = 0
⊢ ↑n ≤ f.order

Tactic:
by
  simp_rw [degree_eq_weight_one] at h
  exact nat_le_weightedOrder _ h

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
p : ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ (if (weight w) d = p then f d + g d else 0) =
    (if (weight w) d = p then f d else 0) + if (weight w) d = p then g d else 0

Tactic:
split_ifs with h

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
p : ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (weight w) d = p
⊢ f d + g d = f d + g d

case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
p : ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ¬(weight w) d = p
⊢ 0 = 0 + 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
⊢ f = (weightedHomogeneousComponent w p) f → IsWeightedHomogeneous w f p

Tactic:
· intro hf
    rw [hf]
    exact isWeightedHomogeneous_weightedHomogeneousComponent w f p

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
⊢ f ∈ closure[instTopologicalSpace R] (Set.range MvPolynomial.toMvPowerSeries)

Tactic:
by
  classical
  exact mem_closure_of_tendsto (tendsto_trunc'_atTop f) <| .of_forall fun _ ↦ Set.mem_range_self _

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

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

Tactic:
rintro ⟨a, h⟩ n

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
a : MvPowerSeries σ R
h : ∀ (d : σ →₀ ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)
n : σ →₀ ℕ
⊢ ∃ a, HasSum (fun i ↦ (coeff n) (f i)) a
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (if h : φ = 0 then ⊤ else ↑(Nat.find ⋯)) < ⊤ ↔ φ ≠ 0

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ = 0
⊢ ⊤ < ⊤ ↔ φ ≠ 0

case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : ¬φ = 0
⊢ ↑(Nat.find ⋯) < ⊤ ↔ φ ≠ 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ ((monomial n) a).order = if a = 0 then ⊤ else ↑n

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ ((monomial n) a).order = ⊤

case neg
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ((monomial n) a).order = ↑n
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
⊢ (if d < n then ((trunc m) f).coeff d else 0) = if d < n then (coeff d) f else 0

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
h : d < n
⊢ ((trunc m) f).coeff d = (coeff d) f

case neg
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
h : ¬d < n
⊢ 0 = 0
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
⊢ (if m < n then (coeff m) (↑((trunc n) f) * g) else 0) = if m < n then (coeff m) (f * g) else 0

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
⊢ (coeff m) (↑((trunc n) f) * g) = (coeff m) (f * g)

case neg
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : ¬m < n
⊢ 0 = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ (if f.order.toNat ≤ n then (coeff (n - f.order.toNat)) f.divXPowOrder else 0) = (coeff n) f

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
h : f.order.toNat ≤ n
⊢ (coeff (n - f.order.toNat)) f.divXPowOrder = (coeff n) f

case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
h : ¬f.order.toNat ≤ n
⊢ 0 = (coeff n) f
Module: Mathlib.RingTheory.PowerSeries.PiTopology

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

Tactic:
rintro ⟨a, h⟩ n

Goal state after:
case mp
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
a : R⟦X⟧
h : ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)
n : ℕ
⊢ ∃ a, HasSum (fun i ↦ (coeff n) (f i)) a
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✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
I : Ideal S
hI : ↑I ∈ 𝓝 0
n : σ → ℕ := fun s ↦ sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
s : σ
has : a s ∈ ↑I
⊢ n s = 0 s

Tactic:
simpa [n, Pi.zero_apply, Nat.sInf_eq_zero, or_iff_left (hn_ne s).ne_empty] using has

Goal state after:
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
⊢ ⋯.extend (MvPolynomial.eval₂ φ a) f =
    if H : ∃ p, ↑p = f then MvPolynomial.eval₂ φ a H.choose else ⋯.extend (MvPolynomial.eval₂ φ a) f

Tactic:
split_ifs with h

Goal state after:
case pos
σ : 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
h : ∃ p, ↑p = f
⊢ ⋯.extend (MvPolynomial.eval₂ φ a) f = MvPolynomial.eval₂ φ a h.choose

case neg
σ : 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
h : ¬∃ p, ↑p = f
⊢ ⋯.extend (MvPolynomial.eval₂ φ a) f = ⋯.extend (MvPolynomial.eval₂ φ a) f
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
n : ℕ
⊢ (if n = 0 then 0 else f n / ↑n ^ s) = f n * ↑n ^ (-s)

Tactic:
split_ifs with h

Goal state after:
case pos
f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
n : ℕ
h : n = 0
⊢ 0 = f n * ↑n ^ (-s)

case neg
f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
n : ℕ
h : ¬n = 0
⊢ f n / ↑n ^ s = f n * ↑n ^ (-s)
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra A R
τ : Type u_3
f : MvPowerSeries τ R
a : A
hf : HasSubst f
⊢ HasSubst (a • f)

Tactic:
simp only [HasSubst, MvPowerSeries.constantCoeff_smul]

Goal state after:
A : Type u_1
inst✝² : CommRing A
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra A R
τ : Type u_3
f : MvPowerSeries τ R
a : A
hf : HasSubst f
⊢ IsNilpotent (a • MvPowerSeries.constantCoeff 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
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
d : τ →₀ ℕ
hd : Finsupp.degree d < k
h1 : Function.HasFiniteSupport fun d_1 ↦ (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
h2 :
  Function.HasFiniteSupport fun d_1 ↦
    (coeff d_1) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
this : Set.Finite.toFinset h2 ⊆ Set.Finite.toFinset h1
n : σ →₀ ℕ
⊢ Finsupp.degree d < Finsupp.degree n → (coeff d) (n.prod fun s e ↦ a s ^ e) = 0

Tactic:
intro hc

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
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
d : τ →₀ ℕ
hd : Finsupp.degree d < k
h1 : Function.HasFiniteSupport fun d_1 ↦ (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
h2 :
  Function.HasFiniteSupport fun d_1 ↦
    (coeff d_1) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
this : Set.Finite.toFinset h2 ⊆ Set.Finite.toFinset h1
n : σ →₀ ℕ
hc : Finsupp.degree d < Finsupp.degree n
⊢ (coeff d) (n.prod fun s e ↦ a s ^ e) = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

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

Tactic:
rw [ofPowerSeries_apply (one_lt_pow' hq hk), Function.extend_apply', Pi.zero_apply]
        simp_rw [← pow_mul, Nat.pow_right_inj hq, eq_comm, ← dvd_def]
        exact hn

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

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
⊢ (coeff n) (subst (X ^ k) f) = if k ∣ n then (algebraMap R S) ((coeff (n / k)) f) else 0

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : k ∣ n
⊢ (coeff n) (subst (X ^ k) f) = (algebraMap R S) ((coeff (n / k)) f)

case neg
R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : ¬k ∣ n
⊢ (coeff n) (subst (X ^ k) f) = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
n : ℕ
hn : ¬∃ i, q ^ i = n
⊢ 0 n = Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) (PowerSeries.subst (PowerSeries.X ^ k) f)) 0 n

pp: case neg.hb
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
n : ℕ
hn : ¬∃ i, q ^ i = n
⊢ ¬∃ a, (q ^ k) ^ a = n

Tactic:
Function.extend_apply'

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
n : ℕ
hn : ¬∃ i, q ^ i = n
⊢ 0 n = 0 n

case neg.hb
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
n : ℕ
hn : ¬∃ i, q ^ i = n
⊢ ¬∃ a, q ^ a = n

case neg.hb
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
n : ℕ
hn : ¬∃ i, q ^ i = n
⊢ ¬∃ a, (q ^ k) ^ a = n
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos.succ.succ
R : Type u_1
inst✝ : CommRing R
f : PowerSeries R
hf : PowerSeries.constantCoeff f = 1
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
n✝¹ n✝ : ℕ
hmn : (p ^ (n✝¹ + 1)).Coprime (p ^ (n✝ + 1))
⊢ ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) (p ^ (n✝¹ + 1) * p ^ (n✝ + 1)) =
    ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) (p ^ (n✝¹ + 1)) *
      ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) (p ^ (n✝ + 1))

Tactic:
simp [hp.ne_one] at hmn

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

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ 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✝
ε : MvPowerSeries τ S →ₐ[R✝] T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a : σ → R
n : σ →₀ ℕ
⊢ ((coeff n) fun n ↦ if n = 0 then n.prod fun s m ↦ a s ^ m else 0) = if n = 0 then 1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ 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✝
ε : MvPowerSeries τ S →ₐ[R✝] T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a : σ → R
n : σ →₀ ℕ
h : n = 0
⊢ ((coeff n) fun n ↦ if n = 0 then n.prod fun s m ↦ a s ^ m else 0) = 1

case neg
σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ 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✝
ε : MvPowerSeries τ S →ₐ[R✝] T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a : σ → R
n : σ →₀ ℕ
h : ¬n = 0
⊢ ((coeff n) fun n ↦ if n = 0 then n.prod fun s m ↦ a s ^ m else 0) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: case pos
σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ 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✝
ε : MvPowerSeries τ S →ₐ[R✝] T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a : σ → R
n : σ →₀ ℕ
h : n = 0
⊢ ((coeff n) fun n ↦ if n = 0 then n.prod fun s m ↦ a s ^ m else 0) = 1

Tactic:
simp [h, coeff_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NNNorm 𝕜
inst✝² : Nonempty 𝕜
E : Type u_2
inst✝¹ : Zero E
inst✝ : SMulZeroClass 𝕜 E
x : E
⊢ egauge 𝕜 0 x = ∞ ↔ x ≠ 0

Tactic:
by
  simp [egauge_eq_top]

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

Goal state before:
pp: σ : Type u_1
R : Type u_9
inst✝ : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ((coeff n) fun n ↦ (n.prod fun s m ↦ 0 ^ m) * (coeff n) x) = if n = 0 then constantCoeff x else 0

Tactic:
split_ifs with h

Goal state after:
case pos
σ : Type u_1
R : Type u_9
inst✝ : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
h : n = 0
⊢ ((coeff n) fun n ↦ (n.prod fun s m ↦ 0 ^ m) * (coeff n) x) = constantCoeff x

case neg
σ : Type u_1
R : Type u_9
inst✝ : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
h : ¬n = 0
⊢ ((coeff n) fun n ↦ (n.prod fun s m ↦ 0 ^ m) * (coeff n) x) = 0
Module: Mathlib.Analysis.Calculus.TangentCone.Real

Goal state before:
pp: a b : ℝ
hab : a < b
⊢ (interior (Icc a b)).Nonempty

Tactic:
simp only [interior_Icc, nonempty_Ioo, hab]

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

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
⊢ x ∈ support (fderiv 𝕜 f) → x ∈ tsupport f

Tactic:
rw [← not_imp_not, notMem_support]
  exact fderiv_of_notMem_tsupport _

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
hf : AnalyticOnNhd 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ x - y ∈ s

Tactic:
convert hx

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
s : Set E
hf : AnalyticOnNhd 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ x - y = 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
s : Set E
hf : AnalyticOn 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ x - y ∈ s

Tactic:
convert hx

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
s : Set E
hf : AnalyticOn 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ x - y = x + -y