mathlib-initiative/mathlib-tactics huggingface dataset:
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 Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₁ : x ∈ M₁
y : K
H₁ : v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
left✝ : y ∈ M₀
y_in₁ : y ∈ M₁
x_in₀ : ↑γ₀ ≤ v.restrict x
⊢ min ↑(γ * (γ₀ * γ₀)) ↑γ₀ ≤ min (↑γ * (v.restrict x * v.restrict x)) (v.restrict x)

Tactic:
Units.val_mul,

Goal state after:
case h
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₁ : x ∈ M₁
y : K
H₁ : v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
left✝ : y ∈ M₀
y_in₁ : y ∈ M₁
x_in₀ : ↑γ₀ ≤ v.restrict x
⊢ min (↑γ * ↑(γ₀ * γ₀)) ↑γ₀ ≤ min (↑γ * (v.restrict x * v.restrict x)) (v.restrict x)
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 Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₁ : x ∈ M₁
y : K
H₁ : v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
left✝ : y ∈ M₀
y_in₁ : y ∈ M₁
x_in₀ : ↑γ₀ ≤ v.restrict x
⊢ min (↑γ * ↑(γ₀ * γ₀)) ↑γ₀ ≤ min (↑γ * (v.restrict x * v.restrict x)) (v.restrict x)

Tactic:
Units.val_mul,

Goal state after:
case h
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₁ : x ∈ M₁
y : K
H₁ : v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
left✝ : y ∈ M₀
y_in₁ : y ∈ M₁
x_in₀ : ↑γ₀ ≤ v.restrict x
⊢ min (↑γ * (↑γ₀ * ↑γ₀)) ↑γ₀ ≤ min (↑γ * (v.restrict x * v.restrict x)) (v.restrict x)
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
⊢ (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀

Tactic:
have l : Function.LeftInverse (fun x : hat K => x * x₀⁻¹) fun x : hat K => x * x₀ := by
        intro x
        simp only [mul_assoc, mul_inv_cancel₀ h, mul_one]

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x ↦ x * x₀⁻¹) fun x ↦ x * x₀
⊢ (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G✝ : Type u_1
inst✝⁷ : CommGroup G✝
inst✝⁶ : LinearOrder G✝
inst✝⁵ : IsOrderedMonoid G✝
inst✝⁴ : MulArchimedean G✝
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x : G
h : IsLeast {y | 0 < y} x
⊢ IsLeast {y | y ∈ ⊤ ∧ 0 < y} x

Tactic:
simpa using h

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case pos
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
H : ∃ x, IsLeast {y | 0 < y} x
⊢ Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G

Tactic:
obtain ⟨x, hx⟩ := H

Goal state after:
case pos
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x : G
hx : IsLeast {y | 0 < y} x
⊢ Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case neg
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
H : ∀ (x : G), ¬IsLeast {y | 0 < y} x
⊢ Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G

Tactic:
· refine Or.inr ⟨?_⟩
    intro x y hxy
    specialize H (y - x)
    obtain ⟨z, hz⟩ : ∃ z : G, 0 < z ∧ z < y - x := by
      contrapose! H
      refine ⟨by simp [hxy], fun _ ↦ H _⟩
    refine ⟨x + z, ?_, ?_⟩
    · simp [hz.left]
    · simpa [lt_sub_iff_add_lt'] using hz.right

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : γ₀ < ↑γ
s : Set (hat K)
hs : s ∈ 𝓝 x
y : K
hy₁ : ↑y ∈ extension ⁻¹' {γ₀'}
hy₂ : ↑y ∈ s
⊢ ∃ y, ↑y ∈ s

Tactic:
replace hy₁ : v y = γ₀ := by
      simp only [mem_preimage, extension_extends, mem_singleton_iff, v.restrict_def] at hy₁
      apply_fun embedding at hy₁
      simpa [heq] using hy₁

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : γ₀ < ↑γ
s : Set (hat K)
hs : s ∈ 𝓝 x
y : K
hy₂ : ↑y ∈ s
hy₁ : v y = γ₀
⊢ ∃ y, ↑y ∈ s
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_3
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
x : G₀
hxg : x ≤ g
hx : ¬x = 0
⊢ 0 < x

Tactic:
simp [zero_lt_iff, hx]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this : ∀ p ∈ antidiagonal m, (coeff p.1) ((monomial n) a) * (coeff p.2) φ ≠ 0 → p.1 = n
⊢ (if n ≤ m then ∑ x ∈ {(n, m - n)}, (coeff x.1) ((monomial n) a) * (coeff x.2) φ
    else ∑ x ∈ ∅, (coeff x.1) ((monomial n) a) * (coeff x.2) φ) =
    if n ≤ m then a * (coeff (m - n)) φ else 0

Tactic:
simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this : ∀ p ∈ antidiagonal m, (coeff p.1) φ * (coeff p.2) ((monomial n) a) ≠ 0 → p.2 = n
⊢ (if n ≤ m then ∑ x ∈ {(m - n, n)}, (coeff x.1) φ * (coeff x.2) ((monomial n) a)
    else ∑ x ∈ ∅, (coeff x.1) φ * (coeff x.2) ((monomial n) a)) =
    if n ≤ m then (coeff (m - n)) φ * a else 0

Tactic:
simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
⊢ φ * (monomial n) a = (monomial n) a * φ ↔ ∀ (m : σ →₀ ℕ), Commute ((coeff m) φ) a

Tactic:
MvPowerSeries.ext_iff

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
⊢ (∀ (n_1 : σ →₀ ℕ), (coeff n_1) (φ * (monomial n) a) = (coeff n_1) ((monomial n) a * φ)) ↔
    ∀ (m : σ →₀ ℕ), Commute ((coeff m) φ) a
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (m : σ →₀ ℕ), Commute ((coeff m) φ) a
m : σ →₀ ℕ
⊢ (coeff m) (φ * (monomial n) a) = (coeff m) ((monomial n) a * φ)

Tactic:
rw [coeff_mul_monomial, coeff_monomial_mul]
    split_ifs <;> [apply h; rfl]

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
⊢ (1 * (coeff (i, j).2) fun m ↦ (coeff (m + single s n)) φ) = 0

Tactic:
exfalso
          apply H
          rw [← hij, hi]
          ext
          rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm]

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
r : R
n : ℕ
⊢ v.intValuation r ≤ exp (-↑n) ↔ r ∈ v.asIdeal ^ n

Tactic:
intValuation_le_pow_iff_dvd,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ v.asIdeal ^ n ∣ Ideal.span {r} ↔ r ∈ v.asIdeal ^ n
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 : ℕ
⊢ v.intValuation r ≤ exp (-↑n) ↔ ↑n ≤ emultiplicity v.asIdeal (Ideal.span {r})

Tactic:
intValuation_le_pow_iff_dvd,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ v.asIdeal ^ n ∣ Ideal.span {r} ↔ ↑n ≤ emultiplicity v.asIdeal (Ideal.span {r})
Module: Mathlib.RingTheory.PowerSeries.Basic

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

Tactic:
by
  ext
  simp [coeff_coe, PowerSeries.coeff_monomial, Polynomial.coeff_monomial, eq_comm]

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

Goal state before:
pp: case inr
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
n d : R
hd : d ∈ nonZeroDivisors R
hx : IsLocalization.mk' K n ⟨d, hd⟩ * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hn0 : n ≠ 0
hd0 : d ≠ 0
ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥
v : Ideal R
hv✝ : Irreducible (Associates.mk v)
hv : Prime v
hv' : Irreducible (Associates.mk v)
h :
  -↑(Multiset.count ⟨Associates.mk v, hv'⟩ (Associates.factors' (Ideal.span {n}))) -
      -↑(Multiset.count ⟨Associates.mk v, hv'⟩ (Associates.factors' (Ideal.span {d}))) ≤
    0
⊢ Multiset.count ⟨Associates.mk v, hv✝⟩ (Associates.factors' (Ideal.span {d})) ≤
    Multiset.count ⟨Associates.mk v, hv✝⟩ (Associates.factors' (Ideal.span {n}))

Tactic:
simpa using h

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 f : MvPowerSeries σ R
⊢ ℕ∞

Tactic:
classical
  exact dite (f = 0) (fun _ => ⊤) fun h =>
    Nat.find ((ne_zero_iff_exists_coeff_ne_zero_and_weight w).mp h)

Goal state after:
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
a s : R
hs : s ∈ v.asIdeal.primeCompl
this : (valuation K v) (↑a / ↑s) ≤ 1
⊢ (algebraMap R K) a * ((algebraMap R K) s)⁻¹ ∈ (valuation K v).valuationSubring

Tactic:
by rwa [division_def (a : K) s] 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
p : ℕ
hf : ↑p = weightedOrder w f
hf' : (weightedHomogeneousComponent w p) f = 0
d : σ →₀ ℕ
hd : ¬(coeff d) f = 0 ∧ (weight w) d = p
⊢ (coeff d) f = 0

Tactic:
MvPowerSeries.ext_iff

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p = weightedOrder w f
hf' : ∀ (n : σ →₀ ℕ), (coeff n) ((weightedHomogeneousComponent w p) f) = (coeff n) 0
d : σ →₀ ℕ
hd : ¬(coeff d) f = 0 ∧ (weight w) d = p
⊢ (coeff d) f = 0
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
r : R
x : ↥(adicCompletionIntegers K v)
⊢ (algebraMap R (adicCompletion K v)) r * ↑x ∈ adicCompletionIntegers K v

Tactic:
refine ValuationSubring.mul_mem _ _ _ ?_ x.2

Goal state after:
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
r : R
x : ↥(adicCompletionIntegers K v)
⊢ (algebraMap R (adicCompletion K v)) r ∈ adicCompletionIntegers K v
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
inst✝ : FaithfulSMul R K
⊢ FaithfulSMul R ↥(adicCompletionIntegers K v)

Tactic:
faithfulSMul_iff_algebraMap_injective

Goal state after:
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
inst✝ : FaithfulSMul R K
⊢ Function.Injective ⇑(algebraMap R ↥(adicCompletionIntegers K v))
Module: Mathlib.RingTheory.PowerSeries.Order

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

Tactic:
simpa using h

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

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

Tactic:
simpa using h

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

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

Tactic:
← eq_shift_mul_X_pow_add_trunc

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
f : R⟦X⟧
⊢ f = f
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⟧
a : ℕ → R
h : ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) (a d)
⊢ ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) (mk a))

Tactic:
simpa using h

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

Goal state before:
pp: 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))
⊢ ↑n < (X ^ (φ.order.toNat + 1)).order

Tactic:
rw [X_pow_eq, order_monomial]
        split_ifs
        · simp
        · rw [← hn, ENat.natCast_lt_natCast]
          simp

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
⊢ Multipliable fun n ↦ 1 - X ^ (n + 1)

Tactic:
by
  nontriviality R
  simp_rw [sub_eq_add_neg]
  apply multipliable_one_add_of_tendsto_order_atTop_nhds_top
  refine ENat.tendsto_nhds_top_iff_natCast_lt.mpr (fun n ↦ Filter.eventually_atTop.mpr ⟨n, ?_⟩)
  intro m hm
  rw [order_neg, order_X_pow]
  norm_cast
  exact Nat.lt_add_one_iff.mpr hm

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ X ^ (f.order.toNat + g.order.toNat) * (f * g).divXPowOrder = X ^ (f.order + g.order).toNat * (f * g).divXPowOrder

Tactic:
ENat.toNat_add (order_eq_top.not.mpr h.1) (order_eq_top.not.mpr h.2)

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ X ^ (f.order.toNat + g.order.toNat) * (f * g).divXPowOrder =
    X ^ (f.order.toNat + g.order.toNat) * (f * g).divXPowOrder
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
ha' : ∀ (i : σ), constantCoeff (a i) = 0
f : MvPowerSeries σ R
hf : constantCoeff f = 0
⊢ constantCoeff (subst a f) = 0

Tactic:
constantCoeff_subst ha,

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
ha : HasSubst a
ha' : ∀ (i : σ), constantCoeff (a i) = 0
f : MvPowerSeries σ R
hf : constantCoeff f = 0
⊢ ∑ᶠ (d : σ →₀ ℕ), (coeff d) f • constantCoeff (d.prod fun s e ↦ a s ^ e) = 0
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case hbc
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
n : ℕ
ih : ∀ {f g : ℕ → Bool}, (∀ k < n, f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ k < n + 1, f k = g k
fn : f (n + 1) = false
gn : g (n + 1) = true
⊢ (cantorFunction c fun n ↦ f (n + 1)) < cantorFunction c fun n ↦ g (n + 1)

Tactic:
exact ih (fun k hk => hn _ <| Nat.succ_lt_succ hk) fn gn

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

Goal state before:
pp: a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x ↦ a + a - x) '' Ioi a = Iio a
⊢ #↑((fun x ↦ a + a - x) '' Ioi a) + #↑{a} < 𝔠

Tactic:
refine add_lt_of_lt (cantor _).le (mk_image_le.trans_lt h) ?_

Goal state after:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x ↦ a + a - x) '' Ioi a = Iio a
⊢ #↑{a} < 𝔠
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case refine_2
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
⊢ ∀ᶠ (i : ℕ) in Filter.atTop, ‖‖↑i ^ (-(s + (1 - ↑x)))‖‖ ≤ ↑i ^ (-s.re + x - 1)

Tactic:
simp only [norm_norm, Filter.eventually_atTop]
      refine ⟨1, fun n hn ↦ le_of_eq ?_⟩
      simp only [norm_natCast_cpow_of_pos hn, add_re, sub_re, neg_re, ofReal_re, one_re]
      ring_nf

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
m : ℝ
h : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ m
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n ≠ 0
⊢ ‖f n‖ ≤ m * ↑n ^ (1 - 1)

Tactic:
simp [h n 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
⊢ subst (subst p (a • X)) f =
    MvPowerSeries.subst (fun s ↦ MvPowerSeries.subst (Function.const σ a • MvPowerSeries.X) p) f

Tactic:
MvPowerSeries.ext_iff

Goal state after:
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)
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
⊢ (∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, ∃ (_ : x ∈ i • s), ‖i‖ₑ < b) ↔ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ c • s

Tactic:
(nhds_basis_uniformity uniformity_basis_edist).frequently_iff

Goal state after:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
⊢ (∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, ∃ (_ : x ∈ i • s), ‖i‖ₑ < b) ↔
    ∀ (i : ℝ≥0∞), 0 < i → ∃ x_1 ∈ {y | (y, 0) ∈ {p | edist p.1 p.2 < i}}, x ∈ x_1 • s
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : 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‖ₑ
hc : x = 0
⊢ x = 0

Tactic:
exact hc

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 : σ →₀ ℕ
s : σ
h : ¬n s = 0
⊢ s ∈ n.support

Tactic:
simpa using h

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a b : σ → R
⊢ rescaleAlgHom (a * b) = (rescaleAlgHom b).comp (rescaleAlgHom a)

Tactic:
ext1 f
  simp [rescaleAlgHom_apply, rescale_rescale]

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
hP' : IsUnit ((coeff 1) P)
this : Invertible ((coeff 1) P) := hP'.invertible
⊢ subst P.substInv P = X

Tactic:
P.subst_substInv_right hP

Goal state after:
R : Type u_2
inst✝ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
hP' : IsUnit ((coeff 1) P)
this : Invertible ((coeff 1) P) := hP'.invertible
⊢ X = X
Module: Mathlib.Analysis.Calculus.TangentCone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Semiring 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
x : E
s : Set E
𝕜' : Type u_3
inst✝³ : Semiring 𝕜'
inst✝² : SMul 𝕜 𝕜'
inst✝¹ : Module 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure[inst✝⁴] s
⊢ ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ⊆ ↑(Submodule.span 𝕜' (tangentConeAt 𝕜' s x))

Tactic:
trans ↑(Submodule.span 𝕜 (tangentConeAt 𝕜' s x)) <;>
    simp [Submodule.span_mono tangentConeAt_mono_field]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: case right
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : E →ₗ[𝕜] F
hg : comap (⇑g) (𝓝 0) ≤ 𝓝 0
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV : V ∈ 𝓝 0
hgV : ⇑g ⁻¹' V ⊆ U
a : α
c : 𝕜
hc₀ : c ≠ 0
hc : (⇑g ∘ f) a ∈ c • V
⊢ f a ∈ ⇑g ⁻¹' (c • V)

Tactic:
exact hc

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
h : DifferentiableAt 𝕜 f x
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f univ x) univ x

Tactic:
rw [← differentiableWithinAt_univ] at 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
h : DifferentiableWithinAt 𝕜 f univ x
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f univ x) univ x
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
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
h : Tendsto (fun x ↦ (f x)⁻¹ • g x) l (𝓝 0)
x : α
hx : f x = 0 → g x = 0
⊢ (fun x ↦ f x • (f x)⁻¹ • g x) x = g x

Tactic:
by_cases h : f x = 0 <;> simp [h, hx]

Goal state after: