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

Goal state before:
pp: case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
⊢ ↑(B i) ∈ {U | ∃ i, U = ↑(B i)}

pp: case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
⊢ ↑(B i) ⊆ (fun x ↦ x₀ • x) ⁻¹' ↑(B i)

Tactic:
· use i

Goal state after:
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
⊢ ↑(B i) ⊆ (fun x ↦ x₀ • x) ⁻¹' ↑(B i)
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := ⋯
this : TopologicalSpace M := ⋯
a : M
a_in : a ∈ (B i).toAddSubgroup.carrier
⊢ ↑(B i) ∈ hB.toModuleFilterBasis.toAddGroupFilterBasis

pp: case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := ⋯
this : TopologicalSpace M := ⋯
a : M
a_in : a ∈ (B i).toAddSubgroup.carrier
⊢ (fun y ↦ a + y) '' ↑(B i) ⊆ (B i).toAddSubgroup.carrier

Tactic:
· use i

Goal state after:
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := ⋯
this : TopologicalSpace M := ⋯
a : M
a_in : a ∈ (B i).toAddSubgroup.carrier
⊢ (fun y ↦ a + y) '' ↑(B i) ⊆ (B i).toAddSubgroup.carrier
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
u : F
hu : IsUnit u
⊢ toAffine W (u • P) = toAffine W P

Tactic:
by
  by_cases hP : W.Nonsingular P
  · by_cases hPz : P z = 0
    · rw [toAffine_of_Z_eq_zero <| mul_eq_zero_of_right u hPz, toAffine_of_Z_eq_zero hPz]
    · rw [toAffine_of_Z_ne_zero ((nonsingular_smul P hu).mpr hP) <| mul_ne_zero hu.ne_zero hPz,
        toAffine_of_Z_ne_zero hP hPz, Affine.Point.some.injEq]
      simp only [smul_fin3_ext, mul_pow, mul_div_mul_left _ _ (hu.pow _).ne_zero, and_self]
  · rw [toAffine_of_singular <| hP.comp (nonsingular_smul P hu).mp, toAffine_of_singular hP]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : R
y : ↥(posSubmonoid R)
h : x ≤ᵥ 0
⊢ x * ↑1 ≤ᵥ 0 * ↑y

Tactic:
by simpa using h

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

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

Tactic:
set u : (ValueGroup₀ (.ofClass v))ˣ := Units.mk0 ((restrict₀ (.ofClass v)) x)
          (by simp [restrict₀_apply]; aesop) with hu_def

Goal state after:
case inr
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
u : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu_def : u = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
⊢ ∃ j,
    ↑(v.ltAddSubgroup ((Units.map ↑embedding) j)) ⊆
      (fun x_1 ↦ x * x_1) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

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

Tactic:
set u : (ValueGroup₀ (.ofClass v))ˣ := Units.mk0 ((restrict₀ (.ofClass v)) x)
          (by simp [restrict₀_apply]; aesop) with hu_def

Goal state after:
case inr
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
u : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu_def : u = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
⊢ ∃ j,
    ↑(v.ltAddSubgroup ((Units.map ↑embedding) j)) ⊆
      (fun x_1 ↦ x_1 * x) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : ¬w ≤ᵥ 0
hz : ¬z ≤ᵥ 0
h : x * ↑v ≤ᵥ z * ↑s
⊢ z * ↑s * (↑t * w) =ᵥ w * ↑t * ↑s * z

Tactic:
grw [veq_mul_comm, veq_mul_comm _ w, veq_mul_comm z, ← mul_assoc]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
x : ↥(posSubmonoid R)
⊢ ¬↑x ≤ᵥ 0

Tactic:
exact x.prop

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
⊢ ContinuousAt hatInv x

Tactic:
by
  refine isDenseInducing_coe.continuousAt_extend ?_
  apply mem_of_superset (compl_singleton_mem_nhds h)
  intro y y_ne
  rw [mem_compl_singleton_iff] at y_ne
  apply CompleteSpace.complete
  have : (fun (x : K) => (↑x⁻¹ : hat K)) =
      ((fun (y : K) => (↑y : hat K)) ∘ (fun (x : K) => (x⁻¹ : K))) := by
    simp [Function.comp_def]
  rw [this, ← Filter.map_map]
  apply Cauchy.map _ (Completion.uniformContinuous_coe K)
  apply CompletableTopField.nice
  · have := isDenseInducing_coe.comap_nhds_neBot y
    apply cauchy_nhds.comap
    rw [Completion.comap_coe_eq_uniformity]
  · have eq_bot : 𝓝 (0 : hat K) ⊓ 𝓝 y = ⊥ := by
      by_contra h
      exact y_ne (eq_of_nhds_neBot <| neBot_iff.mpr h).symm
    rw [isDenseInducing_coe.nhds_eq_comap (0 : K), ← Filter.comap_inf]
    norm_cast
    rw [eq_bot]
    exact comap_bot

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 Γ
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 : ℕ
hn : m = ↑n
hpow : v (↑π.val ^ (-m) * ↑r) = 1
⊢ ↑π.val ^ (-m) * ↑r ∈ v.valuationSubring

Tactic:
apply le_of_eq hpow

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✝ : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : maximalIdeal ↥v.valuationSubring = span {r}
hr₀ : r ≠ 0
π : ↥v.valuationSubring
hπ : v.IsUniformizer ↑π
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : ↑r = ↑({ val := π, valuation_gt_one := hπ }.val ^ n) * ↑↑u
⊢ v.IsUniformizer ↑r

Tactic:
rw [Uniformizer.is_generator ⟨π, hπ⟩, span_singleton_eq_span_singleton] at hr

Goal state after:
Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝¹ : Field K
v : Valuation K Γ
inst✝ : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr₀ : r ≠ 0
π : ↥v.valuationSubring
hπ : v.IsUniformizer ↑π
hr : Associated { val := π, valuation_gt_one := hπ }.val r
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : ↑r = ↑({ val := π, valuation_gt_one := hπ }.val ^ n) * ↑↑u
⊢ v.IsUniformizer ↑r
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Jacobian R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).dblXYZ (⇑f ∘ P) = ⇑f ∘ (W'⁄A).dblXYZ P

Tactic:
by
  rw [← RingHom.coe_coe, ← map_dblXYZ, map_baseChange]

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 Γ₀
⊢ IsClosedMap ⇑v.restrict

Tactic:
refine IsClosedMap.of_nonempty ?_

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ ∀ (s : Set K), IsClosed[hv.toTopologicalSpace] s → s.Nonempty → IsClosed (⇑v.restrict '' s)
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
k : ℤ
hk : k ≤ 0
⊢ 1 ≤ (b ^ k)⁻¹

Tactic:
← zpow_neg

Goal state after:
case refine_2
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
k : ℤ
hk : k ≤ 0
⊢ 1 ≤ b ^ (-k)
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
⊢ v.restrict z₀ ≠ 0

Tactic:
Valuation.ne_zero_iff

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
⊢ z₀ ≠ 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 Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
this : γ₀ ≠ 0 → (x ∈ closure (Completion.coe' '' {x | v x < ↑γ}) ↔ γ₀ < ↑γ)
⊢ x ∈ closure (Completion.coe' '' {x | v x < ↑γ}) ↔ x ∈ {x | extensionValuation x < ↑γ}

Tactic:
rcases eq_or_ne γ₀ 0 with h | h
    · simp only [(Valuation.zero_iff _).mp h, mem_ofPred_eq, Valuation.map_zero, Units.zero_lt,
        iff_true]
      apply subset_closure
      exact ⟨0, by simp only [mem_ofPred_eq, Valuation.map_zero, Units.zero_lt, true_and]; rfl⟩
    · exact this h

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
⊢ ∀ (n : ℕ), (monomial 0) ↑(n + 1) = (monomial 0) ↑n + 1

Tactic:
simp [Nat.cast, monomial_zero_one]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
inst✝ : DecidableEq σ
⊢ antidiagonal n = antidiagonal n

Tactic:
Subsingleton.elim (Classical.decEq σ) ‹DecidableEq σ›

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
inst✝ : DecidableEq σ
⊢ antidiagonal n = antidiagonal n
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ X s ∣ φ ↔ ∀ (m : σ →₀ ℕ), m s = 0 → (coeff m) φ = 0

Tactic:
rw [← pow_one (X s : MvPowerSeries σ R), X_pow_dvd_iff]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ (∀ (m : σ →₀ ℕ), m s < 1 → (coeff m) φ = 0) ↔ ∀ (m : σ →₀ ℕ), m s = 0 → (coeff m) φ = 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
r : R
⊢ (valuation K v) ↑r < 1 ↔ r ∈ v.asIdeal

Tactic:
rw [valuation_of_algebraMap]; exact v.intValuation_lt_one_iff_mem r

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 b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
hv : b ∈ v.asIdeal
x✝ : a = 0
⊢ False

Tactic:
by simp_all

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
n d : R
hd : d ∈ nonZeroDivisors R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K n ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K n ⟨d, hd⟩ * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hn0 : n ≠ 0
hd0 : d ≠ 0
this : Ideal.span {d} ∣ Ideal.span {n}
⊢ IsLocalization.mk' K n ⟨d, hd⟩ ∈ (algebraMap R K).range

Tactic:
obtain ⟨z, rfl⟩ := Ideal.span_singleton_le_span_singleton.1 (Ideal.le_of_dvd this)

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
d : R
hd : d ∈ nonZeroDivisors R
hd0 : d ≠ 0
z : R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K (d * z) ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K (d * z) ⟨d, hd⟩ * (algebraMap R K) ↑(d * z, ⟨d, hd⟩).2 = (algebraMap R K) (d * z, ⟨d, hd⟩).1
hn0 : d * z ≠ 0
this : Ideal.span {d} ∣ Ideal.span {d * z}
⊢ IsLocalization.mk' K (d * z) ⟨d, hd⟩ ∈ (algebraMap R K).range
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: A : Type u_2
inst✝ : CommRing A
⊢ (rescale (-1)) X = -X

Tactic:
by
  rw [rescale_X, map_neg, map_one, neg_one_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
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
⊢ ∃ d, (coeff d) (f + g) ≠ 0 ∧ (weight w) d = n

Tactic:
refine ⟨d, ?_, hd⟩

Goal state after:
case left
σ : 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
⊢ (coeff d) (f + g) ≠ 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:
← intValuation_eq_one_iff_mem_primeCompl

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.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x y : K
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm (x * y)) }.toCompletion =
    ({ toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm x) } *
        { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm y) }).toCompletion

Tactic:
simp [UniformSpace.Completion.coe_mul]

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

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

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

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

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

pp: case mpr
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
⊢ (∀ (d : σ →₀ ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a) →
    ∃ a, ∀ (d : σ →₀ ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)

Tactic:
· rintro ⟨a, h⟩ n
    exact ⟨coeff n a, h n⟩

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
⊢ (∀ (d : σ →₀ ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a) →
    ∃ a, ∀ (d : σ →₀ ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)
Module: Mathlib.RingTheory.PowerSeries.Order

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

Tactic:
by simpa using h

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

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

pp: case mpr
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
⊢ (∀ (d : ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a) → ∃ a, ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)

Tactic:
· rintro ⟨a, h⟩ n
    exact ⟨coeff n a, h n⟩

Goal state after:
case mpr
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
⊢ (∀ (d : ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a) → ∃ a, ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)
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⟧
a : ℕ → R
h : ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) (a d)
⊢ ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) (mk a))

Tactic:
by simpa using h

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

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ.order = emultiplicity X φ

Tactic:
rcases eq_or_ne φ 0 with (rfl | hφ)
  · simp
  cases ho : order φ with
  | top => simp [hφ] at ho
  | coe n =>
    have hn : φ.order.toNat = n := by simp [ho]
    rw [← hn, eq_comm]
    apply le_antisymm _
    · apply le_emultiplicity_of_pow_dvd
      apply X_pow_order_dvd
    · apply Order.le_of_lt_add_one
      rw [← not_le, ← Nat.cast_one, ← Nat.cast_add, ← pow_dvd_iff_le_emultiplicity]
      rintro ⟨ψ, H⟩
      have := congr_arg (coeff n) H
      rw [X_pow_mul, coeff_mul_of_lt_order, ← hn] at this
      · exact coeff_order hφ this
      · rw [X_pow_eq, order_monomial]
        split_ifs
        · simp
        · rw [← hn, ENat.natCast_lt_natCast]
          simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝⁶ : CommRing R
τ : Type u_4
S : Type u_5
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
⊢ Continuous (subst a)

Tactic:
rw [subst_eq_eval₂]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝⁶ : CommRing R
τ : Type u_4
S : Type u_5
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
⊢ Continuous (eval₂ (algebraMap R (MvPowerSeries τ S)) a)
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
n : ℕ
hn : ∃ i, q ^ i = n
⊢ ((ofPowerSeries (q ^ k)) f) n = ((ofPowerSeries q) (PowerSeries.subst (PowerSeries.X ^ k) f)) n

pp: case neg
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
n : ℕ
hn : ¬∃ i, q ^ i = n
⊢ ((ofPowerSeries (q ^ k)) f) n = ((ofPowerSeries q) (PowerSeries.subst (PowerSeries.X ^ k) f)) n

Tactic:
· obtain ⟨i, rfl⟩ := hn
      rw [ofPowerSeries_apply_pow hq, PowerSeries.coeff_subst_X_pow hk]
      split_ifs with hn
      · obtain ⟨j, rfl⟩ := hn
        rw [pow_mul, ofPowerSeries_apply_pow (one_lt_pow' hq hk)]
        simp [hk]
      · rw [ofPowerSeries_apply (one_lt_pow' hq hk), Function.extend_apply', Pi.zero_apply]
        simp_rw [← pow_mul, Nat.pow_right_inj hq, eq_comm, ← dvd_def]
        exact hn

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
n : ℕ
hn : ¬∃ i, q ^ i = n
⊢ ((ofPowerSeries (q ^ k)) f) n = ((ofPowerSeries q) (PowerSeries.subst (PowerSeries.X ^ k) f)) n
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), PowerSeries.constantCoeff (f i) = 1
n✝ : ℕ
i : ι
n : ℕ
hi : n + 1 + 1 + 1 ≤ q i
hqi : 1 < q i
k : ℕ
hk : q i ^ k = n + 1 + 1
h : k = 0
⊢ False

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Analysis.Calculus.TangentCone.Defs

Goal state before:
pp: R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∃ᶠ (n : α) in l, x + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
this : Tendsto (fun n ↦ c n • d n) (l ⊓ 𝓟 {y | x + d y ∈ s}) (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)
⊢ y ∈ tangentConeAt R s x

Tactic:
rw [frequently_iff_neBot] at hds

Goal state after:
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds✝ : ∃ᶠ (n : α) in l, x + d n ∈ s
hds : (l ⊓ 𝓟 {x_1 | x + d x_1 ∈ s}).NeBot
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
this : Tendsto (fun n ↦ c n • d n) (l ⊓ 𝓟 {y | x + d y ∈ s}) (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)
⊢ y ∈ tangentConeAt R s x