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

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
⊢ (-P x * Q y ^ 2 * P z + Q x * P y ^ 2 * Q z - 2 * P x * P y * Q y * Q z + 2 * Q x * P y * Q y * P z -
                                  W'.a₁ * P x ^ 2 * Q y * Q z +
                                W'.a₁ * Q x ^ 2 * P y * P z +
                              W'.a₂ * P x ^ 2 * Q x * Q z -
                            W'.a₂ * P x * Q x ^ 2 * P z -
                          W'.a₃ * P x * P y * Q z ^ 2 +
                        W'.a₃ * Q x * Q y * P z ^ 2 -
                      2 * W'.a₃ * P x * Q y * P z * Q z +
                    2 * W'.a₃ * Q x * P y * P z * Q z +
                  W'.a₄ * P x ^ 2 * Q z ^ 2 -
                W'.a₄ * Q x ^ 2 * P z ^ 2 +
              3 * W'.a₆ * P x * P z * Q z ^ 2 -
            3 * W'.a₆ * Q x * P z ^ 2 * Q z) *
          (P z * Q z) ^ 2 +
        ((2 * Q x * P z * Q z ^ 3 - P x * Q z ^ 4) * 0 + (Q x * P z ^ 4 - 2 * P x * P z ^ 3 * Q z) * 0) -
      (((P y * Q z - Q y * P z) ^ 2 * P z * Q z +
                  W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                W'.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
              P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
            Q x * P z * (P x * Q z - Q x * P z) ^ 2) *
          (P x * Q z - Q x * P z) +
        ((2 * Q x * P z * Q z ^ 3 - P x * Q z ^ 4) *
            (P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
              (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3)) +
          (Q x * P z ^ 4 - 2 * P x * P z ^ 3 * Q z) *
            (Q y ^ 2 * Q z + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * Q z ^ 2 -
              (Q x ^ 3 + W'.a₂ * Q x ^ 2 * Q z + W'.a₄ * Q x * Q z ^ 2 + W'.a₆ * Q z ^ 3)))) =
    0

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ -(u * P x) * (v * Q y) ^ 2 * (u * P z) + v * Q x * (u * P y) ^ 2 * (v * Q z) -
                                2 * (u * P x) * (u * P y) * (v * Q y) * (v * Q z) +
                              2 * (v * Q x) * (u * P y) * (v * Q y) * (u * P z) -
                            W'.a₁ * (u * P x) ^ 2 * (v * Q y) * (v * Q z) +
                          W'.a₁ * (v * Q x) ^ 2 * (u * P y) * (u * P z) +
                        W'.a₂ * (u * P x) ^ 2 * (v * Q x) * (v * Q z) -
                      W'.a₂ * (u * P x) * (v * Q x) ^ 2 * (u * P z) -
                    W'.a₃ * (u * P x) * (u * P y) * (v * Q z) ^ 2 +
                  W'.a₃ * (v * Q x) * (v * Q y) * (u * P z) ^ 2 -
                2 * W'.a₃ * (u * P x) * (v * Q y) * (u * P z) * (v * Q z) +
              2 * W'.a₃ * (v * Q x) * (u * P y) * (u * P z) * (v * Q z) +
            W'.a₄ * (u * P x) ^ 2 * (v * Q z) ^ 2 -
          W'.a₄ * (v * Q x) ^ 2 * (u * P z) ^ 2 +
        3 * W'.a₆ * (u * P x) * (u * P z) * (v * Q z) ^ 2 -
      3 * W'.a₆ * (v * Q x) * (u * P z) ^ 2 * (v * Q z) =
    (u * v) ^ 2 *
      (-P x * Q y ^ 2 * P z + Q x * P y ^ 2 * Q z - 2 * P x * P y * Q y * Q z + 2 * Q x * P y * Q y * P z -
                              W'.a₁ * P x ^ 2 * Q y * Q z +
                            W'.a₁ * Q x ^ 2 * P y * P z +
                          W'.a₂ * P x ^ 2 * Q x * Q z -
                        W'.a₂ * P x * Q x ^ 2 * P z -
                      W'.a₃ * P x * P y * Q z ^ 2 +
                    W'.a₃ * Q x * Q y * P z ^ 2 -
                  2 * W'.a₃ * P x * Q y * P z * Q z +
                2 * W'.a₃ * Q x * P y * P z * Q z +
              W'.a₄ * P x ^ 2 * Q z ^ 2 -
            W'.a₄ * Q x ^ 2 * P z ^ 2 +
          3 * W'.a₆ * P x * P z * Q z ^ 2 -
        3 * W'.a₆ * Q x * P z ^ 2 * Q z)

Tactic:
ring1

Goal state after:
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁶ : CommRing R
A : Type u
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : CommRing B
inst✝² : Algebra A B
D : DescentAux A B
inst✝¹ : Finite D.vars
inst✝ : Finite D.rels
⊢ (⋃ i, ⋃ x ∈ (D.q i).coeffs, ↑(coeffs x)).Finite

Tactic:
refine Set.finite_iUnion fun i ↦ ?_

Goal state after:
case refine_3
R : Type u_1
inst✝⁶ : CommRing R
A : Type u
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : CommRing B
inst✝² : Algebra A B
D : DescentAux A B
inst✝¹ : Finite D.vars
inst✝ : Finite D.rels
i : D.vars
⊢ (⋃ x ∈ (D.q i).coeffs, ↑(coeffs x)).Finite
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_4
R : Type u_1
inst✝⁶ : CommRing R
A : Type u
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : CommRing B
inst✝² : Algebra A B
D : DescentAux A B
inst✝¹ : Finite D.vars
inst✝ : Finite D.rels
⊢ (⋃ i, ⋃ x ∈ (D.p i).coeffs, ↑x.coeffs).Finite

Tactic:
refine Set.finite_iUnion fun i ↦ ?_

Goal state after:
case refine_4
R : Type u_1
inst✝⁶ : CommRing R
A : Type u
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : CommRing B
inst✝² : Algebra A B
D : DescentAux A B
inst✝¹ : Finite D.vars
inst✝ : Finite D.rels
i : D.rels
⊢ (⋃ x ∈ (D.p i).coeffs, ↑x.coeffs).Finite
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -P x * P y ^ 2 * P z + P x * P y ^ 2 * P z - 2 * P x * P y * P y * P z + 2 * P x * P y * P y * P z -
                            W'.a₁ * P x ^ 2 * P y * P z +
                          W'.a₁ * P x ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * P x * P z -
                      W'.a₂ * P x * P x ^ 2 * P z -
                    W'.a₃ * P x * P y * P z ^ 2 +
                  W'.a₃ * P x * P y * P z ^ 2 -
                2 * W'.a₃ * P x * P y * P z * P z +
              2 * W'.a₃ * P x * P y * P z * P z +
            W'.a₄ * P x ^ 2 * P z ^ 2 -
          W'.a₄ * P x ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * P z ^ 2 -
      3 * W'.a₆ * P x * P z ^ 2 * P z =
    0

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -0 * Q y ^ 2 * 0 + Q x * P y ^ 2 * Q z - 2 * 0 * P y * Q y * Q z + 2 * Q x * P y * Q y * 0 -
                            W'.a₁ * 0 ^ 2 * Q y * Q z +
                          W'.a₁ * Q x ^ 2 * P y * 0 +
                        W'.a₂ * 0 ^ 2 * Q x * Q z -
                      W'.a₂ * 0 * Q x ^ 2 * 0 -
                    W'.a₃ * 0 * P y * Q z ^ 2 +
                  W'.a₃ * Q x * Q y * 0 ^ 2 -
                2 * W'.a₃ * 0 * Q y * 0 * Q z +
              2 * W'.a₃ * Q x * P y * 0 * Q z +
            W'.a₄ * 0 ^ 2 * Q z ^ 2 -
          W'.a₄ * Q x ^ 2 * 0 ^ 2 +
        3 * W'.a₆ * 0 * 0 * Q z ^ 2 -
      3 * W'.a₆ * Q x * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * Q x

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -P x * Q y ^ 2 * P z + 0 * P y ^ 2 * 0 - 2 * P x * P y * Q y * 0 + 2 * 0 * P y * Q y * P z -
                            W'.a₁ * P x ^ 2 * Q y * 0 +
                          W'.a₁ * 0 ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * 0 * 0 -
                      W'.a₂ * P x * 0 ^ 2 * P z -
                    W'.a₃ * P x * P y * 0 ^ 2 +
                  W'.a₃ * 0 * Q y * P z ^ 2 -
                2 * W'.a₃ * P x * Q y * P z * 0 +
              2 * W'.a₃ * 0 * P y * P z * 0 +
            W'.a₄ * P x ^ 2 * 0 ^ 2 -
          W'.a₄ * 0 ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * 0 ^ 2 -
      3 * W'.a₆ * 0 * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * P x

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ ((P y * Q z - Q y * P z) ^ 2 * P z * Q z + W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (Q x * P z - Q x * P z) -
            W'.a₂ * P z * Q z * (Q x * P z - Q x * P z) ^ 2 -
          Q x * P z * (Q x * P z - Q x * P z) ^ 2 -
        Q x * P z * (Q x * P z - Q x * P z) ^ 2) *
      (Q x * P z - Q x * P z) =
    0

Tactic:
ring1

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

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
⊢ (-3 * P x ^ 2 * Q x * Q y + 3 * P x * Q x ^ 2 * P y - P y ^ 2 * Q y * Q z + P y * Q y ^ 2 * P z +
                                      W'.a₁ * P x * Q y ^ 2 * P z -
                                    W'.a₁ * Q x * P y ^ 2 * Q z -
                                  W'.a₂ * P x ^ 2 * Q y * Q z +
                                W'.a₂ * Q x ^ 2 * P y * P z +
                              2 * W'.a₂ * P x * Q x * P y * Q z -
                            2 * W'.a₂ * P x * Q x * Q y * P z -
                          W'.a₃ * P y ^ 2 * Q z ^ 2 +
                        W'.a₃ * Q y ^ 2 * P z ^ 2 +
                      W'.a₄ * P x * P y * Q z ^ 2 -
                    2 * W'.a₄ * P x * Q y * P z * Q z +
                  2 * W'.a₄ * Q x * P y * P z * Q z -
                W'.a₄ * Q x * Q y * P z ^ 2 +
              3 * W'.a₆ * P y * P z * Q z ^ 2 -
            3 * W'.a₆ * Q y * P z ^ 2 * Q z) *
          (P z * Q z) ^ 2 +
        ((2 * Q y * P z * Q z ^ 3 - P y * Q z ^ 4) * 0 + (Q y * P z ^ 4 - 2 * P y * P z ^ 3 * Q z) * 0) -
      ((P y * Q z - Q y * P z) *
            ((P y * Q z - Q y * P z) ^ 2 * P z * Q z +
                      W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                    W'.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
                  P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
                Q x * P z * (P x * Q z - Q x * P z) ^ 2 -
              P x * Q z * (P x * Q z - Q x * P z) ^ 2) +
          P y * Q z * (P x * Q z - Q x * P z) ^ 3 +
        ((2 * Q y * P z * Q z ^ 3 - P y * Q z ^ 4) *
            (P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
              (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3)) +
          (Q y * P z ^ 4 - 2 * P y * P z ^ 3 * Q z) *
            (Q y ^ 2 * Q z + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * Q z ^ 2 -
              (Q x ^ 3 + W'.a₂ * Q x ^ 2 * Q z + W'.a₄ * Q x * Q z ^ 2 + W'.a₆ * Q z ^ 3)))) =
    0

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ -3 * (u * P x) ^ 2 * (v * Q x) * (v * Q y) + 3 * (u * P x) * (v * Q x) ^ 2 * (u * P y) -
                                    (u * P y) ^ 2 * (v * Q y) * (v * Q z) +
                                  u * P y * (v * Q y) ^ 2 * (u * P z) +
                                W'.a₁ * (u * P x) * (v * Q y) ^ 2 * (u * P z) -
                              W'.a₁ * (v * Q x) * (u * P y) ^ 2 * (v * Q z) -
                            W'.a₂ * (u * P x) ^ 2 * (v * Q y) * (v * Q z) +
                          W'.a₂ * (v * Q x) ^ 2 * (u * P y) * (u * P z) +
                        2 * W'.a₂ * (u * P x) * (v * Q x) * (u * P y) * (v * Q z) -
                      2 * W'.a₂ * (u * P x) * (v * Q x) * (v * Q y) * (u * P z) -
                    W'.a₃ * (u * P y) ^ 2 * (v * Q z) ^ 2 +
                  W'.a₃ * (v * Q y) ^ 2 * (u * P z) ^ 2 +
                W'.a₄ * (u * P x) * (u * P y) * (v * Q z) ^ 2 -
              2 * W'.a₄ * (u * P x) * (v * Q y) * (u * P z) * (v * Q z) +
            2 * W'.a₄ * (v * Q x) * (u * P y) * (u * P z) * (v * Q z) -
          W'.a₄ * (v * Q x) * (v * Q y) * (u * P z) ^ 2 +
        3 * W'.a₆ * (u * P y) * (u * P z) * (v * Q z) ^ 2 -
      3 * W'.a₆ * (v * Q y) * (u * P z) ^ 2 * (v * Q z) =
    (u * v) ^ 2 *
      (-3 * P x ^ 2 * Q x * Q y + 3 * P x * Q x ^ 2 * P y - P y ^ 2 * Q y * Q z + P y * Q y ^ 2 * P z +
                                  W'.a₁ * P x * Q y ^ 2 * P z -
                                W'.a₁ * Q x * P y ^ 2 * Q z -
                              W'.a₂ * P x ^ 2 * Q y * Q z +
                            W'.a₂ * Q x ^ 2 * P y * P z +
                          2 * W'.a₂ * P x * Q x * P y * Q z -
                        2 * W'.a₂ * P x * Q x * Q y * P z -
                      W'.a₃ * P y ^ 2 * Q z ^ 2 +
                    W'.a₃ * Q y ^ 2 * P z ^ 2 +
                  W'.a₄ * P x * P y * Q z ^ 2 -
                2 * W'.a₄ * P x * Q y * P z * Q z +
              2 * W'.a₄ * Q x * P y * P z * Q z -
            W'.a₄ * Q x * Q y * P z ^ 2 +
          3 * W'.a₆ * P y * P z * Q z ^ 2 -
        3 * W'.a₆ * Q y * P z ^ 2 * Q z)

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * P x * P y + 3 * P x * P x ^ 2 * P y - P y ^ 2 * P y * P z + P y * P y ^ 2 * P z +
                                W'.a₁ * P x * P y ^ 2 * P z -
                              W'.a₁ * P x * P y ^ 2 * P z -
                            W'.a₂ * P x ^ 2 * P y * P z +
                          W'.a₂ * P x ^ 2 * P y * P z +
                        2 * W'.a₂ * P x * P x * P y * P z -
                      2 * W'.a₂ * P x * P x * P y * P z -
                    W'.a₃ * P y ^ 2 * P z ^ 2 +
                  W'.a₃ * P y ^ 2 * P z ^ 2 +
                W'.a₄ * P x * P y * P z ^ 2 -
              2 * W'.a₄ * P x * P y * P z * P z +
            2 * W'.a₄ * P x * P y * P z * P z -
          W'.a₄ * P x * P y * P z ^ 2 +
        3 * W'.a₆ * P y * P z * P z ^ 2 -
      3 * W'.a₆ * P y * P z ^ 2 * P z =
    0

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -3 * 0 ^ 2 * Q x * Q y + 3 * 0 * Q x ^ 2 * P y - P y ^ 2 * Q y * Q z + P y * Q y ^ 2 * 0 + W'.a₁ * 0 * Q y ^ 2 * 0 -
                              W'.a₁ * Q x * P y ^ 2 * Q z -
                            W'.a₂ * 0 ^ 2 * Q y * Q z +
                          W'.a₂ * Q x ^ 2 * P y * 0 +
                        2 * W'.a₂ * 0 * Q x * P y * Q z -
                      2 * W'.a₂ * 0 * Q x * Q y * 0 -
                    W'.a₃ * P y ^ 2 * Q z ^ 2 +
                  W'.a₃ * Q y ^ 2 * 0 ^ 2 +
                W'.a₄ * 0 * P y * Q z ^ 2 -
              2 * W'.a₄ * 0 * Q y * 0 * Q z +
            2 * W'.a₄ * Q x * P y * 0 * Q z -
          W'.a₄ * Q x * Q y * 0 ^ 2 +
        3 * W'.a₆ * P y * 0 * Q z ^ 2 -
      3 * W'.a₆ * Q y * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * (-Q y - W'.a₁ * Q x - W'.a₃ * Q z)

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -3 * P x ^ 2 * 0 * Q y + 3 * P x * 0 ^ 2 * P y - P y ^ 2 * Q y * 0 + P y * Q y ^ 2 * P z +
                                W'.a₁ * P x * Q y ^ 2 * P z -
                              W'.a₁ * 0 * P y ^ 2 * 0 -
                            W'.a₂ * P x ^ 2 * Q y * 0 +
                          W'.a₂ * 0 ^ 2 * P y * P z +
                        2 * W'.a₂ * P x * 0 * P y * 0 -
                      2 * W'.a₂ * P x * 0 * Q y * P z -
                    W'.a₃ * P y ^ 2 * 0 ^ 2 +
                  W'.a₃ * Q y ^ 2 * P z ^ 2 +
                W'.a₄ * P x * P y * 0 ^ 2 -
              2 * W'.a₄ * P x * Q y * P z * 0 +
            2 * W'.a₄ * 0 * P y * P z * 0 -
          W'.a₄ * 0 * Q y * P z ^ 2 +
        3 * W'.a₆ * P y * P z * 0 ^ 2 -
      3 * W'.a₆ * Q y * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * (-P y - W'.a₁ * P x - W'.a₃ * P z)

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z = Q x * P z
⊢ (P y * Q z - Q y * P z) *
        ((P y * Q z - Q y * P z) ^ 2 * P z * Q z +
                  W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (Q x * P z - Q x * P z) -
                W'.a₂ * P z * Q z * (Q x * P z - Q x * P z) ^ 2 -
              Q x * P z * (Q x * P z - Q x * P z) ^ 2 -
            Q x * P z * (Q x * P z - Q x * P z) ^ 2 -
          Q x * P z * (Q x * P z - Q x * P z) ^ 2) +
      P y * Q z * (Q x * P z - Q x * P z) ^ 3 =
    (P y * Q z - Q y * P z) ^ 3 * (P z * Q z)

Tactic:
ring1

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z) (n / d) =
    (n *
            (n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 -
                Q x * P z * d ^ 2 -
              P x * Q z * d ^ 2) +
          P y * Q z * d ^ 3) /
        (P z * Q z) ^ 2 /
      (d ^ 3 / (P z * Q z))

Tactic:
Affine.negAddY,

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ n / d * (W.toAffine.addX (P x / P z) (Q x / Q z) (n / d) - P x / P z) + P y / P z =
    (n *
            (n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 -
                Q x * P z * d ^ 2 -
              P x * Q z * d ^ 2) +
          P y * Q z * d ^ 3) /
        (P z * Q z) ^ 2 /
      (d ^ 3 / (P z * Q z))
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case inr
X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this✝ :
  ∀ {X : Scheme} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst : LocallyOfFinitePresentation f],
    CompactSpace ↥X → Dense ↑(smoothLocus f)
H : ¬CompactSpace ↥X
x : ↥X
U : X.Opens
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this : ⟨x, hxU⟩ ∈ closure ↑(U.ι ⁻¹ᵁ smoothLocus f)
⊢ x ∈ closure ↑(smoothLocus f)

Tactic:
Scheme.Hom.coe_preimage,

Goal state after:
case inr
X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this✝ :
  ∀ {X : Scheme} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst : LocallyOfFinitePresentation f],
    CompactSpace ↥X → Dense ↑(smoothLocus f)
H : ¬CompactSpace ↥X
x : ↥X
U : X.Opens
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this : ⟨x, hxU⟩ ∈ closure (⇑U.ι ⁻¹' ↑(smoothLocus f))
⊢ x ∈ closure ↑(smoothLocus f)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ -((u * v) ^ 2 * W'.negAddY P Q) - W'.a₁ * ((u * v) ^ 2 * W'.addX P Q) - W'.a₃ * ((u * v) ^ 2 * W'.addZ P Q) =
    (u * v) ^ 2 * (-W'.negAddY P Q - W'.a₁ * W'.addX P Q - W'.a₃ * W'.addZ P Q)

Tactic:
ring1

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
hF'' : (aeval a) F'' = 0
hpm : p * F''.totalDegree ≤ F.totalDegree
hF''0 : F''.totalDegree = 0
⊢ F'' = 0

Tactic:
rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, aeval_C, map_eq_zero] at hF''

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
hF'' : coeff 0 F'' = 0
hpm : p * F''.totalDegree ≤ F.totalDegree
hF''0 : F''.totalDegree = 0
⊢ F'' = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -(P y ^ 2 * Q z * (-Q y - W'.a₁ * Q x - W'.a₃ * Q z)) - W'.a₁ * (P y ^ 2 * Q z * Q x) -
      W'.a₃ * (P y ^ 2 * Q z * Q z) =
    P y ^ 2 * Q z * Q y

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -(-(Q y ^ 2 * P z) * (-P y - W'.a₁ * P x - W'.a₃ * P z)) - W'.a₁ * (-(Q y ^ 2 * P z) * P x) -
      W'.a₃ * (-(Q y ^ 2 * P z) * P z) =
    -(Q y ^ 2 * P z) * P y

Tactic:
ring1

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

Goal state before:
pp: case a
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ (-W'.negAddY P Q - W'.a₁ * 0 - W'.a₃ * 0) * (P z * Q z) ^ 3 +
        -(P z * Q z) * ((P y * Q z - Q y * P z) ^ 3 * (P z * Q z)) -
      (-(P y * Q z - Q y * P z) ^ 3 * (P z * Q z) ^ 2 + -(P z * Q z) * (W'.negAddY P Q * (P z * Q z) ^ 2)) =
    0

Tactic:
ring1

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

Goal state before:
pp: case a
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W'.addY P Q * (P z * Q z) ^ 3 + -(P z * Q z) * ((P y * Q z - Q y * P z) ^ 3 * (P z * Q z)) -
      (-(P y * Q z - Q y * P z) ^ 3 * (P z * Q z) ^ 2 + -(P z * Q z) * (W'.negAddY P Q * (P z * Q z) ^ 2)) =
    0

Tactic:
rw [addY, negY_eq, addX_of_X_eq hP hQ hPz hQz hx,
    addZ_of_X_eq hP hQ hPz hQz hx]; ring1

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

Goal state before:
pp: X Y Z : Scheme
f✝ : X ⟶ Y
g✝ : Y ⟶ Z
inst✝ : FormallyUnramified (f✝ ≫ g✝)
R S T : Type u_1
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
g : S →+* T
H : (g.comp f).FormallyUnramified
⊢ g.FormallyUnramified

Tactic:
by
    algebraize [f, g, g.comp f]
    exact Algebra.FormallyUnramified.of_restrictScalars R S T

Goal state after: