mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: case inr.inr.inr
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
⊢ 1 < 3

pp: case inr.inr.inr
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
⊢ 0 < 3

Tactic:
<;>

Goal state after:
case inr.inr.inr
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
⊢ 1 < 3

case inr.inr.inr
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
⊢ 0 < 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ evalEval x y W.polynomial = y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆)

Tactic:
by
  simp only [polynomial]
  eval_simp
  rw [add_mul, ← add_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: case e'_1
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ 2 * y + W.a₁ * x + W.a₃ = 1 ^ 3 * (W.a₃ + x * W.a₁ + 2 * y)

pp: case e'_2
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ -(W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)) =
    1 ^ 4 * (W.a₄ - 0 * W.a₃ + 2 * x * W.a₂ - (y + x * 0) * W.a₁ + 3 * x ^ 2 - 2 * 0 * y)

Tactic:
<;>

Goal state after:
case e'_1
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ 2 * y + W.a₁ * x + W.a₃ = 1 ^ 3 * (W.a₃ + x * W.a₁ + 2 * y)

case e'_2
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ -(W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)) =
    1 ^ 4 * (W.a₄ - 0 * W.a₃ + 2 * x * W.a₂ - (y + x * 0) * W.a₁ + 3 * x ^ 2 - 2 * 0 * y)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case a₁
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ 1 * (W.a₁ + 2 * 0) = W.a₁

pp: case a₂
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ 1 ^ 2 * (W.a₂ - 0 * W.a₁ + 3 * 0 - 0 ^ 2) = W.a₂

pp: case a₃
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ 1 ^ 3 * (W.a₃ + 0 * W.a₁ + 2 * 0) = W.a₃

pp: case a₄
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ 1 ^ 4 * (W.a₄ - 0 * W.a₃ + 2 * 0 * W.a₂ - (0 + 0 * 0) * W.a₁ + 3 * 0 ^ 2 - 2 * 0 * 0) = W.a₄

pp: case a₆
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ 1 ^ 6 * (W.a₆ + 0 * W.a₄ + 0 ^ 2 * W.a₂ + 0 ^ 3 - 0 * W.a₃ - 0 ^ 2 - 0 * 0 * W.a₁) = W.a₆

Tactic:
<;>

Goal state after:
case a₁
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ 1 * (W.a₁ + 2 * 0) = W.a₁

case a₂
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ 1 ^ 2 * (W.a₂ - 0 * W.a₁ + 3 * 0 - 0 ^ 2) = W.a₂

case a₃
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ 1 ^ 3 * (W.a₃ + 0 * W.a₁ + 2 * 0) = W.a₃

case a₄
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ 1 ^ 4 * (W.a₄ - 0 * W.a₃ + 2 * 0 * W.a₂ - (0 + 0 * 0) * W.a₁ + 3 * 0 ^ 2 - 2 * 0 * 0) = W.a₄

case a₆
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C : VariableChange R
W : WeierstrassCurve R
⊢ 1 ^ 6 * (W.a₆ + 0 * W.a₄ + 0 ^ 2 * W.a₂ + 0 ^ 3 - 0 * W.a₃ - 0 ^ 2 - 0 * 0 * W.a₁) = W.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (C • W).c₆ = ↑C.u⁻¹ ^ 6 * W.c₆

Tactic:
by
  simp only [c₆, variableChange_b₂, variableChange_b₄, variableChange_b₆]
  ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case u
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ ↑x✝¹.u = ↑x✝.u

pp: case r
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ x✝¹.r = x✝.r

pp: case s
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ x✝¹.s = x✝.s

pp: case t
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ x✝¹.t = x✝.t

Tactic:
<;>

Goal state after:
case u
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ ↑x✝¹.u = ↑x✝.u

case r
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ x✝¹.r = x✝.r

case s
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ x✝¹.s = x✝.s

case t
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ x✝¹.t = x✝.t
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case u
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ φ ↑x✝¹.u = φ ↑x✝.u

pp: case r
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ φ x✝¹.r = φ x✝.r

pp: case s
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ φ x✝¹.s = φ x✝.s

pp: case t
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ φ x✝¹.t = φ x✝.t

Tactic:
<;>

Goal state after:
case u
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ φ ↑x✝¹.u = φ ↑x✝.u

case r
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ φ x✝¹.r = φ x✝.r

case s
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ φ x✝¹.s = φ x✝.s

case t
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ φ x✝¹.t = φ x✝.t
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
⊢ x✝¹ = x✝

Tactic:
by
  rcases mk.inj h with ⟨h, _, _, _⟩
  replace h := (Units.mk.inj h).left
  ext <;> apply_fun _ using hφ <;> assumption

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case u
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ ↑{ u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 }.u = ↑{ u := 1, r := 0, s := 0, t := 0 }.u

pp: case r
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 }.r = { u := 1, r := 0, s := 0, t := 0 }.r

pp: case s
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 }.s = { u := 1, r := 0, s := 0, t := 0 }.s

pp: case t
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 }.t = { u := 1, r := 0, s := 0, t := 0 }.t

Tactic:
<;>

Goal state after:
case u
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ ↑{ u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 }.u = ↑{ u := 1, r := 0, s := 0, t := 0 }.u

case r
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 }.r = { u := 1, r := 0, s := 0, t := 0 }.r

case s
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 }.s = { u := 1, r := 0, s := 0, t := 0 }.s

case t
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 }.t = { u := 1, r := 0, s := 0, t := 0 }.t
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case r
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ φ C.r * φ ↑C'.u ^ 2 + φ C'.r = φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r

pp: case s
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ φ ↑C'.u * φ C.s + φ C'.s = ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s

pp: case t
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ φ C.t * φ ↑C'.u ^ 3 + φ C.r * φ C'.s * φ ↑C'.u ^ 2 + φ C'.t =
    φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t

Tactic:
<;>

Goal state after:
case r
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ φ C.r * φ ↑C'.u ^ 2 + φ C'.r = φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r

case s
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ φ ↑C'.u * φ C.s + φ C'.s = ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s

case t
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ φ C.t * φ ↑C'.u ^ 3 + φ C.r * φ C'.s * φ ↑C'.u ^ 2 + φ C'.t =
    φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hC
R : Type u_2
inst✝ : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf : ∀ (i : Fin n), (f (MvPolynomial.X i)).degrees ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
x : R
⊢ ((g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)))).comp MvPolynomial.C)
      x =
    ((↑f).comp MvPolynomial.C) x

pp: case hX
R : Type u_2
inst✝ : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf : ∀ (i : Fin n), (f (MvPolynomial.X i)).degrees ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
x : Fin n
m✝ : Fin m →₀ ℕ
⊢ MvPolynomial.coeff m✝
      ((g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))))
        (MvPolynomial.X x)) =
    MvPolynomial.coeff m✝ (↑f (MvPolynomial.X x))

Tactic:
<;>

Goal state after:
case hC
R : Type u_2
inst✝ : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf : ∀ (i : Fin n), (f (MvPolynomial.X i)).degrees ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
x : R
⊢ ((g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)))).comp MvPolynomial.C)
      x =
    ((↑f).comp MvPolynomial.C) x

case hX
R : Type u_2
inst✝ : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf : ∀ (i : Fin n), (f (MvPolynomial.X i)).degrees ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
x : Fin n
m✝ : Fin m →₀ ℕ
⊢ MvPolynomial.coeff m✝
      ((g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))))
        (MvPolynomial.X x)) =
    MvPolynomial.coeff m✝ (↑f (MvPolynomial.X x))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span {XClass W x₁ * XClass W x₂} * span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
          span
              {YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
                  YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))} *
            span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
        span {XClass W x₁ * YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))} *
          span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
      span {YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * XClass W x₂} *
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})

Tactic:
span_singleton_mul_span_singleton

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span {XClass W x₁ * XClass W x₂ * XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
          span
            {YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
                  YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
                XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
        span
          {XClass W x₁ * YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
              XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
      span
        {YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * XClass W x₂ *
            XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (![s ^ 2 - C W.b₄ * s * u - C W.b₆ * t * u - C W.b₈ * u ^ 2,
          C 2 * t * s + C W.b₂ * s * u + C W.b₄ * t * u + C W.b₆ * u ^ 2, t ^ 2 - C 4 * s * u]
        ((fun i ↦ i) ⟨0, ⋯⟩)).IsHomogeneous
    2

pp: case «1»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (![s ^ 2 - C W.b₄ * s * u - C W.b₆ * t * u - C W.b₈ * u ^ 2,
          C 2 * t * s + C W.b₂ * s * u + C W.b₄ * t * u + C W.b₆ * u ^ 2, t ^ 2 - C 4 * s * u]
        ((fun i ↦ i) ⟨1, ⋯⟩)).IsHomogeneous
    2

pp: case «2»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (![s ^ 2 - C W.b₄ * s * u - C W.b₆ * t * u - C W.b₈ * u ^ 2,
          C 2 * t * s + C W.b₂ * s * u + C W.b₄ * t * u + C W.b₆ * u ^ 2, t ^ 2 - C 4 * s * u]
        ((fun i ↦ i) ⟨2, ⋯⟩)).IsHomogeneous
    2

Tactic:
<;>

Goal state after:
case «0»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (![s ^ 2 - C W.b₄ * s * u - C W.b₆ * t * u - C W.b₈ * u ^ 2,
          C 2 * t * s + C W.b₂ * s * u + C W.b₄ * t * u + C W.b₆ * u ^ 2, t ^ 2 - C 4 * s * u]
        ((fun i ↦ i) ⟨0, ⋯⟩)).IsHomogeneous
    2

case «1»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (![s ^ 2 - C W.b₄ * s * u - C W.b₆ * t * u - C W.b₈ * u ^ 2,
          C 2 * t * s + C W.b₂ * s * u + C W.b₄ * t * u + C W.b₆ * u ^ 2, t ^ 2 - C 4 * s * u]
        ((fun i ↦ i) ⟨1, ⋯⟩)).IsHomogeneous
    2

case «2»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (![s ^ 2 - C W.b₄ * s * u - C W.b₆ * t * u - C W.b₈ * u ^ 2,
          C 2 * t * s + C W.b₂ * s * u + C W.b₄ * t * u + C W.b₆ * u ^ 2, t ^ 2 - C 4 * s * u]
        ((fun i ↦ i) ⟨2, ⋯⟩)).IsHomogeneous
    2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b : ℤ
h : |a| = a
⊢ atom W |a| b = atom W a b

pp: case inr
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b : ℤ
h : |a| = -a
⊢ atom W |a| b = atom W a b

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b : ℤ
h : |a| = a
⊢ atom W |a| b = atom W a b

case inr
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b : ℤ
h : |a| = -a
⊢ atom W |a| b = atom W a b
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b : ℤ
h : |b| = b
⊢ atom W a |b| = atom W a b

pp: case inr
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b : ℤ
h : |b| = -b
⊢ atom W a |b| = atom W a b

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b : ℤ
h : |b| = b
⊢ atom W a |b| = atom W a b

case inr
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b : ℤ
h : |b| = -b
⊢ atom W a |b| = atom W a b
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
parity : d % 2 = a % 2 ∧ d % 2 = b % 2 ∧ d % 2 = c % 2
⊢ W ((a + b + (c + d) - (d + c)).tdiv 2) * W (((a + b + (c + d)) / 2 - d - ((a + b + (c + d)) / 2 - c)).tdiv 2) *
          (W ((a + b + (c + d) - (b + a)).tdiv 2) *
            W (((a + b + (c + d)) / 2 - b - ((a + b + (c + d)) / 2 - a)).tdiv 2)) -
        W ((a + b + (c + d) - (d + b)).tdiv 2) * W (((a + b + (c + d)) / 2 - d - ((a + b + (c + d)) / 2 - b)).tdiv 2) *
          (W ((a + b + (c + d) - (c + a)).tdiv 2) *
            W (((a + b + (c + d)) / 2 - c - ((a + b + (c + d)) / 2 - a)).tdiv 2)) +
      W ((a + b + (c + d) - (d + a)).tdiv 2) * W (((a + b + (c + d)) / 2 - d - ((a + b + (c + d)) / 2 - a)).tdiv 2) *
        (W ((a + b + (c + d) - (c + b)).tdiv 2) *
          W (((a + b + (c + d)) / 2 - c - ((a + b + (c + d)) / 2 - b)).tdiv 2)) =
    W ((a + b).tdiv 2) * W ((a - b).tdiv 2) * (W ((c + d).tdiv 2) * W ((c - d).tdiv 2)) -
        W ((a + c).tdiv 2) * W ((a - c).tdiv 2) * (W ((b + d).tdiv 2) * W ((b - d).tdiv 2)) +
      W ((a + d).tdiv 2) * W ((a - d).tdiv 2) * (W ((b + c).tdiv 2) * W ((b - c).tdiv 2))

pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
parity : d % 2 = a % 2 ∧ d % 2 = b % 2 ∧ d % 2 = c % 2
⊢ 2 ∣ a + b + (c + d)

Tactic:
<;>

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
parity : d % 2 = a % 2 ∧ d % 2 = b % 2 ∧ d % 2 = c % 2
⊢ W ((a + b + (c + d) - (d + c)).tdiv 2) * W (((a + b + (c + d)) / 2 - d - ((a + b + (c + d)) / 2 - c)).tdiv 2) *
          (W ((a + b + (c + d) - (b + a)).tdiv 2) *
            W (((a + b + (c + d)) / 2 - b - ((a + b + (c + d)) / 2 - a)).tdiv 2)) -
        W ((a + b + (c + d) - (d + b)).tdiv 2) * W (((a + b + (c + d)) / 2 - d - ((a + b + (c + d)) / 2 - b)).tdiv 2) *
          (W ((a + b + (c + d) - (c + a)).tdiv 2) *
            W (((a + b + (c + d)) / 2 - c - ((a + b + (c + d)) / 2 - a)).tdiv 2)) +
      W ((a + b + (c + d) - (d + a)).tdiv 2) * W (((a + b + (c + d)) / 2 - d - ((a + b + (c + d)) / 2 - a)).tdiv 2) *
        (W ((a + b + (c + d) - (c + b)).tdiv 2) *
          W (((a + b + (c + d)) / 2 - c - ((a + b + (c + d)) / 2 - b)).tdiv 2)) =
    W ((a + b).tdiv 2) * W ((a - b).tdiv 2) * (W ((c + d).tdiv 2) * W ((c - d).tdiv 2)) -
        W ((a + c).tdiv 2) * W ((a - c).tdiv 2) * (W ((b + d).tdiv 2) * W ((b - d).tdiv 2)) +
      W ((a + d).tdiv 2) * W ((a - d).tdiv 2) * (W ((b + c).tdiv 2) * W ((b - c).tdiv 2))

R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
parity : d % 2 = a % 2 ∧ d % 2 = b % 2 ∧ d % 2 = c % 2
⊢ 2 ∣ a + b + (c + d)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
b c d : R
n : ℕ
hn : n = 0
⊢ preNormEDS b c d ↑n = preNormEDS' b c d n

Tactic:
simp [hn, preNormEDS]

Goal state after: