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

Goal state before:
pp: case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
x : R
hx : Valued.v.restrict x * Valued.v.restrict s.ofVal < Valued.v.restrict r.ofVal
⊢ Valued.v.restrict (toVal v x) < ↑γ

pp: case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
x : R
hx : Valued.v.restrict x < Valued.v.restrict r.ofVal / Valued.v.restrict s.ofVal
⊢ 0 < Valued.v.restrict s.ofVal

Tactic:
← map_mul,

Goal state after:
case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
x : R
hx : Valued.v.restrict (x * s.ofVal) < Valued.v.restrict r.ofVal
⊢ Valued.v.restrict (toVal v x) < ↑γ

case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
x : R
hx : Valued.v.restrict x < Valued.v.restrict r.ofVal / Valued.v.restrict s.ofVal
⊢ 0 < Valued.v.restrict s.ofVal
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
x : R
hx : v x * v s.ofVal < v r.ofVal
⊢ Valued.v.restrict (toVal v x) * Valued.v.restrict s < Valued.v.restrict r

Tactic:
← map_mul,

Goal state after:
case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
x : R
hx : v x * v s.ofVal < v r.ofVal
⊢ Valued.v.restrict (toVal v x * s) < Valued.v.restrict r
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 : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ v (x⁻¹ * (y - x) * y⁻¹) = v x⁻¹ * v (y - x) * v y⁻¹

Tactic:
Valuation.map_mul

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ v (x⁻¹ * (y - x)) * v y⁻¹ = v x⁻¹ * v (y - x) * v y⁻¹
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 : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ v (x⁻¹ * (y - x)) * v y⁻¹ = v x⁻¹ * v (y - x) * v y⁻¹

Tactic:
Valuation.map_mul

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ v x⁻¹ * v (y - x) * v y⁻¹ = v x⁻¹ * v (y - x) * v y⁻¹
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
x : (ofClass Valued.v).ValueGroup₀ˣ
u : ↥(ofClass Valued.v).valueGroup := WithZero.unzero ⋯
a : R
ha : (ofClass Valued.v) a ≠ 0
y✝ : R
hu : (ofClass Valued.v) a * ↑↑u = (ofClass Valued.v) y✝
y₀ : (ofClass Valued.v).ValueGroup₀ := h_val.orderMonoidIso ↑x
hy₀_def : y₀ = h_val.orderMonoidIso ↑x
hy₀_ne_zero : y₀ ≠ 0
y : (ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 y₀ hy₀_ne_zero
hy_def : y = Units.mk0 y₀ hy₀_ne_zero
b : R
⊢ Valued.v.restrict b < ↑y → Valued.v.restrict b < ↑x

Tactic:
hb

Goal state after:
case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
x : (ofClass Valued.v).ValueGroup₀ˣ
u : ↥(ofClass Valued.v).valueGroup := WithZero.unzero ⋯
a : R
ha : (ofClass Valued.v) a ≠ 0
y✝ : R
hu : (ofClass Valued.v) a * ↑↑u = (ofClass Valued.v) y✝
y₀ : (ofClass Valued.v).ValueGroup₀ := h_val.orderMonoidIso ↑x
hy₀_def : y₀ = h_val.orderMonoidIso ↑x
hy₀_ne_zero : y₀ ≠ 0
y : (ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 y₀ hy₀_ne_zero
hy_def : y = Units.mk0 y₀ hy₀_ne_zero
b : R
hb : Valued.v.restrict b < ↑y
⊢ Valued.v.restrict b < ↑x
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀'
K : Type u_7
inst✝ : Field K
v : Valuation K Γ₀
w : Valuation K Γ₀'
h : v.IsEquiv w
x : v.Completion
⊢ Valued.v x ≤ 1 ↔ Valued.v ((mapEquiv h.uniformEquiv) x) ≤ 1

Tactic:
induction x using induction_on with

Goal state after:
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
⊢ DenselyOrdered X ↔ Subsingleton X

Tactic:
by
  refine ⟨fun H ↦ ?_, fun h ↦ h.instDenselyOrdered⟩
  rw [← not_nontrivial_iff_subsingleton, nontrivial_iff_lt]
  rintro ⟨a, b, hab⟩
  exact not_lt_of_denselyOrdered_of_locallyFinite a b hab

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

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

Tactic:
refine lt_of_lt_of_le H₁ ?_
          grw [Units.min_val, mul_assoc, Units.val_mul, Units.val_mul, x_in₀]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mp
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
⊢ ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) → Nonempty (G ≃+o ℤ)

pp: case mpr
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
⊢ Nonempty (G ≃+o ℤ) → {x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2

Tactic:
· intro h
    replace h : WellFounded (α := {x : G | 0 ≤ x}) (· < ·) := h
    rw [WellFounded.wellFounded_iff_has_min] at h
    by_cases! H : ∀ (x : G) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y -- Archimedean
    · replace H : Archimedean G := ⟨H⟩
      rw [LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered]
      intro hd
      obtain ⟨y, hy⟩ := exists_ne (0 : G)
      wlog! hy' : 0 < y generalizing y
      · refine this (-y) ?_ ?_
        · simp [hy]
        · simp [lt_of_le_of_ne hy' hy]
      obtain ⟨⟨z, hz⟩, hz', hz''⟩ := h ({x | ⟨0, le_rfl⟩ < x}) ⟨⟨y, hy'.le⟩, hy'⟩
      obtain ⟨w, hw, hw'⟩ := exists_between hz'
      exact hz'' ⟨w, hw.le⟩ hw hw'
    · exfalso
      obtain ⟨x, y, hy0, H⟩ := H
      obtain ⟨_, ⟨n, rfl⟩, hz⟩ :=
        h (Set.range (fun n : ℕ ↦ ⟨x - n • y, sub_nonneg.mpr (H _).le⟩)) (range_nonempty _)
      refine hz ⟨x - (n + 1) • y, sub_nonneg.mpr (H _).le⟩ ⟨_, rfl⟩ ?_
      simp [add_smul, hy0]

Goal state after:
case mpr
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
⊢ Nonempty (G ≃+o ℤ) → {x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: 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
⊢ ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ))

Tactic:
rw [this, LinearOrderedCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete]
    refine Nonempty.congr (fun f ↦ ⟨?_, ?_⟩) (fun f ↦ ⟨?_, ?_⟩)
    · exact WithZero.withZeroUnitsEquiv.symm.trans f.withZero
    · 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]
    · exact MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans f)
    · intros
      rw [← WithZero.coe_le_coe]
      simp

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

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

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 ∈ {x | x ≤ g} \ {0}, ∀ b ∈ {x | x ≤ g} \ {0}, a > b → Function.onFun (fun x1 x2 ↦ x1 < x2) (fun x ↦ x⁻¹) a b

Tactic:
· intro x
    simp only [mem_sdiff, mem_ofPred_eq, mem_singleton_iff, and_imp]
    intro hxg hx
    refine inv_anti₀ ?_ hxg
    simp [zero_lt_iff, hx]

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 ∈ {x | x ≤ g} \ {0}, ∀ b ∈ {x | x ≤ g} \ {0}, a > b → Function.onFun (fun x1 x2 ↦ x1 < x2) (fun x ↦ x⁻¹) a b
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔ ∃ d, (coeff d) f ≠ 0

Tactic:
by
  simp only [MvPowerSeries.ext_iff, ne_eq, coeff_zero, not_forall]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
φ ψ : R⟦X⟧
h : φ * X ^ k = ψ * X ^ k
⊢ φ = ψ

Tactic:
rw [PowerSeries.ext_iff] at h ⊢
  intro n
  simpa using h (n + k)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
φ ψ : R⟦X⟧
h : X ^ k * φ = X ^ k * ψ
⊢ φ = ψ

Tactic:
rw [PowerSeries.ext_iff] at h ⊢
  intro n
  simpa using h (n + k)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
⊢ f ((coeff n) 1) = (coeff n) 1

Tactic:
rw [coeff_one, coeff_one]

Goal state after:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
⊢ f (if n = 0 then 1 else 0) = if n = 0 then 1 else 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

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

Tactic:
dsimp at h

Goal state after:
case mp.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
h : i = single s n
⊢ n ≤ m s
Module: Mathlib.RingTheory.MvPowerSeries.Basic

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

Tactic:
rw [coeff_X_pow]

Goal state after:
case pos.h₀
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
⊢ ((if (i, j).1 = single s n then 1 else 0) * (coeff (i, j).2) fun m ↦ (coeff (m + single s n)) φ) = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
⊢ v.intValuation x ≤ 1

Tactic:
by
  obtain rfl | hx := eq_or_ne x 0
  · simp
  · rw [v.intValuation_if_neg hx, ← exp_zero, exp_le_exp, Right.neg_nonpos_iff]
    exact Int.natCast_nonneg _

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

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

Tactic:
rw [coeff_X_pow]

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
⊢ ((if (i, j).1 = single s n then 1 else 0) * (coeff (i, j).2) fun m ↦ (coeff (m + single s n)) φ) = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

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

Tactic:
Ideal.dvd_span_singleton,

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
hr : r = 0
⊢ 0 ≤ exp (-↑n) ↔ 0 ∈ v.asIdeal ^ 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
⊢ n ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors ↔ v.asIdeal ^ n ∣ Ideal.span {r}

Tactic:
Ideal.dvd_span_singleton,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
hr : ¬r = 0
⊢ n ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors ↔ r ∈ v.asIdeal ^ n
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff d) f ≠ 0
⊢ weightedOrder w f ≤ ↑((weight w) d)

Tactic:
rw [weightedOrder, dif_neg]
  · simp only [ne_eq, Nat.cast_le, Nat.find_le_iff]
    exact ⟨weight w d, le_rfl, d, h, rfl⟩
  · exact (f.ne_zero_iff_exists_coeff_ne_zero_and_weight w).mpr ⟨weight w d, d, h, rfl⟩

Goal state after:
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:
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.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a s : R
hs : s ∈ v.asIdeal.primeCompl
x✝ : s ∈ v.asIdeal
⊢ a ∉ v.asIdeal

Tactic:
by contradiction

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

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

Tactic:
hb

Goal state after:
case neg.right
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ (coeff b) ((monomial d) a) = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
hv : (valuation K v) x ≤ 1
n : R
d : ↥v.asIdeal.primeCompl
hnd : x * (algebraMap R K) n = (algebraMap R K) ↑d
⊢ (valuation K v) ↑↑d ≤ (valuation K v) x * (valuation K v) ↑n

Tactic:
← map_mul,

Goal state after:
case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
hv : (valuation K v) x ≤ 1
n : R
d : ↥v.asIdeal.primeCompl
hnd : x * (algebraMap R K) n = (algebraMap R K) ↑d
⊢ (valuation K v) ↑↑d ≤ (valuation K v) (x * ↑n)
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Zero α
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq ι
f✝ g✝ : ι →₀ α
i✝ : ι
a : α
f g : ι →₀ α
i : ι
⊢ i ∈ f.support ∪ g.support ↔ Icc (f i) (g i) ≠ 0

Tactic:
rw [mem_union, ← not_iff_not, not_or, notMem_support_iff, notMem_support_iff, not_ne_iff]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝³ : Zero α
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq ι
f✝ g✝ : ι →₀ α
i✝ : ι
a : α
f g : ι →₀ α
i : ι
⊢ f i = 0 ∧ g i = 0 ↔ Icc (f i) (g i) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case right
σ : 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 : σ →₀ ℕ
⊢ (weight w) b < n → (coeff b) (f + g) = 0

Tactic:
hb

Goal state after:
case right
σ : 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
⊢ (coeff b) (f + g) = 0
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : Lattice α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ #(uIcc f g) = ∏ i ∈ f.support ∪ g.support, #(uIcc (f i) (g i))

Tactic:
rw [← support_inf_union_support_sup]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : Lattice α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ #(uIcc f g) = ∏ i ∈ (f ⊓ g).support ∪ (f ⊔ g).support, #(uIcc (f i) (g i))
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = p
⊢ ↑p < weightedOrder w f

Tactic:
exact hf

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:
hb

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
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
⊢ ¬Valued.v a = 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
r : R
i : M
hi : i ∈ A
⊢ 0 ∈ A

Tactic:
exact zero_mem _

Goal state after:
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
⊢ 0 ∈ A

Tactic:
exact zero_mem _

Goal state after: