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

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
Hx : v x = 0
⊢ ∃ j,
    ↑(v.ltAddSubgroup ((Units.map ↑embedding) j)) ⊆
      (fun x_1 ↦ x_1 * x) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))

Tactic:
use 1

Goal state after:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
Hx : v x = 0
⊢ ↑(v.ltAddSubgroup ((Units.map ↑embedding) 1)) ⊆ (fun x_1 ↦ x_1 * x) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ 𝓝 0 = ⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)

Tactic:
by
  rw [nhds_eq_update, update_self]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
h : ∀ (x : R), x ≠ 0 → v x = 1
⊢ ∃ γ, ∀ (y : R), v.restrict y < ↑γ → y = 0

Tactic:
use 1

Goal state after:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
h : ∀ (x : R), x ≠ 0 → v x = 1
⊢ ∀ (y : R), v.restrict y < ↑1 → y = 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: K : Type u_2
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
a : K
⊢ 0 =ᵥ a ↔ 0 = a

Tactic:
veq_comm,

Goal state after:
K : Type u_2
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
a : K
⊢ a =ᵥ 0 ↔ 0 = a
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
h : ∀ (x : R), x ≠ 0 → v x = 1
⊢ ∃ γ, ∀ (y : R), v.restrict y < ↑γ → y = 0

Tactic:
use 1

Goal state after:
case h
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
h : ∀ (x : R), x ≠ 0 → v x = 1
⊢ ∀ (y : R), v.restrict y < ↑1 → y = 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: 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 y : R
r s : ↥(posSubmonoid R)
⊢ v x * v ↑r = v y * v ↑s →
    (restrict₀ (ofClass v)) x / (restrict₀ (ofClass v)) ↑s = (restrict₀ (ofClass v)) y / (restrict₀ (ofClass v)) ↑r

Tactic:
div_eq_div_iff

Goal state after:
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 y : R
r s : ↥(posSubmonoid R)
⊢ v x * v ↑r = v y * v ↑s →
    (restrict₀ (ofClass v)) x * (restrict₀ (ofClass v)) ↑r = (restrict₀ (ofClass v)) y * (restrict₀ (ofClass v)) ↑s

case hb
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 y : R
r s : ↥(posSubmonoid R)
⊢ (restrict₀ (ofClass v)) ↑s ≠ 0

case hd
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 y : R
r s : ↥(posSubmonoid R)
⊢ (restrict₀ (ofClass v)) ↑r ≠ 0
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x ↦ x * x.hatInv
c : K → hat K := fun x ↦ ↑x
⊢ f x = 1

Tactic:
have cont : ContinuousAt f x := by fun_prop

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x ↦ x * x.hatInv
c : K → hat K := fun x ↦ ↑x
cont : ContinuousAt f x
⊢ f x = 1
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 : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : v (a * ↑s) < v (b * ↑r)
⊢ embedding ((restrict₀ (ofClass v)) a) * embedding ((restrict₀ (ofClass v)) ↑s) <
    embedding ((restrict₀ (ofClass v)) b) * embedding ((restrict₀ (ofClass v)) ↑r)

Tactic:
rw [embedding_restrict₀ a, embedding_restrict₀ b, embedding_restrict₀ r.1,
      embedding_restrict₀ s.1]

Goal state after:
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : v (a * ↑s) < v (b * ↑r)
⊢ (ofClass v) a * (ofClass v) ↑s < (ofClass v) b * (ofClass v) ↑r
Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y u : R
hi : u * x ∈ I
v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I ↑(span {v * x}) = span {y}
⊢ ∃ z, z * y = u

Tactic:
← mem_span_singleton',

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y u : R
hi : u * x ∈ I
v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I ↑(span {v * x}) = span {y}
⊢ u ∈ span {y}
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).dblU (⇑f ∘ P) = f (W'.dblU P)

Tactic:
simp only [dblU_eq]

Goal state after:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).a₁ * (⇑f ∘ P) y * (⇑f ∘ P) z -
      (3 * (⇑f ∘ P) x ^ 2 + 2 * (W'.map f).a₂ * (⇑f ∘ P) x * (⇑f ∘ P) z ^ 2 + (W'.map f).a₄ * (⇑f ∘ P) z ^ 4) =
    f (W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4))
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case neg
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := ⋯.some
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : ↑x = ↑(π.val ^ n) * ↑↑u
hn : ¬n = 0
⊢ Submodule.IsPrincipal P

Tactic:
· rw [← Subring.coe_mul, SetLike.coe_eq_coe] at hu
      rw [hu, Ideal.mul_unit_mem_iff_mem P u.isUnit,
        IsPrime.pow_mem_iff_mem hP _ (pos_iff_ne_zero.mpr hn),
        ← Ideal.span_singleton_le_iff_mem] at hx_mem
      replace hx_mem := π.is_generator ▸ hx_mem
      rw [← Ideal.IsMaximal.eq_of_le (IsLocalRing.maximalIdeal.isMaximal K₀) hP.ne_top hx_mem]
      exact ⟨π.1, π.is_generator⟩

Goal state after:
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✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
⊢ maximalIdeal ↥v.valuationSubring ≠ ⊥

Tactic:
rw [ne_eq, ← isField_iff_maximalIdeal_eq]; exact valuationSubring_not_isField v

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

Goal state before:
pp: 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
⊢ UniformContinuous ⇑(WithVal.congr v w (RingEquiv.refl R))

Tactic:
have hcomp : WithVal.congr v w (.refl R) = _ := RingEquiv.ext_iff.mpr (congrFun rfl)

Goal state after:
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
hcomp : WithVal.congr v w (RingEquiv.refl R) = WithVal.congr v w (RingEquiv.refl R)
⊢ UniformContinuous ⇑(WithVal.congr v w (RingEquiv.refl R))
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero G
inst✝ : MulArchimedean G
b : Gˣ
ha : 0 < 1
⊢ ∃ n, 0 ^ n < ↑b

Tactic:
use 1

Goal state after:
case h
G : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero G
inst✝ : MulArchimedean G
b : Gˣ
ha : 0 < 1
⊢ 0 ^ 1 < ↑b
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
⊢ min (↑γ * (↑γ₀ * ↑γ₀)) ↑γ₀ ≤ min (↑γ * (v.restrict x * v.restrict x)) (v.restrict x)

Tactic:
x_in₀

Goal state after:
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
⊢ min (↑γ * (v.restrict x * v.restrict x)) (v.restrict x) ≤ min (↑γ * (v.restrict x * v.restrict x)) (v.restrict x)
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : hat K
h : x ≠ 0
⊢ IsClosed {b | ∃ r, extensionValuation b = v r}

Tactic:
simp only [extensionValuation_toFun]
      have hr (r : K) : ValueGroup₀.embedding (restrict₀ (.ofClass hv.v) r) = v r := by
        simp [embedding_restrict₀]
      have h (a b : ValueGroup₀ (.ofClass hv.v)) :
          ValueGroup₀.embedding a = ValueGroup₀.embedding b ↔ a = b := by
        rw [embedding_strictMono.injective.eq_iff]
      simp_rw [← hr, ← Valuation.restrict_def, h]
      convert! valuation_isClosedMap.isClosed_range.preimage (continuous_extension (hv := hv))
      simp_rw [eq_comm (a := extension _)]
      #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
      (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
      goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in
      the new canonicalizer; a minimization would help. The original proof was: `grind` -/
      ext; simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
⊢ (map f) X = X

Tactic:
ext
  simp [coeff_X, apply_ite f]

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

Goal state before:
pp: case empty
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
⊢ (coeff d) (∏ j ∈ ∅, f j) = ∑ l ∈ ∅.finsuppAntidiag d, ∏ i ∈ ∅, (coeff (l i)) (f i)

Tactic:
simp only [prod_empty, sum_const, nsmul_eq_mul, mul_one, coeff_one, finsuppAntidiag_empty]

Goal state after:
case empty
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
⊢ (if d = 0 then 1 else 0) = ↑(#(if d = 0 then {0} else ∅))
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
⊢ (valuation K v) (↑a / ↑b) ≤ 1 ↔ b ∉ v.asIdeal

Tactic:
refine ⟨fun hv ↦ ?_, fun hb ↦ by
    simp [valuation_of_algebraMap, intValuation_eq_one_iff.2 hb, intValuation_le_one]⟩

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
a b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hv : (valuation K v) (↑a / ↑b) ≤ 1
⊢ b ∉ v.asIdeal
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
⊢ ∃ π, (valuation K v) ↑π = exp (-1)

Tactic:
have ⟨π, hπ⟩ := intValuation_exists_uniformizer v

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
π : R
hπ : v.intValuation π = exp (-1)
⊢ ∃ π, (valuation K v) ↑π = exp (-1)
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case neg.hnc
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₀ˣ
hx0 : ¬x = 0
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : v y = embedding ↑γ
⊢ y ≠ 0

Tactic:
apply_fun v

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₀ˣ
hx0 : ¬x = 0
y : K := ⋯
hy_def : y = ⋯.choose
hy : v y = embedding ↑γ
⊢ v y ≠ v 0
Module: Mathlib.RingTheory.PowerSeries.Basic

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

Tactic:
exact not_isField_of_subsingleton _

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

Tactic:
rw [hm', pow_add, hf, zero_mul]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0
H : weightedOrder w f < ↑n
⊢ ↑(weightedOrder w f).toNat = weightedOrder w f

Tactic:
rw [natCast_toNat_eq_self]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0
H : weightedOrder w f < ↑n
⊢ weightedOrder w f ≠ ⊤
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
k : ℕ
ih : ∀ m ≤ k, ∀ {x : σ →₀ ℕ}, degree x < n → MvPolynomial.coeff x ((truncTotal n) p ^ m) = (coeff x) (p ^ m)
x : σ →₀ ℕ
h : degree x < n
x✝ : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x✝ ∈ antidiagonal x
⊢ degree x✝.1 < n

Tactic:
by grind [mem_antidiagonal]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
k : ℕ
ih : ∀ m ≤ k, ∀ {x : σ →₀ ℕ}, degree x < n → MvPolynomial.coeff x ((truncTotal n) p ^ m) = (coeff x) (p ^ m)
x : σ →₀ ℕ
h : degree x < n
x✝ : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x✝ ∈ antidiagonal x
⊢ degree x✝.2 < n

Tactic:
by grind [mem_antidiagonal]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), (coeff n) p ∈ T
d : σ →₀ ℕ
hd : ↑(degree d) < p.order
⊢ (coeff d) (p.toSubring T hp) = 0

Tactic:
exact_mod_cast (coeff_toSubring p T hp) ▸ (coeff_of_lt_order hd)

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

Goal state before:
pp: R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
a b : R
ha : IsTopologicallyNilpotent a
hab : Commute a b
⊢ IsTopologicallyNilpotent (a * b)

Tactic:
by
  simp_rw [IsTopologicallyNilpotent, hab.mul_pow]
  exact IsLinearTopology.tendsto_mul_zero_of_left _ _ ha

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

Goal state before:
pp: case ofCompletion
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
y : adicCompletion K v
toCompletion✝ : (HeightOneSpectrum.valuation K v).Completion
h : { toCompletion := toCompletion✝ }.toCompletion = y.toCompletion
⊢ { toCompletion := toCompletion✝ } = y

Tactic:
cases y

Goal state after:
case ofCompletion.ofCompletion
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
toCompletion✝¹ toCompletion✝ : (HeightOneSpectrum.valuation K v).Completion
h : { toCompletion := toCompletion✝¹ }.toCompletion = { toCompletion := toCompletion✝ }.toCompletion
⊢ { toCompletion := toCompletion✝¹ } = { toCompletion := toCompletion✝ }
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
g : MvPowerSeries σ R
⊢ HasSum f g ↔ ∀ (d : σ →₀ ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) g)

Tactic:
by
  simp_rw [HasSum, ← map_sum]
  apply tendsto_iff_coeff_tendsto

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

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (fun i ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
hempty : IsEmpty ι
⊢ Summable f

pp: case inr
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (fun i ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
hempty : Nonempty ι
⊢ Summable f

Tactic:
· apply summable_empty

Goal state after:
case inr
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (fun i ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
hempty : Nonempty ι
⊢ Summable f
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

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

Tactic:
use 1

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
a : adicCompletion K v
ha : a ∈ adicCompletionIntegers K v
⊢ 1 ∈ R⁰ ∧ a * ↑1 ∈ adicCompletionIntegers K v
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
H : IsLinearTopology R M
⊢ IsLinearTopology Rᵐᵒᵖ M

Tactic:
exact mk_of_hasBasis' Rᵐᵒᵖ (IsLinearTopology.hasBasis_submodule R)
      fun S r m hm ↦ unop_smul_eq_smul r m ▸ S.smul_mem _ hm

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

Goal state before:
pp: R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
g : R⟦X⟧
⊢ HasSum f g ↔ ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) g)

Tactic:
by
  simp_rw [HasSum, ← map_sum]
  apply tendsto_iff_coeff_tendsto

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

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
h : Tendsto (fun i ↦ (f i).order) atTop (𝓝 ⊤)
hempty : IsEmpty ι
⊢ Summable f

pp: case inr
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
h : Tendsto (fun i ↦ (f i).order) atTop (𝓝 ⊤)
hempty : Nonempty ι
⊢ Summable f

Tactic:
· apply summable_empty

Goal state after:
case inr
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
h : Tendsto (fun i ↦ (f i).order) atTop (𝓝 ⊤)
hempty : Nonempty ι
⊢ Summable f
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : UniformSpace R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : IsUniformAddGroup R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : CompleteSpace S
inst✝² : T2Space S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁹.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑φ
ha : HasEval a
ε : MvPowerSeries σ R → S
hε : Continuous[instTopologicalSpace R, inst✝⁷.toTopologicalSpace] ε
h : ∀ (p : MvPolynomial σ R), ε ↑p = MvPolynomial.eval₂ φ a p
⊢ ε = eval₂ φ a

Tactic:
by
  rw [← coe_eval₂Hom hφ ha]
  exact (toMvPowerSeries_isDenseInducing.extend_unique h hε).symm

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: case a
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ 2 ^ ℵ₀ ≤ x ^ ℵ₀

Tactic:
exact power_le_power_right h₁

Goal state after:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case a.convert_1
⊢ ℝ

pp: case a.convert_2
⊢ 0 < ?a.convert_1✝

pp: case a.convert_3
⊢ ?a.convert_1✝ < 1 / 2

Tactic:
· exact 1 / 3

Goal state after:
case a.convert_2
⊢ 0 < 1 / 3

case a.convert_3
⊢ 1 / 3 < 1 / 2
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ℵ₀ < 𝔠

Tactic:
exact aleph0_lt_continuum

Goal state after:
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : s.Nonempty
⊢ egauge 𝕜 s 0 = 0

Tactic:
by
  have : 0 ∈ (0 : 𝕜) • s := by simp [zero_smul_set hs]
  simpa using egauge_le_of_mem_smul this

Goal state after: