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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ) ↔ eval (W'.addX x₁ x₂ ℓ) (W'.addPolynomial x₁ y₁ ℓ) = 0

Tactic:
rw [Equation, negAddY, addPolynomial, linePolynomial, polynomial]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ evalEval (W'.addX x₁ x₂ ℓ) (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁)
        (Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) =
      0 ↔
    eval (W'.addX x₁ x₂ ℓ)
        (eval (C ℓ * (X - C x₁) + C y₁)
          (Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆))) =
      0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case a
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := ⋯
hxy : (y₁ - W.negY x₁ y₁) ^ 2 ≠ 0
⊢ C (C 1) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) +
        -4 * C (C (x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆)) -
      (C (C ((y₁ - W.negY x₁ y₁) ^ 2)) * 1 +
              C (C (1 * 4)) * (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) +
            C
              ((C (1 * 4) * X ^ 2 + C (1 * 4 * x₁ + 1 * b₂ W) * X + C (1 * 4 * x₁ ^ 2 + 1 * b₂ W * x₁ + 1 * 2 * b₄ W)) *
                (X - C x₁)) +
          C (C ((y₁ - W.negY x₁ y₁) ^ 2)) * 0 * C (X - C x₁) +
        -4 * C (C (y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁))) =
    0

Tactic:
b₂,

Goal state after:
case a
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := (y₁ - W.negY x₁ y₁) ^ 2
hxy : (y₁ - W.negY x₁ y₁) ^ 2 ≠ 0
⊢ C (C 1) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) +
        -4 * C (C (x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆)) -
      (C (C ((y₁ - W.negY x₁ y₁) ^ 2)) * 1 +
              C (C (1 * 4)) * (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) +
            C
              ((C (1 * 4) * X ^ 2 + C (1 * 4 * x₁ + 1 * (W.a₁ ^ 2 + 4 * W.a₂)) * X +
                  C (1 * 4 * x₁ ^ 2 + 1 * (W.a₁ ^ 2 + 4 * W.a₂) * x₁ + 1 * 2 * b₄ W)) *
                (X - C x₁)) +
          C (C ((y₁ - W.negY x₁ y₁) ^ 2)) * 0 * C (X - C x₁) +
        -4 * C (C (y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁))) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆) = W.toAffine.polynomialY ^ 2 - 4 * W.toAffine.polynomial

Tactic:
b₂,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C (C 4 * X ^ 3 + C (W.a₁ ^ 2 + 4 * W.a₂) * X ^ 2 + C (2 * W.b₄) * X + C W.b₆) =
    W.toAffine.polynomialY ^ 2 - 4 * W.toAffine.polynomial
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case mpr
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
P : W.Point
⊢ P = 0 → toClass P = 0

Tactic:
exact congr_arg toClass

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : IsReduced R
x : Fin 3 → R
hx : (fun i ↦ (eval x) (W.addSubMap i)) = 0
⊢ x = 0

Tactic:
ext i

Goal state after:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : IsReduced R
x : Fin 3 → R
hx : (fun i ↦ (eval x) (W.addSubMap i)) = 0
i : Fin 3
⊢ x i = 0 i
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.b₂ = 4 * W.a₂

Tactic:
b₂,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.a₁ ^ 2 + 4 * W.a₂ = 4 * W.a₂
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsShortNF
⊢ W.Δ = -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

Tactic:
Δ_of_isCharNeTwoNF,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsShortNF
⊢ -64 * W.a₂ ^ 3 * W.a₆ + 16 * W.a₂ ^ 2 * W.a₄ ^ 2 - 64 * W.a₄ ^ 3 - 432 * W.a₆ ^ 2 + 288 * W.a₂ * W.a₄ * W.a₆ =
    -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
⊢ 2 * 2 = 1

Tactic:
linear_combination CharP.cast_eq_zero F 3

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.b₂ = 1 + 4 * W.a₂

Tactic:
b₂,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.a₁ ^ 2 + 4 * W.a₂ = 1 + 4 * W.a₂
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆ = W.a₆

Tactic:
b₂_of_isCharTwoJNeZeroNF_of_char_two,

Goal state after:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ -1 ^ 2 * W.b₈ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * 1 * W.b₄ * W.b₆ = W.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ W.b₂ = 0

Tactic:
b₂,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ W.a₁ ^ 2 + 4 * W.a₂ = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ W.b₂ = 0

Tactic:
rw [b₂, a₁_of_isCharTwoJEqZeroNF, a₂_of_isCharTwoJEqZeroNF]
  ring1

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

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 2
W : WeierstrassCurve F
⊢ ∃ C, (C • W).IsCharTwoNF

Tactic:
by
  classical
  exact ⟨_, W.toCharTwoNF_spec⟩

Goal state after:
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
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
⊢ 2 = -1

Tactic:
linear_combination CharP.cast_eq_zero F 3

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

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomial / P z ^ 6 +
        (W.a₁ * P x * P y / P z ^ 5 * 1 + W.a₃ * P y / P z ^ 3 * 1 + W.a₂ * P x ^ 2 / P z ^ 4 * (P z ^ 2 / P z ^ 2) +
            W.a₄ * P x / P z ^ 2 * (P z ^ 4 / P z ^ 4) +
          W.a₆ * (P z ^ 6 / P z ^ 6)) -
      (Polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) W.toAffine.polynomial +
        (W.a₁ * P x * P y / P z ^ 5 * (P z / P z) + W.a₃ * P y / P z ^ 3 * (P z ^ 3 / P z ^ 3) +
              W.a₂ * P x ^ 2 / P z ^ 4 * 1 +
            W.a₄ * P x / P z ^ 2 * 1 +
          W.a₆ * 1)) =
    0

Tactic:
eval_polynomial,

Goal state after:
case a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (P y ^ 2 + W.a₁ * P x * P y * P z + W.a₃ * P y * P z ^ 3 -
            (P x ^ 3 + W.a₂ * P x ^ 2 * P z ^ 2 + W.a₄ * P x * P z ^ 4 + W.a₆ * P z ^ 6)) /
          P z ^ 6 +
        (W.a₁ * P x * P y / P z ^ 5 * 1 + W.a₃ * P y / P z ^ 3 * 1 + W.a₂ * P x ^ 2 / P z ^ 4 * (P z ^ 2 / P z ^ 2) +
            W.a₄ * P x / P z ^ 2 * (P z ^ 4 / P z ^ 4) +
          W.a₆ * (P z ^ 6 / P z ^ 6)) -
      (Polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) W.toAffine.polynomial +
        (W.a₁ * P x * P y / P z ^ 5 * (P z / P z) + W.a₃ * P y / P z ^ 3 * (P z ^ 3 / P z ^ 3) +
              W.a₂ * P x ^ 2 / P z ^ 4 * 1 +
            W.a₄ * P x / P z ^ 2 * 1 +
          W.a₆ * 1)) =
    0
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
inst✝² : CharP F 3
inst✝¹ : E.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
⊢ 4 = 1

Tactic:
linear_combination CharP.cast_eq_zero F 3

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
⊢ 6 * (eval P) W'.polynomial =
    2 * P x * (eval P) W'.polynomialX + 3 * P y * (eval P) W'.polynomialY + P z * (eval P) W'.polynomialZ

Tactic:
eval_polynomial,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ 6 *
      (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
        (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6)) =
    2 * P x * (eval P) W'.polynomialX + 3 * P y * (eval P) W'.polynomialY + P z * (eval P) W'.polynomialZ
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ W.Nonsingular P ↔ W.Equation P ∧ (eval P) W.polynomialX ≠ 0

Tactic:
have hy' : eval P W.polynomialY = P y - W.negY P := by rw [negY, eval_polynomialY]; ring1
  rw [nonsingular_iff_of_Z_ne_zero hPz, hy', hy, sub_self, ne_self_iff_false, or_false]

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ![P x, W.negY P, P z] = ![P x, P z ^ 3 * (W.negY P / P z ^ 3), P z * 1]

Tactic:
mul_div_cancel₀ _ <| pow_ne_zero 3 hPz,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ![P x, W.negY P, P z] = ![P x, W.negY P, P z * 1]
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he : 1 < e
⊢ (toNNReal ⋯) m ≤ 1 ↔ m ≤ 1

Tactic:
rw [← (toNNReal_strictMono he).le_iff_le, map_one]

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := ⋯
⊢ ∀ U ∈ 𝓝 0, ∃ V, ↑V ⊆ U

Tactic:
intro U

Goal state after:
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := hB.topology
U : Set A
⊢ U ∈ 𝓝 0 → ∃ V, ↑V ⊆ U
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
this : TopologicalSpace M := ⋯
⊢ ∀ U ∈ 𝓝 0, ∃ V, ↑V ⊆ U

Tactic:
intro U

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
this : TopologicalSpace M := hB.topology
U : Set M
⊢ U ∈ 𝓝 0 → ∃ V, ↑V ⊆ U
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
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
⊢ toAffine W (W.add P Q) = toAffine W Q

Tactic:
· rw [add_of_Z_eq_zero_left hP.left hPz hQz,
        toAffine_smul _ <| (isUnit_X_of_Z_eq_zero hP hPz).mul <| Ne.isUnit hQz]

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

Goal state before:
pp: case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ₀ γ₁ : (ofClass v).ValueGroup₀ˣ
⊢ v.ltAddSubgroup ((Units.map ↑embedding) (min γ₀ γ₁)) ≤
    v.ltAddSubgroup ((Units.map ↑embedding) γ₀) ⊓ v.ltAddSubgroup ((Units.map ↑embedding) γ₁)

Tactic:
have hmin : embedding (min γ₀.1 γ₁.1) = min (embedding γ₀.1) (embedding γ₁.1) :=
        embedding_strictMono.monotone.map_inf γ₀.1 γ₁.1

Goal state after:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ₀ γ₁ : (ofClass v).ValueGroup₀ˣ
hmin : embedding (min ↑γ₀ ↑γ₁) = min (embedding ↑γ₀) (embedding ↑γ₁)
⊢ v.ltAddSubgroup ((Units.map ↑embedding) (min γ₀ γ₁)) ≤
    v.ltAddSubgroup ((Units.map ↑embedding) γ₀) ⊓ v.ltAddSubgroup ((Units.map ↑embedding) γ₁)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : ValuativeRel R
α : Type u_2
inst✝ : Mul α
f : R → ↥(posSubmonoid R) → α
hf : ∀ (x y : R) (t s : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t
hdist : ∀ (a b : R) (r s : ↥(posSubmonoid R)), f (a * b) (r * s) = f a r * f b s
a b : ValueGroupWithZero R
⊢ ValueGroupWithZero.lift f hf (a * b) = ValueGroupWithZero.lift f hf a * ValueGroupWithZero.lift f hf b

Tactic:
induction a using ValueGroupWithZero.ind

Goal state after:
case mk
R : Type u_1
inst✝² : Semiring R
inst✝¹ : ValuativeRel R
α : Type u_2
inst✝ : Mul α
f : R → ↥(posSubmonoid R) → α
hf : ∀ (x y : R) (t s : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t
hdist : ∀ (a b : R) (r s : ↥(posSubmonoid R)), f (a * b) (r * s) = f a r * f b s
b : ValueGroupWithZero R
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.lift f hf (ValueGroupWithZero.mk x✝ y✝ * b) =
    ValueGroupWithZero.lift f hf (ValueGroupWithZero.mk x✝ y✝) * ValueGroupWithZero.lift f hf b
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
a b c : ValueGroupWithZero R
⊢ a * b * c = a * (b * c)

Tactic:
induction a using ValueGroupWithZero.ind

Goal state after:
case mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
b c : ValueGroupWithZero R
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x✝ y✝ * b * c = ValueGroupWithZero.mk x✝ y✝ * (b * c)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
a b : ValueGroupWithZero R
⊢ a * b = b * a

Tactic:
induction a using ValueGroupWithZero.ind

Goal state after:
case mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
b : ValueGroupWithZero R
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x✝ y✝ * b = b * ValueGroupWithZero.mk x✝ y✝
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

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

Tactic:
veq_mul_right_comm,

Goal state after:
case pos.refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : w ≤ᵥ 0
hz : z ≤ᵥ 0
h : x * ↑v ≤ᵥ z * ↑s
⊢ y * ↑(s * v) * ↑u ≤ᵥ 0 * ↑(s * v)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

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

Tactic:
veq_mul_right_comm,

Goal state after:
case pos.refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : w ≤ᵥ 0
hz : z ≤ᵥ 0
h : y * ↑u ≤ᵥ w * ↑t
⊢ x * ↑(t * u) * ↑v ≤ᵥ 0 * ↑(t * u)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

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

Tactic:
apply vle_mul_cancel u.prop

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : w ≤ᵥ 0
hz : ¬z ≤ᵥ 0
⊢ z * ↑u ≤ᵥ 0 * ↑u
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
a b : ValueGroupWithZero R
hab : a ≤ b
hba : b ≤ a
⊢ a = b

Tactic:
induction a using ValueGroupWithZero.ind

Goal state after:
case mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
b : ValueGroupWithZero R
x✝ : R
y✝ : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk x✝ y✝ ≤ b
hba : b ≤ ValueGroupWithZero.mk x✝ y✝
⊢ ValueGroupWithZero.mk x✝ y✝ = b
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
a b : ValueGroupWithZero R
⊢ a ≤ b ∨ b ≤ a

Tactic:
induction a using ValueGroupWithZero.ind

Goal state after:
case mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
b : ValueGroupWithZero R
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x✝ y✝ ≤ b ∨ b ≤ ValueGroupWithZero.mk x✝ y✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addX P Q = addU P Q ^ 2

Tactic:
rw [addU, neg_sq, div_pow, ← addX_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
a b : ValueGroupWithZero R
hab : a ≤ b
c : ValueGroupWithZero R
⊢ a * c ≤ b * c

Tactic:
induction a using ValueGroupWithZero.ind

Goal state after:
case mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
b c : ValueGroupWithZero R
x✝ : R
y✝ : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk x✝ y✝ ≤ b
⊢ ValueGroupWithZero.mk x✝ y✝ * c ≤ b * c
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁷ : UniformSpace α
inst✝⁶ : AddGroup α
inst✝⁵ : IsUniformAddGroup α
inst✝⁴ : UniformSpace β
inst✝³ : AddGroup β
inst✝² : IsUniformAddGroup β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
f : α →+ β
hf✝ : Continuous ⇑f
hf : UniformContinuous ⇑f
a✝ b✝ : Completion α
a b : α
⊢ f (a + b) = f a + f b

Tactic:
f.map_add

Goal state after:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁷ : UniformSpace α
inst✝⁶ : AddGroup α
inst✝⁵ : IsUniformAddGroup α
inst✝⁴ : UniformSpace β
inst✝³ : AddGroup β
inst✝² : IsUniformAddGroup β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
f : α →+ β
hf✝ : Continuous ⇑f
hf : UniformContinuous ⇑f
a✝ b✝ : Completion α
a b : α
⊢ f a + f b = f a + f b
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : IsUniformAddGroup α
a✝ : Completion α
a : α
⊢ ↑a * 1 = ↑a

Tactic:
rw [← coe_one, ← coe_mul, mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝⁹ : Ring α
inst✝⁸ : UniformSpace α
inst✝⁷ : IsTopologicalRing α
inst✝⁶ : IsUniformAddGroup α
β : Type u
inst✝⁵ : UniformSpace β
inst✝⁴ : Ring β
inst✝³ : IsUniformAddGroup β
inst✝² : IsTopologicalRing β
f : α →+* β
hf✝ : Continuous ⇑f
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
hf' : Continuous ⇑↑f
hf : UniformContinuous ⇑f
a✝ b✝ : Completion α
a b : α
⊢ f (a + b) = f a + f b

Tactic:
f.map_add

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x ↦ x * x.hatInv
c : K → hat K := fun x ↦ ↑x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' c '' {0}ᶜ)
⊢ f '' c '' {0}ᶜ ⊆ {1}

Tactic:
rw [image_image]

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x ↦ x * x.hatInv
c : K → hat K := fun x ↦ ↑x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' c '' {0}ᶜ)
⊢ (fun x ↦ f (c x)) '' {0}ᶜ ⊆ {1}
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 Γ
inst✝ : v.IsRankOneDiscrete
⊢ zpowers ↑(generator' v) = (MonoidWithZeroHom.ofClass v).valueGroup

Tactic:
apply generator_zpowers_eq_valueGroup

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

Goal state before:
pp: case hJ
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
h : span {π.val} = ⊤
⊢ False

Tactic:
Ideal.span_singleton_eq_top

Goal state after:
case hJ
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
h : IsUnit π.val
⊢ False
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case neg
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : x ∈ maximalIdeal ↥v.valuationSubring
hx₀ : ¬x = 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : ↑x = ↑(π.val ^ n) * ↑↑u
⊢ x ∈ span {π.val}

Tactic:
rw [← Subring.coe_mul, Subtype.coe_inj] at hu

Goal state after:
case neg
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : x ∈ maximalIdeal ↥v.valuationSubring
hx₀ : ¬x = 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = π.val ^ n * ↑u
⊢ x ∈ span {π.val}