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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ ((CoordinateRing.basis W').repr ((p • 1 + q • (mk W') Y) * 1)) 0 *
        ((CoordinateRing.basis W').repr ((p • 1 + q • (mk W') Y) * (CoordinateRing.basis W') 1)) 1 -
      ((CoordinateRing.basis W').repr ((p • 1 + q • (mk W') Y) * (CoordinateRing.basis W') 1)) 0 *
        ((CoordinateRing.basis W').repr ((p • 1 + q • (mk W') Y) * 1)) 1 =
    p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)

Tactic:
mul_one,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ ((CoordinateRing.basis W').repr (p • 1 + q • (mk W') Y)) 0 *
        ((CoordinateRing.basis W').repr ((p • 1 + q • (mk W') Y) * (CoordinateRing.basis W') 1)) 1 -
      ((CoordinateRing.basis W').repr ((p • 1 + q • (mk W') Y) * (CoordinateRing.basis W') 1)) 0 *
        ((CoordinateRing.basis W').repr (p • 1 + q • (mk W') Y)) 1 =
    p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
P : ℕ → Sort u_4
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x✝ : ℕ
ih : (k : ℕ) → k < 2 * (x✝ + 3) → P k
⊢ P (2 * (x✝ + 3))

Tactic:
apply even

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
P : ℕ → Sort u_4
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x✝ : ℕ
ih : (k : ℕ) → k < 2 * (x✝ + 3) → P k
⊢ P (x✝ + 1)

case a
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
P : ℕ → Sort u_4
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x✝ : ℕ
ih : (k : ℕ) → k < 2 * (x✝ + 3) → P k
⊢ P (x✝ + 2)

case a
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
P : ℕ → Sort u_4
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x✝ : ℕ
ih : (k : ℕ) → k < 2 * (x✝ + 3) → P k
⊢ P (x✝ + 3)

case a
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
P : ℕ → Sort u_4
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x✝ : ℕ
ih : (k : ℕ) → k < 2 * (x✝ + 3) → P k
⊢ P (x✝ + 4)

case a
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
P : ℕ → Sort u_4
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x✝ : ℕ
ih : (k : ℕ) → k < 2 * (x✝ + 3) → P k
⊢ P (x✝ + 5)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
m : ℕ
⊢ complEDS' b c d k (2 * (m + 1)) = complEDS' b c d k (m + 1) * complEDS₂ b c d ((↑m + 1) * k)

Tactic:
by
  rw [show 2 * (m + 1) = 2 * m + 2 by rfl, complEDS', dif_pos <| even_two_mul m,
    m.mul_div_cancel_left two_pos, Nat.cast_succ]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
ih : ∀ (n : ℕ), complEDS b c d k (2 * ↑n) = complEDS b c d k ↑n * complEDS₂ b c d (↑n * k)
n✝ : ℕ
⊢ complEDS b c d k (2 * -↑n✝) = complEDS b c d k (-↑n✝) * complEDS₂ b c d (-↑n✝ * k)

Tactic:
mul_neg,

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
ih : ∀ (n : ℕ), complEDS b c d k (2 * ↑n) = complEDS b c d k ↑n * complEDS₂ b c d (↑n * k)
n✝ : ℕ
⊢ complEDS b c d k (-(2 * ↑n✝)) = complEDS b c d k (-↑n✝) * complEDS₂ b c d (-↑n✝ * k)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (X * W.Ψ₃ ^ 2 * 1 - W.preΨ' (2 + 2) * W.preΨ' 2 * if Even 2 then W.Ψ₂Sq else 1) = X * W.Ψ₃ ^ 2 - W.preΨ₄ * W.Ψ₂Sq

Tactic:
mul_one,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (X * W.Ψ₃ ^ 2 - W.preΨ' (2 + 2) * W.preΨ' 2 * if Even 2 then W.Ψ₂Sq else 1) = X * W.Ψ₃ ^ 2 - W.preΨ₄ * W.Ψ₂Sq
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (X * W.Ψ₃ ^ 2 - W.preΨ₄ * 1 * if Even 2 then W.Ψ₂Sq else 1) = X * W.Ψ₃ ^ 2 - W.preΨ₄ * W.Ψ₂Sq

Tactic:
mul_one,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (X * W.Ψ₃ ^ 2 - W.preΨ₄ * if Even 2 then W.Ψ₂Sq else 1) = X * W.Ψ₃ ^ 2 - W.preΨ₄ * W.Ψ₂Sq
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsElliptic
x : Fin 3 → R
i : Fin 3
⊢ ∑ j, (eval x) (C ↑W.Δ'⁻¹ * W.addSubMapCoeff (i, j)) * (eval x) (W.addSubMap j) = x i ^ 4

Tactic:
by
  simp only [eval_mul, eval_C, mul_assoc]
  rw [← Finset.mul_sum, Units.inv_mul_eq_iff_eq_mul, Fin.sum_univ_three, addSubMap, addSubMapCoeff,
    Function.uncurry_apply_pair, coe_Δ', Δ]
  fin_cases i <;> simp <;> grind only [b_relation]

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

Goal state before:
pp: case h.a₄
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ 1 ^ 4 * (E.a₄ - s * 0 + 2 * 0 * E.a₂ - (0 + 0 * s) * E.a₁ + 3 * 0 ^ 2 - 2 * s * 0) = E'.a₄

Tactic:
a₄_of_isCharTwoJNeZeroNF

Goal state after:
case h.a₄
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ 1 ^ 4 * (0 - s * 0 + 2 * 0 * E.a₂ - (0 + 0 * s) * E.a₁ + 3 * 0 ^ 2 - 2 * s * 0) = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ 2 * W.a₄ + W.a₁ * 0 = 0

Tactic:
a₄_of_isCharTwoJNeZeroNF

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ 1 ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - 1 * 0 * W.a₄ + W.a₂ * 0 ^ 2 - W.a₄ ^ 2 = W.a₆ + 4 * W.a₂ * W.a₆

Tactic:
a₄_of_isCharTwoJNeZeroNF

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

Goal state before:
pp: case pos
R : Type u_1
inst✝⁴ : CommRing R
F : Type u_2
inst✝³ : Field F
W✝ : WeierstrassCurve R
inst✝² : CharP R 2
inst✝¹ : CharP F 2
W : WeierstrassCurve F
inst✝ : DecidableEq F
ha₁ : W.a₁ = 0
⊢ (W.toCharTwoJEqZeroNF • W).IsCharTwoNF

Tactic:
have := W.toCharTwoJEqZeroNF_spec ha₁

Goal state after:
case pos
R : Type u_1
inst✝⁴ : CommRing R
F : Type u_2
inst✝³ : Field F
W✝ : WeierstrassCurve R
inst✝² : CharP R 2
inst✝¹ : CharP F 2
W : WeierstrassCurve F
inst✝ : DecidableEq F
ha₁ : W.a₁ = 0
this : (W.toCharTwoJEqZeroNF • W).IsCharTwoJEqZeroNF
⊢ (W.toCharTwoJEqZeroNF • W).IsCharTwoNF
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
heq : E.j = E'.j
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝ : NeZero 2
this : NeZero 4
⊢ 6 ≠ 0

Tactic:
have := mul_ne_zero hchar2 hchar3

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
heq : E.j = E'.j
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝¹ : NeZero 2
this✝ : NeZero 4
this : 2 * 3 ≠ 0
⊢ 6 ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
        (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
      0 →
    (W'.a₁ * b * 1 - (3 * a ^ 2 + 2 * W'.a₂ * a * 1 + W'.a₄ * 1) = 0 ∧
        2 * b + W'.a₁ * a * 1 + W'.a₃ * 1 = 0 ∧
          W'.a₁ * a * b + 3 * W'.a₃ * b * 1 - (2 * W'.a₂ * a ^ 2 * 1 + 4 * W'.a₄ * a * 1 + 6 * W'.a₆ * 1) = 0 ↔
      W'.toAffine.a₁ * b - (3 * a ^ 2 + 2 * W'.toAffine.a₂ * a + W'.toAffine.a₄) = 0 ∧
        2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0)

Tactic:
mul_one,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
        (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
      0 →
    (W'.a₁ * b - (3 * a ^ 2 + 2 * W'.a₂ * a + W'.a₄) = 0 ∧
        2 * b + W'.a₁ * a + W'.a₃ = 0 ∧
          W'.a₁ * a * b + 3 * W'.a₃ * b - (2 * W'.a₂ * a ^ 2 + 4 * W'.a₄ * a + 6 * W'.a₆) = 0 ↔
      W'.toAffine.a₁ * b - (3 * a ^ 2 + 2 * W'.toAffine.a₂ * a + W'.toAffine.a₄) = 0 ∧
        2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
⊢ P ≈ Q

Tactic:
have hQy : IsUnit <| Q y := isUnit_Y_of_Z_eq_zero hQ hQz

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
⊢ P ≈ Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ ![P x, -P y, 0] = ![P x * ![1, 1, 0] x, (-(P y / P x)) ^ 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]

Tactic:
mul_one,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ ![P x, -P y, 0] = ![P x, (-(P y / P x)) ^ 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ ![P x, -P y, 0] = ![P x, -P y * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]

Tactic:
mul_one,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ ![P x, -P y, 0] = ![P x, -P y, -(P y / P x) * ![1, 1, 0] z]
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case mpr
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
⊢ (∃ i, {b | b - a ∈ B i} ⊆ s) → ∃ i ∈ hB.toRingFilterBasis.toAddGroupFilterBasis, (fun y ↦ a + y) '' i ⊆ s

Tactic:
· rintro ⟨i, hi⟩
      use B i
      constructor
      · use i
      · rw [image_subset_iff]
        rintro b b_in
        apply hi
        simpa using b_in

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

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : P z = 0
⊢ (MulAction.orbitRel Fˣ (Fin 3 → F)) ![1, 1, 0] P

Tactic:
exact Setoid.symm <| equiv_zero_of_Z_eq_zero hP hPz

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
⊢ addZ (u • P) (v • Q) = (u * v) ^ 2 * addZ P Q

Tactic:
by
  simp only [addZ, smul_fin3_ext]
  ring1

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

Goal state before:
pp: case h₂
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
⊢ y * w * ↑(s * v) ≤ᵥ x * z * ↑(t * u)

Tactic:
grw [Submonoid.coe_mul, Submonoid.coe_mul,
        veq_mul_mul_mul_comm x, veq_mul_mul_mul_comm y]
      exact mul_vle_mul h₂ h₄

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

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Jacobian R
W : Jacobian F
x✝ : W.Point
⊢ x✝ + 0 = x✝

Tactic:
classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, add_zero]

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

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).neg (⇑f ∘ P) = ⇑f ∘ W'.neg P

Tactic:
simp only [neg, map_negY, comp_fin3]

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 ∘ P) x, f (W'.negY P), (⇑f ∘ P) z] = ![f (P x), f (W'.negY P), f (P z)]
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 x : R
y : ↥(posSubmonoid R)
h : ¬x ≤ᵥ 0
⊢ ValueGroupWithZero.mk (x * ↑y) (y * ⟨x, h⟩) = ValueGroupWithZero.mk 1 1

Tactic:
ValueGroupWithZero.mk_eq_mk,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x : R
y : ↥(posSubmonoid R)
h : ¬x ≤ᵥ 0
⊢ x * ↑y * ↑1 ≤ᵥ 1 * ↑(y * ⟨x, h⟩) ∧ 1 * ↑(y * ⟨x, h⟩) ≤ᵥ x * ↑y * ↑1
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ 𝓝 0 ⊓ Filter.comap coe' (𝓝 y) = ⊥

Tactic:
rw [isDenseInducing_coe.nhds_eq_comap (0 : K), ← Filter.comap_inf]

Goal state after:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ Filter.comap coe' (𝓝 ↑0 ⊓ 𝓝 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.negAddY P Q = (-addU P Q) ^ 3

Tactic:
rw [addU, neg_neg, div_pow, ← negAddY_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]

Goal state after:
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.valuationSubring
h1 : v.IsUniformizer ↑π₁
u : (↥v.valuationSubring)ˣ
hu : π₁ * ↑u = π₂
this : v ↑↑u = 1
⊢ v ↑π₁ * 1 = ↑(generator v)

Tactic:
mul_one,

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer ↑π₁
u : (↥v.valuationSubring)ˣ
hu : π₁ * ↑u = π₂
this : v ↑↑u = 1
⊢ v ↑π₁ = ↑(generator v)
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 = ⊥
⊢ Submodule.IsPrincipal P

Tactic:
rw [h_ne_bot]

Goal state after:
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 = ⊥
⊢ Submodule.IsPrincipal ⊥
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)) ⋯)}
y : R := (equiv v) x
hy : toVal v y = x
hs0' : 0 < Valued.v.restrict (toVal v s)
h' : v.restrict.IsEquiv w.restrict
⊢ (equiv v) x ∈ {x | Valued.v.restrict x < ↑γ}

Tactic:
rw [← hr, equiv_apply, Set.mem_ofPred_eq, lt_div_iff₀ ((restrict_pos_iff Valued.v s).mpr hs₀), hv,
    ← map_mul, ← lt_def, ← ofVal_mul,
    ← hy, ← toVal_mul, ←  h'.orderRingIso_apply, ← h'.orderRingIso.lt_symm_apply]

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
hy : toVal v y = x
hs0' : 0 < Valued.v.restrict (toVal v s)
h' : v.restrict.IsEquiv w.restrict
⊢ toVal v.restrict (y * s) < h'.orderRingIso.symm (toVal w.restrict r)
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
⊢ x⁻¹ - y⁻¹ = x⁻¹ * 1 - 1 * y⁻¹

Tactic:
mul_one,

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
⊢ x⁻¹ - y⁻¹ = x⁻¹ - 1 * y⁻¹
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)))⁻¹ *
      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

Tactic:
mul_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
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.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
this : (some ⁻¹' s).Subsingleton
x y : ↑s
H : x < y
z : ↑s
hz : x < z
hz' : z < y
⊢ ⊥ < ↑z

Tactic:
simp [(Subtype.coe_lt_coe.mpr hz).trans_le']

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: e : ℤ ≃+o ℤ
H : ↑e = AddEquiv.neg ℤ
⊢ False

Tactic:
replace H : e 1 = -1 := congr($H 1)

Goal state after:
e : ℤ ≃+o ℤ
H : e 1 = -1
⊢ False
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 ∈ 𝓝 1, ∀ (x : K), ↑x ∈ V → v x = 1

Tactic:
Completion.isDenseInducing_coe.nhds_eq_comap,

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} ∈ Filter.comap Completion.coe' (𝓝 ↑1)
⊢ ∃ V ∈ 𝓝 1, ∀ (x : K), ↑x ∈ V → v x = 1
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
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₀, ∃ y₀ ∈ V', ↑z₀ = y₀ * x₀ ∧ z₀ ≠ 0

Tactic:
rcases Completion.denseRange_coe.mem_nhds nhds_right with ⟨z₀, y₀, y₀_in, H : y₀ * x₀ = z₀⟩

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'
H : y₀ * x₀ = ↑z₀
⊢ ∃ z₀, ∃ y₀ ∈ V', ↑z₀ = y₀ * x₀ ∧ z₀ ≠ 0
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 ↔ ¬DenselyOrdered A

Tactic:
by
  rw [← discrete_iff_not_denselyOrdered, isAddCyclic_iff_nonempty_equiv_int]

Goal state after: