mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
f : G₀ˣ ≃*o Multiplicative ℤ
⊢ ∀ {a b : G₀},
    (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun a ≤
        (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun b ↔
      a ≤ b

pp: case refine_3
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
f : G₀ ≃*o WithZero (Multiplicative ℤ)
⊢ G₀ˣ ≃* Multiplicative ℤ

pp: case refine_4
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
f : G₀ ≃*o WithZero (Multiplicative ℤ)
⊢ ∀ {a b : G₀ˣ}, (MulEquiv.toEquiv ?refine_3).toFun a ≤ (MulEquiv.toEquiv ?refine_3).toFun b ↔ a ≤ b

Tactic:
· intro a b
      rcases eq_or_ne a 0 with rfl | ha
      · simp [WithZero.withZeroUnitsEquiv]
      rcases eq_or_ne b 0 with rfl | hb
      · simp [WithZero.withZeroUnitsEquiv]
      simp [WithZero.withZeroUnitsEquiv, ha, hb, ← Units.val_le_val]

Goal state after:
case refine_3
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
f : G₀ ≃*o WithZero (Multiplicative ℤ)
⊢ G₀ˣ ≃* Multiplicative ℤ

case refine_4
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
f : G₀ ≃*o WithZero (Multiplicative ℤ)
⊢ ∀ {a b : G₀ˣ}, (MulEquiv.toEquiv ?refine_3).toFun a ≤ (MulEquiv.toEquiv ?refine_3).toFun b ↔ a ≤ b
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_5
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a✝ : G₀
⊢ g ≤ a✝ →
    ¬a✝ = 0 →
      ∀ (b : G₀),
        g ≤ b → ¬b = 0 → a✝ < b → (if h : a✝ = 0 then 1 else Units.mk0 a✝ h) < if h : b = 0 then 1 else Units.mk0 b h

Tactic:
_

Goal state after:
case refine_5
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a✝¹ : G₀
a✝ : g ≤ a✝¹
⊢ ¬a✝¹ = 0 →
    ∀ (b : G₀),
      g ≤ b → ¬b = 0 → a✝¹ < b → (if h : a✝¹ = 0 then 1 else Units.mk0 a✝¹ h) < if h : b = 0 then 1 else Units.mk0 b h
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_5
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a✝¹ : G₀
a✝ : g ≤ a✝¹
ha0 : ¬a✝¹ = 0
⊢ ∀ (b : G₀),
    g ≤ b → ¬b = 0 → a✝¹ < b → (if h : a✝¹ = 0 then 1 else Units.mk0 a✝¹ h) < if h : b = 0 then 1 else Units.mk0 b h

Tactic:
_

Goal state after:
case refine_5
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a✝¹ : G₀
a✝ : g ≤ a✝¹
ha0 : ¬a✝¹ = 0
b✝ : G₀
⊢ g ≤ b✝ → ¬b✝ = 0 → a✝¹ < b✝ → (if h : a✝¹ = 0 then 1 else Units.mk0 a✝¹ h) < if h : b✝ = 0 then 1 else Units.mk0 b✝ h
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_5
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a✝¹ : G₀
a✝ : g ≤ a✝¹
ha0 : ¬a✝¹ = 0
b✝ : G₀
⊢ g ≤ b✝ → ¬b✝ = 0 → a✝¹ < b✝ → (if h : a✝¹ = 0 then 1 else Units.mk0 a✝¹ h) < if h : b✝ = 0 then 1 else Units.mk0 b✝ h

Tactic:
_

Goal state after:
case refine_5
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a✝² : G₀
a✝¹ : g ≤ a✝²
ha0 : ¬a✝² = 0
b✝ : G₀
a✝ : g ≤ b✝
⊢ ¬b✝ = 0 → a✝² < b✝ → (if h : a✝² = 0 then 1 else Units.mk0 a✝² h) < if h : b✝ = 0 then 1 else Units.mk0 b✝ h
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 > x2
a : G₀
ha : g⁻¹ ≤ a
b : G₀
⊢ g⁻¹ ≤ b → a < b → b⁻¹ < a⁻¹

Tactic:
_

Goal state after:
case refine_2
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 > x2
a : G₀
ha : g⁻¹ ≤ a
b : G₀
x✝ : g⁻¹ ≤ b
⊢ a < b → b⁻¹ < a⁻¹
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_4
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
a : G₀
⊢ a ≤ g → ¬a = 0 → ∀ b ≤ g, ¬b = 0 → b < a → a⁻¹ < b⁻¹

Tactic:
_

Goal state after:
case refine_4
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
a : G₀
a✝ : a ≤ g
⊢ ¬a = 0 → ∀ b ≤ g, ¬b = 0 → b < a → a⁻¹ < b⁻¹
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_4
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
a : G₀
a✝ : a ≤ g
⊢ ¬a = 0 → ∀ b ≤ g, ¬b = 0 → b < a → a⁻¹ < b⁻¹

Tactic:
_

Goal state after:
case refine_4
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
a : G₀
a✝¹ : a ≤ g
a✝ : ¬a = 0
⊢ ∀ b ≤ g, ¬b = 0 → b < a → a⁻¹ < b⁻¹
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_4
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
a : G₀
a✝¹ : a ≤ g
a✝ : ¬a = 0
b : G₀
⊢ b ≤ g → ¬b = 0 → b < a → a⁻¹ < b⁻¹

Tactic:
_

Goal state after:
case refine_4
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
a : G₀
a✝² : a ≤ g
a✝¹ : ¬a = 0
b : G₀
a✝ : b ≤ g
⊢ ¬b = 0 → b < a → a⁻¹ < b⁻¹
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hsr : Ideal.span {r} ≠ 0
⊢ v.intValuation r = exp (-↑(multiplicity v.asIdeal (Ideal.span {r})))

Tactic:
have hfm : FiniteMultiplicity v.asIdeal (Ideal.span {r}) :=
    FiniteMultiplicity.of_prime_left v.prime hsr

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hsr : Ideal.span {r} ≠ 0
hfm : FiniteMultiplicity v.asIdeal (Ideal.span {r})
⊢ v.intValuation r = exp (-↑(multiplicity v.asIdeal (Ideal.span {r})))
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hsr : Ideal.span {r} ≠ 0
hfm : FiniteMultiplicity v.asIdeal (Ideal.span {r})
⊢ -↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors) =
    -↑(multiplicity v.asIdeal (Ideal.span {r}))

Tactic:
neg_inj,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hsr : Ideal.span {r} ≠ 0
hfm : FiniteMultiplicity v.asIdeal (Ideal.span {r})
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors) =
    ↑(multiplicity v.asIdeal (Ideal.span {r}))
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
u v : σ →₀ ℕ
⊢ ∀ x ∈ (s.finsuppAntidiag v).attach,
    (coeff u) (f a) * ∏ i ∈ s, (coeff (↑x i)) (f i) =
      ∏ x_1 ∈ insert a s, (coeff (Function.update (⇑↑x) a u x_1)) (f x_1)

Tactic:
simp only [mem_attach, Finset.prod_insert ha, Function.update_self, forall_true_left,
        Subtype.forall]

Goal state after:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
u v : σ →₀ ℕ
⊢ ∀ a_1 ∈ s.finsuppAntidiag v,
    (coeff u) (f a) * ∏ x ∈ s, (coeff (a_1 x)) (f x) =
      (coeff u) (f a) * ∏ x ∈ s, (coeff (Function.update (⇑a_1) a u x)) (f x)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: 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 φ * ↑n' * (coeff 1) φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'

Tactic:
1,

Goal state after:
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 φ * ↑n' * (coeff 1) φ
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: 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' - 1) * constantCoeff φ * ↑n' * (coeff 1) φ

Tactic:
1,

Goal state after:
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' - 1) * constantCoeff φ * ↑n'
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: 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' - 1) * constantCoeff φ * ↑n'

Tactic:
1,

Goal state after:
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' - 1) * constantCoeff φ
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: 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'

Tactic:
1,

Goal state after:
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) φ
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: 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' - 1 + 1) * ↑n' * (coeff 1) φ

Tactic:
1,

Goal state after:
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' - 1 + 1) * ↑n'
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B : Type u_4
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
⊢ ⊥ ≠ ⊤

Tactic:
by
      classical
      rw [Ne, SetLike.ext_iff, not_forall]
      inhabit σ
      refine ⟨X default, ?_⟩
      simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top]
      intro x
      rw [MvPowerSeries.ext_iff, not_forall]
      refine ⟨Finsupp.single default 1, ?_⟩
      simp [algebraMap_apply, coeff_C]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
x : σ
⊢ x ∈ e.support → (a x • MvPowerSeries.X x) ^ e x = (MvPowerSeries.C ((algebraMap A R) (a x)) * MvPowerSeries.X x) ^ e x

Tactic:
_

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
x : σ
a✝ : x ∈ e.support
⊢ (a x • MvPowerSeries.X x) ^ e x = (MvPowerSeries.C ((algebraMap A R) (a x)) * MvPowerSeries.X x) ^ e x
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: 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) < ↑γ

Tactic:
have hvaz := intValuation_ne_zero v a ha
    have hγz : WithZero.coe γ ≠ 0 := WithZero.coe_ne_zero
    -- Otherwise, find `n : ℕ` such that `exp (-n) < γ` and `exp(-n) < v a`.
    obtain ⟨n, hna, hnγ⟩ := exists_exp_neg_natCast_lt_and_lt hvaz hγz
    apply Exists.imp (fun _ h ↦ lt_of_le_of_lt h hnγ)
    -- `v b ≤ v a`, so `b ∈ v.asIdeal ^ -log (v a)`.
    -- From `irreducible_pow_sup_of_ge` we know that
    -- `v.asIdeal ^ -log (v a) = v.asIdeal ^ n ⊔ Ideal.span {a}`.
    -- So, `∃ z ∈ v.asIdeal ^ n, ∃ (y: R), b = z + y * a`. This gives `z` and `y` such that
    -- `b - y * a = z` and `v z ≤ exp (-n)`, as required.
    have hvn : emultiplicity v.asIdeal (Ideal.span {a}) ≤ n := by
      grw [← exp_le_intValuation_iff_emultiplicity_le, hna]
    have hb : b ∈ v.asIdeal ^ multiplicity v.asIdeal (Ideal.span {a}) := by
      rwa [← intValuation_le_pow_iff_mem, ← v.intValuation_eq_exp_neg_multiplicity ha]
    have hnz : Ideal.span {a} ≠ ⊥ := by rwa [ne_eq, Ideal.span_singleton_eq_bot]
    simpa [← Ideal.irreducible_pow_sup_of_ge hnz v.irreducible n hvn, Submodule.mem_sup,
      ← eq_sub_iff_add_eq, ← intValuation_le_pow_iff_mem, Ideal.mem_span_singleton'] using hb

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
d : σ →₀ ℕ
a : R
h : a ≠ 0
⊢ ((monomial d) a).order = ↑(degree d)

Tactic:
rw [degree_eq_weight_one]
  exact weightedOrder_monomial_of_ne_zero _ h

Goal state after:
Module: Mathlib.Topology.Algebra.TopologicallyNilpotent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : TopologicalSpace R
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
inst✝² : TopologicalSpace S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
φ : F
hφ : Continuous[inst✝⁵, inst✝²] ⇑φ
a : R
ha : IsTopologicallyNilpotent a
⊢ IsTopologicallyNilpotent (φ a)

Tactic:
unfold IsTopologicallyNilpotent at ha ⊢
  simp_rw [← map_pow]
  exact (map_zero φ ▸ hφ.tendsto 0).comp ha

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f : MvPowerSeries σ R
d n : σ →₀ ℕ
hdn : d ≤ n
⊢ (coeff d) ↑((trunc' R n) f) = (coeff d) f

Tactic:
simp [coeff_trunc', hdn]

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 : adicCompletion K v
ha : 1 < Valued.v a
ϖ : R
hϖ : v.intValuation ϖ = exp (-1)
this : Valued.v ((algebraMap R (adicCompletion K v)) ϖ) = (exp 1)⁻¹
hϖ0 : ϖ ≠ 0
⊢ exp (Valued.v a).log ≤ exp |(Valued.v a).log|

Tactic:
by simp [le_abs_self]

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

Goal state before:
pp: case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
i : ℕ
hi : ↑i = φ.order
⊢ (coeff i) (φ + ψ) ≠ 0

Tactic:
rw [← hi] at H

Goal state after:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
i : ℕ
H : ↑i < ψ.order
hi : ↑i = φ.order
⊢ (coeff i) (φ + ψ) ≠ 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case self
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ (↑{ val := u, inv := v, val_inv := hu, inv_val := hv }).order + ?m.34 ≤ order 1

pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ ℕ∞

Tactic:
← hu

Goal state after:
case self
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ (↑{ val := u, inv := v, val_inv := hu, inv_val := hv }).order + ?m.34 ≤ (u * v).order

R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ ℕ∞
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: σ : Type u_1
S : Type u_3
inst✝³ : CommRing S
inst✝² : TopologicalSpace S
inst✝¹ : ContinuousAdd S
inst✝ : IsLinearTopology S S
a b : σ → S
ha : HasEval a
hb : HasEval b
⊢ Tendsto (a + b) cofinite (𝓝 (0 + 0))

Tactic:
exact ha.tendsto_zero.add hb.tendsto_zero

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✝² : 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
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this : ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, φ (MvPolynomial.coeff i x) ∈ I
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (MvPolynomial.coeff i p) ∈ I
d : σ →₀ ℕ
⊢ d ∈ p.support → φ (MvPolynomial.coeff d p) * ∏ i ∈ d.support, a i ^ d i ∈ I

Tactic:
_

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✝² : 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
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this : ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, φ (MvPolynomial.coeff i x) ∈ I
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (MvPolynomial.coeff i p) ∈ I
d : σ →₀ ℕ
a✝ : d ∈ p.support
⊢ φ (MvPolynomial.coeff d p) * ∏ i ∈ d.support, a i ^ d i ∈ I
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: case mp.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff e) a ∈ J) → ∀ e_1 ≤ e, (coeff e_1) a ∈ K
h' : ¬e ≤ d
x : R
⊢ x ∈ ⊤ → x ∈ K

Tactic:
_

Goal state after:
case mp.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff e) a ∈ J) → ∀ e_1 ≤ e, (coeff e_1) a ∈ K
h' : ¬e ≤ d
x : R
a✝ : x ∈ ⊤
⊢ x ∈ K
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case zero
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hn : f 0 = true
⊢ f_max 0 = true

Tactic:
rw [fn] at hn
        contradiction

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:
← 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
f : MvPowerSeries σ R
n : τ →₀ ℕ
⊢ HasSubst 0

Tactic:
by simp [hasSubst_def]

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

Goal state before:
pp: case pos
σ : 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
hf : IsNilpotent (constantCoeff f)
d : σ →₀ ℕ
hd : d = 0
⊢ IsNilpotent ((coeff d) f • constantCoeff (d.prod fun s e ↦ a s ^ e))

Tactic:
rw [← algebraMap_smul S, smul_eq_mul, mul_comm, ← smul_eq_mul, hd]

Goal state after:
case pos
σ : 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
hf : IsNilpotent (constantCoeff f)
d : σ →₀ ℕ
hd : d = 0
⊢ IsNilpotent (constantCoeff (Finsupp.prod 0 fun s e ↦ a s ^ e) • (algebraMap R S) ((coeff 0) f))
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
⊢ (ofPowerSeries (q ^ k)) f = (ofPowerSeries q) (PowerSeries.subst (PowerSeries.X ^ k) f)

Tactic:
· simp [ofPowerSeries, hq, hk]

Goal state after:
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
f : R⟦X⟧
⊢ a.order * f.order ≤ (subst a f).order

Tactic:
by
  refine .trans ?_ (MvPowerSeries.le_order_subst (PowerSeries.hasSubst_iff.mp ha) _)
  simp [order_eq_order]

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: