mathlib-initiative/mathlib-tactics huggingface dataset:
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
I : Ideal ↥v.valuationSubring
⊢ Submodule.IsPrincipal I

Tactic:
suffices ∀ P : Ideal K₀, P.IsPrime → Submodule.IsPrincipal P by
    exact (IsPrincipalIdealRing.of_prime this).principal I

Goal state after:
Γ : 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 : Ideal ↥v.valuationSubring
⊢ ∀ (P : Ideal ↥v.valuationSubring), P.IsPrime → Submodule.IsPrincipal P
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 : v.IsEquiv w
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : R
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
x : WithVal v
hx :
  x ∈
    {x |
      Valued.v.restrict x <
        ↑(Units.mk0 (Valued.v.restrict ((equiv v).symm r) / Valued.v.restrict ((equiv v).symm s)) ⋯)}
⊢ (equiv v) x ∈ {x | Valued.v.restrict x < ↑γ}

Tactic:
let y := (WithVal.equiv v) x

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 : v.IsEquiv w
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : R
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
x : WithVal v
hx :
  x ∈
    {x |
      Valued.v.restrict x <
        ↑(Units.mk0 (Valued.v.restrict ((equiv v).symm r) / Valued.v.restrict ((equiv v).symm s)) ⋯)}
y : R := (equiv v) x
⊢ (equiv v) x ∈ {x | Valued.v.restrict x < ↑γ}
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
h : x = 0
⊢ y = 0

Tactic:
rw [h, v.map_zero] at key

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 : 0 = v y
h : x = 0
⊢ y = 0
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case refine_1
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
b : A
h : (valuation K (maximalIdeal A)) ((algebraMap A K) b) = 1
⊢ ∃ x ∈ IsUnit.submonoid A, (algebraMap A K) x = (algebraMap A K) b

Tactic:
valuation_eq_one_iff_notMem

Goal state after:
case refine_1
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
b : A
h : b ∉ (maximalIdeal A).asIdeal
⊢ ∃ x ∈ IsUnit.submonoid A, (algebraMap A K) x = (algebraMap A K) b
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
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
vz₀_ne : v.restrict z₀ ≠ 0
⊢ ∀ᶠ (b : hat K) in 𝓝 x₀, ∀ (a : K), ↑a = b → v.restrict a = v.restrict z₀

Tactic:
filter_upwards [nhds_right] with x x_in a ha

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
vz₀_ne : v.restrict z₀ ≠ 0
x : hat K
x_in : x ∈ (fun x ↦ x * x₀) '' V'
a : K
ha : ↑a = x
⊢ v.restrict a = v.restrict z₀
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K) (integralModel R W).a₁ = W.a₁

Tactic:
by
  conv_rhs => rw [← baseChange_integralModel_eq R W]
  simp [baseChange]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K) (integralModel R W).a₂ = W.a₂

Tactic:
by
  conv_rhs => rw [← baseChange_integralModel_eq R W]
  simp [baseChange]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K) (integralModel R W).a₃ = W.a₃

Tactic:
by
  conv_rhs => rw [← baseChange_integralModel_eq R W]
  simp [baseChange]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: A : Type u_2
inst✝⁴ : AddCommGroup A
inst✝³ : LinearOrder A
inst✝² : IsOrderedAddMonoid A
inst✝¹ : Archimedean A
inst✝ : Nontrivial A
⊢ IsAddCyclic A ↔ Nonempty (A ≃+o ℤ)

Tactic:
isAddCyclic_iff_nonempty_equiv_int

Goal state after:
A : Type u_2
inst✝⁴ : AddCommGroup A
inst✝³ : LinearOrder A
inst✝² : IsOrderedAddMonoid A
inst✝¹ : Archimedean A
inst✝ : Nontrivial A
⊢ Nonempty (A ≃+o ℤ) ↔ Nonempty (A ≃+o ℤ)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K) (integralModel R W).a₄ = W.a₄

Tactic:
by
  conv_rhs => rw [← baseChange_integralModel_eq R W]
  simp [baseChange]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K) (integralModel R W).a₆ = W.a₆

Tactic:
by
  conv_rhs => rw [← baseChange_integralModel_eq R W]
  simp [baseChange]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
⊢ (G ≃*o WithZero (Multiplicative ℤ)) → Gˣ ≃*o Multiplicative ℤ

Tactic:
intro f

Goal state after:
case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : G ≃*o WithZero (Multiplicative ℤ)
⊢ Gˣ ≃*o Multiplicative ℤ
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
⊢ (Gˣ ≃*o Multiplicative ℤ) → G ≃*o WithZero (Multiplicative ℤ)

Tactic:
intro f

Goal state after:
case refine_2
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
⊢ G ≃*o WithZero (Multiplicative ℤ)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K) (integralModel R W).b₂ = W.b₂

Tactic:
by
  conv_rhs => rw [← baseChange_integralModel_eq R W]
  simp [baseChange]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K) (integralModel R W).b₄ = W.b₄

Tactic:
by
  conv_rhs => rw [← baseChange_integralModel_eq R W]
  simp [baseChange]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K) (integralModel R W).b₆ = W.b₆

Tactic:
by
  conv_rhs => rw [← baseChange_integralModel_eq R W]
  simp [baseChange]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K) (integralModel R W).b₈ = W.b₈

Tactic:
by
  conv_rhs => rw [← baseChange_integralModel_eq R W]
  simp [baseChange]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K) (integralModel R W).c₄ = W.c₄

Tactic:
by
  conv_rhs => rw [← baseChange_integralModel_eq R W]
  simp [baseChange]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K) (integralModel R W).c₆ = W.c₆

Tactic:
by
  conv_rhs => rw [← baseChange_integralModel_eq R W]
  simp [baseChange]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K) (integralModel R W).Δ = W.Δ

Tactic:
by
  conv_rhs => rw [← baseChange_integralModel_eq R W]
  simp [baseChange]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_4
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
f : G₀ ≃*o WithZero (Multiplicative ℤ)
a✝ b✝ : G₀ˣ
⊢ (MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans ↑f)).toFun a✝ ≤
      (MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans ↑f)).toFun b✝ ↔
    a✝ ≤ b✝

Tactic:
← WithZero.coe_le_coe

Goal state after:
case refine_4
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
f : G₀ ≃*o WithZero (Multiplicative ℤ)
a✝ b✝ : G₀ˣ
⊢ ↑((MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans ↑f)).toFun a✝) ≤
      ↑((MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans ↑f)).toFun b✝) ↔
    a✝ ≤ b✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
C : VariableChange K
hC : MaximalFor (fun C ↦ IsIntegral R (C • W)) (fun C ↦ valuation_Δ_aux R (C • W)) C
j : VariableChange K
hj : IsIntegral R (j • C • W)
⊢ (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) 1 ≤ (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) j →
    (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) j ≤ (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) 1

Tactic:
← smul_assoc

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
C : VariableChange K
hC : MaximalFor (fun C ↦ IsIntegral R (C • W)) (fun C ↦ valuation_Δ_aux R (C • W)) C
j : VariableChange K
hj : IsIntegral R ((j • C) • W)
⊢ (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) 1 ≤ (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) j →
    (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) j ≤ (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
C : VariableChange K
hC : MaximalFor (fun C ↦ IsIntegral R (C • W)) (fun C ↦ valuation_Δ_aux R (C • W)) C
j : VariableChange K
hj : IsIntegral R ((j • C) • W)
h : (fun C ↦ valuation_Δ_aux R (C • W)) C ≤ (fun C ↦ valuation_Δ_aux R (C • W)) (j • C) →
  (fun C ↦ valuation_Δ_aux R (C • W)) (j • C) ≤ (fun C ↦ valuation_Δ_aux R (C • W)) C :=
  hC.right hj
⊢ valuation_Δ_aux R (C • W) ≤ valuation_Δ_aux R (j • C • W) → valuation_Δ_aux R (j • C • W) ≤ valuation_Δ_aux R (C • W)

Tactic:
← smul_assoc

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
C : VariableChange K
hC : MaximalFor (fun C ↦ IsIntegral R (C • W)) (fun C ↦ valuation_Δ_aux R (C • W)) C
j : VariableChange K
hj : IsIntegral R ((j • C) • W)
h : (fun C ↦ valuation_Δ_aux R (C • W)) C ≤ (fun C ↦ valuation_Δ_aux R (C • W)) (j • C) →
  (fun C ↦ valuation_Δ_aux R (C • W)) (j • C) ≤ (fun C ↦ valuation_Δ_aux R (C • W)) C :=
  hC.right hj
⊢ valuation_Δ_aux R (C • W) ≤ valuation_Δ_aux R ((j • C) • W) →
    valuation_Δ_aux R ((j • C) • W) ≤ valuation_Δ_aux R (C • W)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff n) (C a * φ) = a * (coeff n) φ

Tactic:
simpa using coeff_add_monomial_mul 0 n φ a

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
| constantCoeff φ ^ n' * (coeff 1) φ + ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1) * constantCoeff φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'

Tactic:
lhs

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
| constantCoeff φ ^ n' * (coeff 1) φ + ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1) * constantCoeff φ
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
hr : (valuation K v) ↑r = exp (-1)
⊢ ∃ π, (valuation K v) π = exp (-1)

Tactic:
use (algebraMap _ _ r)

Goal state after:
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 | (valuation K v).restrict x < ↑γ} ⊆ s

Tactic:
refine ⟨Units.mapEquiv (valueGroupOrderIso K v).symm.toMulEquiv δ, fun x hx ↦ hts (hδ ?_)⟩

Goal state after:
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 : x ∈ {x | (valuation K v).restrict x < ↑((Units.mapEquiv (valueGroupOrderIso K v).symm.toMulEquiv) δ)}
⊢ x.toCompletion ∈ {x | Valued.v.restrict x < ↑δ}
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
⊢ (weightedHomogeneousComponent w p) f = 0

Tactic:
by
  ext d
  rw [coeff_weightedHomogeneousComponent]
  split_ifs with hd
  · rw [coeff_zero]
    apply coeff_eq_zero_of_lt_weightedOrder w
    rw [hd]
    exact hf
  · rw [map_zero]

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

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

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ ≠ 0
⊢ (coeff (↑(Nat.find ⋯)).toNat) φ ≠ 0

Tactic:
generalize_proofs h

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h✝ : φ ≠ 0
h : ∃ n, (coeff n) φ ≠ 0
⊢ (coeff (↑(Nat.find h)).toNat) φ ≠ 0
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ ∑ m ∈ range n.succ, (Polynomial.monomial m) ((coeff m) f) = (trunc n) f + (Polynomial.monomial n) ((coeff n) f)

Tactic:
sum_range_succ,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ ∑ x ∈ range n, (Polynomial.monomial x) ((coeff x) f) + (Polynomial.monomial n) ((coeff n) f) =
    (trunc n) f + (Polynomial.monomial n) ((coeff n) f)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ ¬(v.intAdicAbv hb) r = 1 ↔ (v.intAdicAbv hb) r < 1

Tactic:
ne_iff_lt_iff_le

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ (v.intAdicAbv hb) r ≤ 1
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case zero
R : Type u_2
inst✝ : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ (trunc n) 1 = (trunc n) (f ^ 0)

Tactic:
pow_zero

Goal state after:
case zero
R : Type u_2
inst✝ : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ (trunc n) 1 = (trunc n) 1
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace M
inst✝ : IsLinearTopology R M
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : Tendsto m f (𝓝 0)
⊢ Tendsto (a • m) f (𝓝 0)

Tactic:
by
  rw [hasBasis_submodule R |>.tendsto_right_iff] at ha ⊢
  intro I hI
  filter_upwards [ha I hI] with i ai_mem
  exact I.smul_mem _ ai_mem

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

Goal state before:
pp: R : Type u_2
ι : Type u_3
inst✝ : CommRing R
k : ℕ
s : Finset ι
φ : R⟦X⟧
f : ι → R⟦X⟧
⊢ (∀ i ∈ s, ↑k < (f i).order) → (coeff k) (φ * ∏ i ∈ s, (1 - f i)) = (coeff k) φ

Tactic:
by
  classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s ha ih =>
    intro t
    simp only [Finset.mem_insert, forall_eq_or_imp] at t
    rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm, coeff_mul_one_sub_of_lt_order _ t.1]
    exact ih t.2

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

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
⊢ φ.order.toNat = n

Tactic:
simp [ho]

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

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

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

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
D : Set (σ →₀ ℕ)
I : TwoSidedIdeal R
⊢ (D, I).1.Finite ∧ ↑(D, I).2 ∈ 𝓝 0 → ∃ i', ↑i'.1 ∈ 𝓝 0 ∧ ↑(basis σ R i') ⊆ (D, I).1.pi fun x ↦ ↑(D, I).2

Tactic:
⟨hD, hI⟩

Goal state after:
case refine_1
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
D : Set (σ →₀ ℕ)
I : TwoSidedIdeal R
hD : (D, I).1.Finite
hI : ↑(D, I).2 ∈ 𝓝 0
⊢ ∃ i', ↑i'.1 ∈ 𝓝 0 ∧ ↑(basis σ R i') ⊆ (D, I).1.pi fun x ↦ ↑(D, I).2
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: ⊢ lift.{v, u_1} (2 ^ ℵ₀) = 𝔠

Tactic:
lift_two_power,

Goal state after:
⊢ 2 ^ lift.{v, u_1} ℵ₀ = 𝔠
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
⊢ Function.Injective (cantorFunction c)

Tactic:
intro f

Goal state after:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f : ℕ → Bool
⊢ ∀ ⦃a₂ : ℕ → Bool⦄, cantorFunction c f = cantorFunction c a₂ → f = a₂
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
⊢ Function.Injective (cantorFunction c)

Tactic:
intro f g hfg
  classical
    contrapose hfg with h
    have : ∃ n, f n ≠ g n := Function.ne_iff.mp h
    let n := Nat.find this
    have hn : ∀ k : ℕ, k < n → f k = g k := by
      intro k hk
      apply of_not_not
      exact Nat.find_min this hk
    cases fn : f n
    · apply _root_.ne_of_lt
      refine increasing_cantorFunction h1 h2 hn fn ?_
      apply Bool.eq_true_of_not_eq_false
      rw [← fn]
      apply Ne.symm
      exact Nat.find_spec this
    · apply _root_.ne_of_gt
      refine increasing_cantorFunction h1 h2 (fun k hk => (hn k hk).symm) ?_ fn
      apply Bool.eq_false_of_not_eq_true
      rw [← fn]
      apply Ne.symm
      exact Nat.find_spec this

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
⊢ ‖term f s n‖ ≤ ‖term g s n‖

Tactic:
simp only [norm_term_eq]
  split
  · rfl
  · gcongr

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
⊢ { toFun := Function.extend (fun x ↦ q ^ x) (fun x_1 ↦ (PowerSeries.coeff x_1) ((algebraMap R (PowerSeries R)) x)) 0,
        map_zero' := ⋯ }
      n =
    ((algebraMap R (ArithmeticFunction R)) x) n

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, coe_mk]
      by_cases hn : ∃ k, q ^ k = n
      · obtain ⟨k, rfl⟩ := hn
        simp [(Nat.pow_right_injective hq).extend_apply, one_apply, hq.ne']
      · rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply, smul_map, one_apply_ne, smul_zero]
        contrapose hn
        exact ⟨0, by simp [hn]⟩

Goal state after: