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

Goal state before:
pp: 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

Tactic:
· simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: 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 𝒰
i : 𝒰.I₀
⊢ d.transitionMap (𝟙 i) = (MorphismProperty.Over.mapId ⊤ (𝒰.X i) (Cover.trans 𝒰 (𝟙 i)) ⋯).hom.app (d.cocone i).pt

Tactic:
apply (isColimitOfPreserves (Over.map ⊤ (d.prop_trans <| 𝟙 i)) (d.isColimit i)).hom_ext
  intro
  ext
  simp [cocone_ι_transitionMap]

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : Finite ι
inst✝ : TopologicalSpace S
hf : ∀ (i : ι), IsSpectralMap (f i)
U : Set S
hs : ∀ x ∈ U, ∃ i, x ∈ Set.range (f i)
hU : IsOpen U
hc : IsCompact U
i : ι
y : X i
hx : f i y ∈ U
⊢ f i y ∈ ⋃ i, ⋃ (h : i ∈ Set.univ), f i '' ↑((fun i x ↦ { carrier := f i ⁻¹' U, is_open' := ⋯ }) i h)

Tactic:
simpa using ⟨i, y, hx, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y S : Scheme
inst✝⁴ : IsAffine X
inst✝³ : IsAffine Y
π : X ⟶ Y
inst✝² : Surjective π
inst✝¹ : Flat π
f : X ⟶ S
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
inst✝ : IsAffine S
⊢ ∃ u, π ≫ u = f

Tactic:
by
  have : EffectiveEpi (AffineScheme.ofHom π) := by
    apply AffineScheme.equivCommRingCat.functor.effectiveEpi_of_map
    apply CommRingCat.Opposite.effectiveEpi_of_faithfullyFlat
    exact (Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine π).mp ⟨‹_›, ‹_›⟩
  obtain ⟨u, hu⟩ := IsRegularEpi.exists_of_isKernelPair
    (AffineScheme.ofHom π)
    (IsPullback.of_map (f := AffineScheme.ofHom (pullback.fst π π)) (AffineScheme.forgetToScheme)
      (InducedCategory.Hom.ext pullback.condition) (.of_hasPullback _ _))
    (AffineScheme.ofHom f) (InducedCategory.Hom.ext hf)
  use u.hom, InducedCategory.Hom.ext_iff.mp hu

Goal state after:
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
⊢ ∃ 𝒰, ∀ (i : 𝒰.I₀), ∃ u, fst π (𝒰.f i) ≫ f = snd π (𝒰.f i) ≫ u

Tactic:
obtain ⟨b, hfac⟩ : ∃ (u : Y.carrier ⟶ S.carrier), π.base ≫ u = f.base := by
    apply IsRegularEpi.exists_of_isKernelPair _ (IsPullback.of_hasPullback _ _)
    have := congr(Scheme.forgetToTop.map $hf)
    rwa [Functor.map_comp, Functor.map_comp, ← pullbackComparison_comp_fst_assoc,
      ← pullbackComparison_comp_snd_assoc, cancel_epi] at this
  let 𝒰 := Y.openCoverOfIsOpenCover _ <| Y.isBasis_affineOpens.isOpenCover_mem_and_le
    (S.isBasis_affineOpens.isOpenCover.comap b.hom)
  refine ⟨𝒰, fun i ↦ ?_⟩
  have : IsAffine (𝒰.X i) := i.2.1
  let f' : pullback π (𝒰.f i) ⟶ i.1.2.1 := by
    apply IsOpenImmersion.lift (Scheme.Opens.ι i.1.2.1) (pullback.fst _ _ ≫ f)
    dsimp
    rw [← hfac, ← TopCat.coe_comp, ← Scheme.Hom.comp_base_assoc, pullback.condition]
    simp only [Hom.comp_base, TopCat.hom_comp, ContinuousMap.coe_comp, Set.range_comp,
      range_eq_univ, Set.image_univ, Opens.range_ι, Set.image_subset_iff]
    exact trans (by simp [𝒰]) i.2.2
  have h1 : fst (snd π (𝒰.f i)) _ ≫ fst _ _ = map _ _ _ _ (fst _ _) (fst _ _) _
    condition.symm condition.symm ≫ fst π π := by simp
  have h2 : snd (snd π (𝒰.f i)) _ ≫ fst _ _ = map _ _ _ _ (fst _ _) (fst _ _) _
    condition.symm condition.symm ≫ snd π π := by simp
  obtain ⟨u, hu⟩ := of_isAffine_target (pullback.snd π (𝒰.f i)) f' <| by
    simp only [← cancel_mono (Scheme.Opens.ι i.1.2.1),
      Category.assoc, IsOpenImmersion.lift_fac, f', reassoc_of% h1, reassoc_of% h2, hf]
  refine ⟨u ≫ Scheme.Opens.ι _, ?_⟩
  simp [reassoc_of% hu, f']

Goal state after:
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case h₁
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.499} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.499} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := ⋯
s : Cocone D
m : d.gluedCocone.pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone.ι.app j ≫ m = s.ι.app j
i : 𝒱.I₀
a : J
⊢ ((d.cocone i).ι.app a ≫ (d.pullbackGluedIso i).inv ≫ (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).map m).left ≫
      pullback.snd s.pt.hom (𝒰.f i) =
    (((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s).ι.app a).left ≫ pullback.snd s.pt.hom (𝒰.f i)

Tactic:
· simp

Goal state after:
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
o : I := IsCofiltered.min i j
k : I
hik : k ⟶ IsCofiltered.min i j
heq : D.map hik ≫ D.map (IsCofiltered.minToLeft i j) ≫ a = D.map hik ≫ D.map (IsCofiltered.minToRight i j) ≫ b
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b

Tactic:
use k, hik ≫ IsCofiltered.minToLeft i j, hik ≫ IsCofiltered.minToRight i j

Goal state after:
case h
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 := ⋯
k : I
hik : k ⟶ IsCofiltered.min i j
heq : D.map hik ≫ D.map (IsCofiltered.minToLeft i j) ≫ a = D.map hik ≫ D.map (IsCofiltered.minToRight i j) ≫ b
⊢ D.map (hik ≫ IsCofiltered.minToLeft i j) ≫ a = D.map (hik ≫ IsCofiltered.minToRight i j) ≫ b
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_3
I : Type u
inst✝³ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
x : ↥(D.obj i)
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : x ∈ ↑U
this : ∀ (j : Over i), IsAffine ((opensDiagram D i U).obj j)
⊢ 0 = (CommRingCat.Hom.hom (c.pt.presheaf.map (homOfLE ⋯).op)) 0

Tactic:
· simp

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.twoTorsionPolynomial = { a := 0, b := W.b₂, c := 0, d := W.b₆ }

Tactic:
rw [twoTorsionPolynomial]

Goal state after:
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 := 0, b := W.b₂, c := 0, d := W.b₆ }
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

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

Tactic:
rw [twoTorsionPolynomial]

Goal state after:
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 := 1, b := W.b₂, c := -W.b₄, d := W.b₆ }
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_3
I : Type u
inst✝³ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
x : ↥(D.obj i)
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : x ∈ ↑U
this : ∀ (j : Over i), IsAffine ((opensDiagram D i U).obj j)
j : Over i
f : j ⟶ Over.mk (𝟙 i)
hj :
  (ConcreteCategory.hom (Scheme.Hom.appTop ((opensDiagram D i U).map f)))
      ((ConcreteCategory.hom (Scheme.Hom.appTop ((opensDiagramι D i U).app (Over.mk (𝟙 i))))) s) =
    0
hf : Over.Hom.left f = j.hom
t' : Γ(↑(D.map j.hom ⁻¹ᵁ U), ⊤) ⟶ Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ U) := (D.obj j.left).presheaf.map (eqToHom ⋯).op
⊢ 0 = (ConcreteCategory.hom t') 0

Tactic:
· simp

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W.polynomial
f g : R[X]
h0 : W.polynomial.coeff 0 = f * g
h1 : W.polynomial.coeff 1 = f + g
⊢ False

Tactic:
simp only [polynomial_eq, Cubic.coeff_eq_c, Cubic.coeff_eq_d] at h0 h1

Goal state after:
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W.polynomial
f g : R[X]
h0 : { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly = f * g
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly = f + g
⊢ False
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_3
I : Type u
inst✝³ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
U : ↥(D.obj i) → (D.obj i).Opens
hU : ∀ (x : ↥(D.obj i)), IsAffineOpen (U x)
hxU : ∀ (x : ↥(D.obj i)), x ∈ U x
j : ↥(D.obj i) → I
f : (x : ↥(D.obj i)) → j x ⟶ i
H : ∀ (x : ↥(D.obj i)), (ConcreteCategory.hom (Scheme.Hom.app (D.map (f x)) (U x))) ((s |_ U x) ⋯) = 0
t : Finset ↥(D.obj i)
ht : ⋃ x ∈ t, ↑(U x) = ⊤
k : I
fk : {X : I} → X ∈ insert i (Finset.image j t) → (k ⟶ X)
hk :
  ∀ {X Y : I} (mX : X ∈ insert i (Finset.image j t)) (mY : Y ∈ insert i (Finset.image j t)) {f_1 : X ⟶ Y},
    ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ Finset.image (fun x ↦ ⟨j ↑x, ⟨i, ⟨⋯, ⟨⋯, f ↑x⟩⟩⟩⟩) t.attach → fk mX ≫ f_1 = fk mY
x : ↥(D.obj k)
l : ↥(D.obj i)
hl : l ∈ t
hlU : (D.map (fk ⋯)) x ∈ ↑(U l)
h₁ : fk ⋯ = fk ⋯ ≫ f l
h₂ : D.map (fk ⋯) ⁻¹ᵁ U l ≤ D.map (fk ⋯) ⁻¹ᵁ D.map (f l) ⁻¹ᵁ U l
⊢ 0 = (ConcreteCategory.hom (Scheme.Hom.appLE (D.map (fk ⋯)) (D.map (f l) ⁻¹ᵁ U l) (D.map (fk ⋯) ⁻¹ᵁ U l) h₂)) 0

Tactic:
· simp

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

Goal state before:
pp: case a₆
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C✝ C C' : VariableChange R
W : WeierstrassCurve R
⊢ (↑C.u⁻¹ * ↑C'.u⁻¹) ^ 6 *
      (W.a₆ + (C.r * ↑C'.u ^ 2 + C'.r) * W.a₄ + (C.r * ↑C'.u ^ 2 + C'.r) ^ 2 * W.a₂ + (C.r * ↑C'.u ^ 2 + C'.r) ^ 3 -
            (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) * W.a₃ -
          (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) ^ 2 -
        (C.r * ↑C'.u ^ 2 + C'.r) * (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) * W.a₁) =
    ↑C.u⁻¹ ^ 6 *
      (↑C'.u⁻¹ ^ 6 * (W.a₆ + C'.r * W.a₄ + C'.r ^ 2 * W.a₂ + C'.r ^ 3 - C'.t * W.a₃ - C'.t ^ 2 - C'.r * C'.t * W.a₁) +
                  C.r *
                    (↑C'.u⁻¹ ^ 4 *
                      (W.a₄ - C'.s * W.a₃ + 2 * C'.r * W.a₂ - (C'.t + C'.r * C'.s) * W.a₁ + 3 * C'.r ^ 2 -
                        2 * C'.s * C'.t)) +
                C.r ^ 2 * (↑C'.u⁻¹ ^ 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - C'.s ^ 2)) +
              C.r ^ 3 -
            C.t * (↑C'.u⁻¹ ^ 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t)) -
          C.t ^ 2 -
        C.r * C.t * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)))

Tactic:
linear_combination
        C.r * C.u⁻¹ ^ 6 * C'.u⁻¹ ^ 4 * (C'.r * W.a₂ * 2 - C'.r * C'.s * W.a₁ + C'.r ^ 2 * 3 + W.a₄
            - C'.s * C'.t * 2 - C'.s * W.a₃ - C'.t * W.a₁) * pow_mul_pow_eq_one 2 C'.u.inv_mul
          - C.u⁻¹ ^ 6 * C'.u⁻¹ ^ 3 * C.t * (C'.r * W.a₁ + C'.t * 2 + W.a₃)
            * pow_mul_pow_eq_one 3 C'.u.inv_mul
          + C.r ^ 2 * C.u⁻¹ ^ 6 * C'.u⁻¹ ^ 2 * (C'.r * 3 + W.a₂ - C'.s * W.a₁ - C'.s ^ 2)
            * pow_mul_pow_eq_one 4 C'.u.inv_mul
          - C.r * C.t * C.u⁻¹ ^ 6 * ↑C'.u⁻¹ * (C'.s * 2 + W.a₁) * pow_mul_pow_eq_one 5 C'.u.inv_mul
          + C.u⁻¹ ^ 6 * (C.r ^ 3 - C.t ^ 2) * pow_mul_pow_eq_one 6 C'.u.inv_mul

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_3
I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
hU : IsCompact ↑U
s : ↑Γ(D.obj i, U)
hs : (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) s = 0
this : CompactSpace ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
H : (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U
j : Over i
f : j ⟶ Over.mk (𝟙 i)
hf :
  (ConcreteCategory.hom
        (Scheme.Hom.appTop (Scheme.Hom.resLE (D.map (Over.Hom.left f)) (D.map (𝟙 i) ⁻¹ᵁ U) (D.map j.hom ⁻¹ᵁ U) ⋯)))
      ((ConcreteCategory.hom ((D.obj i).presheaf.map (homOfLE ⋯).op)) s) =
    0
hf' : Over.Hom.left f = j.hom
⊢ 0 = (ConcreteCategory.hom ((D.obj j.left).presheaf.map (homOfLE ⋯).op)) 0

Tactic:
· simp

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective ⇑f
p q : R[X]
hy : Polynomial.map f p • 1 + Polynomial.map f q • (mk (W'.map f)) Y = 0
hp : p = 0
hq : q = 0
⊢ p • 1 + q • (mk W') Y = 0

Tactic:
hp,

Goal state after:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective ⇑f
p q : R[X]
hy : Polynomial.map f p • 1 + Polynomial.map f q • (mk (W'.map f)) Y = 0
hp : p = 0
hq : q = 0
⊢ 0 • 1 + q • (mk W') Y = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
hx : ¬x₁ = x₂
⊢ W.Nonsingular x₂ (-(W.slope x₁ x₂ y₁ y₂ * (x₁ - x₂)) + y₁)

Tactic:
slope_of_X_ne hx,

Goal state after:
case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : ¬W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
hx₂ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
hx : ¬x₁ = x₂
⊢ W.Nonsingular x₂ (-((y₁ - y₂) / (x₁ - x₂) * (x₁ - x₂)) + y₁)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) =
    W.addX x₁ x₂ (W.slope x₁ x₂ y₁ (W.negY x₂ y₂)) - (y₁ - W.negY x₁ y₁) * (y₂ - W.negY x₂ y₂) / (x₂ - x₁) ^ 2

Tactic:
slope_of_X_ne hx,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)) =
    W.addX x₁ x₂ ((y₁ - W.negY x₂ y₂) / (x₁ - x₂)) - (y₁ - W.negY x₁ y₁) * (y₂ - W.negY x₂ y₂) / (x₂ - x₁) ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ y₁ * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) + y₂ * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) +
      W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) * (x₁ - x₂) =
    0

Tactic:
slope_of_X_ne hx,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ y₁ * (x₂ - W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))) + y₂ * (W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)) - x₁) +
      W.negAddY x₁ x₂ y₁ ((y₁ - y₂) / (x₁ - x₂)) * (x₁ - x₂) =
    0
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case neg
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
hg : g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) = ↑f
σ : MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) (MvPolynomial (Fin n) R) :=
  MvPolynomial.map (algebraMap R (MvPolynomial (Fin n) R))
hσ : g.comp σ = RingHom.id (MvPolynomial (Fin m) R)
hσ' : ∀ (x : MvPolynomial (Fin m) R), g (σ x) = x
hg' : Surjective ⇑g
S' : ConstructibleSetData (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Finset.image
    (fun x ↦
      match x with
      | { f := fk, n := k, g := gk } =>
        { f := σ fk, n := k + n,
          g := fun s ↦
            Sum.elim (⇑σ ∘ gk) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i)))
              (finSumFinEquiv.symm s) })
    S
s₀ : Set (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Set.range fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))
hs : zeroLocus s₀ = Set.range (comap g)
hg'' : ∀ (t : Set (PrimeSpectrum (MvPolynomial (Fin m) R))), comap g '' t = comap σ ⁻¹' t ∩ zeroLocus s₀
hS' : comap g '' S.toSet = S'.toSet
x : BasicConstructibleSetData (MvPolynomial (Fin m) R)
hx : x ∈ S
i : Fin m →₀ ℕ
j : Fin n
h : ¬0 = i
⊢ 0 ≤ Finset.univ.val

Tactic:
· simp

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c : ℤ
⊢ atomRel W a b c b = W b * W 0 * atom W c a

Tactic:
linear_combination (norm := (simp_rw [atomRel, atom_same]; ring1))
    W b * W 0 * neg_atom odd a c - atom W a b * neg_atom odd b c

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
⊢ preNormEDS b c d (2 * -↑0 + 1) =
    (preNormEDS b c d (-↑0 + 2) * preNormEDS b c d (-↑0) ^ 3 * if Even (-↑0) then b else 1) -
      preNormEDS b c d (-↑0 - 1) * preNormEDS b c d (-↑0 + 1) ^ 3 * if Even (-↑0) then 1 else b

pp: case neg.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
m : ℕ
⊢ preNormEDS b c d (2 * -↑(m + 1) + 1) =
    (preNormEDS b c d (-↑(m + 1) + 2) * preNormEDS b c d (-↑(m + 1)) ^ 3 * if Even (-↑(m + 1)) then b else 1) -
      preNormEDS b c d (-↑(m + 1) - 1) * preNormEDS b c d (-↑(m + 1) + 1) ^ 3 * if Even (-↑(m + 1)) then 1 else b

Tactic:
· simp

Goal state after:
case neg.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
m : ℕ
⊢ preNormEDS b c d (2 * -↑(m + 1) + 1) =
    (preNormEDS b c d (-↑(m + 1) + 2) * preNormEDS b c d (-↑(m + 1)) ^ 3 * if Even (-↑(m + 1)) then b else 1) -
      preNormEDS b c d (-↑(m + 1) - 1) * preNormEDS b c d (-↑(m + 1) + 1) ^ 3 * if Even (-↑(m + 1)) then 1 else b
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ complEDS b c d k (2 * ↑0) = complEDS b c d k ↑0 * complEDS₂ b c d (↑0 * k)

pp: case nat.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n✝ : ℕ
⊢ complEDS b c d k (2 * ↑(n✝ + 1)) = complEDS b c d k ↑(n✝ + 1) * complEDS₂ b c d (↑(n✝ + 1) * k)

Tactic:
· simp

Goal state after:
case nat.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n✝ : ℕ
⊢ complEDS b c d k (2 * ↑(n✝ + 1)) = complEDS b c d k ↑(n✝ + 1) * complEDS₂ b c d (↑(n✝ + 1) * k)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ complEDS b c d k (2 * ↑0 + 1) =
    complEDS b c d k ↑0 ^ 2 * normEDS b c d ((↑0 + 1) * k + 1) * normEDS b c d ((↑0 + 1) * k - 1) -
      complEDS b c d k (↑0 + 1) ^ 2 * normEDS b c d (↑0 * k + 1) * normEDS b c d (↑0 * k - 1)

pp: case nat.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n✝ : ℕ
⊢ complEDS b c d k (2 * ↑(n✝ + 1) + 1) =
    complEDS b c d k ↑(n✝ + 1) ^ 2 * normEDS b c d ((↑(n✝ + 1) + 1) * k + 1) * normEDS b c d ((↑(n✝ + 1) + 1) * k - 1) -
      complEDS b c d k (↑(n✝ + 1) + 1) ^ 2 * normEDS b c d (↑(n✝ + 1) * k + 1) * normEDS b c d (↑(n✝ + 1) * k - 1)

Tactic:
· simp

Goal state after:
case nat.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n✝ : ℕ
⊢ complEDS b c d k (2 * ↑(n✝ + 1) + 1) =
    complEDS b c d k ↑(n✝ + 1) ^ 2 * normEDS b c d ((↑(n✝ + 1) + 1) * k + 1) * normEDS b c d ((↑(n✝ + 1) + 1) * k - 1) -
      complEDS b c d k (↑(n✝ + 1) + 1) ^ 2 * normEDS b c d (↑(n✝ + 1) * k + 1) * normEDS b c d (↑(n✝ + 1) * k - 1)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (2 * ↑n + 1) =
      complEDS b c d k ↑n ^ 2 * normEDS b c d ((↑n + 1) * k + 1) * normEDS b c d ((↑n + 1) * k - 1) -
        complEDS b c d k (↑n + 1) ^ 2 * normEDS b c d (↑n * k + 1) * normEDS b c d (↑n * k - 1)
⊢ complEDS b c d k (2 * -↑0 + 1) =
    complEDS b c d k (-↑0) ^ 2 * normEDS b c d ((-↑0 + 1) * k + 1) * normEDS b c d ((-↑0 + 1) * k - 1) -
      complEDS b c d k (-↑0 + 1) ^ 2 * normEDS b c d (-↑0 * k + 1) * normEDS b c d (-↑0 * k - 1)

pp: case neg.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (2 * ↑n + 1) =
      complEDS b c d k ↑n ^ 2 * normEDS b c d ((↑n + 1) * k + 1) * normEDS b c d ((↑n + 1) * k - 1) -
        complEDS b c d k (↑n + 1) ^ 2 * normEDS b c d (↑n * k + 1) * normEDS b c d (↑n * k - 1)
m : ℕ
⊢ complEDS b c d k (2 * -↑(m + 1) + 1) =
    complEDS b c d k (-↑(m + 1)) ^ 2 * normEDS b c d ((-↑(m + 1) + 1) * k + 1) *
        normEDS b c d ((-↑(m + 1) + 1) * k - 1) -
      complEDS b c d k (-↑(m + 1) + 1) ^ 2 * normEDS b c d (-↑(m + 1) * k + 1) * normEDS b c d (-↑(m + 1) * k - 1)

Tactic:
· simp

Goal state after:
case neg.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (2 * ↑n + 1) =
      complEDS b c d k ↑n ^ 2 * normEDS b c d ((↑n + 1) * k + 1) * normEDS b c d ((↑n + 1) * k - 1) -
        complEDS b c d k (↑n + 1) ^ 2 * normEDS b c d (↑n * k + 1) * normEDS b c d (↑n * k - 1)
m : ℕ
⊢ complEDS b c d k (2 * -↑(m + 1) + 1) =
    complEDS b c d k (-↑(m + 1)) ^ 2 * normEDS b c d ((-↑(m + 1) + 1) * k + 1) *
        normEDS b c d ((-↑(m + 1) + 1) * k - 1) -
      complEDS b c d k (-↑(m + 1) + 1) ^ 2 * normEDS b c d (-↑(m + 1) * k + 1) * normEDS b c d (-↑(m + 1) * k - 1)