mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
⊢ ∀ (x y : β), ⋯.extend (⇑f) (x + y) = ⋯.extend (⇑f) x + ⋯.extend (⇑f) y

Tactic:
refine fun x y => DenseRange.induction_on₂ dr ?_ (fun a b => ?_) x y

Goal state after:
case refine_1
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
x y : β
⊢ IsClosed {q | ⋯.extend (⇑f) (q.1 + q.2) = ⋯.extend (⇑f) q.1 + ⋯.extend (⇑f) q.2}

case refine_2
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
x y : β
a b : α
⊢ ⋯.extend (⇑f) (i a + i b) = ⋯.extend (⇑f) (i a) + ⋯.extend (⇑f) (i b)
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
x y : β
⊢ Continuous fun q ↦ ⋯.extend (⇑f) (q.1 + q.2)

Tactic:
by fun_prop

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

Goal state before:
pp: α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
h : Continuous (⋯.extend ⇑f)
x y : β
⊢ Continuous fun q ↦ ⋯.extend (⇑f) q.1 + ⋯.extend (⇑f) q.2

Tactic:
by fun_prop

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Ring B
inst✝⁵ : ValuativeRel A
inst✝⁴ : ValuativeRel B
inst✝³ : Algebra A B
inst✝² : ValuativeExtension A B
Γ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ
w : Valuation B Γ
inst✝ : w.Compatible
⊢ ∀ (x y : A), x ≤ᵥ y ↔ (Valuation.comap (algebraMap A B) w) x ≤ (Valuation.comap (algebraMap A B) w) y

Tactic:
simp [← vle_iff_vle (A := A) (B := B), Valuation.Compatible.vle_iff_le (v := w)]

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

Goal state before:
pp: Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝¹ : Ring A
v : Valuation A Γ
inst✝ : v.IsRankOneDiscrete
⊢ zpowers ((MonoidWithZeroHom.ofClass v).valueGroup.subtype (generator' v)) =
    Subgroup.map (MonoidWithZeroHom.ofClass v).valueGroup.subtype ⊤

Tactic:
subtype_apply,

Goal state after:
Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝¹ : Ring A
v : Valuation A Γ
inst✝ : v.IsRankOneDiscrete
⊢ zpowers ↑(generator' v) = Subgroup.map (MonoidWithZeroHom.ofClass v).valueGroup.subtype ⊤
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
⊢ addU (⇑f ∘ P) (⇑f ∘ Q) = f (addU P Q)

Tactic:
by
  simp only [addU]
  map_simp

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 : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ (↑n - ↑m) ≤ ↑(ofAdd 0)
v_π_lt_one : (maximalIdeal A).intValuation π < 1
v_π_ne_zero : (maximalIdeal A).intValuation π ≠ 0
⊢ ↑m ≤ ↑n

Tactic:
← sub_nonneg,

Goal state after:
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 : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ (↑n - ↑m) ≤ ↑(ofAdd 0)
v_π_lt_one : (maximalIdeal A).intValuation π < 1
v_π_ne_zero : (maximalIdeal A).intValuation π ≠ 0
⊢ 0 ≤ ↑n - ↑m
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case h
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 : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation π ^ m ≤ 1
h_mn : m ≤ n
⊢ (algebraMap A K) ↑u * ((algebraMap A K) π ^ (n - m) * ((algebraMap A K) ↑w)⁻¹) =
    (algebraMap A K) ↑u * ((algebraMap A K) π ^ n / ((algebraMap A K) ↑w * (algebraMap A K) π ^ m))

Tactic:
congr 1

Goal state after:
case h.e_a
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 : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation π ^ m ≤ 1
h_mn : m ≤ n
⊢ (algebraMap A K) π ^ (n - m) * ((algebraMap A K) ↑w)⁻¹ =
    (algebraMap A K) π ^ n / ((algebraMap A K) ↑w * (algebraMap A K) π ^ m)
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y r s : K
y_ne : y ≠ 0
hr : r ≠ 0
hs : s ≠ 0
h : v (x - y) < min (v s / v r * (v y * v y)) (v y)
hr' : 0 < v r
γ : Γ₀ˣ := Units.mk0 (v s / v r) ⋯
⊢ v (x⁻¹ - y⁻¹) * v r < v s

Tactic:
calc
    v (x⁻¹ - y⁻¹) * v r < γ * v r := by gcongr; exact Valuation.inversion_estimate v y_ne h
    _ = v s := div_mul_cancel₀ _ (by simpa)

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: e : ℤ ≃+o ℤᵒᵈ
⊢ e.toAddEquiv =
    { toAddEquiv := (AddEquiv.neg ℤ).trans { toEquiv := toDual, map_add' := ⋯ },
        map_le_map_iff' := @instUniqueOrderAddMonoidIsoIntOrderDual._proof_1 }.toAddEquiv

Tactic:
simp only [OrderAddMonoidIso.toAddEquiv_eq_coe]
    refine Int.addEquiv_eq_refl_or_neg ((e : ℤ ≃+ ℤᵒᵈ).trans ⟨toDual, toDual_add⟩)
        |>.resolve_left fun H => by
      replace H : e 1 = 1 := congr($H 1)
      have h1 : 0 < e 1 := by
        rw [← map_zero e, map_lt_map_iff]
        simp
      simp [H, ← ofDual_lt_ofDual] at h1

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 Γ₀
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
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : v.restrict z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑a = (fun x ↦ x * x₀) y
this : ↑z₀⁻¹ = (↑z₀)⁻¹
⊢ ↑(a * z₀⁻¹) ∈ V

Tactic:
Completion.coe_mul,

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
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : v.restrict z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑a = (fun x ↦ x * x₀) y
this : ↑z₀⁻¹ = (↑z₀)⁻¹
⊢ ↑a * ↑z₀⁻¹ ∈ V
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 y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
cont : Continuous extension
⊢ Continuous fun x ↦ extension (x.1 + x.2)

Tactic:
by fun_prop

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
a b : R
⊢ (monomial m) a * (monomial n) b = (monomial (m + n)) (a * b)

Tactic:
simpa [monomial] using
    MvPowerSeries.monomial_mul_monomial (Finsupp.single () m) (Finsupp.single () n) a b

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
⊢ (coeff (m + n - n)) φ * a = (coeff m) φ * a

pp: case hc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ n ≤ m + n

Tactic:
add_tsub_cancel_right

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

case hc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ n ≤ m + n
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : n ≤ d
⊢ (coeff (d - n)) p = (coeff (d - n + n - n)) p

Tactic:
add_tsub_cancel_right

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : n ≤ d
⊢ (coeff (d - n)) p = (coeff (d - n)) p
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬m + n - n = m
h₃ : k = m + n
⊢ 0 * b = a * b

Tactic:
add_tsub_cancel_right

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬m = m
h₃ : k = m + n
⊢ 0 * b = a * b
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
⊢ v.intValuationDef (x + 0) ≤ max (v.intValuationDef x) (v.intValuationDef 0)

Tactic:
add_zero

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
⊢ v.intValuationDef x ≤ max (v.intValuationDef x) (v.intValuationDef 0)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
φ ψ : R⟦X⟧
this : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (coeff 1) (φ * ψ) = (coeff 1) φ * constantCoeff ψ + (coeff 1) ψ * constantCoeff φ

Tactic:
rw [coeff_mul, this, Finset.sum_insert, Finset.sum_singleton, coeff_zero_eq_constantCoeff,
    mul_comm, add_comm]

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
φ ψ : R⟦X⟧
this : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (0, 1) ∉ {(1, 0)}
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)}
⊢ (coeff 1) (φ ^ (n' + 1)) = ↑(n' + 1) * (coeff 1) φ * constantCoeff φ ^ (n' + 1 - 1)

Tactic:
rw [h₁, coeff_mul, h₂, Finset.sum_insert, Finset.sum_singleton]

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)}
⊢ (coeff (0, 1).1) (φ ^ n') * (coeff (0, 1).2) φ + (coeff (1, 0).1) (φ ^ n') * (coeff (1, 0).2) φ =
    ↑(n' + 1) * (coeff 1) φ * constantCoeff φ ^ (n' + 1 - 1)

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)}
⊢ (0, 1) ∉ {(1, 0)}
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 Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
⊢ extensionValuation.restrict x < ↑((Units.map valueGroup₀_equiv_extensionValuation.toMonoidHom) γ) ↔
    embedding (extension x) < embedding ↑γ

Tactic:
simp only [MulEquiv.toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe]

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
⊢ extensionValuation.restrict x < valueGroup₀_equiv_extensionValuation ↑γ ↔ embedding (extension x) < embedding ↑γ
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)}
h₀ : n' = 0 ∨ 1 ≤ n'
⊢ constantCoeff φ ^ n' * (coeff 1) φ + (coeff 1) (φ ^ n') * constantCoeff φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'

Tactic:
rcases h₀ with h' | h'

Goal state after:
case inr.succ.inl
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' : n' = 0
⊢ constantCoeff φ ^ n' * (coeff 1) φ + (coeff 1) (φ ^ n') * constantCoeff φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'

case inr.succ.inr
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
⊢ constantCoeff φ ^ n' * (coeff 1) φ + (coeff 1) (φ ^ n') * constantCoeff φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'
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
r : R
⊢ (valuation K v) ↑r = v.intValuation r

Tactic:
by
  rw [valuation_def, Valuation.extendToLocalization_apply_map_apply]

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

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

Tactic:
by
  by_cases hA : Subsingleton A
  · exact not_isField_of_subsingleton _
  · 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✝ : ℕ
⊢ (coeff n✝) ((rescale a) X) = (coeff n✝) (C a * X)

Tactic:
simp only [coeff_rescale, coeff_C_mul, coeff_X]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R[X]
⊢ ↑φ = 0 ↔ φ = 0

Tactic:
rw [← coe_zero, coe_inj]

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}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
⊢ ∀ x ∈ range n \ s, 1 ≤ degree (k x)

Tactic:
simp only [hs_def, mem_filter, mem_sdiff, mem_range, not_and, and_imp]

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
⊢ ∀ x < n, (x < n → ¬k x = 0) → 1 ≤ degree (k x)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
⊢ ↑φ = 0 ↔ φ = 0

Tactic:
rw [← coe_zero, coe_inj]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
p : ℕ
r : R
⊢ MvPowerSeries.C r * ∏ x ∈ e.support, MvPowerSeries.X x ^ (p • e) x =
    MvPowerSeries.C r * ∏ a ∈ e.support, (MvPowerSeries.X a ^ p) ^ e a

Tactic:
simp [pow_mul]

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

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

Tactic:
add_zero

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

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

Tactic:
add_zero

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

Goal state before:
pp: case succ
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
hs : IsLowerSet ↑s
k : ℕ
p : MvPowerSeries σ R
n : ℕ
hmn : 1 ≤ n
ih : (truncFinset R s) (↑((truncFinset R s) p) ^ n) = (truncFinset R s) (p ^ n)
⊢ (truncFinset R s) (↑((truncFinset R s) p) ^ (n + 1)) = (truncFinset R s) (p ^ (n + 1))

Tactic:
| succ n hmn ih =>

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
hs : IsLowerSet ↑s
k : ℕ
hk : 1 ≤ k
p : MvPowerSeries σ R
⊢ (truncFinset R s) (↑((truncFinset R s) p) ^ k) = (truncFinset R s) (p ^ k)

Tactic:
induction k, hk using Nat.le_induction with

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
h : ∃ᶠ (m : σ →₀ ℕ) in atTop, (trunc' R m) f = (trunc' R m) g
n : σ →₀ ℕ
⊢ (coeff n) f = (coeff n) g

Tactic:
obtain ⟨m, hm₁, hm₂⟩ := h.forall_exists_of_atTop n

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
h : ∃ᶠ (m : σ →₀ ℕ) in atTop, (trunc' R m) f = (trunc' R m) g
n m : σ →₀ ℕ
hm₁ : n ≤ m
hm₂ : (trunc' R m) f = (trunc' R m) g
⊢ (coeff n) f = (coeff n) g
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: x : ℕ∞
s : Set ℕ∞
hx : x ≠ ⊤
⊢ s ∈ 𝓝 x ↔ x ∈ s

Tactic:
by
  simp [hx]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g p
d : σ →₀ ℕ
hd : ¬(weight w) d = p
⊢ 0 + 0 = 0

Tactic:
add_zero

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g p
d : σ →₀ ℕ
hd : ¬(weight w) d = p
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

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

Tactic:
add_zero

Goal state after:
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
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
⊢ ↑(weightedOrder w f).toNat = weightedOrder w f

Tactic:
← hf,

Goal state after:
σ : 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
⊢ ↑(↑p).toNat = ↑p
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
⊢ (weightedHomogeneousComponent w p) f ≠ 0

Tactic:
by
  intro hf'
  obtain ⟨d, hd⟩ := f.exists_coeff_ne_zero_and_weightedOrder w (by rw [← hf, toNat_natCast])
  simp only [ne_eq, ← hf, Nat.cast_inj] at hd
  apply hd.1
  rw [MvPowerSeries.ext_iff] at hf'
  specialize hf' d
  simp only [coeff_weightedHomogeneousComponent, coeff_zero, ite_eq_right_iff] at hf'
  exact hf' hd.2

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

Tactic:
by rw [hb]; exact ha0

Goal state after: