awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
hΔ : Δ W ≠ 0
rwa : HPow.hPow (β := ℕ) (↑(VariableChange.u { u := 1, r := x, s := 0, t := y : VariableChange R })⁻¹ : R) 12 * Δ W ≠ 0
rwa₁ : HPow.hPow (α := R) (β := ℕ) (↑1 : R) 12 * Δ W ≠ 0
⊢ Δ (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)) ≠ 0
have rwa₂ : HPow.hPow (α := R) (β := ℕ) 1 12 * Δ W ≠ 0
Tactic: rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
hΔ : Δ W ≠ 0
rwa : HPow.hPow (β := ℕ) (↑(VariableChange.u { u := 1, r := x, s := 0, t := y : VariableChange R })⁻¹ : R) 12 * Δ W ≠ 0
rwa₁ : HPow.hPow (α := R) (β := ℕ) (↑1 : R) 12 * Δ W ≠ 0
rwa₂ : HPow.hPow (α := R) (β := ℕ) 1 12 * Δ W ≠ 0
⊢ Δ (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)) ≠ 0
have rwa₃ : 1 * Δ W ≠ 0
Tactic: rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
hΔ : Δ W ≠ 0
⊢ W.Equation x y ↔ W.Nonsingular x y
have rw : (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).Equation 0 0 ↔
  W.Nonsingular x y
Tactic: rw [equation_iff_variableChange, nonsingular_iff_variableChange,
    equation_zero_iff_nonsingular_zero_of_Δ_ne_zero <| by
      rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
hΔ : Δ W ≠ 0
rw :
  (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).Equation 0
      0 ↔
    W.Nonsingular x y
⊢ W.Equation x y ↔ W.Nonsingular x y
have rw₁ : (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).Equation 0 0 ↔
  (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).Nonsingular 0
    0
Tactic: rw [equation_iff_variableChange, nonsingular_iff_variableChange,
    equation_zero_iff_nonsingular_zero_of_Δ_ne_zero <| by
      rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
hΔ : Δ W ≠ 0
rw :
  (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).Equation 0
      0 ↔
    W.Nonsingular x y
rw₁ :
  (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).Equation 0
      0 ↔
    (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).Nonsingular
      0 0
⊢ W.Equation x y ↔ W.Nonsingular x y
have rw₂ : (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).Nonsingular 0
    0 ↔
  (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).Nonsingular 0
    0
Tactic: rw [equation_iff_variableChange, nonsingular_iff_variableChange,
    equation_zero_iff_nonsingular_zero_of_Δ_ne_zero <| by
      rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
f : R →+* S
x y : R
h : W.Equation x y
⊢ (W.map f).Equation ((f : (a : R) → S) x) ((f : (a : R) → S) y)
have rw : Eq.{s + 1} (α := S) (evalEval ((f : (a : R) → S) x) ((f : (a : R) → S) y) (W.map f).polynomial : S) (0 : S)
Tactic: rw [Equation, map_polynomial, map_mapRingHom_evalEval, h, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
f : R →+* S
x y : R
h : W.Equation x y
rw : Eq.{s + 1} (α := S) (evalEval ((f : (a : R) → S) x) ((f : (a : R) → S) y) (W.map f).polynomial : S) (0 : S)
⊢ (W.map f).Equation ((f : (a : R) → S) x) ((f : (a : R) → S) y)
have rw₁ : Eq.{s + 1} (α := S)
  (evalEval ((f : (a : R) → S) x) ((f : (a : R) → S) y) (Polynomial.map (mapRingHom f) W.polynomial) : S) (0 : S)
Tactic: rw [Equation, map_polynomial, map_mapRingHom_evalEval, h, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
f : R →+* S
x y : R
h : W.Equation x y
rw : Eq.{s + 1} (α := S) (evalEval ((f : (a : R) → S) x) ((f : (a : R) → S) y) (W.map f).polynomial : S) (0 : S)
rw₁ :
  Eq.{s + 1} (α := S)
    (evalEval ((f : (a : R) → S) x) ((f : (a : R) → S) y) (Polynomial.map (mapRingHom f) W.polynomial) : S) (0 : S)
⊢ (W.map f).Equation ((f : (a : R) → S) x) ((f : (a : R) → S) y)
have rw₂ : Eq.{s + 1} (α := S) ((f : (a : R) → S) (evalEval x y W.polynomial) : S) (0 : S)
Tactic: rw [Equation, map_polynomial, map_mapRingHom_evalEval, h, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
f : R →+* S
x y : R
h : W.Equation x y
rw : Eq.{s + 1} (α := S) (evalEval ((f : (a : R) → S) x) ((f : (a : R) → S) y) (W.map f).polynomial : S) (0 : S)
rw₁ :
  Eq.{s + 1} (α := S)
    (evalEval ((f : (a : R) → S) x) ((f : (a : R) → S) y) (Polynomial.map (mapRingHom f) W.polynomial) : S) (0 : S)
rw₂ : Eq.{s + 1} (α := S) ((f : (a : R) → S) (evalEval x y W.polynomial) : S) (0 : S)
⊢ (W.map f).Equation ((f : (a : R) → S) x) ((f : (a : R) → S) y)
have rw₃ : Eq.{s + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
Tactic: rw [Equation, map_polynomial, map_mapRingHom_evalEval, h, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
f : R →+* S
x y : R
h : W.Equation x y
rw : Eq.{s + 1} (α := S) (evalEval ((f : (a : R) → S) x) ((f : (a : R) → S) y) (W.map f).polynomial : S) (0 : S)
rw₁ :
  Eq.{s + 1} (α := S)
    (evalEval ((f : (a : R) → S) x) ((f : (a : R) → S) y) (Polynomial.map (mapRingHom f) W.polynomial) : S) (0 : S)
rw₂ : Eq.{s + 1} (α := S) ((f : (a : R) → S) (evalEval x y W.polynomial) : S) (0 : S)
rw₃ : Eq.{s + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
⊢ (W.map f).Equation ((f : (a : R) → S) x) ((f : (a : R) → S) y)
have rw₄ : Eq.{s + 1} (α := S) 0 0
Tactic: rw [Equation, map_polynomial, map_mapRingHom_evalEval, h, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine 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 (α := B[X][Y]) (W⁄B).polynomial (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) (W⁄A).polynomial)
have rw : Eq (α := B[X][Y]) (W⁄B).polynomial ((W⁄A).map (↑f : A →+* B)).polynomial
Tactic: rw [← map_polynomial, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine 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 (α := B[X][Y]) (W⁄B).polynomial ((W⁄A).map (↑f : A →+* B)).polynomial
⊢ Eq (α := B[X][Y]) (W⁄B).polynomial (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) (W⁄A).polynomial)
have rw₁ : Eq (α := B[X][Y]) (W⁄B).polynomial (W⁄B).polynomial
Tactic: rw [← map_polynomial, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine 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
x y : A
h : (W⁄A).Equation x y
⊢ (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y)
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.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine 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
x y : A
h : (W⁄A).Equation x y
⊢ 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.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine 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
x y : A
h : (W⁄A).Equation x y
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.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine 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)
x y : A
⊢ (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔ (W⁄A).Equation x y
have rw : (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
  ((W⁄A).map f.toRingHom).Equation ((f.toRingHom : (a : A) → B) x) ((f.toRingHom : (a : A) → B) y)
Tactic: rw [← map_equation _ hf, AlgHom.toRingHom_eq_coe, map_baseChange, RingHom.coe_coe]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine 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)
x y : A
rw :
  (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    ((W⁄A).map f.toRingHom).Equation ((f.toRingHom : (a : A) → B) x) ((f.toRingHom : (a : A) → B) y)
⊢ (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔ (W⁄A).Equation x y
have rw₁ : (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
  ((W⁄A).map (↑f : A →+* B)).Equation (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
Tactic: rw [← map_equation _ hf, AlgHom.toRingHom_eq_coe, map_baseChange, RingHom.coe_coe]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine 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)
x y : A
rw :
  (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    ((W⁄A).map f.toRingHom).Equation ((f.toRingHom : (a : A) → B) x) ((f.toRingHom : (a : A) → B) y)
rw₁ :
  (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    ((W⁄A).map (↑f : A →+* B)).Equation (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
⊢ (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔ (W⁄A).Equation x y
have rw₂ : (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
  (W⁄B).Equation (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
Tactic: rw [← map_equation _ hf, AlgHom.toRingHom_eq_coe, map_baseChange, RingHom.coe_coe]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine 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)
x y : A
rw :
  (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    ((W⁄A).map f.toRingHom).Equation ((f.toRingHom : (a : A) → B) x) ((f.toRingHom : (a : A) → B) y)
rw₁ :
  (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    ((W⁄A).map (↑f : A →+* B)).Equation (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
rw₂ :
  (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    (W⁄B).Equation (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
⊢ (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔ (W⁄A).Equation x y
have rw₃ : (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔ (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y)
Tactic: rw [← map_equation _ hf, AlgHom.toRingHom_eq_coe, map_baseChange, RingHom.coe_coe]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine 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 (α := B[X][Y]) (W⁄B).polynomialX (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) (W⁄A).polynomialX)
have rw : Eq (α := B[X][Y]) (W⁄B).polynomialX ((W⁄A).map (↑f : A →+* B)).polynomialX
Tactic: rw [← map_polynomialX, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine 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 (α := B[X][Y]) (W⁄B).polynomialX ((W⁄A).map (↑f : A →+* B)).polynomialX
⊢ Eq (α := B[X][Y]) (W⁄B).polynomialX (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) (W⁄A).polynomialX)
have rw₁ : Eq (α := B[X][Y]) (W⁄B).polynomialX (W⁄B).polynomialX
Tactic: rw [← map_polynomialX, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine 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 (α := B[X][Y]) (W⁄B).polynomialY (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) (W⁄A).polynomialY)
have rw : Eq (α := B[X][Y]) (W⁄B).polynomialY ((W⁄A).map (↑f : A →+* B)).polynomialY
Tactic: rw [← map_polynomialY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine 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 (α := B[X][Y]) (W⁄B).polynomialY ((W⁄A).map (↑f : A →+* B)).polynomialY
⊢ Eq (α := B[X][Y]) (W⁄B).polynomialY (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) (W⁄A).polynomialY)
have rw₁ : Eq (α := B[X][Y]) (W⁄B).polynomialY (W⁄B).polynomialY
Tactic: rw [← map_polynomialY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine 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)
x y : A
⊢ (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔ (W⁄A).Nonsingular x y
have rw : (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
  ((W⁄A).map f.toRingHom).Nonsingular ((f.toRingHom : (a : A) → B) x) ((f.toRingHom : (a : A) → B) y)
Tactic: rw [← map_nonsingular _ hf, AlgHom.toRingHom_eq_coe, map_baseChange, RingHom.coe_coe]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine 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)
x y : A
rw :
  (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    ((W⁄A).map f.toRingHom).Nonsingular ((f.toRingHom : (a : A) → B) x) ((f.toRingHom : (a : A) → B) y)
⊢ (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔ (W⁄A).Nonsingular x y
have rw₁ : (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
  ((W⁄A).map (↑f : A →+* B)).Nonsingular (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
Tactic: rw [← map_nonsingular _ hf, AlgHom.toRingHom_eq_coe, map_baseChange, RingHom.coe_coe]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine 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)
x y : A
rw :
  (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    ((W⁄A).map f.toRingHom).Nonsingular ((f.toRingHom : (a : A) → B) x) ((f.toRingHom : (a : A) → B) y)
rw₁ :
  (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    ((W⁄A).map (↑f : A →+* B)).Nonsingular (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
⊢ (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔ (W⁄A).Nonsingular x y
have rw₂ : (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
  (W⁄B).Nonsingular (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
Tactic: rw [← map_nonsingular _ hf, AlgHom.toRingHom_eq_coe, map_baseChange, RingHom.coe_coe]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : Affine 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)
x y : A
rw :
  (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    ((W⁄A).map f.toRingHom).Nonsingular ((f.toRingHom : (a : A) → B) x) ((f.toRingHom : (a : A) → B) y)
rw₁ :
  (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    ((W⁄A).map (↑f : A →+* B)).Nonsingular (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
rw₂ :
  (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    (W⁄B).Nonsingular (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
⊢ (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔ (W⁄A).Nonsingular x y
have rw₃ : (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
  (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y)
Tactic: rw [← map_nonsingular _ hf, AlgHom.toRingHom_eq_coe, map_baseChange, RingHom.coe_coe]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
⊢ Y -
      HAdd.hAdd (β := R[X][Y])
        (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) 2) : R[X][Y]) Y)
        ((C : (a : R[X]) → R[X][Y])
            (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
              ((C : (a : R) → R[X]) W'.a₃ : R[X])) :
          R[X][Y]) =
    HSub.hSub (α := R[X][Y]) (β := R[X][Y]) (-Y)
      ((C : (a : R[X]) → R[X][Y])
          (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
            ((C : (a : R) → R[X]) W'.a₃ : R[X])) :
        R[X][Y])
have C_simp : Y -
    (HMul.hMul (α := R[X][Y]) 2 Y +
      HAdd.hAdd (β := R[X][Y])
        (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₁) : R[X][Y])
          ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
        ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₃) : R[X][Y])) =
  -Y -
    HAdd.hAdd (β := R[X][Y])
      (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₁) : R[X][Y])
        ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
      ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₃) : R[X][Y])
Tactic: C_simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
⊢ HSub.hSub (α := R[X][Y]) Y W'.negPolynomial = W'.polynomialY
have rw : Y - HSub.hSub (α := R[X][Y]) Y W'.polynomialY = W'.polynomialY
Tactic: rw [← Y_sub_polynomialY, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
rw : Y - HSub.hSub (α := R[X][Y]) Y W'.polynomialY = W'.polynomialY
⊢ HSub.hSub (α := R[X][Y]) Y W'.negPolynomial = W'.polynomialY
have rw₁ : Eq (α := R[X][Y]) W'.polynomialY W'.polynomialY
Tactic: rw [← Y_sub_polynomialY, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
⊢ W'.negY x (W'.negY x y) = y
have simp : -(-y - W'.a₁ * x - W'.a₃) - W'.a₁ * x - W'.a₃ = y
Tactic: simp only [negY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y W'.negPolynomial = W'.negY x y
have rw : evalEval x y
    (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) (-Y)
      ((C : (a : R[X]) → R[X][Y])
          (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
            ((C : (a : R) → R[X]) W'.a₃ : R[X])) :
        R[X][Y])) =
  -y - (W'.a₁ * x + W'.a₃)
Tactic: rw [negY, sub_sub, negPolynomial]