awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
a₄ :
  W.a₁ * (W.a₁ * W.a₄ + 2 * W.a₃ * W.a₂) - (HPow.hPow (β := ℕ) W.a₁ 2 * W.a₄ + HPow.hPow (β := ℕ) W.a₃ 2) +
      HPow.hPow (β := ℕ) W.a₃ 2 * 3 =
    0
⊢ (W.toCharTwoJNeZeroNF ha₁ • W).a₄ = 0

Tactic:
simp [field, toCharTwoJNeZeroNF, variableChange_a₄, -mul_eq_zero]

Premises used: WeierstrassCurve.toCharTwoJNeZeroNF, mul_eq_zero, WeierstrassCurve.variableChange_a₄
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ W.a₁ * (W.a₁ * W.a₄ + 2 * W.a₃ * W.a₂) - (HPow.hPow (β := ℕ) W.a₁ 2 * W.a₄ + HPow.hPow (β := ℕ) W.a₃ 2) +
      HPow.hPow (β := ℕ) W.a₃ 2 * 3 =
    0

Tactic:
linear_combination (W.a₃ ^ 2 + W.a₁ * W.a₃ * W.a₂) * CharP.cast_eq_zero F 2

Premises used: CharP.cast_eq_zero, HMul.hMul, WeierstrassCurve.a₂, WeierstrassCurve.a₃, HPow.hPow, HAdd.hAdd, OfNat.ofNat, WeierstrassCurve.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W_1 : WeierstrassCurve R
inst_2 : CharP R 2
inst_3 : CharP F 2
W : WeierstrassCurve F
inst_4 : DecidableEq F
pos : ∀ (ha₁ : W.a₁ = 0), (HSMul.hSMul (α := VariableChange F) W.toCharTwoNF W).IsCharTwoNF
neg : ∀ (ha₁ : ¬W.a₁ = 0), (HSMul.hSMul (α := VariableChange F) W.toCharTwoNF W).IsCharTwoNF
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharTwoNF W).IsCharTwoNF

Tactic:
by_cases ha₁ : W.a₁ = 0

Premises used: WeierstrassCurve.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W_1 : WeierstrassCurve R
inst_2 : CharP R 2
inst_3 : CharP F 2
W : WeierstrassCurve F
inst_4 : DecidableEq F
ha₁ : W.a₁ = 0
pos : (HSMul.hSMul (α := VariableChange F) W.toCharTwoJEqZeroNF W).IsCharTwoNF
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharTwoNF W).IsCharTwoNF

Tactic:
rw [toCharTwoNF, dif_pos ha₁]

Premises used: dif_pos, WeierstrassCurve.toCharTwoNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W_1 : WeierstrassCurve R
inst_2 : CharP R 2
inst_3 : CharP F 2
W : WeierstrassCurve F
inst_4 : DecidableEq F
ha₁ : W.a₁ = 0
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharTwoJEqZeroNF W).IsCharTwoJEqZeroNF

Tactic:
haveI := W.toCharTwoJEqZeroNF_spec ha₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W_1 : WeierstrassCurve R
inst_2 : CharP R 2
inst_3 : CharP F 2
W : WeierstrassCurve F
inst_4 : DecidableEq F
ha₁ : W.a₁ = 0
this : (HSMul.hSMul (α := VariableChange F) W.toCharTwoJEqZeroNF W).IsCharTwoJEqZeroNF
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharTwoJEqZeroNF W).IsCharTwoNF

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W_1 : WeierstrassCurve R
inst_2 : CharP R 2
inst_3 : CharP F 2
W : WeierstrassCurve F
inst_4 : DecidableEq F
ha₁ : ¬W.a₁ = 0
neg : (W.toCharTwoJNeZeroNF ha₁ • W).IsCharTwoNF
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharTwoNF W).IsCharTwoNF

Tactic:
rw [toCharTwoNF, dif_neg ha₁]

Premises used: dif_neg, WeierstrassCurve.toCharTwoNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W_1 : WeierstrassCurve R
inst_2 : CharP R 2
inst_3 : CharP F 2
W : WeierstrassCurve F
inst_4 : DecidableEq F
ha₁ : ¬W.a₁ = 0
⊢ (W.toCharTwoJNeZeroNF ha₁ • W).IsCharTwoJNeZeroNF

Tactic:
haveI := W.toCharTwoJNeZeroNF_spec ha₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W_1 : WeierstrassCurve R
inst_2 : CharP R 2
inst_3 : CharP F 2
W : WeierstrassCurve F
inst_4 : DecidableEq F
ha₁ : ¬W.a₁ = 0
this : (W.toCharTwoJNeZeroNF ha₁ • W).IsCharTwoJNeZeroNF
⊢ (W.toCharTwoJNeZeroNF ha₁ • W).IsCharTwoNF

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 2
W : WeierstrassCurve F
⊢ ∃ (C : VariableChange F), (C • W).IsCharTwoNF

Tactic:
⟨_, W.toCharTwoNF_spec⟩

Premises used: Exists.intro, WeierstrassCurve.toCharTwoNF_spec
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 2
W : WeierstrassCurve F
⊢ ∃ (C : VariableChange F), (C • W).IsCharTwoNF

Tactic:
exact ⟨_, W.toCharTwoNF_spec⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 2
W : WeierstrassCurve F
⊢ ∃ (C : VariableChange F), (C • W).IsCharTwoNF

Tactic:
classical
  exact ⟨_, W.toCharTwoNF_spec⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
P : Fin 3 → R
h : ∀ (n : Fin (Nat.succ 0).succ.succ), ![P x, P y, P z] n = P n
⊢ ![P x, P y, P z] = P

Tactic:
ext n
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
P : Fin 3 → R
n : Fin (Nat.succ 0).succ.succ
h :
  ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₁ :
  ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
h₂ :
  ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
⊢ ![P x, P y, P z] n = P n

Tactic:
fin_cases n
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    P ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
a b c : R
⊢ ![a, b, c] x = a ∧ ![a, b, c] y = b ∧ ![a, b, c] z = c

Tactic:
⟨rfl, rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
S : Type s
f : R → S
a b c : R
⊢ f ∘ ![a, b, c] = ![f a, f b, f c]

Tactic:
(FinVec.map_eq ..).symm

Premises used: Eq.mpr, FinVec.map, Fin.cons, Fin.induction.go, Fin.induction, FinVec.map_eq, Fin.cases, FinVec.seq, Eq.symm, Matrix.vecTail, Matrix.vecCons
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
P : Fin 3 → R
u : R
⊢ u • P = ![u * P x, u * P y, u * P z]

Tactic:
simp [← List.ofFn_inj, List.ofFn_succ]

Premises used: List.ofFn_inj, List.ofFn_succ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
P : Fin 3 → R
u : R
⊢ (u • P) x = u * P x ∧ (u • P) y = u * P y ∧ (u • P) z = u * P z

Tactic:
⟨rfl, rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
h :
  ∀ («x» : Fin 3),
    ((⇑f : (a : R) → S) ∘ (u • P)) «x» =
      HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P) «x»
⊢ (⇑f : (a : R) → S) ∘ (u • P) =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P)

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
x : Fin 3
⊢ ((⇑f : (a : R) → S) ∘ (u • P)) «x» =
    HSMul.hSMul (α := S) (β := Fin 3 → S) ((f : (a : R) → S) u : S) ((⇑f : (a : R) → S) ∘ P) «x»

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
P : Fin 3 → R
u : R
hu : IsUnit u
⊢ u • P ≈ P

Tactic:
⟨hu.unit, rfl⟩

Premises used: Set.Mem, setOf, MulAction.orbit, Exists.intro, IsUnit.unit, Set.range, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
P : Fin 3 → R
u : R
hu : IsUnit u
⊢ Eq (α := Quotient (α := Fin 3 → R) (MulAction.orbitRel Rˣ (Fin 3 → R))) ⟦u • P⟧ ⟦P⟧

Tactic:
Quotient.eq.mpr <| smul_equiv P hu

Premises used: Iff.mpr, Quotient.eq, WeierstrassCurve.Projective.smul_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
rw : Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦u • P⟧ ⟦v • Q⟧ ↔ P ≈ Q
rw₁ :
  Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦u • P⟧ ⟦v • Q⟧ ↔
    Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦Q⟧
rw₂ :
  Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦v • Q⟧ ↔
    Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦Q⟧
rw₃ rw₄ :
  Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦Q⟧ ↔
    Eq (α := Quotient (α := Fin 3 → R) instSetoidForallFinOfNatNat) ⟦P⟧ ⟦Q⟧
⊢ u • P ≈ v • Q ↔ P ≈ Q

Tactic:
rw [← Quotient.eq_iff_equiv, ← Quotient.eq_iff_equiv, smul_eq P hu, smul_eq Q hv]

Premises used: WeierstrassCurve.Projective.smul_eq, Quotient.eq_iff_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
hz : P z = Q z
hQz : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (Q z)
⊢ P ≈ Q ↔ P = Q

Tactic:
⟨?_, Quotient.exact.comp <| congrArg _⟩

Premises used: congrArg, Function.comp, Iff.intro, Quotient.exact
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
hz : P z = Q z
hQz : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (Q z)
refine : P ≈ Q → P = Q
⊢ P ≈ Q ↔ P = Q

Tactic:
refine ⟨?_, Quotient.exact.comp <| congrArg _⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
Q : Fin 3 → R
hQz : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (Q z)
u : Rˣ
hz : (fun (m : Rˣ) ↦ m • Q) u z = Q z
simp : HSMul.hSMul (α := R) 1 Q = Q
⊢ (fun (m : Rˣ) ↦ m • Q) u = Q

Tactic:
simp only [Units.smul_def, (mul_cancel_right_mem_nonZeroDivisors hQz).mp <| one_mul (Q z) ▸ hz]

Premises used: mul_cancel_right_mem_nonZeroDivisors, Units.smul_def, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
Q : Fin 3 → R
hQz : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (Q z)
u : Rˣ
hz : (fun (m : Rˣ) ↦ m • Q) u z = Q z
rw rw₁ : Q = Q
⊢ HSMul.hSMul (α := R) 1 Q = Q

Tactic:
rw [one_smul]

Premises used: one_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hz : P z = Q z
hQz : Q z ≠ 0
⊢ P ≈ Q ↔ P = Q

Tactic:
equiv_iff_eq_of_Z_eq' hz <| mem_nonZeroDivisors_of_ne_zero hQz

Premises used: WeierstrassCurve.Projective.equiv_iff_eq_of_Z_eq', mem_nonZeroDivisors_of_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
rcases : ∀ (w : Rˣ), Eq.{r + 1} (α := R) ((fun (m : Rˣ) ↦ m • Q) w z) 0 ↔ Q z = 0
⊢ P z = 0 ↔ Q z = 0

Tactic:
rcases h with ⟨_, rfl⟩

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
Q : Fin 3 → R
w : Rˣ
⊢ Eq.{r + 1} (α := R) ((fun (m : Rˣ) ↦ m • Q) w z) 0 ↔ Q z = 0

Tactic:
simp only [Units.smul_def, smul_fin3_ext, Units.mul_right_eq_zero]

Premises used: Units.mul_right_eq_zero, Units.smul_def, WeierstrassCurve.Projective.smul_fin3_ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
rcases : ∀ (u : Rˣ), (fun (m : Rˣ) ↦ m • Q) u x * Q z = Q x * (fun (m : Rˣ) ↦ m • Q) u z
⊢ P x * Q z = Q x * P z

Tactic:
rcases h with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
Q : Fin 3 → R
u : Rˣ
simp : (↑u : R) * Q x * Q z = Q x * ((↑u : R) * Q z)
⊢ (fun (m : Rˣ) ↦ m • Q) u x * Q z = Q x * (fun (m : Rˣ) ↦ m • Q) u z

Tactic:
simp only [Units.smul_def, smul_fin3_ext]

Premises used: Units.smul_def, WeierstrassCurve.Projective.smul_fin3_ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ (↑u : R) * Q x * Q z = Q x * ((↑u : R) * Q z)

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
rcases : ∀ (u : Rˣ), (fun (m : Rˣ) ↦ m • Q) u y * Q z = Q y * (fun (m : Rˣ) ↦ m • Q) u z
⊢ P y * Q z = Q y * P z

Tactic:
rcases h with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
Q : Fin 3 → R
u : Rˣ
simp : (↑u : R) * Q y * Q z = Q y * ((↑u : R) * Q z)
⊢ (fun (m : Rˣ) ↦ m • Q) u y * Q z = Q y * (fun (m : Rˣ) ↦ m • Q) u z

Tactic:
simp only [Units.smul_def, smul_fin3_ext]

Premises used: Units.smul_def, WeierstrassCurve.Projective.smul_fin3_ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ (↑u : R) * Q y * Q z = Q y * ((↑u : R) * Q z)

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
hPz : P z = 0
hQz : Q z ≠ 0
⊢ ¬P ≈ Q

Tactic:
fun h => hQz <| (Z_eq_zero_of_equiv h).mp hPz

Premises used: WeierstrassCurve.Projective.Z_eq_zero_of_equiv, Iff.mp, Not
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
hPz : P z ≠ 0
hQz : Q z = 0
⊢ ¬P ≈ Q

Tactic:
fun h => hPz <| (Z_eq_zero_of_equiv h).mpr hQz

Premises used: Iff.mpr, WeierstrassCurve.Projective.Z_eq_zero_of_equiv, Not
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
hx : P x * Q z ≠ Q x * P z
⊢ ¬P ≈ Q

Tactic:
hx.comp X_eq_of_equiv

Premises used: Function.comp, WeierstrassCurve.Projective.X_eq_of_equiv, Not
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
hy : P y * Q z ≠ Q y * P z
⊢ ¬P ≈ Q

Tactic:
hy.comp Y_eq_of_equiv

Premises used: Function.comp, Not, WeierstrassCurve.Projective.Y_eq_of_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
h : (fun (m : Fˣ) ↦ m • Q) (HDiv.hDiv (α := Fˣ) (Units.mk0 (P z) hPz) (Units.mk0 (Q z) hQz)) = P
⊢ P ≈ Q

Tactic:
use Units.mk0 _ hPz / Units.mk0 _ hQz

Premises used: Units.mk0
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
⊢ (fun (m : Fˣ) ↦ m • Q) (HDiv.hDiv (α := Fˣ) (Units.mk0 (P z) hPz) (Units.mk0 (Q z) hQz)) = P

Tactic:
simp only [Units.smul_def, smul_fin3, Units.val_div_eq_div_val, Units.val_mk0, mul_comm, mul_div,
    ← hx, ← hy, mul_div_cancel_right₀ _ hQz, fin3_def]

Premises used: mul_div, Units.val_div_eq_div_val, WeierstrassCurve.Projective.smul_fin3, mul_div_cancel_right₀, WeierstrassCurve.Projective.fin3_def, Units.smul_def, mul_comm, Units.val_mk0
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
a : P x * 1 + -P x * 1 - (P x / P z * P z + -P x * (P z / P z)) = 0
⊢ P x * ![P x / P z, P y / P z, 1] z + -P x * 1 - (![P x / P z, P y / P z, 1] x * P z + -P x * (P z / P z)) = 0

Tactic:
matrix_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P x * 1 + -P x * 1 - (P x / P z * P z + -P x * (P z / P z)) = 0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
a : P x * ![P x / P z, P y / P z, 1] z + -P x * 1 - (![P x / P z, P y / P z, 1] x * P z + -P x * (P z / P z)) = 0
⊢ P x * ![P x / P z, P y / P z, 1] z = ![P x / P z, P y / P z, 1] x * P z

Tactic:
linear_combination (norm := (matrix_simp; ring1)) -P x * div_self hPz

Premises used: OfNat.ofNat, div_self
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
a : P y * 1 + -P y * 1 - (P y / P z * P z + -P y * (P z / P z)) = 0
⊢ P y * ![P x / P z, P y / P z, 1] z + -P y * 1 - (![P x / P z, P y / P z, 1] y * P z + -P y * (P z / P z)) = 0

Tactic:
matrix_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P y * 1 + -P y * 1 - (P y / P z * P z + -P y * (P z / P z)) = 0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
P : Fin 3 → F
hPz : P z ≠ 0
a : P y * ![P x / P z, P y / P z, 1] z + -P y * 1 - (![P x / P z, P y / P z, 1] y * P z + -P y * (P z / P z)) = 0
⊢ P y * ![P x / P z, P y / P z, 1] z = ![P x / P z, P y / P z, 1] y * P z

Tactic:
linear_combination (norm := (matrix_simp; ring1)) -P y * div_self hPz

Premises used: OfNat.ofNat, div_self
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ P x * Q z = Q x * P z ↔ P x / P z = Q x / Q z

Tactic:
(div_eq_div_iff hPz hQz).symm

Premises used: div_eq_div_iff, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ P y * Q z = Q y * P z ↔ P y / P z = Q y / Q z

Tactic:
(div_eq_div_iff hPz hQz).symm

Premises used: div_eq_div_iff, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
rw :
  (eval P : (a : MvPolynomial (Fin 3) R) → R)
      (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Y 2 * Z +
            HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
                  ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₁ : MvPolynomial (Fin 3) R) X *
                Y *
              Z +
          HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
              ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₃ : MvPolynomial (Fin 3) R) Y *
            HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 2 -
        (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) X 3 +
              HMul.hMul (α := MvPolynomial (Fin 3) R)
                  ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₂ : MvPolynomial (Fin 3) R)
                  (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) X 2) *
                Z +
            HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
                ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₄ : MvPolynomial (Fin 3) R) X *
              HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 2 +
          HMul.hMul (α := MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₆ : MvPolynomial (Fin 3) R)
            (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 3))) =
    HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
      (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
          W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₆ * HPow.hPow (β := ℕ) (P z) 3)
⊢ (eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomial =
    HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
      (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
          W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₆ * HPow.hPow (β := ℕ) (P z) 3)

Tactic:
rw [polynomial]

Premises used: WeierstrassCurve.Projective.polynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P : (a : MvPolynomial (Fin 3) R) → R)
      (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Y 2 * Z +
            HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
                  ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₁ : MvPolynomial (Fin 3) R) X *
                Y *
              Z +
          HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
              ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₃ : MvPolynomial (Fin 3) R) Y *
            HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 2 -
        (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) X 3 +
              HMul.hMul (α := MvPolynomial (Fin 3) R)
                  ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₂ : MvPolynomial (Fin 3) R)
                  (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) X 2) *
                Z +
            HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
                ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₄ : MvPolynomial (Fin 3) R) X *
              HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 2 +
          HMul.hMul (α := MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₆ : MvPolynomial (Fin 3) R)
            (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 3))) =
    HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
      (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
          W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₆ * HPow.hPow (β := ℕ) (P z) 3)

Tactic:
simp