mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₂
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
inst✝ : Algebra R₀✝ R
f : R[X]
M : Type u_2 := R[X] ⧸ Ideal.span {g.val i}
this✝ : Module.Free R M
this : Module.Finite R M
⊢ ∃ T,
    comap Polynomial.C '' (zeroLocus (Set.range g.val) \ zeroLocus {f}) = T.toSet ∧
      ∀ C ∈ T, C.n ≤ g.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ coeffSubmodule R₀✝ g ^ g.powBound

Tactic:
refine ⟨(Finset.range (Module.finrank R M)).image
      fun j ↦ ⟨(Algebra.lmul R M (Ideal.Quotient.mk _ f)).charpoly.coeff j, 0, 0⟩, ?_, ?_⟩

Goal state after:
case hP₂.refine_1
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
inst✝ : Algebra R₀✝ R
f : R[X]
M : Type u_2 := R[X] ⧸ Ideal.span {g.val i}
this✝ : Module.Free R M
this : Module.Finite R M
⊢ comap Polynomial.C '' (zeroLocus (Set.range g.val) \ zeroLocus {f}) =
    ConstructibleSetData.toSet
      (Finset.image
        (fun j ↦
          { f := (LinearMap.charpoly ((Algebra.lmul R M) ((Ideal.Quotient.mk (Ideal.span {g.val i})) f))).coeff j,
            n := 0, g := 0 })
        (Finset.range (Module.finrank R M)))

case hP₂.refine_2
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
inst✝ : Algebra R₀✝ R
f : R[X]
M : Type u_2 := R[X] ⧸ Ideal.span {g.val i}
this✝ : Module.Free R M
this : Module.Finite R M
⊢ ∀
    C ∈
      Finset.image
        (fun j ↦
          { f := (LinearMap.charpoly ((Algebra.lmul R M) ((Ideal.Quotient.mk (Ideal.span {g.val i})) f))).coeff j,
            n := 0, g := 0 })
        (Finset.range (Module.finrank R M)),
    C.n ≤ g.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ coeffSubmodule R₀✝ g ^ g.powBound
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₂.refine_1
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
inst✝ : Algebra R₀✝ R
f : R[X]
M : Type u_2 := R[X] ⧸ Ideal.span {g.val i}
this✝¹ : Module.Free R M
this✝ : Module.Finite R M
x : PrimeSpectrum R
this : zeroLocus (Set.range g.val) = zeroLocus {g.val i}
⊢ ¬IsNilpotent ((algebraMap M ((R[X] ⧸ Ideal.span {g.val i}) ⊗[R] x.asIdeal.ResidueField)) ((algebraMap R[X] M) f)) ↔
    x ∈
      ConstructibleSetData.toSet
        (Finset.image
          (fun j ↦
            { f := (LinearMap.charpoly ((Algebra.lmul R M) ((Ideal.Quotient.mk (Ideal.span {g.val i})) f))).coeff j,
              n := 0, g := 0 })
          (Finset.range (Module.finrank R M)))

Tactic:
isNilpotent_tensor_residueField_iff

Goal state after:
case hP₂.refine_1
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
inst✝ : Algebra R₀✝ R
f : R[X]
M : Type u_2 := R[X] ⧸ Ideal.span {g.val i}
this✝¹ : Module.Free R M
this✝ : Module.Finite R M
x : PrimeSpectrum R
this : zeroLocus (Set.range g.val) = zeroLocus {g.val i}
⊢ (¬∀ i_1 < Module.finrank R M,
        (LinearMap.charpoly ((Algebra.lmul R M) ((algebraMap R[X] M) f))).coeff i_1 ∈ x.asIdeal) ↔
    x ∈
      ConstructibleSetData.toSet
        (Finset.image
          (fun j ↦
            { f := (LinearMap.charpoly ((Algebra.lmul R M) ((Ideal.Quotient.mk (Ideal.span {g.val i})) f))).coeff j,
              n := 0, g := 0 })
          (Finset.range (Module.finrank R M)))
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case refine_1.inl
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
U : Set S
inst✝ : Unique ι
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hcov : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
h✝ : s = ∅
⊢ ∃ V, IsCompact V.carrier ∧ f default '' V.carrier = U

pp: case refine_1.inr
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
U : Set S
inst✝ : Unique ι
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hcov : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
h✝ : s = {default}
⊢ ∃ V, IsCompact V.carrier ∧ f default '' V.carrier = U

Tactic:
<;>

Goal state after:
case refine_1.inl
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
U : Set S
inst✝ : Unique ι
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hcov : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
h✝ : s = ∅
⊢ ∃ V, IsCompact V.carrier ∧ f default '' V.carrier = U

case refine_1.inr
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
U : Set S
inst✝ : Unique ι
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hcov : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
h✝ : s = {default}
⊢ ∃ V, IsCompact V.carrier ∧ f default '' V.carrier = U
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝² : Category.{v_2, u_2} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone i).pt ≅ ((MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)).mapCocone (d.cocone j)).pt :=
  (d.isColimit i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)) (d.isColimit j))
    (D.isoWhiskerLeft (MorphismProperty.Over.pullbackComp (Cover.trans 𝒰 hij) (𝒰.f j) (𝒰.f i) ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))).symm)
heq :
  (MorphismProperty.Over.map ⊤ ⋯).map iso1.hom ≫
      (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans 𝒰 hij) ⋯ trivial).counit.app (d.cocone j).pt =
    d.transitionMap hij
iso2 : (d.cocone i).pt.left ≅ pullback (d.cocone j).pt.hom (Cover.trans 𝒰 hij) :=
  (MorphismProperty.Over.forget P ⊤ (𝒰.X i) ⋙ CategoryTheory.Over.forget (𝒰.X i)).mapIso iso1
⊢ pullback.snd (d.cocone j).pt.hom (Cover.trans 𝒰 hij) ≫ (Iso.refl (𝒰.X i)).hom = iso2.symm.hom ≫ (d.cocone i).pt.hom

Tactic:
· exact (Over.w iso1.inv).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Sigma

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : UnivLE.{v, u}
𝒰 : Cover (precoverage P) S
i : 𝒰.I₀
y : ↥(𝒰.X i)
⊢ ∃ i_1, (𝒰.f i) y ∈ Set.range ⇑({ I₀ := PUnit.{v + 1}, X := fun x ↦ ∐ 𝒰.X, f := fun x ↦ Sigma.desc 𝒰.f }.f i_1)

Tactic:
refine ⟨default, Sigma.ι 𝒰.X i y, by simp [← Scheme.Hom.comp_apply]⟩

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.c₄ = W.a₁ ^ 4

Tactic:
rw [c₄, b₂_of_char_two]

Goal state after:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ (W.a₁ ^ 2) ^ 2 - 24 * W.b₄ = W.a₁ ^ 4
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁴ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝³ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a : D.obj i ⟶ X
ha : t.app i = a ≫ f
j : I
b : D.obj j ⟶ X
hb : t.app j = b ≫ f
hab : c.π.app i ≫ a = c.π.app j ≫ b
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b

Tactic:
let o := IsCofiltered.min i j

Goal state after:
I : Type u
inst✝⁴ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝³ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a : D.obj i ⟶ X
ha : t.app i = a ≫ f
j : I
b : D.obj j ⟶ X
hb : t.app j = b ≫ f
hab : c.π.app i ≫ a = c.π.app j ≫ b
o : I := IsCofiltered.min i j
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ (W.map f).b₈ = f W.b₈

Tactic:
simp only [b₈, map_a₁, map_a₂, map_a₃, map_a₄, map_a₆]
  map_simp

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.a = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.a

pp: case b
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.b = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.b

pp: case c
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.c = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.c

pp: case d
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.d = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.d

Tactic:
<;>

Goal state after:
case a
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.a = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.a

case b
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.b = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.b

case c
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.c = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.c

case d
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.d = { a := 0, b := W.b₂, c := 0, d := W.b₆ }.d
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: case a
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.a = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.a

pp: case b
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.b = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.b

pp: case c
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.c = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.c

pp: case d
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.d = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.d

Tactic:
<;>

Goal state after:
case a
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.a = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.a

case b
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.b = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.b

case c
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.c = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.c

case d
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ }.d = { a := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }.d
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case u
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ ↑(x✝² * x✝¹ * x✝).u = ↑(x✝² * (x✝¹ * x✝)).u

pp: case r
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ (x✝² * x✝¹ * x✝).r = (x✝² * (x✝¹ * x✝)).r

pp: case s
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ (x✝² * x✝¹ * x✝).s = (x✝² * (x✝¹ * x✝)).s

pp: case t
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ (x✝² * x✝¹ * x✝).t = (x✝² * (x✝¹ * x✝)).t

Tactic:
<;>

Goal state after:
case u
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ ↑(x✝² * x✝¹ * x✝).u = ↑(x✝² * (x✝¹ * x✝)).u

case r
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ (x✝² * x✝¹ * x✝).r = (x✝² * (x✝¹ * x✝)).r

case s
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ (x✝² * x✝¹ * x✝).s = (x✝² * (x✝¹ * x✝)).s

case t
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ (x✝² * x✝¹ * x✝).t = (x✝² * (x✝¹ * x✝)).t
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case u
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ ↑x✝².u * ↑x✝¹.u * ↑x✝.u = ↑x✝².u * (↑x✝¹.u * ↑x✝.u)

pp: case r
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ (x✝².r * ↑x✝¹.u ^ 2 + x✝¹.r) * ↑x✝.u ^ 2 + x✝.r = x✝².r * (↑x✝¹.u * ↑x✝.u) ^ 2 + (x✝¹.r * ↑x✝.u ^ 2 + x✝.r)

pp: case s
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ ↑x✝.u * (↑x✝¹.u * x✝².s + x✝¹.s) + x✝.s = ↑x✝¹.u * ↑x✝.u * x✝².s + (↑x✝.u * x✝¹.s + x✝.s)

pp: case t
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ (x✝².t * ↑x✝¹.u ^ 3 + x✝².r * x✝¹.s * ↑x✝¹.u ^ 2 + x✝¹.t) * ↑x✝.u ^ 3 +
        (x✝².r * ↑x✝¹.u ^ 2 + x✝¹.r) * x✝.s * ↑x✝.u ^ 2 +
      x✝.t =
    x✝².t * (↑x✝¹.u * ↑x✝.u) ^ 3 + x✝².r * (↑x✝.u * x✝¹.s + x✝.s) * (↑x✝¹.u * ↑x✝.u) ^ 2 +
      (x✝¹.t * ↑x✝.u ^ 3 + x✝¹.r * x✝.s * ↑x✝.u ^ 2 + x✝.t)

Tactic:
<;>

Goal state after:
case u
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ ↑x✝².u * ↑x✝¹.u * ↑x✝.u = ↑x✝².u * (↑x✝¹.u * ↑x✝.u)

case r
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ (x✝².r * ↑x✝¹.u ^ 2 + x✝¹.r) * ↑x✝.u ^ 2 + x✝.r = x✝².r * (↑x✝¹.u * ↑x✝.u) ^ 2 + (x✝¹.r * ↑x✝.u ^ 2 + x✝.r)

case s
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ ↑x✝.u * (↑x✝¹.u * x✝².s + x✝¹.s) + x✝.s = ↑x✝¹.u * ↑x✝.u * x✝².s + (↑x✝.u * x✝¹.s + x✝.s)

case t
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C C' x✝² x✝¹ x✝ : VariableChange R
⊢ (x✝².t * ↑x✝¹.u ^ 3 + x✝².r * x✝¹.s * ↑x✝¹.u ^ 2 + x✝¹.t) * ↑x✝.u ^ 3 +
        (x✝².r * ↑x✝¹.u ^ 2 + x✝¹.r) * x✝.s * ↑x✝.u ^ 2 +
      x✝.t =
    x✝².t * (↑x✝¹.u * ↑x✝.u) ^ 3 + x✝².r * (↑x✝.u * x✝¹.s + x✝.s) * (↑x✝¹.u * ↑x✝.u) ^ 2 +
      (x✝¹.t * ↑x✝.u ^ 3 + x✝¹.r * x✝.s * ↑x✝.u ^ 2 + x✝.t)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: case inl
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 = 0 ∧ g.degree = 3
⊢ 1 < g.degree

pp: case inl
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 = 0 ∧ g.degree = 3
⊢ f.degree < g.degree

Tactic:
<;>

Goal state after:
case inl
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 = 0 ∧ g.degree = 3
⊢ 1 < g.degree

case inl
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 = 0 ∧ g.degree = 3
⊢ f.degree < g.degree
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: case inl
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 = 0 ∧ g.degree = 3
⊢ 1 < 3

pp: case inl
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 = 0 ∧ g.degree = 3
⊢ 0 < 3

Tactic:
<;>

Goal state after:
case inl
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 = 0 ∧ g.degree = 3
⊢ 1 < 3

case inl
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 = 0 ∧ g.degree = 3
⊢ 0 < 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: case inr.inl
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 = 1 ∧ g.degree = 2
⊢ 1 < g.degree

pp: case inr.inl
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 = 1 ∧ g.degree = 2
⊢ f.degree < g.degree

Tactic:
<;>

Goal state after:
case inr.inl
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 = 1 ∧ g.degree = 2
⊢ 1 < g.degree

case inr.inl
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 = 1 ∧ g.degree = 2
⊢ f.degree < g.degree
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: case inr.inl
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 = 1 ∧ g.degree = 2
⊢ 1 < 2

pp: case inr.inl
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 = 1 ∧ g.degree = 2
⊢ 1 < 2

Tactic:
<;>

Goal state after:
case inr.inl
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 = 1 ∧ g.degree = 2
⊢ 1 < 2

case inr.inl
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 = 1 ∧ g.degree = 2
⊢ 1 < 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: case inr.inr.inl
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 = 2 ∧ g.degree = 1
⊢ 1 < f.degree

pp: case inr.inr.inl
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 = 2 ∧ g.degree = 1
⊢ g.degree < f.degree

Tactic:
<;>

Goal state after:
case inr.inr.inl
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 = 2 ∧ g.degree = 1
⊢ 1 < f.degree

case inr.inr.inl
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 = 2 ∧ g.degree = 1
⊢ g.degree < f.degree
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: case inr.inr.inl
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 = 2 ∧ g.degree = 1
⊢ 1 < 2

pp: case inr.inr.inl
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 = 2 ∧ g.degree = 1
⊢ 1 < 2

Tactic:
<;>

Goal state after:
case inr.inr.inl
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 = 2 ∧ g.degree = 1
⊢ 1 < 2

case inr.inr.inl
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 = 2 ∧ g.degree = 1
⊢ 1 < 2
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 < f.degree

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
⊢ g.degree < f.degree

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 < f.degree

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
⊢ g.degree < f.degree