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

Goal state before:
pp: K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
F : Filter ↥K
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
F_cau : Cauchy (map (⇑i) F)
hi : IsUniformInducing ⇑i
⊢ map (⇑i) (𝓝 0 ⊓ F) = ⊥

Tactic:
inf_F,

Goal state after:
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
F : Filter ↥K
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
F_cau : Cauchy (map (⇑i) F)
hi : IsUniformInducing ⇑i
⊢ map ⇑i ⊥ = ⊥
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : IsTopologicalDivisionRing L
inst✝¹ : T0Space L
inst✝ : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : F.NeBot
⊢ Cauchy (map (fun x ↦ x⁻¹) F)

Tactic:
rcases CompleteSpace.complete cau_F with ⟨x, hx⟩

Goal state after:
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : IsTopologicalDivisionRing L
inst✝¹ : T0Space L
inst✝ : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : F.NeBot
x : L
hx : F ≤ 𝓝 x
⊢ Cauchy (map (fun x ↦ x⁻¹) F)
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm : (⇑f ∘ fun x ↦ x⁻¹) = (fun x ↦ x⁻¹) ∘ ⇑f
⊢ map (⇑f) (𝓝 0 ⊓ F) = ⊥

Tactic:
inf_F,

Goal state after:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm : (⇑f ∘ fun x ↦ x⁻¹) = (fun x ↦ x⁻¹) ∘ ⇑f
⊢ map ⇑f ⊥ = ⊥
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.negAddY P Q = (-addU P Q) ^ 3

Tactic:
addU,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.negAddY P Q = (- -((P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z))) ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addY P Q = addU P Q ^ 3

Tactic:
addU,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addY P Q = (-((P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z))) ^ 3
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
⊢ ∃ n u, ↑r = ↑(π.val ^ n) * ↑↑u

Tactic:
have hm₀ : 0 ≤ m := by
    rw [← zpow_le_one_iff_right_of_lt_one₀ π.2.val_pos π.2.val_lt_one, hm']
    exact r.2

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
⊢ ∃ n u, ↑r = ↑(π.val ^ n) * ↑↑u
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
π : ↥v.valuationSubring
hπ : v.IsUniformizer ↑π
h : ∀ {a : ↥v.valuationSubring}, a ≠ 0 → ∃ b, a * b = 1
this : ¬π = 0
⊢ False

Tactic:
specialize h this

Goal state after:
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
π : ↥v.valuationSubring
hπ : v.IsUniformizer ↑π
h : ∃ b, π * b = 1
this : ¬π = 0
⊢ False
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case neg
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 : (valuation K (maximalIdeal A)) ((algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m)) ≤ 1
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
⊢ ∃ a, (algebraMap A K) a = x

Tactic:
rw [mul_comm (w : A) _, map_mul _ (u : A) _, map_mul _ _ (w : A), div_eq_mul_inv, mul_assoc,
      Valuation.map_mul, Integers.one_of_isUnit' u.isUnit (valuation_le_one _), one_mul,
      mul_inv, ← mul_assoc, Valuation.map_mul, map_mul, map_inv₀, map_inv₀,
      Integers.one_of_isUnit' w.isUnit (valuation_le_one _), inv_one, mul_one, ← div_eq_mul_inv,
      ← map_div₀, ← IsFractionRing.mk'_mk_eq_div hb,
      valuation_of_mk', map_pow, map_pow] at H

Goal state after:
case neg
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
⊢ ∃ a, (algebraMap A K) a = x
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
⊢ DenselyOrdered ↑s ↔ s.Subsingleton

Tactic:
refine ⟨fun H ↦ ?_, fun h ↦ h.denselyOrdered⟩
  rw [← Set.subsingleton_coe, ← not_nontrivial_iff_subsingleton, nontrivial_iff_lt]
  suffices DenselyOrdered (WithBot.some ⁻¹' s) by
    rintro ⟨x, y, H⟩
    rw [_root_.denselyOrdered_set_iff_subsingleton] at this
    obtain ⟨z, hz, hz'⟩ := exists_between H
    have hz0 : (⊥ : WithBot X) < z := by simp [(Subtype.coe_lt_coe.mpr hz).trans_le']
    replace hz' : WithBot.unbot z.val hz0.ne' < WithBot.unbot y (hz0.trans hz').ne' := by
      rwa [← WithBot.coe_lt_coe, WithBot.coe_unbot, WithBot.coe_unbot]
    refine absurd (this ?_ ?_) hz'.ne <;>
    simp
  constructor
  simp only [Subtype.exists, Set.mem_preimage, Subtype.forall, Subtype.mk_lt_mk, exists_and_right,
    exists_prop]
  intro x hx y hy hxy
  have : (⟨_, hx⟩ : s) < ⟨_, hy⟩ := by simp [hxy]
  obtain ⟨z, hz, hz'⟩ := exists_between this
  simp only [← Subtype.coe_lt_coe] at hz hz'
  refine ⟨WithBot.unbot z (hz.trans_le' (by simp)).ne', ⟨?_, ?_⟩, ?_⟩
  · simp
  · rw [← WithBot.coe_lt_coe]
    simp [hz.trans_le]
  · rw [← WithBot.coe_lt_coe]
    simp [hz'.trans_le']

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

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective ⇑v
x : K
h : x ≠ 0
h0 : v x ≠ 0
⊢ ContinuousAt (⇑v) x

Tactic:
rw [ContinuousAt, WithZeroTopology.tendsto_of_ne_zero h0]

Goal state after:
case inr
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective ⇑v
x : K
h : x ≠ 0
h0 : v x ≠ 0
⊢ ∀ᶠ (x_1 : K) in 𝓝 x, v x_1 = v 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 Γ₀
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₀ : ↑γ₀ ≤ 0
h : v.restrict x = 0
⊢ False

Tactic:
simp at x_in₀

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

Goal state before:
pp: case l₂
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
| 𝓝 1

Tactic:
rw [← one_mul (1 : hat K)]

Goal state after:
case l₂
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
| 𝓝 (1 * 1)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (n, d)
⊢ 0 * (coeff (i, j).2) p = 0

pp: case h₀.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (n, d)
⊢ ¬(i, j).1 = n

Tactic:
zero_mul

Goal state after:
case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (n, d)
⊢ 0 = 0

case h₀.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (n, d)
⊢ ¬(i, j).1 = n
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ 0 * (coeff x.2) p = 0

pp: case neg.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ ¬x.1 = n

Tactic:
zero_mul

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ 0 = 0

case neg.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ ¬x.1 = n
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
⊢ 0 = 0 * if y = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors))

Tactic:
zero_mul

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : x = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : m s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ 0 * (coeff (i, j).2) φ = 0

pp: case mp.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : m s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ ¬(i, j).1 = single s n

Tactic:
zero_mul

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : m s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ 0 = 0

case mp.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : m s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ ¬(i, j).1 = single s n
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
hr : ¬r = 0
⊢ v.intValuation r ≤ exp (-↑n) ↔ v.asIdeal ^ n ∣ Ideal.span {r}

Tactic:
rw [v.intValuation_if_neg hr, exp_le_exp, neg_le_neg_iff, Int.ofNat_le,
      Ideal.dvd_span_singleton, ← Associates.le_singleton_iff,
      Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hr) v.associates_irreducible]

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:
by
  rw [intValuation_le_pow_iff_dvd, Ideal.dvd_span_singleton]

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ -↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors) = -1

Tactic:
apply congr_arg

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors) = 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' * (coeff 1) φ + constantCoeff φ ^ (n' - 1) * constantCoeff φ * ↑n' * (coeff 1) φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'

Tactic:
enter [1, 2, 1, 1, 2]

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 φ
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
this : m ≤ #s
m' : ℕ
hm' : #s = m + m'
⊢ 0 * constantCoeff f ^ m' = 0

Tactic:
zero_mul

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
this : m ≤ #s
m' : ℕ
hm' : #s = m + m'
⊢ 0 = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R[X]
x✝ : ℕ
a✝ : x✝ ∈ Finset.range (φ.natDegree + 1)
⊢ PowerSeries.C (φ.coeff x✝) * PowerSeries.X ^ x✝ = PowerSeries.C (φ.coeff x✝) * ↑X ^ x✝

Tactic:
coe_X

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R[X]
x✝ : ℕ
a✝ : x✝ ∈ Finset.range (φ.natDegree + 1)
⊢ PowerSeries.C (φ.coeff x✝) * PowerSeries.X ^ x✝ = PowerSeries.C (φ.coeff x✝) * PowerSeries.X ^ x✝
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case mp
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
a : hat K
ha : v a = γ
⊢ ∃ a, v a = γ

Tactic:
induction a using Completion.induction_on

Goal state after:
case mp.hp
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
⊢ IsClosed {a | v a = γ → ∃ a, v a = γ}

case mp.ih
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
a✝ : K
ha : v ↑a✝ = γ
⊢ ∃ a, v a = γ
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ weightedOrder w ((monomial d) a) = ↑((weight w) d)

Tactic:
· rw [weightedOrder_eq_nat]
    constructor
    · use d
      simp only [coeff_monomial_same, ne_eq, h, not_false_eq_true, and_self]
    · intro b hb
      rw [coeff_monomial, if_neg]
      rintro rfl
      exact hb.false

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 Γ₀
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Algebra R K
inst✝¹ : UniformContinuousConstSMul R K
inst✝ : FaithfulSMul R K
⊢ FaithfulSMul R (hat K)

Tactic:
by
  rw [faithfulSMul_iff_algebraMap_injective R (hat K)]
  exact (FaithfulSMul.algebraMap_injective K (hat K)).comp (FaithfulSMul.algebraMap_injective R K)

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑((weight w) d) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : ↑((weight w) i) < weightedOrder w f
⊢ 0 * (coeff (i, j).2) g = 0

Tactic:
zero_mul

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑((weight w) d) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : ↑((weight w) i) < weightedOrder w f
⊢ 0 = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
hv : (valuation K v) x ≤ 1
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd : d ∈ v.asIdeal.primeCompl
hnd : x * (algebraMap R K) ↑⟨d, hd⟩ = (algebraMap R K) n
⊢ ∃ a, (valuation K v) ((algebraMap R K) a - x) < ↑γ

Tactic:
rw [← intValuation_eq_one_iff_mem_primeCompl] at hd

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
hv : (valuation K v) x ≤ 1
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd✝ : d ∈ v.asIdeal.primeCompl
hd : v.intValuation d = 1
hnd : x * (algebraMap R K) ↑⟨d, hd✝⟩ = (algebraMap R K) n
⊢ ∃ a, (valuation K v) ((algebraMap R K) a - x) < ↑γ
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
hd : ¬(weight w) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = d
hp : (weight w) x.1 ≠ p
⊢ 0 * (coeff x.2) g = 0

Tactic:
zero_mul

Goal state after:
case inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
hd : ¬(weight w) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = d
hp : (weight w) x.1 ≠ p
⊢ 0 = 0
Module: Mathlib.Topology.Algebra.TopologicallyNilpotent

Goal state before:
pp: R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : MonoidWithZero R
a : R
n : ℕ
hn : a ^ n = 0
i : ℕ
hi : i ≥ n
⊢ 0 * a ^ (i - n) = 0

Tactic:
zero_mul

Goal state after:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : MonoidWithZero R
a : R
n : ℕ
hn : a ^ n = 0
i : ℕ
hi : i ≥ n
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case pos.inr.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : (weight w) x.1 + (weight w) x.2 = p + q
hx : x.1 + x.2 = d
h : (weight w) x.1 < p
⊢ (coeff x.1) f * (coeff x.2) g = 0 * if (weight w) x.2 = q then (coeff x.2) g else 0

Tactic:
zero_mul

Goal state after:
case pos.inr.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : (weight w) x.1 + (weight w) x.2 = p + q
hx : x.1 + x.2 = d
h : (weight w) x.1 < p
⊢ (coeff x.1) f * (coeff x.2) g = 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case pos.inr.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : (weight w) x.1 + (weight w) x.2 = p + q
hx : x.1 + x.2 = d
h : ↑((weight w) x.1) < ↑p
⊢ 0 * (coeff x.2) g = 0

Tactic:
zero_mul

Goal state after:
case pos.inr.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : (weight w) x.1 + (weight w) x.2 = p + q
hx : x.1 + x.2 = d
h : ↑((weight w) x.1) < ↑p
⊢ 0 = 0
Module: Mathlib.RingTheory.PowerSeries.Order

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

Tactic:
simpa using ext (by simpa using h)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
this : (φ + ψ).order = φ.order
⊢ (φ + ψ).order ≤ min φ.order ψ.order

Tactic:
by
    rw [le_inf_iff, this]
    exact ⟨le_rfl, le_of_lt H⟩

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : ↑i < φ.order
⊢ 0 * (coeff (i, j).2) ψ = 0

Tactic:
zero_mul

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : ↑i < φ.order
⊢ 0 = 0
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
hRS : uR • S ⊆ S
hR'S : uR' • S ⊆ S
A : AddSubgroup M := AddSubgroup.closure S
hRA : ∀ (r : R), ∀ i ∈ A, r • i ∈ A
r' : R'
i : M
hi : i ∈ A
⊢ r' • i ∈ A

Tactic:
refine AddSubgroup.closure_induction (fun x hx => ?base) ?zero (fun x y _ _ hx hy ↦ ?add)
      (fun x _ hx ↦ ?neg) hi
    case base => exact AddSubgroup.subset_closure <| hR'S <| Set.smul_mem_smul trivial hx
    case zero => simp_rw [smul_zero]; exact zero_mem _
    case add => simp_rw [smul_add]; exact add_mem hx hy
    case neg => simp_rw [smul_neg]; exact neg_mem hx

Goal state after: