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

Goal state before:
pp: case refine_1
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ sX x = sX ((X.fromSpecStalk x) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)))

Tactic:
Scheme.fromSpecStalk_closedPoint

Goal state after:
case refine_1
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ sX x = sX x
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X.PartialMap Y
e✝ : f.toRationalMap.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
U : X.Opens
hU : Dense ↑U
hUl : U ≤ ((fun x ↦ x.compHom (Y ↘ S)) f).domain
hUr : U ≤ (Hom.toPartialMap (X ↘ S)).domain
e : (((fun x ↦ x.compHom (Y ↘ S)) f).restrict U hU hUl).hom = ((Hom.toPartialMap (X ↘ S)).restrict U hU hUr).hom
⊢ PartialMap.IsOver S (f.restrict U hU hUl)

Tactic:
by simpa using! e

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: case a
⊢ @UniversallyInjective ≤ diagonal @Surjective

Tactic:
intro X Y f hf

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
hf : UniversallyInjective f
⊢ diagonal (@Surjective) f
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, ↑t = U
H : ∀ t ∈ s, IsCompactOpenCovered f ↑t
⊢ IsCompactOpenCovered f U

Tactic:
obtain ⟨t, ht⟩ := hU.elim_finite_subcover (fun V : s ↦ V.1) (fun V ↦ V.1.2) (by simp [← hs])
  refine of_biUnion_eq_of_finite (SetLike.coe '' (t.image Subtype.val : Set (Opens S))) ?_ ?_ ?_
  · exact subset_antisymm (fun x h ↦ by aesop) (subset_trans ht <| by simp)
  · exact Set.toFinite _
  · grind

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case neg
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
l : Fin n
m : ℕ
hlj : ¬l = j
⊢ (c.val l).coeff m ∈ coeffSubmodule R₀ c ^ (c.val j).degree.succ

Tactic:
have : (c.val j).degree.succ ≠ 0 := by
            rw [← Nat.pos_iff_ne_zero]
            apply WithBot.succ_lt_succ (x := ⊥)
            refine lt_of_lt_of_le ?_ hle
            rw [bot_lt_iff_ne_bot, ne_eq, degree_eq_bot]
            intro e
            simp [e] at hi
          refine le_self_pow c.one_le_coeffSubmodule this ?_
          exact Submodule.subset_span (.inr (Set.mem_iUnion_of_mem l ⟨m, rfl⟩))

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.b₂ = W.a₁ ^ 2 + W.a₂

Tactic:
rw [b₂]
  linear_combination W.a₂ * CharP.cast_eq_zero R 3

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k : ℕ
D : ℕ → ℕ
⊢ numBound k D 0 = k

Tactic:
numBound

Goal state after:
k : ℕ
D : ℕ → ℕ
⊢ k = k
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ numBound k D (n + 1) = numBound k D n * degBound k D n * D n

Tactic:
numBound

Goal state after:
k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ numBound k D n * degBound k D n * D n = numBound k D n * degBound k D n * D n
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ degBound k₁ D₁ (n + 1) ≤ degBound k₂ D₂ (n + 1)

Tactic:
rw [degBound_succ, degBound_succ]
    refine Nat.mul_le_mul (Nat.pow_self_mono (numBound_mono hk _ hD)) (degBound_le_degBound hk _
      fun i hi ↦ hD _ (hi.trans n.lt_succ_self))

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y - (C (C 2) * Y + C (C W'.a₁ * X + C W'.a₃)) = -Y - C (C W'.a₁ * X + C W'.a₃)

Tactic:
C_simp

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y - (2 * Y + (C (C W'.a₁) * C X + C (C W'.a₃))) = -Y - (C (C W'.a₁) * C X + C (C W'.a₃))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ C
      ((C ℓ * (X - C x) + C y) ^ 2 + (C W'.a₁ * X + C W'.a₃) * (C ℓ * (X - C x) + C y) -
        (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) =
    (Y - C (C ℓ * (X - C x) + C y)) * (-Y - C (C W'.a₁ * X + C W'.a₃) - C (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₆))

Tactic:
C_simp

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ (C ℓ * (X - C x) + C y) ^ 2 + (C W'.a₁ * X + C W'.a₃) * (C ℓ * (X - C x) + C y) -
      (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) =
    -(C 1 * X ^ 3 + C (-ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂) * X ^ 2 +
          C (2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄)) * X +
        C (-x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆)))

Tactic:
C_simp

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ (C ℓ * (X - C x) + C y) ^ 2 + (C W'.a₁ * X + C W'.a₃) * (C ℓ * (X - C x) + C y) -
      (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) =
    -(1 * X ^ 3 + (-C ℓ ^ 2 - C W'.a₁ * C ℓ + C W'.a₂) * X ^ 2 +
          (2 * C x * C ℓ ^ 2 + (C W'.a₁ * C x - 2 * C y - C W'.a₃) * C ℓ + (-C W'.a₁ * C y + C W'.a₄)) * X +
        (-C x ^ 2 * C ℓ ^ 2 + (2 * C x * C y + C W'.a₃ * C x) * C ℓ - (C y ^ 2 + C W'.a₃ * C y - C W'.a₆)))
Module: Mathlib.LinearAlgebra.FreeModule.Norm

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
i : ι
⊢ (∑ x, if x = i then (smithCoeffs b (span {f}) ⋯ i * 1) • b' x else 0 • b' x) =
    (↑(Algebra.lmul R S).toRingHom f)
      ((LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
        ((b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι)) (b' i)))

Tactic:
zero_smul,

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
i : ι
⊢ (∑ x, if x = i then (smithCoeffs b (span {f}) ⋯ i * 1) • b' x else 0) =
    (↑(Algebra.lmul R S).toRingHom f)
      ((LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
        ((b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι)) (b' i)))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective ⇑f
p q : R[X]
hy : Polynomial.map f p • 1 + Polynomial.map f q • (mk (W'.map f)) Y = 0
hp : p = 0
hq : q = 0
⊢ 0 • 1 + 0 • (mk W') Y = 0

Tactic:
zero_smul,

Goal state after:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective ⇑f
p q : R[X]
hy : Polynomial.map f p • 1 + Polynomial.map f q • (mk (W'.map f)) Y = 0
hp : p = 0
hq : q = 0
⊢ 0 + 0 = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case e_a.e_6
R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ Y - C (C (-(ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - W'.a₁ * W'.addX x₁ x₂ ℓ - W'.a₃)) +
      C (X - C (W'.addX x₁ x₂ ℓ)) * C (C (W'.a₁ + ℓ)) =
    C (C W'.a₁ * X + C W'.a₃) + C (C ℓ * (X - C x₁) + C y₁) + Y

Tactic:
C_simp

Goal state after:
case e_a.e_6
R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ Y -
        (-(C (C ℓ) * (C (C (W'.addX x₁ x₂ ℓ)) - C (C x₁)) + C (C y₁)) - C (C W'.a₁) * C (C (W'.addX x₁ x₂ ℓ)) -
          C (C W'.a₃)) +
      (C X - C (C (W'.addX x₁ x₂ ℓ))) * (C (C W'.a₁) + C (C ℓ)) =
    C (C W'.a₁) * C X + C (C W'.a₃) + (C (C ℓ) * (C X - C (C x₁)) + C (C y₁)) + Y
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case e_a.e_6
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ Y - C (C y) + C (X - C x) * C (C (-ℓ)) = Y - C (C ℓ * (X - C x) + C y)

Tactic:
C_simp

Goal state after:
case e_a.e_6
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ Y - C (C y) + (C X - C (C x)) * -C (C ℓ) = Y - (C (C ℓ) * (C X - C (C x)) + C (C y))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case e_a.e_6
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
⊢ Y - C (C (W.slope x₁ x₂ y₁ y₂ * (x₂ - x₁) + y₁)) + C (X - C x₂) * C (C (-W.slope x₁ x₂ y₁ y₂)) =
    Y - C (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁)

Tactic:
C_simp

Goal state after:
case e_a.e_6
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
⊢ Y - (C (C (W.slope x₁ x₂ y₁ y₂)) * (C (C x₂) - C (C x₁)) + C (C y₁)) +
      (C X - C (C x₂)) * -C (C (W.slope x₁ x₂ y₁ y₂)) =
    Y - (C (C (W.slope x₁ x₂ y₁ y₂)) * (C X - C (C x₁)) + C (C y₁))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ (Y - C (C y)) * (Y - C (C (-y - W.a₁ * x - W.a₃))) -
          C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) +
        C (C (y ^ 2 + W.a₁ * x * y + W.a₃ * 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₆)) * 1 +
        C (C (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆))) =
    0

Tactic:
C_simp

Goal state after:
case a
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ (Y - C (C y)) * (Y - (-C (C y) - C (C W.a₁) * C (C x) - C (C W.a₃))) -
          (C X - C (C x)) *
            (C X ^ 2 + (C (C x) + C (C W.a₂)) * C X + (C (C x) ^ 2 + C (C W.a₂) * C (C x) + C (C W.a₄)) -
              C (C W.a₁) * Y) +
        (C (C y) ^ 2 + C (C W.a₁) * C (C x) * C (C y) + C (C W.a₃) * C (C y)) -
      ((Y ^ 2 + (C (C W.a₁) * C X + C (C W.a₃)) * Y -
            (C X ^ 3 + C (C W.a₂) * C X ^ 2 + C (C W.a₄) * C X + C (C W.a₆))) *
          1 +
        (C (C x) ^ 3 + C (C W.a₂) * C (C x) ^ 2 + C (C W.a₄) * C (C x) + C (C W.a₆))) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case inl
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
hx : W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0
W_X : F := W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)
⊢ C (C (1 * -1)) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    C (C (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄))) * 1 + C (C 1 * -(X + C (2 * x + W.a₂)) * (X - C x)) +
        C (C (1 * W.a₁)) * (Y - C (C y)) +
      C (C (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄))) * 0 * (Y - C (C (W.negY x y)))

Tactic:
C_simp

Goal state after:
case inl
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
hx : W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0
W_X : F := W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)
⊢ 1 * -1 *
      (C X ^ 2 + (C (C x) + C (C W.a₂)) * C X + (C (C x) ^ 2 + C (C W.a₂) * C (C x) + C (C W.a₄)) - C (C W.a₁) * Y) =
    (C (C W.a₁) * C (C y) - (3 * C (C x) ^ 2 + 2 * C (C W.a₂) * C (C x) + C (C W.a₄))) * 1 +
          1 * -(C X + (2 * C (C x) + C (C W.a₂))) * (C X - C (C x)) +
        1 * C (C W.a₁) * (Y - C (C y)) +
      (C (C W.a₁) * C (C y) - (3 * C (C x) ^ 2 + 2 * C (C W.a₂) * C (C x) + C (C W.a₄))) * 0 * (Y - C (C (W.negY x y)))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case inr
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
hy : 2 * y + W.a₁ * x + W.a₃ ≠ 0
W_Y : F := 2 * y + W.a₁ * x + W.a₃
⊢ C (C (2 * y + W.a₁ * x + W.a₃)) * 0 * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    C (C (2 * y + W.a₁ * x + W.a₃)) * 1 + C (C (2 * y + W.a₁ * x + W.a₃)) * 0 * C (X - C x) + C (C 1) * (Y - C (C y)) +
      C (C (1 * -1)) * (Y - C (C (-y - W.a₁ * x - W.a₃)))

Tactic:
C_simp

Goal state after:
case inr
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
hy : 2 * y + W.a₁ * x + W.a₃ ≠ 0
W_Y : F := 2 * y + W.a₁ * x + W.a₃
⊢ (2 * C (C y) + C (C W.a₁) * C (C x) + C (C W.a₃)) * 0 *
      (C X ^ 2 + (C (C x) + C (C W.a₂)) * C X + (C (C x) ^ 2 + C (C W.a₂) * C (C x) + C (C W.a₄)) - C (C W.a₁) * Y) =
    (2 * C (C y) + C (C W.a₁) * C (C x) + C (C W.a₃)) * 1 +
          (2 * C (C y) + C (C W.a₁) * C (C x) + C (C W.a₃)) * 0 * (C X - C (C x)) +
        1 * (Y - C (C y)) +
      1 * -1 * (Y - (-C (C y) - C (C W.a₁) * C (C x) - C (C W.a₃)))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: case pos
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₁
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

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₁
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
· rwa [negAddY, hx₁, sub_self, mul_zero, zero_add]

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₁
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
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 x₂ (-((y₁ - y₂) / (x₁ - x₂) * (x₁ - x₂)) + y₁)

Tactic:
div_mul_cancel₀ _ <| sub_ne_zero_of_ne 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₂ (-(y₁ - y₂) + y₁)
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 := (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₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 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 * (2 * W.a₄ + W.a₁ * W.a₃))) *
                (X - C x₁)) +
          C (C ((y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2)) * 0 * C (X - C x₁) +
        -4 * C (C (y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁))) =
    0

Tactic:
C_simp

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
⊢ 1 * (Y - (-Y - (C (C W.a₁) * C X + C (C W.a₃)))) * (Y - (-Y - (C (C W.a₁) * C X + C (C W.a₃)))) +
        -4 * (C (C x₁) ^ 3 + C (C W.a₂) * C (C x₁) ^ 2 + C (C W.a₄) * C (C x₁) + C (C W.a₆)) -
      ((C (C y₁) - (-C (C y₁) - C (C W.a₁) * C (C x₁) - C (C W.a₃))) ^ 2 * 1 +
              1 * 4 *
                (Y ^ 2 + (C (C W.a₁) * C X + C (C W.a₃)) * Y -
                  (C X ^ 3 + C (C W.a₂) * C X ^ 2 + C (C W.a₄) * C X + C (C W.a₆))) +
            (1 * 4 * C X ^ 2 + (1 * 4 * C (C x₁) + 1 * (C (C W.a₁) ^ 2 + 4 * C (C W.a₂))) * C X +
                (1 * 4 * C (C x₁) ^ 2 + 1 * (C (C W.a₁) ^ 2 + 4 * C (C W.a₂)) * C (C x₁) +
                  1 * 2 * (2 * C (C W.a₄) + C (C W.a₁) * C (C W.a₃)))) *
              (C X - C (C x₁)) +
          (C (C y₁) - (-C (C y₁) - C (C W.a₁) * C (C x₁) - C (C W.a₃))) ^ 2 * 0 * (C X - C (C x₁)) +
        -4 * (C (C y₁) ^ 2 + C (C W.a₁) * C (C x₁) * C (C y₁) + C (C W.a₃) * C (C y₁))) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

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.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
hx : x₁ - x₂ ≠ 0
⊢ C (C (x₁ - x₂)) * 0 * (Y - W.negPolynomial) = C (C (x₁ - x₂)) * 1 + C (C 1 * (X - C x₁)) + C (C (1 * -1) * (X - C x₂))

Tactic:
C_simp

Goal state after:
case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
hx : x₁ - x₂ ≠ 0
⊢ (C (C x₁) - C (C x₂)) * 0 * (Y - W.negPolynomial) =
    (C (C x₁) - C (C x₂)) * 1 + 1 * (C X - C (C x₁)) + 1 * -1 * (C X - C (C x₂))
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
n : ℕ
⊢ normEDS b c d ↑n = preNormEDS' (b ^ 4) c d n * if Even n then b else 1

Tactic:
by
  simp [normEDS]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ normEDS b c d 0 = 0

Tactic:
by
  simp [normEDS]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ normEDS b c d 1 = 1

Tactic:
by
  simp [normEDS]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ normEDS b c d 2 = b

Tactic:
by
  simp [normEDS]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ C (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₆)) -
      (C p + C q * Y) * (C p + C q * (-Y - C (C W'.a₁ * X + C W'.a₃))) =
    (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 q ^ 2

Tactic:
C_simp

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ C p ^ 2 - C p * C q * (C (C W'.a₁) * C X + C (C W'.a₃)) -
        C q ^ 2 * (C X ^ 3 + C (C W'.a₂) * C X ^ 2 + C (C W'.a₄) * C X + C (C W'.a₆)) -
      (C p + C q * Y) * (C p + C q * (-Y - (C (C W'.a₁) * C X + C (C W'.a₃)))) =
    (Y ^ 2 + (C (C W'.a₁) * C X + C (C W'.a₃)) * Y -
        (C X ^ 3 + C (C W'.a₂) * C X ^ 2 + C (C W'.a₄) * C X + C (C W'.a₆))) *
      C q ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case neg
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
hp : ¬p = 0
⊢ (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₆)).degree =
    max (2 • p.degree) (2 • q.degree + 3)

Tactic:
by_cases hq : q = 0

Goal state after:
case pos
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
hp : ¬p = 0
hq : q = 0
⊢ (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₆)).degree =
    max (2 • p.degree) (2 • q.degree + 3)

case neg
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
hp : ¬p = 0
hq : ¬q = 0
⊢ (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₆)).degree =
    max (2 • p.degree) (2 • q.degree + 3)