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

Goal state before:
pp: case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
hx : ¬x₁ = x₂
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (-(W.slope x₁ x₂ y₁ y₂ * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) + y₁)

Tactic:
hx₂,

Goal state after:
case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
hx : ¬x₁ = x₂
⊢ W.Nonsingular x₂ (-(W.slope x₁ x₂ y₁ y₂ * (x₁ - x₂)) + y₁)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
S : Type s
F : Type u
K : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field F
inst✝⁹ : Field K
W' : Affine R
inst✝⁸ : Algebra R S
inst✝⁷ : DecidableEq F
inst✝⁶ : DecidableEq K
inst✝⁵ : Algebra R F
inst✝⁴ : Algebra S F
inst✝³ : IsScalarTower R S F
inst✝² : Algebra R K
inst✝¹ : Algebra S K
inst✝ : IsScalarTower R S K
f : F →ₐ[S] K
x₁ x₂ y₁ y₂ : F
⊢ (W'⁄K).slope (f x₁) (f x₂) (f y₁) (f y₂) = f ((W'⁄F).slope x₁ x₂ y₁ y₂)

Tactic:
by
  rw [← RingHom.coe_coe, ← map_slope, map_baseChange]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
i : Fin 3
⊢ (![s ^ 2 - C W.b₄ * s * u - C W.b₆ * t * u - C W.b₈ * u ^ 2,
          C 2 * t * s + C W.b₂ * s * u + C W.b₄ * t * u + C W.b₆ * u ^ 2, t ^ 2 - C 4 * s * u]
        i).IsHomogeneous
    2

Tactic:
fin_cases i

Goal state after:
case «0»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (![s ^ 2 - C W.b₄ * s * u - C W.b₆ * t * u - C W.b₈ * u ^ 2,
          C 2 * t * s + C W.b₂ * s * u + C W.b₄ * t * u + C W.b₆ * u ^ 2, t ^ 2 - C 4 * s * u]
        ((fun i ↦ i) ⟨0, ⋯⟩)).IsHomogeneous
    2

case «1»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (![s ^ 2 - C W.b₄ * s * u - C W.b₆ * t * u - C W.b₈ * u ^ 2,
          C 2 * t * s + C W.b₂ * s * u + C W.b₄ * t * u + C W.b₆ * u ^ 2, t ^ 2 - C 4 * s * u]
        ((fun i ↦ i) ⟨1, ⋯⟩)).IsHomogeneous
    2

case «2»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (![s ^ 2 - C W.b₄ * s * u - C W.b₆ * t * u - C W.b₈ * u ^ 2,
          C 2 * t * s + C W.b₂ * s * u + C W.b₄ * t * u + C W.b₆ * u ^ 2, t ^ 2 - C 4 * s * u]
        ((fun i ↦ i) ⟨2, ⋯⟩)).IsHomogeneous
    2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
h : IsEllipticSequence W
x : R
p q r : ℤ
⊢ IsEllipticNet.rel (x • W) p q r 0 + x ^ 4 * 0 - (0 + x ^ 4 * IsEllipticNet.rel W p q r 0) = 0

Tactic:
simp [IsEllipticNet.rel]; ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * ↑m) =
    preNormEDS b c d (↑m - 1) ^ 2 * preNormEDS b c d ↑m * preNormEDS b c d (↑m + 2) -
      preNormEDS b c d (↑m - 2) * preNormEDS b c d ↑m * preNormEDS b c d (↑m + 1) ^ 2

Tactic:
rcases m with _ | _ | _ | m
    iterate 3 simp
    simp_rw [Nat.cast_succ, Int.add_sub_cancel, show (m : ℤ) + 1 + 1 + 1 = m + 1 + 2 by rfl,
      Int.add_sub_cancel]
    norm_cast
    simpa only [preNormEDS_ofNat] using preNormEDS'_even ..

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
rcases m with _ | _

Goal state after:
case nat.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ complEDS b c d k (2 * ↑0) = complEDS b c d k ↑0 * complEDS₂ b c d (↑0 * k)

case nat.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n✝ : ℕ
⊢ complEDS b c d k (2 * ↑(n✝ + 1)) = complEDS b c d k ↑(n✝ + 1) * complEDS₂ b c d (↑(n✝ + 1) * k)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat
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 ^ 2 * normEDS b c d ((↑m + 1) * k + 1) * normEDS b c d ((↑m + 1) * k - 1) -
      complEDS b c d k (↑m + 1) ^ 2 * normEDS b c d (↑m * k + 1) * normEDS b c d (↑m * k - 1)

Tactic:
rcases m with _ | _

Goal state after:
case nat.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ complEDS b c d k (2 * ↑0 + 1) =
    complEDS b c d k ↑0 ^ 2 * normEDS b c d ((↑0 + 1) * k + 1) * normEDS b c d ((↑0 + 1) * k - 1) -
      complEDS b c d k (↑0 + 1) ^ 2 * normEDS b c d (↑0 * k + 1) * normEDS b c d (↑0 * k - 1)

case nat.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n✝ : ℕ
⊢ complEDS b c d k (2 * ↑(n✝ + 1) + 1) =
    complEDS b c d k ↑(n✝ + 1) ^ 2 * normEDS b c d ((↑(n✝ + 1) + 1) * k + 1) * normEDS b c d ((↑(n✝ + 1) + 1) * k - 1) -
      complEDS b c d k (↑(n✝ + 1) + 1) ^ 2 * normEDS b c d (↑(n✝ + 1) * k + 1) * normEDS b c d (↑(n✝ + 1) * k - 1)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_1
I : Type u
inst✝⁶ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁵ : IsCofiltered I
inst✝⁴ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝³ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝² : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
𝒰 : c.pt.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : Finite 𝒰.I₀
i : I
V : 𝒰.I₀ → (D.obj i).Opens
hV : TopologicalSpace.IsOpenCover V
hV' : ∀ (j : 𝒰.I₀), IsAffineOpen (V j) ∧ Hom.opensRange (𝒰.f j) = c.π.app i ⁻¹ᵁ V j
hV'' : ∀ (k : 𝒰.I₀), Set.range ⇑(𝒰.f k) = ⇑(c.π.app i) ⁻¹' ↑(V k)
⊢ (Presieve.ofArrows (fun i_1 ↦ Spec ((fun k ↦ Γ(D.obj i, V k)) i_1)) fun k ↦ ⋯.isoSpec.inv ≫ (V k).ι) ∈
    zariskiPrecoverage.coverings (D.obj i)

Tactic:
simp only [IsAffineOpen.isoSpec_inv_ι, ofArrows_mem_precoverage_iff,
      IsAffineOpen.range_fromSpec, SetLike.mem_coe]
    exact ⟨fun x ↦ hV.exists_mem x, inferInstance⟩

Goal state after:
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.a₁ ^ 2 + 4 * W.a₂) * X ^ 2 + C (2 * (2 * W.a₄ + W.a₁ * W.a₃)) * X + C (W.a₃ ^ 2 + 4 * W.a₆)) =
    W.toAffine.polynomialY ^ 2 - 4 * W.toAffine.polynomial

Tactic:
Affine.polynomialY,

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 * (2 * W.a₄ + W.a₁ * W.a₃)) * X + C (W.a₃ ^ 2 + 4 * W.a₆)) =
    (C (C 2) * Y + C (C W.toAffine.a₁ * X + C W.toAffine.a₃)) ^ 2 - 4 * W.toAffine.polynomial
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 0 = 1

Tactic:
simp [Φ]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 1 = X

Tactic:
simp [Φ]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
k : ↥s → I
fk : (j : ↥s) → k j ⟶ i
hk : ∀ (j : ↥s), D.map (fk j) ⁻¹ᵁ 𝒱 j ≤ D.map (fk j) ⁻¹ᵁ t.app i ⁻¹ᵁ ↑(↑(↑↑j).2).2
i' : I
fi'i : i' ⟶ i
fi' : (x : ↥s) → i' ⟶ k x
hfi' : ∀ (x : ↥s), fi' x ≫ fk x = fi'i
j : ↥s
⊢ D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2

Tactic:
← hfi',

Goal state after:
I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
k : ↥s → I
fk : (j : ↥s) → k j ⟶ i
hk : ∀ (j : ↥s), D.map (fk j) ⁻¹ᵁ 𝒱 j ≤ D.map (fk j) ⁻¹ᵁ t.app i ⁻¹ᵁ ↑(↑(↑↑j).2).2
i' : I
fi'i : i' ⟶ i
fi' : (x : ↥s) → i' ⟶ k x
hfi' : ∀ (x : ↥s), fi' x ≫ fk x = fi'i
j : ↥s
⊢ D.map (fi' ?m.418 ≫ fk ?m.418) ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2

I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
k : ↥s → I
fk : (j : ↥s) → k j ⟶ i
hk : ∀ (j : ↥s), D.map (fk j) ⁻¹ᵁ 𝒱 j ≤ D.map (fk j) ⁻¹ᵁ t.app i ⁻¹ᵁ ↑(↑(↑↑j).2).2
i' : I
fi'i : i' ⟶ i
fi' : (x : ↥s) → i' ⟶ k x
hfi' : ∀ (x : ↥s), fi' x ≫ fk x = fi'i
j : ↥s
⊢ ↥s
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 2
inst✝¹ : E.IsCharTwoJEqZeroNF
inst✝ : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero 3
u : F
hu : u ^ 3 = E.a₃ / E'.a₃
s : F
hs : 1 * s ^ 4 + E.a₃ * s + (E.a₄ - u ^ 4 * E'.a₄) = 0
t : F
ht : 1 * t ^ 2 + E.a₃ * t + (s ^ 6 + E.a₄ * s ^ 2 + E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ ∃ C, C • E = E'

Tactic:
use ⟨Units.mk0 u hu0, s ^ 2, s, t⟩

Goal state after:
case h
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJEqZeroNF
inst✝ : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero 3
u : F
hu : u ^ 3 = E.a₃ / E'.a₃
s : F
hs : 1 * s ^ 4 + E.a₃ * s + (E.a₄ - u ^ 4 * E'.a₄) = 0
t : F
ht : 1 * t ^ 2 + E.a₃ * t + (s ^ 6 + E.a₄ * s ^ 2 + E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ { u := Units.mk0 u hu0, r := s ^ 2, s := s, t := t } • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
hQz : Q z ∈ nonZeroDivisors R
u : Rˣ
hz : (fun m ↦ m • Q) u z = Q z
⊢ 1 • Q = Q

Tactic:
rw [one_smul]

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
hP : ∀ (u : R) {P : Fin 3 → R}, W'.Equation P → W'.Equation (u • P)
h : W'.Equation (u • P)
⊢ P = ↑hu.unit⁻¹ • u • P

Tactic:
rw [smul_smul, hu.val_inv_mul, one_smul]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (W.ΨSq n).coeff (n.natAbs ^ 2 - 1) = ↑n ^ 2

Tactic:
by
  induction n using Int.negInduction with
  | nat n => exact_mod_cast (W.natDegree_coeff_ΨSq_ofNat n).right
  | neg ih => rw [ΨSq_neg, Int.natAbs_neg, ← Int.cast_pow, neg_sq, Int.cast_pow, ih]

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
hn : ¬1 < n.natAbs
⊢ W.ΨSq n ≠ 0

Tactic:
rcases hm : n.natAbs with _ | m
    · push_cast [Int.natAbs_eq_zero.mp hm, ne_self_iff_false] at h
    · rcases Int.natAbs_eq_iff.mp hm with rfl | rfl <;>
        rw [hm, Nat.lt_add_left_iff_pos, Nat.not_lt_eq, Nat.le_zero] at hn <;>
        push_cast [hn, ΨSq_neg, ΨSq_one] <;>
        exact fun h' => h <| C_injective <| by push_cast [hn, C_neg, C_1, h', neg_zero, C_0]; rfl

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

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -(-3 * P x ^ 2) * (W'.dblX P - P x * (P y - W'.negY P) ^ 2) + P y * (P y - W'.negY P) ^ 3 +
        (8 * P y ^ 2 - 4 * P x ^ 3) * P x ^ 3 -
      (-(P x ^ 2) ^ 3 + (8 * P y ^ 2 - 4 * P x ^ 3) * P y ^ 2) =
    0

Tactic:
dblX_of_Z_eq_zero hP hPz,

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -(-3 * P x ^ 2) * ((P x ^ 2) ^ 2 - P x * (P y - W'.negY P) ^ 2) + P y * (P y - W'.negY P) ^ 3 +
        (8 * P y ^ 2 - 4 * P x ^ 3) * P x ^ 3 -
      (-(P x ^ 2) ^ 3 + (8 * P y ^ 2 - 4 * P x ^ 3) * P y ^ 2) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
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
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
this :
  W.Nonsingular
    ![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]
⊢ W.Nonsingular (W.add P Q)

Tactic:
by_cases hx : P x * Q z ^ 2 = Q x * P z ^ 2

Goal state after:
case pos
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
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
this :
  W.Nonsingular
    ![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]
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.Nonsingular (W.add P Q)

case neg
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
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
this :
  W.Nonsingular
    ![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]
hx : ¬P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.Nonsingular (W.add P Q)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation 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)
⊢ W.addMap ⟦P⟧ ⟦Q⟧ =
    ⟦![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]⟧

Tactic:
by_cases hx : P x * Q z ^ 2 = Q x * P z ^ 2

Goal state after:
case pos
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation 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)
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addMap ⟦P⟧ ⟦Q⟧ =
    ⟦![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]⟧

case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation 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)
hx : ¬P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addMap ⟦P⟧ ⟦Q⟧ =
    ⟦![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]⟧
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
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
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Tactic:
by_cases hx : P x * Q z ^ 2 = Q x * P z ^ 2

Goal state after:
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

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.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
  induction b using ValueGroupWithZero.ind
  simpa using hdist _ _ _ _

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

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
s : Set Γ₀
⊢ ((0 ∈ s → s ∈ 𝓝 0) ∧ ∀ (b : Γ₀), b ≠ 0 → b ∈ s → s ∈ 𝓝 b) ↔ 0 ∉ s ∨ ∃ γ, γ ≠ 0 ∧ Iio γ ⊆ s

Tactic:
simp +contextual [nhds_of_ne_zero, imp_iff_not_or,
    hasBasis_nhds_zero.mem_iff]

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

Goal state before:
pp: α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
x y : α
⊢ (inseparableSetoid α) x y ↔ (Submodule.quotientRel ⊥.closure) x y

Tactic:
rw [inseparableSetoid_ring]

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

Goal state before:
pp: α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
⊢ Relator.LiftFun (⇑(inseparableSetoid α)) (⇑(Submodule.quotientRel ⊥.closure)) id id

Tactic:
rw [inseparableSetoid_ring]

Goal state after:
α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
⊢ Relator.LiftFun (⇑(Submodule.quotientRel ⊥.closure)) (⇑(Submodule.quotientRel ⊥.closure)) id id
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
⊢ Relator.LiftFun (⇑(Submodule.quotientRel ⊥.closure)) (⇑(inseparableSetoid α)) id id

Tactic:
rw [inseparableSetoid_ring]

Goal state after:
α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
⊢ Relator.LiftFun (⇑(Submodule.quotientRel ⊥.closure)) (⇑(Submodule.quotientRel ⊥.closure)) id id
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
a : G
ha : a ∈ closure {x}
⊢ (fun x_1 ↦ ⟨1, ⋯⟩) ((fun x_1 ↦ ⟨1, ⋯⟩) ⟨a, ha⟩) = ⟨a, ha⟩

Tactic:
simpa [hx, closure_singleton_one, eq_comm] using ha

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

Goal state before:
pp: case h.left
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ : ∀ x ∈ M₀, ↑γ₀ ≤ v.restrict x
γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
H₁ : ∀ x ∈ M₁, ∀ y ∈ M₁, v.restrict (y - x) < ↑(min (γ * γ₀ * γ₀) γ₀)
⊢ M₀ ∩ M₁ ⊆ (fun x ↦ x⁻¹) ⁻¹' (fun x ↦ x⁻¹) '' (M₀ ∩ M₁)

Tactic:
exact subset_preimage_image _ _

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
⊢ 1 < y'

Tactic:
simp [hy', eq_comm, ← hxy, hx]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
⊢ ∀ (x : G ≃+o ℤ), ¬DenselyOrdered G

Tactic:
intro e H

Goal state after:
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
e : G ≃+o ℤ
H : DenselyOrdered G
⊢ False