awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ = W.negY x₂ y₂
⊢ (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)
have pos : Eq.{v + 1} (α := K) (0 : K) ((f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂) : K)
Tactic: rw [slope_of_Y_eq (congr_arg f hx) <| by rw [hy, map_negY], slope_of_Y_eq hx hy, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ = W.negY x₂ y₂
pos : Eq.{v + 1} (α := K) (0 : K) ((f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂) : K)
⊢ (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)
have pos₁ : Eq.{v + 1} (α := K) (0 : K) ((f : (a : F) → K) 0 : K)
Tactic: rw [slope_of_Y_eq (congr_arg f hx) <| by rw [hy, map_negY], slope_of_Y_eq hx hy, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ = W.negY x₂ y₂
pos : Eq.{v + 1} (α := K) (0 : K) ((f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂) : K)
pos₁ : Eq.{v + 1} (α := K) (0 : K) ((f : (a : F) → K) 0 : K)
⊢ (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)
have pos₂ : Eq.{v + 1} (α := K) 0 0
Tactic: rw [slope_of_Y_eq (congr_arg f hx) <| by rw [hy, map_negY], slope_of_Y_eq hx hy, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : ¬y₁ = W.negY x₂ y₂
⊢ (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)
have neg : (3 * HPow.hPow (α := K) (β := ℕ) ((f : (a : F) → K) x₁ : K) 2 +
          HMul.hMul (β := K) (2 * (W.map f).a₂) ((f : (a : F) → K) x₁ : K) +
        (W.map f).a₄ -
      HMul.hMul (β := K) (W.map f).a₁ ((f : (a : F) → K) y₁ : K)) /
    HSub.hSub (α := K) (β := K) ((f : (a : F) → K) y₁ : K) ((f : (a : F) → K) (W.negY x₁ y₁) : K) =
  (f : (a : F) → K) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))
Tactic: rw [slope_of_Y_ne (congr_arg f hx) <| map_negY f x₂ y₂ ▸ fun h => hy <| f.injective h,
        map_negY, slope_of_Y_ne hx hy]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : ¬x₁ = x₂
⊢ (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)
have neg : HSub.hSub (α := K) (β := K) ((f : (a : F) → K) y₁ : K) ((f : (a : F) → K) y₂ : K) /
    HSub.hSub (α := K) (β := K) ((f : (a : F) → K) x₁ : K) ((f : (a : F) → K) x₂ : K) =
  (f : (a : F) → K) ((y₁ - y₂) / (x₁ - x₂))
Tactic: rw [slope_of_X_ne fun h => hx <| f.injective h, slope_of_X_ne hx]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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).negPolynomial (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) (W'⁄A).negPolynomial)
have rw : Eq (α := B[X][Y]) (W'⁄B).negPolynomial ((W'⁄A).map (↑f : A →+* B)).negPolynomial
Tactic: rw [← map_negPolynomial, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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).negPolynomial ((W'⁄A).map (↑f : A →+* B)).negPolynomial
⊢ Eq (α := B[X][Y]) (W'⁄B).negPolynomial (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) (W'⁄A).negPolynomial)
have rw₁ : Eq (α := B[X][Y]) (W'⁄B).negPolynomial (W'⁄B).negPolynomial
Tactic: rw [← map_negPolynomial, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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
⊢ (W'⁄B).negY ((f : (a : A) → B) x) ((f : (a : A) → B) y) = (f : (a : A) → B) ((W'⁄A).negY x y)
have rw : (W'⁄B).negY (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y) =
  ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negY x y)
Tactic: rw [← RingHom.coe_coe, ← map_negY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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
rw :
  (W'⁄B).negY (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negY x y)
⊢ (W'⁄B).negY ((f : (a : A) → B) x) ((f : (a : A) → B) y) = (f : (a : A) → B) ((W'⁄A).negY x y)
have rw₁ : (W'⁄B).negY (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y) =
  ((W'⁄A).map (↑f : A →+* B)).negY (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
Tactic: rw [← RingHom.coe_coe, ← map_negY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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
rw :
  (W'⁄B).negY (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negY x y)
rw₁ :
  (W'⁄B).negY (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y) =
    ((W'⁄A).map (↑f : A →+* B)).negY (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
⊢ (W'⁄B).negY ((f : (a : A) → B) x) ((f : (a : A) → B) y) = (f : (a : A) → B) ((W'⁄A).negY x y)
have rw₂ : (W'⁄B).negY (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y) =
  (W'⁄B).negY (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
Tactic: rw [← RingHom.coe_coe, ← map_negY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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
⊢ Eq (α := B[X]) ((W'⁄B).addPolynomial ((f : (a : A) → B) x) ((f : (a : A) → B) y) ((f : (a : A) → B) ℓ))
    (Polynomial.map (↑f : A →+* B) ((W'⁄A).addPolynomial x y ℓ))
have rw : Eq (α := B[X])
  ((W'⁄B).addPolynomial (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
    (((↑f : A →+* B) : (a : A) → B) ℓ))
  (Polynomial.map (↑f : A →+* B) ((W'⁄A).addPolynomial x y ℓ))
Tactic: rw [← RingHom.coe_coe, ← map_addPolynomial, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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
rw :
  Eq (α := B[X])
    ((W'⁄B).addPolynomial (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
      (((↑f : A →+* B) : (a : A) → B) ℓ))
    (Polynomial.map (↑f : A →+* B) ((W'⁄A).addPolynomial x y ℓ))
⊢ Eq (α := B[X]) ((W'⁄B).addPolynomial ((f : (a : A) → B) x) ((f : (a : A) → B) y) ((f : (a : A) → B) ℓ))
    (Polynomial.map (↑f : A →+* B) ((W'⁄A).addPolynomial x y ℓ))
have rw₁ : Eq (α := B[X])
  ((W'⁄B).addPolynomial (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
    (((↑f : A →+* B) : (a : A) → B) ℓ))
  (((W'⁄A).map (↑f : A →+* B)).addPolynomial (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
    (((↑f : A →+* B) : (a : A) → B) ℓ))
Tactic: rw [← RingHom.coe_coe, ← map_addPolynomial, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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
rw :
  Eq (α := B[X])
    ((W'⁄B).addPolynomial (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
      (((↑f : A →+* B) : (a : A) → B) ℓ))
    (Polynomial.map (↑f : A →+* B) ((W'⁄A).addPolynomial x y ℓ))
rw₁ :
  Eq (α := B[X])
    ((W'⁄B).addPolynomial (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
      (((↑f : A →+* B) : (a : A) → B) ℓ))
    (((W'⁄A).map (↑f : A →+* B)).addPolynomial (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
      (((↑f : A →+* B) : (a : A) → B) ℓ))
⊢ Eq (α := B[X]) ((W'⁄B).addPolynomial ((f : (a : A) → B) x) ((f : (a : A) → B) y) ((f : (a : A) → B) ℓ))
    (Polynomial.map (↑f : A →+* B) ((W'⁄A).addPolynomial x y ℓ))
have rw₂ : Eq (α := B[X])
  ((W'⁄B).addPolynomial (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
    (((↑f : A →+* B) : (a : A) → B) ℓ))
  ((W'⁄B).addPolynomial (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
    (((↑f : A →+* B) : (a : A) → B) ℓ))
Tactic: rw [← RingHom.coe_coe, ← map_addPolynomial, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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₁ x₂ ℓ : A
⊢ (W'⁄B).addX ((f : (a : A) → B) x₁) ((f : (a : A) → B) x₂) ((f : (a : A) → B) ℓ) =
    (f : (a : A) → B) ((W'⁄A).addX x₁ x₂ ℓ)
have rw : (W'⁄B).addX (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂) (((↑f : A →+* B) : (a : A) → B) ℓ) =
  ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).addX x₁ x₂ ℓ)
Tactic: rw [← RingHom.coe_coe, ← map_addX, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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₁ x₂ ℓ : A
rw :
  (W'⁄B).addX (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) ℓ) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).addX x₁ x₂ ℓ)
⊢ (W'⁄B).addX ((f : (a : A) → B) x₁) ((f : (a : A) → B) x₂) ((f : (a : A) → B) ℓ) =
    (f : (a : A) → B) ((W'⁄A).addX x₁ x₂ ℓ)
have rw₁ : (W'⁄B).addX (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂) (((↑f : A →+* B) : (a : A) → B) ℓ) =
  ((W'⁄A).map (↑f : A →+* B)).addX (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
    (((↑f : A →+* B) : (a : A) → B) ℓ)
Tactic: rw [← RingHom.coe_coe, ← map_addX, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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₁ x₂ ℓ : A
rw :
  (W'⁄B).addX (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) ℓ) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).addX x₁ x₂ ℓ)
rw₁ :
  (W'⁄B).addX (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) ℓ) =
    ((W'⁄A).map (↑f : A →+* B)).addX (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) ℓ)
⊢ (W'⁄B).addX ((f : (a : A) → B) x₁) ((f : (a : A) → B) x₂) ((f : (a : A) → B) ℓ) =
    (f : (a : A) → B) ((W'⁄A).addX x₁ x₂ ℓ)
have rw₂ : (W'⁄B).addX (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂) (((↑f : A →+* B) : (a : A) → B) ℓ) =
  (W'⁄B).addX (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂) (((↑f : A →+* B) : (a : A) → B) ℓ)
Tactic: rw [← RingHom.coe_coe, ← map_addX, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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₁ x₂ ℓ : A
⊢ (W'⁄B).negAddY ((f : (a : A) → B) x₁) ((f : (a : A) → B) x₂) ((f : (a : A) → B) y₁) ((f : (a : A) → B) ℓ) =
    (f : (a : A) → B) ((W'⁄A).negAddY x₁ x₂ y₁ ℓ)
have rw : (W'⁄B).negAddY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
    (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ) =
  ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negAddY x₁ x₂ y₁ ℓ)
Tactic: rw [← RingHom.coe_coe, ← map_negAddY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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₁ x₂ ℓ : A
rw :
  (W'⁄B).negAddY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negAddY x₁ x₂ y₁ ℓ)
⊢ (W'⁄B).negAddY ((f : (a : A) → B) x₁) ((f : (a : A) → B) x₂) ((f : (a : A) → B) y₁) ((f : (a : A) → B) ℓ) =
    (f : (a : A) → B) ((W'⁄A).negAddY x₁ x₂ y₁ ℓ)
have rw₁ : (W'⁄B).negAddY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
    (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ) =
  ((W'⁄A).map (↑f : A →+* B)).negAddY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
    (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ)
Tactic: rw [← RingHom.coe_coe, ← map_negAddY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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₁ x₂ ℓ : A
rw :
  (W'⁄B).negAddY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negAddY x₁ x₂ y₁ ℓ)
rw₁ :
  (W'⁄B).negAddY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ) =
    ((W'⁄A).map (↑f : A →+* B)).negAddY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ)
⊢ (W'⁄B).negAddY ((f : (a : A) → B) x₁) ((f : (a : A) → B) x₂) ((f : (a : A) → B) y₁) ((f : (a : A) → B) ℓ) =
    (f : (a : A) → B) ((W'⁄A).negAddY x₁ x₂ y₁ ℓ)
have rw₂ : (W'⁄B).negAddY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
    (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ) =
  (W'⁄B).negAddY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
    (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ)
Tactic: rw [← RingHom.coe_coe, ← map_negAddY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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₁ x₂ ℓ : A
⊢ (W'⁄B).addY ((f : (a : A) → B) x₁) ((f : (a : A) → B) x₂) ((f : (a : A) → B) y₁) ((f : (a : A) → B) ℓ) =
    (f : (a : A) → B) ((W'⁄A).addY x₁ x₂ y₁ ℓ)
have rw : (W'⁄B).addY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂) (((↑f : A →+* B) : (a : A) → B) y₁)
    (((↑f : A →+* B) : (a : A) → B) ℓ) =
  ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).addY x₁ x₂ y₁ ℓ)
Tactic: rw [← RingHom.coe_coe, ← map_addY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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₁ x₂ ℓ : A
rw :
  (W'⁄B).addY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).addY x₁ x₂ y₁ ℓ)
⊢ (W'⁄B).addY ((f : (a : A) → B) x₁) ((f : (a : A) → B) x₂) ((f : (a : A) → B) y₁) ((f : (a : A) → B) ℓ) =
    (f : (a : A) → B) ((W'⁄A).addY x₁ x₂ y₁ ℓ)
have rw₁ : (W'⁄B).addY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂) (((↑f : A →+* B) : (a : A) → B) y₁)
    (((↑f : A →+* B) : (a : A) → B) ℓ) =
  ((W'⁄A).map (↑f : A →+* B)).addY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
    (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ)
Tactic: rw [← RingHom.coe_coe, ← map_addY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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₁ x₂ ℓ : A
rw :
  (W'⁄B).addY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).addY x₁ x₂ y₁ ℓ)
rw₁ :
  (W'⁄B).addY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ) =
    ((W'⁄A).map (↑f : A →+* B)).addY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ)
⊢ (W'⁄B).addY ((f : (a : A) → B) x₁) ((f : (a : A) → B) x₂) ((f : (a : A) → B) y₁) ((f : (a : A) → B) ℓ) =
    (f : (a : A) → B) ((W'⁄A).addY x₁ x₂ y₁ ℓ)
have rw₂ : (W'⁄B).addY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂) (((↑f : A →+* B) : (a : A) → B) y₁)
    (((↑f : A →+* B) : (a : A) → B) ℓ) =
  (W'⁄B).addY (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
    (((↑f : A →+* B) : (a : A) → B) y₁) (((↑f : A →+* B) : (a : A) → B) ℓ)
Tactic: rw [← RingHom.coe_coe, ← map_addY, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
F : Type u
K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field F
inst_3 : Field K
W' : Affine R
inst_4 : Algebra R S
inst_5 : DecidableEq F
inst_6 : DecidableEq K
inst_7 : Algebra R F
inst_8 : Algebra S F
inst_9 : IsScalarTower R S F
inst_10 : Algebra R K
inst_11 : Algebra S K
inst_12 : IsScalarTower R S K
f : F →ₐ[S] K
x₁ x₂ y₁ y₂ : F
⊢ (W'⁄K).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) ((W'⁄F).slope x₁ x₂ y₁ y₂)
have rw : (W'⁄K).slope (((↑f : F →+* K) : (a : F) → K) x₁) (((↑f : F →+* K) : (a : F) → K) x₂) (((↑f : F →+* K) : (a : F) → K) y₁)
    (((↑f : F →+* K) : (a : F) → K) y₂) =
  ((↑f : F →+* K) : (a : F) → K) ((W'⁄F).slope x₁ x₂ y₁ y₂)
Tactic: rw [← RingHom.coe_coe, ← map_slope, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
Goal:
R : Type r
S : Type s
F : Type u
K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field F
inst_3 : Field K
W' : Affine R
inst_4 : Algebra R S
inst_5 : DecidableEq F
inst_6 : DecidableEq K
inst_7 : Algebra R F
inst_8 : Algebra S F
inst_9 : IsScalarTower R S F
inst_10 : Algebra R K
inst_11 : Algebra S K
inst_12 : IsScalarTower R S K
f : F →ₐ[S] K
x₁ x₂ y₁ y₂ : F
rw :
  (W'⁄K).slope (((↑f : F →+* K) : (a : F) → K) x₁) (((↑f : F →+* K) : (a : F) → K) x₂)
      (((↑f : F →+* K) : (a : F) → K) y₁) (((↑f : F →+* K) : (a : F) → K) y₂) =
    ((↑f : F →+* K) : (a : F) → K) ((W'⁄F).slope x₁ x₂ y₁ y₂)
⊢ (W'⁄K).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) ((W'⁄F).slope x₁ x₂ y₁ y₂)
have rw₁ : (W'⁄K).slope (((↑f : F →+* K) : (a : F) → K) x₁) (((↑f : F →+* K) : (a : F) → K) x₂) (((↑f : F →+* K) : (a : F) → K) y₁)
    (((↑f : F →+* K) : (a : F) → K) y₂) =
  ((W'⁄F).map (↑f : F →+* K)).slope (((↑f : F →+* K) : (a : F) → K) x₁) (((↑f : F →+* K) : (a : F) → K) x₂)
    (((↑f : F →+* K) : (a : F) → K) y₁) (((↑f : F →+* K) : (a : F) → K) y₂)
Tactic: rw [← RingHom.coe_coe, ← map_slope, map_baseChange]