mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq :
  (-48 * E.a₄) ^ 3 * (-16 * (4 * E'.a₄ ^ 3 + 27 * E'.a₆ ^ 2)) =
    (-48 * E'.a₄) ^ 3 * (-16 * (4 * E.a₄ ^ 3 + 27 * E.a₆ ^ 2))
⊢ E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2

Tactic:
let : Invertible (47775744 : F) := invertibleOfNonzero <| by
      have := mul_ne_zero (pow_ne_zero 16 hchar2) (pow_ne_zero 6 hchar3)
      norm_num1 at this
      exact this

Goal state after:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝⁴ : NeZero 2
this✝³ : NeZero 4
this✝² : NeZero 6
this✝¹ : Invertible 2 := invertibleOfNonzero hchar2
this✝ : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq :
  (-48 * E.a₄) ^ 3 * (-16 * (4 * E'.a₄ ^ 3 + 27 * E'.a₆ ^ 2)) =
    (-48 * E'.a₄) ^ 3 * (-16 * (4 * E.a₄ ^ 3 + 27 * E.a₆ ^ 2))
this : Invertible 47775744 := invertibleOfNonzero ⋯
⊢ E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑n ≠ 0
⊢ (W.preΨ' n).leadingCoeff = ↑(if Even n then n / 2 else n)

Tactic:
by
  rw [leadingCoeff, W.natDegree_preΨ' h, coeff_preΨ']

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
hn : 2 < n.natAbs
h : ↑n ≠ 0
⊢ 0 < (W.preΨ n).natDegree

Tactic:
by
  induction n using Int.negInduction with
  | nat n => simpa only [preΨ_ofNat] using! W.natDegree_preΨ'_pos hn <| by exact_mod_cast h
  | neg ih n => simpa only [preΨ_neg, natDegree_neg]
        using! ih n (by rwa [← Int.natAbs_neg]) <| neg_ne_zero.mp <| by exact_mod_cast h

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * (u • P) y * (u • P) z - (3 * (u • P) x ^ 2 + 2 * W'.a₂ * (u • P) x * (u • P) z ^ 2 + W'.a₄ * (u • P) z ^ 4) ≠
      0 ∨
    2 * (u • P) y + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * (u • P) z ^ 3 ≠ 0 ∨
      W'.a₁ * (u • P) x * (u • P) y + 3 * W'.a₃ * (u • P) y * (u • P) z ^ 2 -
          (2 * W'.a₂ * (u • P) x ^ 2 * (u • P) z + 4 * W'.a₄ * (u • P) x * (u • P) z ^ 3 + 6 * W'.a₆ * (u • P) z ^ 5) ≠
        0
⊢ W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4) ≠ 0 ∨
    2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3 ≠ 0 ∨
      W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 -
          (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5) ≠
        0

Tactic:
contrapose! hP'

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4) = 0 ∧
    2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3 = 0 ∧
      W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 -
          (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5) =
        0
⊢ W'.a₁ * (u • P) y * (u • P) z - (3 * (u • P) x ^ 2 + 2 * W'.a₂ * (u • P) x * (u • P) z ^ 2 + W'.a₄ * (u • P) z ^ 4) =
      0 ∧
    2 * (u • P) y + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * (u • P) z ^ 3 = 0 ∧
      W'.a₁ * (u • P) x * (u • P) y + 3 * W'.a₃ * (u • P) y * (u • P) z ^ 2 -
          (2 * W'.a₂ * (u • P) x ^ 2 * (u • P) z + 4 * W'.a₄ * (u • P) x * (u • P) z ^ 3 + 6 * W'.a₆ * (u • P) z ^ 5) =
        0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.Nonsingular P ↔ W'.Equation P ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W'.a₁ * P x * P y ≠ 0)

Tactic:
simp only [nonsingular_iff, hPz, add_zero, sub_zero, zero_sub, mul_zero,
    zero_pow <| OfNat.ofNat_ne_zero _, neg_ne_zero]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ -P y - 0 = -P y

Tactic:
sub_zero

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ -P y = -P y
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: case neg.refine_1
F : Type u
inst✝¹ : Field F
W : Jacobian F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ P x * Q z ^ 2 = Q x * P z ^ 2

Tactic:
apply f.injective; map_simp

Goal state after:
case neg.refine_1
F : Type u
inst✝¹ : Field F
W : Jacobian F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ f (P x) * f (Q z) ^ 2 = f (Q x) * f (P z) ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: case neg.refine_2
F : Type u
inst✝¹ : Field F
W : Jacobian F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ P y * Q z ^ 3 = Q y * P z ^ 3

Tactic:
apply f.injective; map_simp

Goal state after:
case neg.refine_2
F : Type u
inst✝¹ : Field F
W : Jacobian F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ f (P y) * f (Q z) ^ 3 = f (Q y) * f (P z) ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
this :
  toAffine W
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1] =
    toAffine W P + toAffine W Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

pp: case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
this :
  toAffine W
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1] =
    toAffine W P + toAffine W Q
hx : ¬P x * Q z ^ 2 = Q x * P z ^ 2
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Tactic:
· rwa [add_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx,
            toAffine_smul _ <| isUnit_dblZ_of_Y_ne' hP.left hQ.left hPz hx <| not_and.mp hxy hx]

Goal state after:
case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
this :
  toAffine W
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1] =
    toAffine W P + toAffine W Q
hx : ¬P x * Q z ^ 2 = Q x * P z ^ 2
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ₁ γ₂ : Γ₀
h : γ₁ < γ₂
⊢ Iio γ₂ ∈ 𝓝 γ₁

Tactic:
by
  rcases eq_or_ne γ₁ 0 with (rfl | h₀) <;> simp [*, h.ne', Iio_mem_nhds_zero]

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

Goal state before:
pp: α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ ContinuousAt Inv.inv γ

Tactic:
by
    rw [ContinuousAt, nhds_of_ne_zero h]
    exact pure_le_nhds γ⁻¹

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : TopologicalSpace R
inst✝ : IsValuativeTopology R
x✝¹ : (ValueGroupWithZero R)ˣ
x✝ : R
⊢ x✝ = x✝ - 0

Tactic:
sub_zero

Goal state after:
R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : TopologicalSpace R
inst✝ : IsValuativeTopology R
x✝¹ : (ValueGroupWithZero R)ˣ
x✝ : R
⊢ x✝ = x✝
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : IsUniformAddGroup α
⊢ mapRingHom (RingHom.id α) ⋯ = RingHom.id (Completion α)

Tactic:
by
  simp [RingHom.ext_iff, mapRingHom_apply]

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

Goal state before:
pp: R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a / (valuation R) ↑r < (valuation R) b / (valuation R) ↑s
⊢ embedding ((embed v) ((valuation R) a / (valuation R) ↑r)) <
    embedding ((embed v) ((valuation R) b / (valuation R) ↑s))

Tactic:
simp only [map_div₀]

Goal state after:
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a / (valuation R) ↑r < (valuation R) b / (valuation R) ↑s
⊢ embedding ((embed v) ((valuation R) a)) / embedding ((embed v) ((valuation R) ↑r)) <
    embedding ((embed v) ((valuation R) b)) / embedding ((embed v) ((valuation R) ↑s))
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
π : v.Uniformizer
n : ℕ
⊢ maximalIdeal ↥v.valuationSubring ^ n = span {π.val ^ n}

Tactic:
← Ideal.span_singleton_pow,

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
n : ℕ
⊢ maximalIdeal ↥v.valuationSubring ^ n = span {π.val} ^ n
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case neg
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 :
  (valuation K (maximalIdeal A)) ((algebraMap A K) (π ^ n)) *
        ((valuation K (maximalIdeal A)) ((algebraMap A K) (π ^ m)))⁻¹ *
      ((valuation K (maximalIdeal A)) ((algebraMap A K) ↑w))⁻¹ ≤
    1
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
⊢ ∃ a, (algebraMap A K) a = x

Tactic:
Integers.one_of_isUnit' w.isUnit (valuation_le_one _),

Goal state after:
case neg
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 :
  (valuation K (maximalIdeal A)) ((algebraMap A K) (π ^ n)) *
        ((valuation K (maximalIdeal A)) ((algebraMap A K) (π ^ m)))⁻¹ *
      1⁻¹ ≤
    1
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
⊢ ∃ a, (algebraMap A K) a = x
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
⊢ UniformContinuous ⇑(WithVal.congr v w (RingEquiv.refl R))

Tactic:
have hcomp : WithVal.congr v w (.refl R) = _ := RingEquiv.ext_iff.mpr (congrFun rfl)
  have h1 := IsEquiv.uniformContinuous_equiv (hval := Valued.mk' w) rfl h
  have h2 := IsEquiv.uniformContinuous_equiv_symm (hval := Valued.mk' v) rfl h
  have hR : @UniformContinuous R R (Valued.mk' w).toUniformSpace (Valued.mk' v).toUniformSpace
      (RingHom.id R) := h.uniformContinuous
  apply @UniformContinuous.comp (WithVal v) R (WithVal w) _ (Valued.mk' w).toUniformSpace _
    ((RingEquiv.refl R).trans (WithVal.equiv w).symm) (WithVal.equiv v) ?_ h1
  exact @UniformContinuous.comp R R (WithVal w) (Valued.mk' w).toUniformSpace
       (Valued.mk' v).toUniformSpace _ (WithVal.equiv w).symm (RingEquiv.refl R) h2 hR

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mp
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : WellFounded fun x1 x2 ↦ x1 < x2
⊢ Nonempty (G ≃+o ℤ)

Tactic:
WellFounded.wellFounded_iff_has_min

Goal state after:
case mp
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
⊢ Nonempty (G ≃+o ℤ)
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:
rwa [← hy₂]

Goal state after:
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
⊢ (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:
by_cases hy : y = 0
    · rw [hy, mul_zero, if_pos rfl, mul_zero]
    · rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← exp_add,
        ← Ideal.span_singleton_mul_span_singleton, ← Associates.mk_mul_mk, ← neg_add,
        Associates.count_mul (Associates.mk_ne_zero'.mpr hx) (Associates.mk_ne_zero'.mpr hy)
          v.associates_irreducible,
        Nat.cast_add]

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
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
rw [hx, zero_add]

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : x = 0
⊢ v.intValuationDef y ≤ max (v.intValuationDef 0) (v.intValuationDef y)
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
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ embedding a = embedding b

Tactic:
by_cases ha0 : a = 0

Goal state after:
case pos
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)
ha0 : a = 0
⊢ embedding a = embedding b

case neg
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)
ha0 : ¬a = 0
⊢ embedding a = embedding b
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_4
f : ι → σ →₀ ℕ
g : ι → R
s : Finset ι
⊢ ∏ i ∈ s, (monomial (f i)) (g i) = (monomial (∑ i ∈ s, f i)) (∏ i ∈ s, g i)

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha h => simp [h, monomial_mul_monomial]

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' - 1 + 1)

Tactic:
rw [Nat.sub_add_cancel h']

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'
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case h
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x✝ : ∃ i, {x | embedding (extension x) < embedding ↑i} ⊆ s
γ : (ofClass v).ValueGroup₀ˣ
h : {x | embedding (extension x) < embedding ↑γ} ⊆ s
⊢ {x | extensionValuation.restrict x < ↑((Units.map valueGroup₀_equiv_extensionValuation.toMonoidHom) γ)} ⊆ s

Tactic:
convert! h

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x✝¹ : ∃ i, {x | embedding (extension x) < embedding ↑i} ⊆ s
γ : (ofClass v).ValueGroup₀ˣ
h : {x | embedding (extension x) < embedding ↑γ} ⊆ s
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ extensionValuation.restrict x✝ < ↑((Units.map valueGroup₀_equiv_extensionValuation.toMonoidHom) γ) ↔
    embedding (extension x✝) < embedding ↑γ
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case h
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x✝ : ∃ γ, {x | extensionValuation.restrict x < ↑γ} ⊆ s
γ : (ofClass extensionValuation).ValueGroup₀ˣ
h : {x | extensionValuation.restrict x < ↑γ} ⊆ s
⊢ {x | embedding (extension x) < embedding ↑((Units.map valueGroup₀_equiv_extensionValuation.symm.toMonoidHom) γ)} ⊆ s

Tactic:
convert! h

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x✝¹ : ∃ γ, {x | extensionValuation.restrict x < ↑γ} ⊆ s
γ : (ofClass extensionValuation).ValueGroup₀ˣ
h : {x | extensionValuation.restrict x < ↑γ} ⊆ s
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ embedding (extension x✝) < embedding ↑((Units.map valueGroup₀_equiv_extensionValuation.symm.toMonoidHom) γ) ↔
    extensionValuation.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
n : ℕ
h : weightedOrder w f = ↑n
⊢ ↑(weightedOrder w f).toNat = weightedOrder w f

Tactic:
simp only [h, toNat_natCast]

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 Γ₀
⊢ Function.Surjective ⇑v ↔ Function.Surjective ⇑v

Tactic:
constructor <;> intro h γ <;> obtain ⟨a, ha⟩ := h γ
  · induction a using Completion.induction_on
    · by_cases H : ∃ x : K, (v : K → Γ₀) x = γ
      · simp [H]
      · simp only [H, imp_false]
        rcases eq_or_ne γ 0 with rfl | hγ
        · simp at H
        · obtain ⟨r, hr⟩ := h γ
          have hr' : restrict₀ (.ofClass (valuedCompletion (K := K)).v) r ≠ 0 := by
            rw [ne_eq, ← embedding_inj, embedding_restrict₀ r]
            simpa [hr]
          convert! isClosed_univ.sdiff (isOpen_sphere (hat K) hr') using 1
          ext x
          simp [← hr, ← v.restrict_def, v.restrict_inj]
    · exact ⟨_, by simpa using ha⟩
  · exact ⟨a, by simp [ha]⟩

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

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

Tactic:
coeff_weightedHomogeneousComponent

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
d : σ →₀ ℕ
⊢ (if (weight w) d = p then (coeff d) f else 0) = (coeff d) 0