mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Birational.Birational

Goal state before:
pp: case mpr
X Y : Scheme
U₁ : X.Opens
hU₁ : Dense ↑U₁
U₂ : Y.Opens
hU₂✝ : Dense ↑U₂
f : ↑U₁ ≅ ↑U₂
V₁ : X.Opens
hV₁ : Dense ↑V₁
V₂ : Y.Opens
hU₂ : Dense ↑V₂
g : ↑V₁ ≅ ↑V₂
⊢ (∃ (e :
      { source := U₁, dense_source := hU₁, target := U₂, dense_target := hU₂✝, iso := f }.source =
        { source := V₁, dense_source := hV₁, target := V₂, dense_target := hU₂, iso := g }.source)
      (e' :
      { source := V₁, dense_source := hV₁, target := V₂, dense_target := hU₂, iso := g }.target =
        { source := U₁, dense_source := hU₁, target := U₂, dense_target := hU₂✝, iso := f }.target),
      { source := U₁, dense_source := hU₁, target := U₂, dense_target := hU₂✝, iso := f }.iso =
        X.isoOfEq e ≪≫
          { source := V₁, dense_source := hV₁, target := V₂, dense_target := hU₂, iso := g }.iso ≪≫ Y.isoOfEq e') →
    { source := U₁, dense_source := hU₁, target := U₂, dense_target := hU₂✝, iso := f } =
      { source := V₁, dense_source := hV₁, target := V₂, dense_target := hU₂, iso := g }

Tactic:
simp only [forall_exists_index]

Goal state after:
case mpr
X Y : Scheme
U₁ : X.Opens
hU₁ : Dense ↑U₁
U₂ : Y.Opens
hU₂✝ : Dense ↑U₂
f : ↑U₁ ≅ ↑U₂
V₁ : X.Opens
hV₁ : Dense ↑V₁
V₂ : Y.Opens
hU₂ : Dense ↑V₂
g : ↑V₁ ≅ ↑V₂
⊢ ∀ (x : U₁ = V₁) (x_1 : V₂ = U₂),
    f = X.isoOfEq ⋯ ≪≫ g ≪≫ Y.isoOfEq ⋯ →
      { source := U₁, dense_source := hU₁, target := U₂, dense_target := hU₂✝, iso := f } =
        { source := V₁, dense_source := hV₁, target := V₂, dense_target := hU₂, iso := g }
Module: Mathlib.AlgebraicGeometry.Birational.Dominant

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
inst✝ : IsDominant f.hom
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
this : IsDominant (X.homOfLE hU')
⊢ IsDominant (X.homOfLE hU' ≫ f.hom)

Tactic:
IsDominant.comp_iff

Goal state after:
X Y : Scheme
f : X.PartialMap Y
inst✝ : IsDominant f.hom
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
this : IsDominant (X.homOfLE hU')
⊢ IsDominant f.hom
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝³ : PreirreducibleSpace ↥X
inst✝² : Nonempty ↥Y
f₁ f₂ : X.PartialMap Y
inst✝¹ : IsDominant f₁.hom
inst✝ : IsDominant f₂.hom
g : Y.PartialMap Z
W : X.Opens
hW : Dense ↑W
hW₁ : W ≤ f₁.domain
hW₂ : W ≤ f₂.domain
e : (f₁.restrict W hW hW₁).hom = (f₂.restrict W hW hW₂).hom
⊢ (f₁.comp g).equiv (f₂.comp g)

Tactic:
replace e : f₁.restrict W hW hW₁ = f₂.restrict W hW hW₂ :=
    PartialMap.ext _ _ rfl (by simpa using e)

Goal state after:
X Y Z : Scheme
inst✝³ : PreirreducibleSpace ↥X
inst✝² : Nonempty ↥Y
f₁ f₂ : X.PartialMap Y
inst✝¹ : IsDominant f₁.hom
inst✝ : IsDominant f₂.hom
g : Y.PartialMap Z
W : X.Opens
hW : Dense ↑W
hW₁ : W ≤ f₁.domain
hW₂ : W ≤ f₂.domain
e : f₁.restrict W hW hW₁ = f₂.restrict W hW hW₂
⊢ (f₁.comp g).equiv (f₂.comp g)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: 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)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU : c.π.app i ⁻¹ᵁ U = ⊤
H : ∀ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≠ ⊤
j k : I
fkj : k ⟶ j
fji : j ⟶ i
x : ↥(D.obj k)
hx : (D.map (fkj ≫ fji)) x ∉ U
⊢ (D.map fkj) x ∈ (↑(D.map fji ⁻¹ᵁ U))ᶜ

Tactic:
by rwa [Functor.map_comp] at hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
I : Set ↑T.affineOpens
hI : I.Finite
e : UT = ⨆ i ∈ I, ↑i
hIUT : ∀ (i : ↑I), ↑↑i ≤ UT
this : Finite ↑I
⊢ IsIso (pushoutSection ⋯ hUSX hUST ⋯)

Tactic:
exact isIso_pushoutSection_of_iSup_eq _ _ _ _ (fun i : I ↦ i) (by rwa [iSup_subtype, eq_comm])
    (fun i ↦ isIso_pushoutSection_of_isQuasiSeparated_of_flat_left _ _ _ _ hUS i.1.2 hUX hUX')
    (fun i j ↦ mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat _ _ _ _ hUS hUX
    (hUT' _ _ (hIUT _) i.1.1.2 i.1.2.isCompact (hIUT _) j.1.1.2 j.1.2.isCompact) hiX) hiX

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_2.refine_2
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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
x : ↥((opensDiagram D i U).obj j)
h : ((opensDiagram D i U).map f) x ∈ V
⊢ ⟨(D.map (Over.Hom.left f)) ↑x, ⋯⟩ ∈ ↑V

Tactic:
convert! h

Goal state after:
case e'_1
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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
x : ↥((opensDiagram D i U).obj j)
h : ((opensDiagram D i U).map f) x ∈ V
⊢ ⟨(D.map (Over.Hom.left f)) ↑x, ⋯⟩ = ((opensDiagram D i U).map f) x
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_2
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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
⊢ (opensDiagram D i U).map f ⁻¹ᵁ V = (D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V

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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
⊢ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V ≤ Scheme.Hom.opensRange (D.map j.hom ⁻¹ᵁ U).ι

Tactic:
· ext x
    change _ ∈ V ↔ _
    refine ⟨fun h ↦ ⟨⟨(D.map f.left).base x.1, ?_⟩, ?_, rfl⟩, ?_⟩
    · change (D.map f.left ≫ D.map k.hom).base x.1 ∈ U
      rw [← D.map_comp, Over.w f]
      exact x.2
    · convert! h
      exact Subtype.ext (by simp)
    · rintro ⟨⟨_, hU⟩, hV, rfl⟩
      convert! hV
      exact Subtype.ext (by simp)

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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
⊢ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V ≤ Scheme.Hom.opensRange (D.map j.hom ⁻¹ᵁ U).ι
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case refine_2
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U
V : Opens ((i : ι) × X i)
hc✝ : IsCompact V.carrier
heq : (fun p ↦ f p.fst p.snd) '' V.carrier = U
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
hc : ∀ (i : ι), IsCompact (t i)
heq' : s.sigma t = V.carrier
this : ∀ i ∈ s, IsOpen (t i)
⊢ ⋃ i, ⋃ (x : i ∈ s), f i '' ↑{ carrier := t i, is_open' := ⋯ } = U

Tactic:
coe_mk,

Goal state after:
case refine_2
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U
V : Opens ((i : ι) × X i)
hc✝ : IsCompact V.carrier
heq : (fun p ↦ f p.fst p.snd) '' V.carrier = U
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
hc : ∀ (i : ι), IsCompact (t i)
heq' : s.sigma t = V.carrier
this : ∀ i ∈ s, IsOpen (t i)
⊢ ⋃ i ∈ s, f i '' t i = U
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)
U : Set S
κ : Type u_4
inst✝ : Finite κ
s : κ → Set S
hs : ⋃ i, s i = U
H : ∀ (i : κ), IsCompactOpenCovered f (s i)
⊢ IsCompactOpenCovered f U

Tactic:
by
  rw [iff_isCompactOpenCovered_sigmaMk, iff_of_unique]
  have (i : κ) : ∃ (V : Opens (Σ i, X i)), IsCompact V.1 ∧ (f _ ·.snd) '' V.1 = s i := by
    convert! H i; rw [iff_isCompactOpenCovered_sigmaMk, iff_of_unique]
  choose V hVeq hVc using this
  exact ⟨⨆ i, V i, by simpa using isCompact_iUnion hVeq, by simp_all [Set.image_iUnion, ← hs]⟩

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

Goal state before:
pp: case refine_1
S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' ↑U' ⊆ ↑U
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
i : (PreZeroHypercover.pullback₁ f 𝒰).I₀
hi : i ∈ s
⊢ IsCompact ((fun i hi ↦ pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i hi) i hi).carrier

Tactic:
exact hU'.isCompact_pullback_inf (hc _ _) hU (by simpa using! hsub) <| by
      simpa [← SetLike.coe_subset_coe, ← heq, Set.range_comp] using! Set.subset_iUnion_of_subset i
        (Set.subset_iUnion_of_subset hi (Set.subset_preimage_image _ _))

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

Goal state before:
pp: case refine_2
S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' ↑U' ⊆ ↑U
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq✝ : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
x : ↥T
hx : x ∈ ↑U'
i : 𝒰.I₀
hi : i ∈ s
y : ↥(𝒰.X i)
hy : y ∈ ↑(V i ⋯)
heq : (fun a ↦ (𝒰.f i) a) y = f x
⊢ ∃ i,
    ∃ (i_1 : i ∈ s),
      x ∈
        (fun a ↦ ((PreZeroHypercover.pullback₁ f 𝒰).f i) a) ''
          ↑(pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i ⋯)

Tactic:
obtain ⟨z, hzl, hzr⟩ := Scheme.Pullback.exists_preimage_pullback x y heq.symm

Goal state after:
case refine_2
S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' ↑U' ⊆ ↑U
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq✝ : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
x : ↥T
hx : x ∈ ↑U'
i : 𝒰.I₀
hi : i ∈ s
y : ↥(𝒰.X i)
hy : y ∈ ↑(V i ⋯)
heq : (fun a ↦ (𝒰.f i) a) y = f x
z : ↥(pullback f (𝒰.f i))
hzl : (pullback.fst f (𝒰.f i)) z = x
hzr : (pullback.snd f (𝒰.f i)) z = y
⊢ ∃ i,
    ∃ (i_1 : i ∈ s),
      x ∈
        (fun a ↦ ((PreZeroHypercover.pullback₁ f 𝒰).f i) a) ''
          ↑(pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i ⋯)
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this : Epi π
⊢ IsRegularEpi π

Tactic:
refine .of_epi_of_exists fun Z f hf ↦ ?_

Goal state after:
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
⊢ ∃ u, π ≫ u = f
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y - (C (C 2) * Y + C (C W'.a₁ * X + C W'.a₃)) = W'.negPolynomial

Tactic:
negPolynomial

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y - (C (C 2) * Y + C (C W'.a₁ * X + C W'.a₃)) = -Y - C (C W'.a₁ * X + C W'.a₃)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y W'.negPolynomial = -y - (W'.a₁ * x + W'.a₃)

Tactic:
negPolynomial

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y (-Y - C (C W'.a₁ * X + C W'.a₃)) = -y - (W'.a₁ * x + W'.a₃)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ C
      (eval (C ℓ * (X - C x) + C y)
        (Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆))) =
    (Y - C (C ℓ * (X - C x) + C y)) * (W'.negPolynomial - C (C ℓ * (X - C x) + C y)) +
      (Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆))

Tactic:
negPolynomial

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ C
      (eval (C ℓ * (X - C x) + C y)
        (Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆))) =
    (Y - C (C ℓ * (X - C x) + C y)) * (-Y - C (C W'.a₁ * X + C W'.a₃) - C (C ℓ * (X - C x) + C y)) +
      (Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ C (W'.addPolynomial x y ℓ) - (Y - C (linePolynomial x y ℓ)) * (W'.negPolynomial - C (linePolynomial x y ℓ)) =
    W'.polynomial * 1

Tactic:
by rw [W'.C_addPolynomial, add_sub_cancel_left, mul_one]

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

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ (Y - C (C y)) * (Y - C (C (W.negY x y))) -
          C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) +
        C (C (y ^ 2 + W.a₁ * x * y + W.a₃ * y)) -
      (W.polynomial * 1 + C (C (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆))) =
    0

Tactic:
rw [negY, polynomial]; C_simp; ring1

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case left
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 := ⋯
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) := ⋯
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)) := ⋯
s₀ : Set (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) := ⋯
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
j : Fin x.n ⊕ Fin n
⊢ ∀ (i : Fin m →₀ ℕ),
    (MvPolynomial.coeff i
          (Sum.elim (⇑σ ∘ x.g) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))) j)).degrees ≤
      Finset.univ.val

Tactic:
intro i
        obtain j | j := j
        · simp [σ, MvPolynomial.coeff_map, degrees_C]
        · simp only [MvPolynomial.algebraMap_eq, Sum.elim_inr, MvPolynomial.coeff_sub,
            MvPolynomial.coeff_C, MvPolynomial.coeff_map, σ]
          refine degrees_sub_le.trans ?_
          simp only [degrees_C, apply_ite, degrees_zero,
            Multiset.union_zero]
          split_ifs with h
          · refine (degrees_X' _).trans ?_
            simp
          · simp

Goal state after:
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).IsHomogeneous 2

Tactic:
exact isHomogeneous_X_pow .. |>.sub CXY |>.sub CXY |>.sub CXX

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ complEDS₂ b c d (-k) = complEDS₂ b c d k

Tactic:
simp_rw [complEDS₂, ← neg_add', ← sub_neg_eq_add, ← neg_sub', preNormEDS_neg, even_neg]
  ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ ((Algebra.leftMulMatrix (CoordinateRing.basis W')) (p • 1 + q • (mk W') Y)).det =
    p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)

Tactic:
Matrix.det_fin_two,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ (Algebra.leftMulMatrix (CoordinateRing.basis W')) (p • 1 + q • (mk W') Y) 0 0 *
        (Algebra.leftMulMatrix (CoordinateRing.basis W')) (p • 1 + q • (mk W') Y) 1 1 -
      (Algebra.leftMulMatrix (CoordinateRing.basis W')) (p • 1 + q • (mk W') Y) 0 1 *
        (Algebra.leftMulMatrix (CoordinateRing.basis W')) (p • 1 + q • (mk W') Y) 1 0 =
    p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: 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)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
inst✝ : c.pt.IsQuasiAffine
i : ↥c.pt → I
f : (x : ↥c.pt) → ↑Γ(D.obj (i x), ⊤)
hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x))
hi : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ (D.obj (i x)).basicOpen (f x)
σ : Finset ↥c.pt
hσ : ⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier = ⊤
σi : ↥c.pt → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi : ∀ (x : ↥c.pt), x ∈ (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))).carrier
j : I
fj : (i_1 : I) → i_1 ∈ Finset.image i σ → (j ⟶ i_1)
⊢ c.π.app j ⁻¹ᵁ ⨆ k, D.map (fj (i (σi k)) ⋯) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤

Tactic:
by
      refine top_le_iff.mp fun x _ ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨x, ?_⟩
      change (c.π.app j ≫ D.map _).base x ∈ (D.obj (i (σi x))).basicOpen (f (σi x))
      rw [Cone.w]
      exact hσi _

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
⊢ ((Algebra.norm R[X]) (p • 1 + q • (mk W') Y)).degree = max (2 • p.degree) (2 • q.degree + 3)

Tactic:
rw [norm_smul_basis]

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
⊢ (p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree =
    max (2 • p.degree) (2 • q.degree + 3)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
inst✝⁴ : IsCofiltered I
R : CommRingCat
inst✝³ : IsAffine (Spec R)
S : CommRingCat
inst✝² : IsAffine (Spec S)
φ : R ⟶ S
inst✝¹ : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
inst✝ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
e : ((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec ≅ (Functor.const I).obj (Spec R) :=
  NatIso.ofComponents (fun x ↦ Iso.refl ((((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec).obj x)) ⋯
t : (Functor.const Iᵒᵖ).obj R ⟶ D.leftOp
c' : Cocone D.leftOp
ψ : S ⟶ Opposite.unop (coneOfCoconeLeftOp c').pt
ha :
  (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    (Functor.const I).map (Spec.map ψ ≫ Spec.map φ)
hc : IsColimit c'
i : Iᵒᵖ
⊢ φ ≫ ψ = t.app i ≫ c'.ι.app i

Tactic:
apply Spec.map_injective; simpa using! congr(($ha).app i.unop).symm

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W⁄B).Ψ₃ = Polynomial.map (↑f) (W⁄A).Ψ₃

Tactic:
by
  rw [← map_Ψ₃, map_baseChange]

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

Goal state before:
pp: case h.a₁
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ ({ u := 1, r := 0, s := s, t := 0 } • E).a₁ = E'.a₁

Tactic:
simp_rw [variableChange_a₁, inv_one, Units.val_one, a₁_of_isCharTwoJNeZeroNF]

Goal state after:
case h.a₁
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ 1 * (1 + 2 * s) = 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ (W.toShortNFOfCharThree • W).a₂ = W.b₂

Tactic:
toShortNFOfCharThree,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ (W.toCharNeTwoNF • W).a₂ = W.b₂
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ W.b₈ = W.a₆

Tactic:
by
  rw [b₈_of_isCharTwoJNeZeroNF]
  linear_combination 2 * W.a₂ * W.a₆ * CharP.cast_eq_zero R 2

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
F : Type u_2
inst✝³ : Field F
W✝ : WeierstrassCurve R
inst✝² : CharP R 2
inst✝¹ : CharP F 2
W : WeierstrassCurve F
inst✝ : DecidableEq F
⊢ (W.toCharTwoNF • W).IsCharTwoNF

Tactic:
by
  by_cases ha₁ : W.a₁ = 0
  · rw [toCharTwoNF, dif_pos ha₁]
    have := W.toCharTwoJEqZeroNF_spec ha₁
    infer_instance
  · rw [toCharTwoNF, dif_neg ha₁]
    have := W.toCharTwoJNeZeroNF_spec ha₁
    infer_instance

Goal state after: