awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
⊢ P y * Q z = Q y * P z
have neg : Eq.{v + 1} (α := K) ((f : (a : F) → K) (P y * Q z) : K) ((f : (a : F) → K) (Q y * P z) : K)
Tactic: apply f.injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
hz : ¬Eq.{v + 1} (α := K) ((f : (a : F) → K) (P z) : K) (0 : K)
⊢ Eq.{v + 1} (α := K) ((f : (a : F) → K) (P y * Q z) : K) ((f : (a : F) → K) (Q y * P z) : K)
have neg : HMul.hMul (α := K) (β := K) ((f : (a : F) → K) (P y) : K) ((f : (a : F) → K) (Q z) : K) =
  HMul.hMul (α := K) (β := K) ((f : (a : F) → K) (Q y) : K) ((f : (a : F) → K) (P z) : K)
Tactic: map_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
K : Type v
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
⊢ HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q)
have refine_2 : ∀ (u : Fˣ) (hP : W.Nonsingular ((fun (m : Fˣ) ↦ m • Q) u)),
  HasEquiv.Equiv.{max 1 (v + 1), 0} (α := Fin 3 → K)
    (Function.comp.{1, u + 1, v + 1} (β := F) (⇑f : (a : F) → K) ((fun (m : Fˣ) ↦ m • Q) u)) ((⇑f : (a : F) → K) ∘ Q)
Tactic: rcases h with ⟨u, rfl⟩
Cleared hypotheses: P, hP, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
⊢ (W'.map f).Equation ((⇑f : (a : R) → S) ∘ P)
have rw : Eq (α := S) ((eval ((⇑f : (a : R) → S) ∘ P) : (a : MvPolynomial (Fin 3) S) → S) (W'.map f).polynomial : S) (0 : S)
Tactic: rw [Equation, map_polynomial, eval_map, ← eval₂_comp, h, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
rw : Eq (α := S) ((eval ((⇑f : (a : R) → S) ∘ P) : (a : MvPolynomial (Fin 3) S) → S) (W'.map f).polynomial : S) (0 : S)
⊢ (W'.map f).Equation ((⇑f : (a : R) → S) ∘ P)
have rw₁ : Eq.{s + 1} (α := S)
  ((eval ((⇑f : (a : R) → S) ∘ P) : (a : MvPolynomial (Fin 3) S) → S)
      (((MvPolynomial.map f : RingHom.{r, s} (MvPolynomial (Fin 3) R) (MvPolynomial (Fin 3) S)) :
            (a : MvPolynomial (Fin 3) R) → MvPolynomial (Fin 3) S)
          W'.polynomial :
        MvPolynomial (Fin 3) S) :
    S)
  (0 : S)
Tactic: rw [Equation, map_polynomial, eval_map, ← eval₂_comp, h, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
rw : Eq (α := S) ((eval ((⇑f : (a : R) → S) ∘ P) : (a : MvPolynomial (Fin 3) S) → S) (W'.map f).polynomial : S) (0 : S)
rw₁ :
  Eq.{s + 1} (α := S)
    ((eval ((⇑f : (a : R) → S) ∘ P) : (a : MvPolynomial (Fin 3) S) → S)
        (((MvPolynomial.map f : RingHom.{r, s} (MvPolynomial (Fin 3) R) (MvPolynomial (Fin 3) S)) :
              (a : MvPolynomial (Fin 3) R) → MvPolynomial (Fin 3) S)
            W'.polynomial :
          MvPolynomial (Fin 3) S) :
      S)
    (0 : S)
⊢ (W'.map f).Equation ((⇑f : (a : R) → S) ∘ P)
have rw₂ : eval₂ f ((⇑f : (a : R) → S) ∘ P) W'.polynomial = 0
Tactic: rw [Equation, map_polynomial, eval_map, ← eval₂_comp, h, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
rw : Eq (α := S) ((eval ((⇑f : (a : R) → S) ∘ P) : (a : MvPolynomial (Fin 3) S) → S) (W'.map f).polynomial : S) (0 : S)
rw₁ :
  Eq.{s + 1} (α := S)
    ((eval ((⇑f : (a : R) → S) ∘ P) : (a : MvPolynomial (Fin 3) S) → S)
        (((MvPolynomial.map f : RingHom.{r, s} (MvPolynomial (Fin 3) R) (MvPolynomial (Fin 3) S)) :
              (a : MvPolynomial (Fin 3) R) → MvPolynomial (Fin 3) S)
            W'.polynomial :
          MvPolynomial (Fin 3) S) :
      S)
    (0 : S)
rw₂ : eval₂ f ((⇑f : (a : R) → S) ∘ P) W'.polynomial = 0
⊢ (W'.map f).Equation ((⇑f : (a : R) → S) ∘ P)
have rw₃ : Eq.{s + 1} (α := S) ((f : (a : R) → S) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomial : R) : S) (0 : S)
Tactic: rw [Equation, map_polynomial, eval_map, ← eval₂_comp, h, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
rw : Eq (α := S) ((eval ((⇑f : (a : R) → S) ∘ P) : (a : MvPolynomial (Fin 3) S) → S) (W'.map f).polynomial : S) (0 : S)
rw₁ :
  Eq.{s + 1} (α := S)
    ((eval ((⇑f : (a : R) → S) ∘ P) : (a : MvPolynomial (Fin 3) S) → S)
        (((MvPolynomial.map f : RingHom.{r, s} (MvPolynomial (Fin 3) R) (MvPolynomial (Fin 3) S)) :
              (a : MvPolynomial (Fin 3) R) → MvPolynomial (Fin 3) S)
            W'.polynomial :
          MvPolynomial (Fin 3) S) :
      S)
    (0 : S)
rw₂ : eval₂ f ((⇑f : (a : R) → S) ∘ P) W'.polynomial = 0
rw₃ :
  Eq.{s + 1} (α := S) ((f : (a : R) → S) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomial : R) : S) (0 : S)
⊢ (W'.map f).Equation ((⇑f : (a : R) → S) ∘ P)
have rw₄ : Eq.{s + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
Tactic: rw [Equation, map_polynomial, eval_map, ← eval₂_comp, h, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
rw : Eq (α := S) ((eval ((⇑f : (a : R) → S) ∘ P) : (a : MvPolynomial (Fin 3) S) → S) (W'.map f).polynomial : S) (0 : S)
rw₁ :
  Eq.{s + 1} (α := S)
    ((eval ((⇑f : (a : R) → S) ∘ P) : (a : MvPolynomial (Fin 3) S) → S)
        (((MvPolynomial.map f : RingHom.{r, s} (MvPolynomial (Fin 3) R) (MvPolynomial (Fin 3) S)) :
              (a : MvPolynomial (Fin 3) R) → MvPolynomial (Fin 3) S)
            W'.polynomial :
          MvPolynomial (Fin 3) S) :
      S)
    (0 : S)
rw₂ : eval₂ f ((⇑f : (a : R) → S) ∘ P) W'.polynomial = 0
rw₃ :
  Eq.{s + 1} (α := S) ((f : (a : R) → S) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomial : R) : S) (0 : S)
rw₄ : Eq.{s + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
⊢ (W'.map f).Equation ((⇑f : (a : R) → S) ∘ P)
have rw₅ : Eq.{s + 1} (α := S) 0 0
Tactic: rw [Equation, map_polynomial, eval_map, ← eval₂_comp, h, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomial
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomial)
have rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomial ((W'⁄A).map (↑f : A →+* B)).polynomial
Tactic: rw [← map_polynomial, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomial ((W'⁄A).map (↑f : A →+* B)).polynomial
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomial
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomial)
have rw₁ : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomial (W'⁄B).polynomial
Tactic: rw [← map_polynomial, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
h : (W'⁄A).Equation P
⊢ (W'⁄B).Equation ((⇑f : (a : A) → B) ∘ P)
have h₁ : W'⁄B = (W'⁄A).map f.toRingHom
Tactic: convert! Equation.map f.toRingHom h using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
h : (W'⁄A).Equation P
⊢ W'⁄B = (W'⁄A).map f.toRingHom
have h₁ : W'⁄B = (W'⁄A).map (↑f : A →+* B)
Tactic: rw [AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
h : (W'⁄A).Equation P
h₁ : W'⁄B = (W'⁄A).map (↑f : A →+* B)
⊢ W'⁄B = (W'⁄A).map f.toRingHom
have h₂ : W'⁄B = W'⁄B
Tactic: rw [AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
⊢ (W'⁄B).Equation ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P
have rw : (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P
Tactic: rw [← RingHom.coe_coe, ← map_equation _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
rw : (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P
⊢ (W'⁄B).Equation ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P
have rw₁ : (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
  ((W'⁄A).map f.toRingHom).Equation ((⇑f.toRingHom : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_equation _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
rw : (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P
rw₁ :
  (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map f.toRingHom).Equation ((⇑f.toRingHom : (a : A) → B) ∘ P)
⊢ (W'⁄B).Equation ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P
have rw₂ : (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
  ((W'⁄A).map (↑f : A →+* B)).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_equation _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
rw : (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P
rw₁ :
  (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map f.toRingHom).Equation ((⇑f.toRingHom : (a : A) → B) ∘ P)
rw₂ :
  (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map (↑f : A →+* B)).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).Equation ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P
have rw₃ : (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_equation _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialX
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomialX)
have rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialX ((W'⁄A).map (↑f : A →+* B)).polynomialX
Tactic: rw [← map_polynomialX, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialX ((W'⁄A).map (↑f : A →+* B)).polynomialX
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialX
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomialX)
have rw₁ : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialX (W'⁄B).polynomialX
Tactic: rw [← map_polynomialX, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialY
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomialY)
have rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialY ((W'⁄A).map (↑f : A →+* B)).polynomialY
Tactic: rw [← map_polynomialY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialY ((W'⁄A).map (↑f : A →+* B)).polynomialY
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialY
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomialY)
have rw₁ : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialY (W'⁄B).polynomialY
Tactic: rw [← map_polynomialY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialZ
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomialZ)
have rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialZ ((W'⁄A).map (↑f : A →+* B)).polynomialZ
Tactic: rw [← map_polynomialZ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialZ ((W'⁄A).map (↑f : A →+* B)).polynomialZ
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialZ
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomialZ)
have rw₁ : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialZ (W'⁄B).polynomialZ
Tactic: rw [← map_polynomialZ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
⊢ (W'⁄B).Nonsingular ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P
have rw : (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P
Tactic: rw [← RingHom.coe_coe, ← map_nonsingular _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
rw : (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P
⊢ (W'⁄B).Nonsingular ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P
have rw₁ : (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
  ((W'⁄A).map f.toRingHom).Nonsingular ((⇑f.toRingHom : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_nonsingular _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
rw : (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P
rw₁ :
  (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map f.toRingHom).Nonsingular ((⇑f.toRingHom : (a : A) → B) ∘ P)
⊢ (W'⁄B).Nonsingular ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P
have rw₂ : (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
  ((W'⁄A).map (↑f : A →+* B)).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_nonsingular _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
rw : (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P
rw₁ :
  (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map f.toRingHom).Nonsingular ((⇑f.toRingHom : (a : A) → B) ∘ P)
rw₂ :
  (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map (↑f : A →+* B)).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).Nonsingular ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P
have rw₃ : (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← map_nonsingular _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ W'.negY (u • P) = u * W'.negY P
have simp : -(u * P y) - W'.a₁ * (u * P x) - W'.a₃ * (u * P z) = u * (-P y - W'.a₁ * P x - W'.a₃ * P z)
Tactic: simp only [negY, smul_fin3_ext]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.negY P = -P y
have rw : -P y - W'.a₁ * P x - W'.a₃ * P z = -P y
Tactic: rw [negY, hPz, X_eq_zero_of_Z_eq_zero hP hPz, mul_zero, sub_zero, mul_zero, sub_zero]