mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case hg
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hπ : exp (-1) ∈ range ⇑v
⊢ Units.mk0 (exp (-1)) ⋯ < 1

Tactic:
exact compareOfLessAndEq_eq_lt.mp rfl

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

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝ : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
⊢ zpowers (Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup) = zpowers (Units.mk0 (v π) ⋯)

Tactic:
congr

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝ : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
⊢ Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup = Units.mk0 (v π) ⋯
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
g : Γˣ := Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup
hg : g = Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup
hγ0 : ↑g ∉ {0}
π : K
hπ : (MonoidWithZeroHom.ofClass v) π = ↑g
⊢ ∃ a, v a ≤ 1 ∧ v a = ↑(generator v)

Tactic:
use π

Goal state after:
case h
Γ : 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
g : Γˣ := ⋯
hg : g = Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup
hγ0 : ↑g ∉ {0}
π : K
hπ : (MonoidWithZeroHom.ofClass v) π = ↑g
⊢ v π ≤ 1 ∧ v π = ↑(generator v)
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}
⊢ v.IsUniformizer ↑r

Tactic:
by
  have hr₀ : r ≠ 0 := by
    intro h
    rw [h, Set.singleton_zero, span_zero] at hr
    exact Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal v.valuationSubring)
      (valuationSubring_not_isField v) hr
  obtain ⟨π, hπ⟩ := exists_isUniformizer_of_isCyclic_of_nontrivial v
  obtain ⟨n, u, hu⟩ := exists_pow_Uniformizer hr₀ ⟨π, hπ⟩
  rw [Uniformizer.is_generator ⟨π, hπ⟩, span_singleton_eq_span_singleton] at hr
  exact hπ.of_associated hr

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

Tactic:
simp only [dblY, negY_eq, map_negDblY, map_dblX, map_dblZ]

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
⊢ -f (W'.negDblY P) - (W'.map f).a₁ * f (W'.dblX P) * f (W'.dblZ P) - (W'.map f).a₃ * f (W'.dblZ P) ^ 3 =
    f (-W'.negDblY P - W'.a₁ * W'.dblX P * W'.dblZ P - W'.a₃ * W'.dblZ P ^ 3)
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

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

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, hn, pow_zero, one_mul, SetLike.coe_eq_coe] at hu
      refine (hP.ne_top (Ideal.eq_top_of_isUnit_mem P hx_mem ?_)).elim
      simp only [hu, Units.isUnit]

Goal state after:
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
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case h.left
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
v : Valuation K (WithZero (Multiplicative ℤ)) := ⋯
π : K := ⋯
hπ : v π = ↑(ofAdd (-1))
⊢ ↑(Units.mk0 (v π) ⋯) ∈ Set.range ⇑(MonoidWithZeroHom.ofClass (valuation K (maximalIdeal A)))

Tactic:
use π

Goal state after:
case h
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
v : Valuation K (WithZero (Multiplicative ℤ)) := ⋯
π : K := ⋯
hπ : v π = ↑(ofAdd (-1))
⊢ (MonoidWithZeroHom.ofClass (valuation K (maximalIdeal A))) π = ↑(Units.mk0 (v π) ⋯)
Module: Mathlib.Topology.Algebra.Valued.ValuedField

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

Tactic:
decomp

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

Goal state before:
pp: case h.e_a
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
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation π ^ m ≤ 1
h_mn : m ≤ n
⊢ (algebraMap A K) π ^ (n - m) * ((algebraMap A K) ↑w)⁻¹ =
    (algebraMap A K) π ^ n * ((algebraMap A K) π ^ m)⁻¹ * ((algebraMap A K) ↑w)⁻¹

Tactic:
congr

Goal state after:
case h.e_a.e_a
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
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation π ^ m ≤ 1
h_mn : m ≤ n
⊢ (algebraMap A K) π ^ (n - m) = (algebraMap A K) π ^ n * ((algebraMap A K) π ^ m)⁻¹
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
hx : ↑x ∈ s
⊢ ∀ (a : X), ↑a ∈ s → x < a → ∃ a_2, (↑a_2 ∈ s ∧ x < a_2) ∧ a_2 < a

Tactic:
y

Goal state after:
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
hx : ↑x ∈ s
y : X
⊢ ↑y ∈ s → x < y → ∃ a, (↑a ∈ s ∧ x < a) ∧ a < y
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 Γ₀
U : Set K
hU' : U.Nonempty
hU : ∀ x ∉ U, ∃ γ, U ⊆ {a | ↑γ ≤ v.restrict (a - x)}
⊢ IsClosed (⇑v.restrict '' U)

Tactic:
simp only [isClosed_iff, mem_image, map_eq_zero, exists_eq_right, ne_eq, image_subset_iff]

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
U : Set K
hU' : U.Nonempty
hU : ∀ x ∉ U, ∃ γ, U ⊆ {a | ↑γ ≤ v.restrict (a - x)}
⊢ 0 ∈ U ∨ ∃ γ, ¬γ = 0 ∧ U ⊆ ⇑v.restrict ⁻¹' Ici γ
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 Γ₀
U : Set K
hU' : U.Nonempty
hU : ∀ x ∉ U, ∃ γ, U ⊆ {a | ↑γ ≤ v.restrict (a - x)}
h✝ : 0 ∉ U
γ : (ofClass v).ValueGroup₀ˣ
h : U ⊆ {a | ↑γ ≤ v.restrict (a - 0)}
⊢ ∃ γ, ¬γ = 0 ∧ U ⊆ ⇑v.restrict ⁻¹' Ici γ

Tactic:
simp only [sub_zero] at h

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
U : Set K
hU' : U.Nonempty
hU : ∀ x ∉ U, ∃ γ, U ⊆ {a | ↑γ ≤ v.restrict (a - x)}
h✝ : 0 ∉ U
γ : (ofClass v).ValueGroup₀ˣ
h : U ⊆ {a | ↑γ ≤ v.restrict a}
⊢ ∃ γ, ¬γ = 0 ∧ U ⊆ ⇑v.restrict ⁻¹' Ici γ
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
| Tendsto (fun p ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 1)

Tactic:
congr

Goal state after:
case f
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
| fun p ↦ p.1 * p.2⁻¹

case l₁
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
| 𝓝 (1, 1)

case l₂
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
| 𝓝 1
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
⊢ IsLeast {y | y ∈ closure {b} ∧ 1 < y} b

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
⊢ b ∈ {y | y ∈ closure {b} ∧ 1 < y}

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
⊢ b ∈ lowerBounds {y | y ∈ closure {b} ∧ 1 < y}
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case neg
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
H : ∀ (x : G), ¬IsLeast {y | 0 < y} x
x : G
⊢ ∀ (a₂ : G), x < a₂ → ∃ a, x < a ∧ a < a₂

Tactic:
y

Goal state after:
case neg
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
H : ∀ (x : G), ¬IsLeast {y | 0 < y} x
x y : G
⊢ x < y → ∃ a, x < a ∧ a < y
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : G ≃*o WithZero (Multiplicative ℤ)
a✝ b✝ : Gˣ
⊢ (MulEquiv.withZero.symm (withZeroUnitsEquiv.trans ↑f)).toFun a✝ ≤
      (MulEquiv.withZero.symm (withZeroUnitsEquiv.trans ↑f)).toFun b✝ ↔
    a✝ ≤ b✝

Tactic:
simp only [MulEquiv.withZero, withZeroUnitsEquiv, MulEquiv.trans_apply,
      MulEquiv.coe_mk, Equiv.coe_fn_mk, recZeroCoe_coe, OrderMonoidIso.coe_mulEquiv,
      MulEquiv.symm_trans_apply, MulEquiv.symm_mk, Equiv.coe_fn_symm_mk, map_eq_zero, coe_ne_zero,
      ↓reduceDIte, unzero_coe, MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe]

Goal state after:
case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : G ≃*o WithZero (Multiplicative ℤ)
a✝ b✝ : Gˣ
⊢ unzero ⋯ ≤ unzero ⋯ ↔ a✝ ≤ b✝
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 Γ₀
⊢ (⇑embedding ∘ extension) 0 = 0

Tactic:
Function.comp_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ embedding (extension 0) = 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 Γ₀
⊢ (⇑embedding ∘ extension) 1 = 1

Tactic:
Function.comp_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ embedding (extension 1) = 1
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case ih
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x✝ y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : K
⊢ ∀ (b : K), extension (↑x * ↑b) = extension ↑x * extension ↑b

Tactic:
y

Goal state after:
case ih
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x✝ y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x y : K
⊢ extension (↑x * ↑y) = extension ↑x * extension ↑y
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case ih
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x✝ y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : K
⊢ ∀ (b : K), extension (↑x + ↑b) ≤ extension ↑x ∨ extension (↑x + ↑b) ≤ extension ↑b

Tactic:
y

Goal state after:
case ih
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x✝ y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x y : K
⊢ extension (↑x + ↑y) ≤ extension ↑x ∨ extension (↑x + ↑y) ≤ extension ↑y
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
inst✝ : IsMinimal R W
⊢ IsIntegral R W

Tactic:
by simpa using IsMinimal.val_Δ_maximal.1

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 Γ₀
⊢ extensionValuation.restrict ↑⋯.choose = 1

Tactic:
by
    apply_fun embedding using embedding_injective
    simpa using (restrict₀_surjective (.ofClass hv.v) 1).choose_spec

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : CommMonoid β
inst✝¹ : PartialOrder β
e : α ≃*o β
inst✝ : MulArchimedean α
x : β
⊢ ∀ {y : β}, 1 < y → ∃ n, x ≤ y ^ n

Tactic:
y

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : CommMonoid β
inst✝¹ : PartialOrder β
e : α ≃*o β
inst✝ : MulArchimedean α
x y : β
⊢ 1 < y → ∃ n, x ≤ y ^ n
Module: Mathlib.Order.Northcott

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst✝² : Preorder β
inst✝¹ : LE γ
inst✝ : Northcott h
H : ∀ (c : γ), BddAbove (h' ⁻¹' {x | x ≤ c})
c : γ
⊢ {a | (h' ∘ h) a ≤ c}.Finite

Tactic:
by
    obtain ⟨b, hb⟩ := bddAbove_def.mp (H c)
    exact (finite_le (h := h) b).subset <| by grind

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
a : R
this : ∀ p ∈ antidiagonal m, (coeff p.1) ((monomial n) a) * (coeff p.2) φ ≠ 0 → p.1 = n
⊢ ∑ p ∈ antidiagonal m, (coeff p.1) ((monomial n) a) * (coeff p.2) φ = if n ≤ m then a * (coeff (m - n)) φ else 0

Tactic:
← Finset.sum_filter_of_ne this,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this : ∀ p ∈ antidiagonal m, (coeff p.1) ((monomial n) a) * (coeff p.2) φ ≠ 0 → p.1 = n
⊢ ∑ x ∈ antidiagonal m with x.1 = n, (coeff x.1) ((monomial n) a) * (coeff x.2) φ =
    if n ≤ m then a * (coeff (m - n)) φ else 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this : ∀ p ∈ antidiagonal m, (coeff p.1) φ * (coeff p.2) ((monomial n) a) ≠ 0 → p.2 = n
⊢ ∑ p ∈ antidiagonal m, (coeff p.1) φ * (coeff p.2) ((monomial n) a) = if n ≤ m then (coeff (m - n)) φ * a else 0

Tactic:
← Finset.sum_filter_of_ne this,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this : ∀ p ∈ antidiagonal m, (coeff p.1) φ * (coeff p.2) ((monomial n) a) ≠ 0 → p.2 = n
⊢ ∑ x ∈ antidiagonal m with x.2 = n, (coeff x.1) φ * (coeff x.2) ((monomial n) a) =
    if n ≤ m then (coeff (m - n)) φ * a else 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h₀.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).2)
h2 : (i, j) ≠ (d, (i, j).2)
⊢ False

Tactic:
apply h2

Goal state after:
case h₀.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).2)
h2 : (i, j) ≠ (d, (i, j).2)
⊢ (i, j) = (d, (i, j).2)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → (coeff (d, n).1) p * (coeff (d, n).2) (X ^ n) = 0

Tactic:
· exact fun h1 => (h1 (mem_antidiagonal.2 rfl)).elim

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

Goal state before:
pp: case h₀.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).1)
h2 : (i, j) ≠ ((i, j).1, d)
⊢ False

Tactic:
apply h2

Goal state after:
case h₀.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).1)
h2 : (i, j) ≠ ((i, j).1, d)
⊢ (i, j) = ((i, j).1, d)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ = (mk fun p ↦ (coeff (p + 1)) φ) * X + C (constantCoeff φ)

Tactic:
by
  ext (_ | n)
  · simp
  · simp only [coeff_succ_mul_X, coeff_mk, map_add, coeff_C, n.succ_ne_zero,
      if_false, add_zero]

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

Goal state before:
pp: case pos
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))) =
    (if x = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors))) *
      if y = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors))

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))) =
    (if x = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors))) *
      if y = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors))

Tactic:
· rw [hy, mul_zero, if_pos rfl, mul_zero]

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
⊢ (if x * y = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x * y})).factors))) =
    (if x = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors))) *
      if y = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors))
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ rescale 0 = C.comp constantCoeff

Tactic:
ext x n
  simp only [Function.comp_apply, RingHom.coe_comp, rescale, RingHom.coe_mk,
    coeff_C]
  split_ifs with h <;> simp [h]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
φ : R →+* S
r : R
f : R⟦X⟧
⊢ (rescale (φ r)) ((map φ) f) = (map φ) ((rescale r) f)

Tactic:
by
  ext n
  simp [coeff_rescale, coeff_map, map_mul, map_pow]

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

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

Tactic:
split_ifs with hi

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

case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : ¬(i, j).1 = single s n
⊢ (0 * (coeff (i, j).2) fun m ↦ (coeff (m + single s n)) φ) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

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

Tactic:
split_ifs with hi

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

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