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

Goal state before:
pp: ι : 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
⊢ ∀ {U : Set M}, U ∈ {U | ∃ i, U = ↑(B i)} → ∃ V ∈ 𝓝 0, ∃ W ∈ {U | ∃ i, U = ↑(B i)}, V • W ⊆ U

Tactic:
rintro _ ⟨i, rfl⟩
    use univ
    constructor
    · exact univ_mem
    · use B i
      constructor
      · use i
      · rintro _ ⟨a, -, m, hm, rfl⟩
        exact (B i).smul_mem _ hm

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Jacobian R
W : Jacobian F
inst✝ : DecidableEq F
point✝ : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P)
hPz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ fromAffine { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }

Tactic:
rw [Point.ext_iff, toAffineLift_eq, toAffine_of_Z_eq_zero hPz]
      exact Quotient.eq.mpr <| Setoid.symm <| equiv_zero_of_Z_eq_zero hP hPz

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

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z x✝¹ : R
y✝¹ : ↥(posSubmonoid R)
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x✝¹ y✝¹ ≤ ValueGroupWithZero.mk x✝ y✝ ∨
    ValueGroupWithZero.mk x✝ y✝ ≤ ValueGroupWithZero.mk x✝¹ y✝¹

Tactic:
ValueGroupWithZero.mk_le_mk,

Goal state after:
case mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z x✝¹ : R
y✝¹ : ↥(posSubmonoid R)
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ x✝¹ * ↑y✝ ≤ᵥ x✝ * ↑y✝¹ ∨ ValueGroupWithZero.mk x✝ y✝ ≤ ValueGroupWithZero.mk x✝¹ y✝¹
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 Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsValuativeTopology R
x : R
⊢ (𝓝 x).HasBasis (fun x ↦ True) fun γ ↦ {z | v.restrict (z - x) < ↑γ}

Tactic:
by
  simp [Filter.hasBasis_iff, v.mem_nhds_iff]

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

Goal state before:
pp: case refine_2
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : IsUniformAddGroup A
inst✝³ : IsTopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion A
a : A
⊢ Completion.map (fun x ↦ r • x) ↑a = ↑((algebraMap R A) r) * ↑a

Tactic:
· simp_rw [map_coe (uniformContinuous_const_smul r) a, Algebra.smul_def, coe_mul]

Goal state after:
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).dblU (⇑f ∘ P) = f ((W'⁄A).dblU P)

Tactic:
rw [← RingHom.coe_coe, ← map_dblU, map_baseChange]

Goal state after:
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).negDblY (⇑f ∘ P) = f ((W'⁄A).negDblY P)

Tactic:
rw [← RingHom.coe_coe, ← map_negDblY, map_baseChange]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mpr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha : a ≠ 1
⊢ (∃! k, a ^ k = b) → ∃ n, a ^ n = b

Tactic:
exact fun h ↦ h.exists

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₁
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ (valuation R K) (a⁻¹ * W.a₁) ≤ 1

Tactic:
simp only [map_mul, map_inv₀, map_pow, ha]

Goal state after:
case h.h₁
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ lmax⁻¹ * (valuation R K) W.a₁ ≤ 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₂
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ (valuation R K) ((a ^ 2)⁻¹ * W.a₂) ≤ 1

Tactic:
simp only [map_mul, map_inv₀, map_pow, ha]

Goal state after:
case h.h₂
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ (lmax ^ 2)⁻¹ * (valuation R K) W.a₂ ≤ 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₃
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ (valuation R K) ((a ^ 3)⁻¹ * W.a₃) ≤ 1

Tactic:
simp only [map_mul, map_inv₀, map_pow, ha]

Goal state after:
case h.h₃
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ (lmax ^ 3)⁻¹ * (valuation R K) W.a₃ ≤ 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₄
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ (valuation R K) ((a ^ 4)⁻¹ * W.a₄) ≤ 1

Tactic:
simp only [map_mul, map_inv₀, map_pow, ha]

Goal state after:
case h.h₄
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ (lmax ^ 4)⁻¹ * (valuation R K) W.a₄ ≤ 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₆
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ (valuation R K) ((a ^ 6)⁻¹ * W.a₆) ≤ 1

Tactic:
simp only [map_mul, map_inv₀, map_pow, ha]

Goal state after:
case h.h₆
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ (lmax ^ 6)⁻¹ * (valuation R K) W.a₆ ≤ 1
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case refine_1
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 γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : ∀ t ∈ 𝓝 x, ∃ y, ↑y ∈ t
y : K
hy₁ : v y < ↑γ
hy₂ : v y = γ₀
⊢ γ₀ < ↑γ

Tactic:
← hy₂

Goal state after:
case refine_1
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 γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : ∀ t ∈ 𝓝 x, ∃ y, ↑y ∈ t
y : K
hy₁ : v y < ↑γ
hy₂ : v y = γ₀
⊢ v y < ↑γ
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : Subsingleton R⟦X⟧
⊢ Subsingleton R

Tactic:
rw [subsingleton_iff] at h ⊢

Goal state after:
R : Type u_1
inst✝ : Semiring R
h : ∀ (x y : R⟦X⟧), x = y
⊢ ∀ (x y : R), x = y
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x * y})).factors))) =
    exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)) *
      exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors))

Tactic:
if_neg (mul_ne_zero hx hy),

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x * y})).factors)) =
    exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)) *
      exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors))
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
hab : extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑⋯.choose
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
⊢ embedding a = embedding b

Tactic:
have : hv.extensionValuation.restrict (algebraMap K _ x) =
       hv.extensionValuation.restrict (algebraMap _ _ y) := hab

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
hab : extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑⋯.choose
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ embedding a = embedding b
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
φ : A →ₐ[R] B
r : R
⊢ (↑↑(map ↑φ)).toFun ((algebraMap R (MvPowerSeries σ A)) r) = (algebraMap R (MvPowerSeries σ B)) r

Tactic:
by
    simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
      MonoidHom.coe_coe, MvPowerSeries.algebraMap_apply, map_C, RingHom.coe_coe, AlgHom.commutes]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ∞
h : ∀ (d : σ →₀ ℕ), ↑((weight fun x ↦ 1) d) < n → (coeff d) f = 0
⊢ n ≤ f.order

Tactic:
exact le_weightedOrder _ h

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
hf : constantCoeff f = 0
⊢ ↑n ≤ (f ^ n).order

Tactic:
refine .trans ?_ (le_order_pow n)

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
hf : constantCoeff f = 0
⊢ ↑n ≤ n • f.order
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
s : Set (adicCompletion K v)
x✝ : ∃ t ∈ 𝓝 0, toCompletion ⁻¹' t ⊆ s
t : Set (HeightOneSpectrum.valuation K v).Completion
ht : t ∈ 𝓝 0
hts : toCompletion ⁻¹' t ⊆ s
δ : (ofClass Valued.v).ValueGroup₀ˣ
hδ : {x | Valued.v.restrict x < ↑δ} ⊆ t
x : adicCompletion K v
hx : (valuation K v).restrict x < ↑((Units.mapEquiv (valueGroupOrderIso K v).symm.toMulEquiv) δ)
⊢ Valued.v.restrict x.toCompletion < ↑δ

Tactic:
simpa [← map_lt_map_iff (valueGroupOrderIso K v), valueGroupOrderIso_restrict] using hx

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
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
x : ↥(adicCompletionIntegers K v)
⊢ r • ↑x ∈ adicCompletionIntegers K v

Tactic:
rw [Algebra.smul_def]
      refine ValuationSubring.mul_mem _ _ _ ?_ x.2
      rw [algebraMap_adicCompletion]
      exact coe_algebraMap_mem _ _ v r

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

Goal state before:
pp: case mp.left
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff e) a ∈ J) → ∀ e_1 ≤ e, (coeff e_1) a ∈ K
x : R
hx : x ∈ ↑J
⊢ x ∈ ↑K

Tactic:
have (d' : _) : coeff d' (C (σ := σ) x) ∈ J := by
        rw [coeff_C]; split_ifs <;> [exact hx; exact J.zero_mem]

Goal state after:
case mp.left
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff e) a ∈ J) → ∀ e_1 ≤ e, (coeff e_1) a ∈ K
x : R
hx : x ∈ ↑J
this : ∀ (d' : σ →₀ ℕ), (coeff d') (C x) ∈ J
⊢ x ∈ ↑K
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f : PowerSeries R
hq : 1 < q
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 0 = 0

Tactic:
by simp [Nat.ne_zero_of_lt hq]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
a b : ℕ
hab : (a, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (a, b) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
ha : ∃ i, q ^ i = a
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 =
    0

Tactic:
by_cases hb : ∃ j, q ^ j = b

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
a b : ℕ
hab : (a, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (a, b) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
ha : ∃ i, q ^ i = a
hb : ∃ j, q ^ j = b
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 =
    0

case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
a b : ℕ
hab : (a, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (a, b) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
ha : ∃ i, q ^ i = a
hb : ¬∃ j, q ^ j = b
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 =
    0
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
T : Type u_6
inst✝¹¹ : CommRing T
inst✝¹⁰ : UniformSpace T
inst✝⁹ : T2Space T
inst✝⁸ : CompleteSpace T
inst✝⁷ : IsUniformAddGroup T
inst✝⁶ : IsTopologicalRing T
inst✝⁵ : IsLinearTopology T T
inst✝⁴ : Algebra R T
ε : MvPowerSeries τ S →ₐ[R] T
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
hε : Continuous ⇑ε
⊢ ⇑ε ∘ subst a = ⇑(aeval ⋯)

Tactic:
← comp_substAlgHom ha hε,

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
T : Type u_6
inst✝¹¹ : CommRing T
inst✝¹⁰ : UniformSpace T
inst✝⁹ : T2Space T
inst✝⁸ : CompleteSpace T
inst✝⁷ : IsUniformAddGroup T
inst✝⁶ : IsTopologicalRing T
inst✝⁵ : IsLinearTopology T T
inst✝⁴ : Algebra R T
ε : MvPowerSeries τ S →ₐ[R] T
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
hε : Continuous ⇑ε
⊢ ⇑ε ∘ subst a = ⇑(ε.comp (substAlgHom ha))
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
⊢ ∀ x ∈ (q ^ k).divisorsAntidiagonal,
    x ∉
        Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
          (Finset.antidiagonal k) →
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 x.1 *
          Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 x.2 =
        0

Tactic:
intro (a, b) hab h
          by_cases ha : ∃ i, q ^ i = a
          · by_cases hb : ∃ j, q ^ j = b
            · obtain ⟨i, rfl⟩ := ha
              obtain ⟨j, rfl⟩ := hb
              rw [Nat.mem_divisorsAntidiagonal, ← pow_add, Nat.pow_right_inj hq] at hab
              simp_rw [Finset.mem_map, not_exists, not_and, Finset.mem_antidiagonal] at h
              simpa using h (i, j) hab.1
            · rwa [mul_comm, Function.extend_apply', Pi.zero_apply, zero_mul]
          · rwa [Function.extend_apply', Pi.zero_apply, zero_mul]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ∃ i, q ^ i = a
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 =
    0

Tactic:
by_cases hb : ∃ j, q ^ j = b

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ∃ i, q ^ i = a
hb : ∃ j, q ^ j = b
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 =
    0

case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ∃ i, q ^ i = a
hb : ¬∃ j, q ^ j = b
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 =
    0
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
⊢ LSeriesSummable f s

Tactic:
obtain ⟨C, hC⟩ := h

Goal state after:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
⊢ LSeriesSummable f s
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: τ : Type u_3
S : Type u_4
inst✝ : CommRing S
n : τ →₀ ℕ
hn : n ≠ 0
s : S
⊢ MvPowerSeries.constantCoeff ((MvPowerSeries.monomial n) s) = 0

Tactic:
rw [← MvPowerSeries.coeff_zero_eq_constantCoeff, MvPowerSeries.coeff_monomial,
    if_neg hn.symm]

Goal state after: