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

Goal state before:
pp: case neg
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : (ofClass v) y = 0
h✝² : ¬(ofClass v) w = 0
h✝¹ : ¬(ofClass v) z = 0
h✝ : ¬(ofClass v) x = 0
⊢ 0 / (↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩) =
    ↑⟨Units.mk0 ((ofClass v) x) h✝, ⋯⟩ / ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * (0 / ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩)

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : ¬(ofClass v) y = 0
h✝² : (ofClass v) x = 0
h✝¹ : (ofClass v) w = 0
h✝ : (ofClass v) z = 0
⊢ 0 / 0 = 0 / 0 * (↑⟨Units.mk0 ((ofClass v) y) h✝³, ⋯⟩ / 0)

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case neg
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : ¬(ofClass v) y = 0
h✝² : (ofClass v) x = 0
h✝¹ : (ofClass v) w = 0
h✝ : ¬(ofClass v) z = 0
⊢ 0 / 0 = 0 / ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * (↑⟨Units.mk0 ((ofClass v) y) h✝³, ⋯⟩ / 0)

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : ¬(ofClass v) y = 0
h✝² : (ofClass v) x = 0
h✝¹ : ¬(ofClass v) w = 0
h✝ : (ofClass v) z = 0
⊢ 0 / 0 = 0 / 0 * (↑⟨Units.mk0 ((ofClass v) y) h✝³, ⋯⟩ / ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩)

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case neg
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : ¬(ofClass v) y = 0
h✝² : (ofClass v) x = 0
h✝¹ : ¬(ofClass v) w = 0
h✝ : ¬(ofClass v) z = 0
⊢ 0 / (↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩) =
    0 / ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * (↑⟨Units.mk0 ((ofClass v) y) h✝³, ⋯⟩ / ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩)

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : ¬(ofClass v) y = 0
h✝² : ¬(ofClass v) x = 0
h✝¹ : (ofClass v) w = 0
h✝ : (ofClass v) z = 0
⊢ ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ / 0 =
    ↑⟨Units.mk0 ((ofClass v) x) h✝², ⋯⟩ / 0 * (↑⟨Units.mk0 ((ofClass v) y) h✝³, ⋯⟩ / 0)

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case neg
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : ¬(ofClass v) y = 0
h✝² : ¬(ofClass v) x = 0
h✝¹ : (ofClass v) w = 0
h✝ : ¬(ofClass v) z = 0
⊢ ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ / 0 =
    ↑⟨Units.mk0 ((ofClass v) x) h✝², ⋯⟩ / ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * (↑⟨Units.mk0 ((ofClass v) y) h✝³, ⋯⟩ / 0)

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : ¬(ofClass v) y = 0
h✝² : ¬(ofClass v) x = 0
h✝¹ : ¬(ofClass v) w = 0
h✝ : (ofClass v) z = 0
⊢ ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ / 0 =
    ↑⟨Units.mk0 ((ofClass v) x) h✝², ⋯⟩ / 0 * (↑⟨Units.mk0 ((ofClass v) y) h✝³, ⋯⟩ / ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩)

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case neg
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : ¬(ofClass v) y = 0
h✝² : ¬(ofClass v) x = 0
h✝¹ : ¬(ofClass v) w = 0
h✝ : ¬(ofClass v) z = 0
⊢ ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ /
      (↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩) =
    ↑⟨Units.mk0 ((ofClass v) x) h✝², ⋯⟩ / ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ *
      (↑⟨Units.mk0 ((ofClass v) y) h✝³, ⋯⟩ / ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩)

Tactic:
simp_all

Goal state after:
case neg
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : ¬(ofClass v) y = 0
h✝² : ¬(ofClass v) x = 0
h✝¹ : ¬(ofClass v) w = 0
h✝ : ¬(ofClass v) z = 0
⊢ ↑⟨Units.mk0 (v x) ⋯, ⋯⟩ * ↑⟨Units.mk0 (v y) ⋯, ⋯⟩ / (↑⟨Units.mk0 (v z) ⋯, ⋯⟩ * ↑⟨Units.mk0 (v w) ⋯, ⋯⟩) =
    ↑⟨Units.mk0 (v x) ⋯, ⋯⟩ / ↑⟨Units.mk0 (v z) ⋯, ⋯⟩ * (↑⟨Units.mk0 (v y) ⋯, ⋯⟩ / ↑⟨Units.mk0 (v w) ⋯, ⋯⟩)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a b : ValueGroupWithZero R
h : a < b
⊢ (embed v) a < (embed v) b

Tactic:
obtain ⟨a, r, rfl⟩ := exists_valuation_div_valuation_eq a

Goal state after:
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
b : ValueGroupWithZero R
a : R
r : ↥(posSubmonoid R)
h : (valuation R) a / (valuation R) ↑r < b
⊢ (embed v) ((valuation R) a / (valuation R) ↑r) < (embed v) b
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case pos
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : (valuation K (maximalIdeal A)) y = (valuation K (maximalIdeal A)) x
hx : x = 0
⊢ ∃ u, u • x = y

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case pos
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : (valuation K (maximalIdeal A)) x = (valuation K (maximalIdeal A)) y
hx : ¬x = 0
hy : y = 0
⊢ ∃ u, u • x = y

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : (valuation K (maximalIdeal A)) x = (valuation K (maximalIdeal A)) y
hx : ¬x = 0
hy : ¬y = 0
⊢ y / x ∈ MonoidHom.mker (valuation K (maximalIdeal A))

Tactic:
simp_all

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case inl
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
h✝ : max x x⁻¹ = x ∧ x⁻¹ ≤ x
⊢ closure {x} = closure {x'}

Tactic:
simp_all

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case inr
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
h✝ : max x x⁻¹ = x⁻¹ ∧ x < x⁻¹
⊢ closure {x} = closure {x'}

Tactic:
simp_all

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case inl
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : closure {x} = closure {x'}
h✝ : max y y⁻¹ = y ∧ y⁻¹ ≤ y
⊢ closure {y} = closure {y'}

Tactic:
simp_all

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case inr
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : closure {x} = closure {x'}
h✝ : max y y⁻¹ = y⁻¹ ∧ y < y⁻¹
⊢ closure {y} = closure {y'}

Tactic:
simp_all

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (coeff (n + 1)) (X * φ) = (coeff n) φ

Tactic:
by
  simp only [coeff, Finsupp.single_add, add_comm n 1]
  convert! φ.coeff_add_monomial_mul (single () 1) (single () n) _
  rw [one_mul]

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

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

Tactic:
have := h (m + n)
    rwa [coeff_add_mul_monomial, add_comm, coeff_add_monomial_mul] at this

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (coeff d) (X ^ n * p) = if n ≤ d then (coeff (d - n)) p else 0

Tactic:
by
  split_ifs with h
  · rw [← tsub_add_cancel_of_le h, coeff_X_pow_mul]
    simp
  · refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)
    rw [coeff_X_pow, if_neg, zero_mul]
    have := mem_antidiagonal.mp hx
    rw [add_comm] at this
    exact ((le_of_add_le_right this.le).trans_lt <| not_le.mp h).ne

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff n) (φ * C a) = (coeff n) φ * a

Tactic:
by simpa using coeff_add_mul_monomial n 0 φ a

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
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) =
    ↑(Multiset.count v.asIdeal (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})))

Tactic:
Ideal.count_associates_factors_eq hsr v.isPrime v.ne_bot

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})
⊢ ↑(Multiset.count v.asIdeal (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r}))) =
    ↑(Multiset.count v.asIdeal (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})))
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
S : Type u_3
inst✝³ : CommSemiring A
inst✝² : Algebra A R
inst✝¹ : CommSemiring S
inst✝ : Algebra A S
φ : R →ₐ[A] S
a : A
f : R⟦X⟧
⊢ (rescale ((algebraMap A S) a)) ((map ↑φ) f) = (map ↑φ) ((rescale ((algebraMap A R) a)) f)

Tactic:
convert! rescale_map (φ : R →+* S) _ _
  simp

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x ≠ 0
⊢ 0 ≤ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)

Tactic:
exact Int.natCast_nonneg _

Goal state after:
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 Γ₀
a b : (ofClass v).ValueGroup₀
hab : extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑⋯.choose
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ha0 : embedding a ≠ embedding 0
h0 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hb0 : embedding b ≠ embedding 0
h : y = 0
⊢ False

Tactic:
simp [h, ← hy] at hb0

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

Goal state before:
pp: case inr.succ
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)}
⊢ ∑ p ∈ antidiagonal 1, (coeff p.1) (φ ^ n') * (coeff p.2) φ = ↑(n' + 1) * (coeff 1) φ * constantCoeff φ ^ (n' + 1 - 1)

Tactic:
h₂,

Goal state after:
case inr.succ
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)}
⊢ ∑ p ∈ {(0, 1), (1, 0)}, (coeff p.1) (φ ^ n') * (coeff p.2) φ =
    ↑(n' + 1) * (coeff 1) φ * constantCoeff φ ^ (n' + 1 - 1)
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 b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hv : b ∈ v.asIdeal
x✝ : a = 0
⊢ False

Tactic:
simp_all

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
⊢ ∏ i ∈ range n, (coeff (k i)) f = 0

Tactic:
have hs : s ⊆ range n := filter_subset _ _

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
⊢ ∏ i ∈ range n, (coeff (k i)) f = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
⊢ ∀ x < n, (x < n → ¬k x = 0) → 1 ≤ degree (k x)

Tactic:
intro i hi hi'

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
⊢ 1 ≤ degree (k i)
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
x : K
⊢ ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

Tactic:
obtain (⟨r, hr⟩ | ⟨r, hr⟩) :=
    ValuationRing.isInteger_or_isInteger (valuationSubringAtPrime K v) x
  <;> obtain ⟨⟨n, d⟩, hnd⟩ := IsLocalization.surj v.asIdeal.primeCompl r
  <;> use n, d

Goal state after:
case h
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
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  r * (algebraMap R ↥(valuationSubringAtPrime K v)) ↑(n, d).2 = (algebraMap R ↥(valuationSubringAtPrime K v)) (n, d).1
⊢ x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

case h
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
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x⁻¹
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  r * (algebraMap R ↥(valuationSubringAtPrime K v)) ↑(n, d).2 = (algebraMap R ↥(valuationSubringAtPrime K v)) (n, d).1
⊢ x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
⊢ (trunc' R n) (C a * p) = MvPolynomial.C a * (trunc' R n) p

Tactic:
by
  ext m; simp [coeff_trunc']

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
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
y : (ofClass Valued.v).ValueGroup₀
⊢ (map' ↑(valueGroupEquiv K v)) ((map' ↑(valueGroupEquiv K v).symm) y) = y

Tactic:
by match y with | 0 => simp | .coe b => simp

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
x y : K
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm (x + y)) } =
    { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm x) } +
      { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm y) }

Tactic:
apply adicCompletion.ext; simp [UniformSpace.Completion.coe_add]

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

Goal state before:
pp: case hc
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : DecidableEq σ
inst✝¹ : CommSemiring R
inst✝ : Nonempty σ
f : MvPowerSeries σ R
d : σ →₀ ℕ
s : σ
h✝ : True
n : σ →₀ ℕ
hn : n ≥ d + Finsupp.single s 1
⊢ d < n

Tactic:
apply lt_of_lt_of_le _ hn

Goal state after:
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : DecidableEq σ
inst✝¹ : CommSemiring R
inst✝ : Nonempty σ
f : MvPowerSeries σ R
d : σ →₀ ℕ
s : σ
h✝ : True
n : σ →₀ ℕ
hn : n ≥ d + Finsupp.single s 1
⊢ d < d + Finsupp.single s 1
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
⊢ Continuous[inst✝¹, instTopologicalSpace R] ⇑C

Tactic:
simp only [continuous_iff_continuousAt]
  refine fun r ↦ (tendsto_iff_coeff_tendsto _ _ _).mpr fun d ↦ ?_
  simp only [coeff_C]
  split_ifs
  · exact tendsto_id
  · exact tendsto_const_nhds

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
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Tactic:
by_cases ha : a ∈ v.adicCompletionIntegers K

Goal state after:
case pos
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 : a ∈ adicCompletionIntegers K v
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

case neg
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 : a ∉ adicCompletionIntegers K v
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
H : ¬m < n + 1
h✝ : m = 0
⊢ 0 = a

Tactic:
simp_all

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : d = 1
⊢ 1 = Polynomial.X.coeff d

Tactic:
h₂,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : d = 1
⊢ 1 = Polynomial.X.coeff 1
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
f : MvPowerSeries σ R
Jd : TwoSidedIdeal R × (σ →₀ ℕ)
⊢ f ∈ basis σ R Jd ↔ ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1

Tactic:
by
  simp [basis]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ (algebraMap R S) ((coeff e) f) = (coeff e) f • (coeff e) ((monomial e) 1)

Tactic:
coeff_monomial_same,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ (algebraMap R S) ((coeff e) f) = (coeff e) f • 1
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
q : ℕ
hq : 1 < q
f : PowerSeries R
k : ℕ
⊢ ((ofPowerSeries q) f) (q ^ k) = (PowerSeries.coeff k) f

Tactic:
rw [ofPowerSeries_apply hq, (Nat.pow_right_injective hq).extend_apply]

Goal state after: