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

Goal state before:
pp: case e'_2.e'_6
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty ↥↑U
e_1✝ : PrimeSpectrum ↑Γ(X, U) = ↥(Spec (X.presheaf.obj (op U)))
⊢ ↑⟨genericPoint ↥X, ⋯⟩ = ↑(genericPoint ↥↑U)

Tactic:
exact (genericPoint_eq_of_isOpenImmersion U.ι).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case mp
X Y : Scheme
f g : X.PartialMap Y
⊢ f = g → ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom

Tactic:
rintro rfl

Goal state after:
case mp
X Y : Scheme
f : X.PartialMap Y
⊢ ∃ (e : f.domain = f.domain), f.hom = (X.isoOfEq e).hom ≫ f.hom
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
e : ⟨x, ⋯⟩ = (X.homOfLE hU') ⟨x, hx⟩
⊢ Spec.map (inv (Hom.stalkMap U.ι ⟨x, hx⟩)) ≫
      Spec.map (Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩) ≫ (↑f.domain).fromSpecStalk ((X.homOfLE hU') ⟨x, hx⟩) ≫ f.hom =
    (Spec.map (inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)) ≫ (↑f.domain).fromSpecStalk ⟨x, ⋯⟩) ≫ f.hom

Tactic:
← SpecMap_stalkSpecializes_fromSpecStalk (Inseparable.of_eq e).specializes,

Goal state after:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
e : ⟨x, ⋯⟩ = (X.homOfLE hU') ⟨x, hx⟩
⊢ Spec.map (inv (Hom.stalkMap U.ι ⟨x, hx⟩)) ≫
      Spec.map (Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩) ≫ (↑f.domain).fromSpecStalk ((X.homOfLE hU') ⟨x, hx⟩) ≫ f.hom =
    (Spec.map (inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)) ≫
        Spec.map ((↑f.domain).presheaf.stalkSpecializes ⋯) ≫ (↑f.domain).fromSpecStalk ((X.homOfLE hU') ⟨x, hx⟩)) ≫
      f.hom
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝ : IrreducibleSpace ↥X
f : X ⤏ Y
⊢ Spec X.functionField ⟶ Y

Tactic:
by
  refine Quotient.lift PartialMap.fromFunctionField ?_ f
  intro f g ⟨W, hW, hWl, hWr, e⟩
  have : f.restrict W hW hWl = g.restrict W hW hWr := by
    ext1
    · rfl
    rw [e]; simp
  rw [← f.fromFunctionField_restrict hW hWl, this, g.fromFunctionField_restrict]

Goal state after:
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✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
⊢ Nonempty ↥c.pt

Tactic:
classical
  cases isEmpty_or_nonempty I
  · have e := (isLimitEquivIsTerminalOfIsEmpty _ _ hc).uniqueUpToIso specULiftZIsTerminal
    exact Nonempty.map e.inv inferInstance
  · have i := Nonempty.some ‹Nonempty I›
    have : IsCofiltered I := ⟨⟩
    let 𝒰 := (D.obj i).affineCover.finiteSubcover
    have (i' : _) : IsAffine (𝒰.X i') := inferInstanceAs (IsAffine (Spec _))
    obtain ⟨j, H⟩ :
        ∃ j : 𝒰.I₀, ∀ {i'} (f : i' ⟶ i), Nonempty ((𝒰.pullback₁ (D.map f)).X j) := by
      by_contra! H
      choose i' f hf using H
      let g (j) := IsCofiltered.infTo (insert i (Finset.univ.image i'))
        (Finset.univ.image fun j : 𝒰.I₀ ↦ ⟨_, _, by simp, by simp, f j⟩) (X := j)
      have (j : 𝒰.I₀) : IsEmpty ((𝒰.pullback₁ (D.map (g i (by simp)))).X j) := by
        let F : (𝒰.pullback₁ (D.map (g i (by simp)))).X j ⟶
            (𝒰.pullback₁ (D.map (f j))).X j :=
          pullback.map _ _ _ _ (D.map (g _ (by simp))) (𝟙 _) (𝟙 _) (by
            rw [← D.map_comp, IsCofiltered.infTo_commutes]
            · simp [g]
            · simp
            · exact Finset.mem_image_of_mem _ (Finset.mem_univ _)) (by simp)
        exact Function.isEmpty F
      obtain ⟨x, -⟩ :=
        Cover.covers (𝒰.pullback₁ (D.map (g i (by simp)))) (Nonempty.some inferInstance)
      exact (this _).elim x
    let F := Over.post D ⋙ Over.pullback (𝒰.f j) ⋙ Over.forget _
    have (i' : _) : IsAffine (F.obj i') :=
      have : IsAffineHom (pullback.snd (D.map i'.hom) (𝒰.f j)) :=
        MorphismProperty.pullback_snd _ _ inferInstance
      isAffine_of_isAffineHom (pullback.snd (D.map i'.hom) (𝒰.f j))
    have (i' : _) : Nonempty (F.obj i') := H i'.hom
    let e : F ⟶ (F ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := Functor.whiskerLeft F ΓSpec.adjunction.unit
    have (i : _) : IsIso (e.app i) := IsAffine.affine
    have : IsIso e := NatIso.isIso_of_isIso_app e
    let c' : LimitCone F := ⟨_, (IsLimit.postcomposeInvEquiv (asIso e) _).symm
      (isLimitOfPreserves Scheme.Spec (limit.isLimit (F ⋙ Scheme.Γ.rightOp)))⟩
    have : Nonempty c'.1.pt := by
      apply +allowSynthFailures PrimeSpectrum.instNonemptyOfNontrivial
      have (i' : _) : Nontrivial ((F ⋙ Scheme.Γ.rightOp).leftOp.obj i') := by
        apply +allowSynthFailures Scheme.component_nontrivial
        simp
      exact CommRingCat.FilteredColimits.nontrivial
        (isColimitCoconeLeftOpOfCone _ (limit.isLimit (F ⋙ Scheme.Γ.rightOp)))
    let α : F ⟶ Over.forget _ ⋙ D := Functor.whiskerRight
      (Functor.whiskerLeft (Over.post D) (Over.mapPullbackAdj (𝒰.f j)).counit) (Over.forget _)
    exact this.map (((Functor.Initial.isLimitWhiskerEquiv (Over.forget i) c).symm hc).lift
        ((Cone.postcompose α).obj c'.1))

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Birational

Goal state before:
pp: case mp
X Y : Scheme
f g : X.PartialIso Y
⊢ f = g → ∃ (e : f.source = g.source) (e' : g.target = f.target), f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e'

Tactic:
rintro rfl

Goal state after:
case mp
X Y : Scheme
f : X.PartialIso Y
⊢ ∃ (e : f.source = f.source) (e' : f.target = f.target), f.iso = X.isoOfEq e ≪≫ f.iso ≪≫ Y.isoOfEq e'
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✝¹ : IsCofilteredOrEmpty I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  { obj := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subscheme,
    map := fun {X Y} f ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D'.map f)
x✝¹ : ∀ (i : I), Nonempty ↥(D'.obj i)
x✝ : ∀ (i : I), CompactSpace ↥(D'.obj i)
c' : Cone D' :=
  { pt := (⨆ i, (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).comap (c.π.app i)).subscheme,
    π :=
      {
        app := fun i ↦
          (⨆ i, (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).comap (c.π.app i)).subschemeMap
            (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }) (c.π.app i) ⋯,
        naturality := ⋯ } }
s : Cone D'
⊢ Scheme.Hom.ker (⨆ i, (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).comap (c.π.app i)).subschemeι ≤
    Scheme.Hom.ker (hc.lift ((Cone.postcompose ι).obj s))

Tactic:
suffices ∀ i, vanishingIdeal ⟨Z i, hZc i⟩ ≤ (s.π.app i ≫ ι.app i).ker by
        simpa [← le_map_iff_comap_le, ← Scheme.Hom.ker_comp]

Goal state after:
I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofilteredOrEmpty I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  { obj := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subscheme,
    map := fun {X Y} f ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D'.map f)
x✝¹ : ∀ (i : I), Nonempty ↥(D'.obj i)
x✝ : ∀ (i : I), CompactSpace ↥(D'.obj i)
c' : Cone D' :=
  { pt := (⨆ i, (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).comap (c.π.app i)).subscheme,
    π :=
      {
        app := fun i ↦
          (⨆ i, (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).comap (c.π.app i)).subschemeMap
            (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }) (c.π.app i) ⋯,
        naturality := ⋯ } }
s : Cone D'
⊢ ∀ (i : I), vanishingIdeal { carrier := Z i, isClosed' := ⋯ } ≤ Scheme.Hom.ker (s.π.app i ≫ ι.app i)
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝¹⁰ : PreirreducibleSpace ↥X
inst✝⁹ : Nonempty ↥Y
S : Scheme
inst✝⁸ : IrreducibleSpace ↥Y
inst✝⁷ : Nonempty ↥Z
inst✝⁶ : X.Over S
inst✝⁵ : Y.Over S
inst✝⁴ : Z.Over S
f : X ⤏ Y
inst✝³ : f.IsDominant
inst✝² : IsOver S f
g : Y ⤏ Z
inst✝¹ : g.IsDominant
inst✝ : IsOver S g
⊢ (f.comp g).comp (Hom.toRationalMap (Z ↘ S)) = Hom.toRationalMap (X ↘ S)

Tactic:
comp_assoc,

Goal state after:
X Y Z : Scheme
inst✝¹⁰ : PreirreducibleSpace ↥X
inst✝⁹ : Nonempty ↥Y
S : Scheme
inst✝⁸ : IrreducibleSpace ↥Y
inst✝⁷ : Nonempty ↥Z
inst✝⁶ : X.Over S
inst✝⁵ : Y.Over S
inst✝⁴ : Z.Over S
f : X ⤏ Y
inst✝³ : f.IsDominant
inst✝² : IsOver S f
g : Y ⤏ Z
inst✝¹ : g.IsDominant
inst✝ : IsOver S g
⊢ f.comp (g.comp (Hom.toRationalMap (Z ↘ S))) = Hom.toRationalMap (X ↘ S)
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: case a
⊢ diagonal @Surjective ≤ @UniversallyInjective

Tactic:
· rw [← universally_eq_iff.mpr (inferInstance : IsStableUnderBaseChange (diagonal @Surjective)),
      universallyInjective_eq]
    apply universally_mono
    intro X Y f hf x₁ x₂ e
    obtain ⟨t, ht₁, ht₂⟩ := Scheme.Pullback.exists_preimage_pullback _ _ e
    obtain ⟨t, rfl⟩ := hf.1 t
    rw [← ht₁, ← ht₂, ← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, pullback.diagonal_fst,
      pullback.diagonal_snd]

Goal state after:
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: case refine_2
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
⊢ ∀ (s : PullbackCone (𝒰.f i) d.toBase), IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯ ≫ d.natTrans.app i = s.fst

Tactic:
intro s
    rw [← cancel_mono (𝒰.f i), Category.assoc, ← ι_toBase, IsOpenImmersion.lift_fac_assoc,
      s.condition]

Goal state after:
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
inst✝ : Unique ι
x✝ : ∃ V, IsCompact V.carrier ∧ f default '' V.carrier = U
V : Opens (X default)
hc : IsCompact V.carrier
h : f default '' V.carrier = U
i : ι
⊢ ∀ (h : i ∈ {default}), IsCompact ((fun i h ↦ ⋯ ▸ V) i h).carrier

Tactic:
rintro rfl

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
inst✝ : Unique ι
x✝ : ∃ V, IsCompact V.carrier ∧ f default '' V.carrier = U
V : Opens (X default)
hc : IsCompact V.carrier
h : f default '' V.carrier = U
⊢ IsCompact ((fun i h ↦ ⋯ ▸ V) default ⋯).carrier
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
inst✝⁴ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝³ : LocallyOfFiniteType f
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
inst✝ : ∀ (i : I), IsAffineHom (A.c.π.app i)
j : A.𝒰D.I₀
this✝² : IsAffine (A.𝒰D.X j)
this✝¹ : ∀ (i : Over A.i'), IsAffine ((Over.post D ⋙ Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).obj i)
this✝ : IsAffine ((Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).mapCone ((Over.conePost D A.i').obj A.c)).pt
this : LocallyOfFiniteType ((A.𝒰X j.fst.fst).f j.fst.snd ≫ Scheme.Cover.pullbackHom A.𝒰S f j.fst.fst)
H₁ :
  pullback.fst (D.map A.hii' ≫ pullback.lift A.a A.b ⋯)
        ((Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩) ≫
      D.map A.hii' ≫ A.a =
    pullback.snd (D.map A.hii' ≫ pullback.lift A.a A.b ⋯)
        ((Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩) ≫
      pullback.fst ((A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.snd f (A.𝒰S.f j.fst.fst))
          ((A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.snd f (A.𝒰S.f j.fst.fst)) ≫
        (A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.fst f (A.𝒰S.f j.fst.fst)
H₂ :
  pullback.fst (D.map A.hii' ≫ pullback.lift A.a A.b ⋯)
        ((Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩) ≫
      D.map A.hii' ≫ A.b =
    pullback.snd (D.map A.hii' ≫ pullback.lift A.a A.b ⋯)
        ((Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩) ≫
      pullback.snd ((A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.snd f (A.𝒰S.f j.fst.fst))
          ((A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.snd f (A.𝒰S.f j.fst.fst)) ≫
        (A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.fst f (A.𝒰S.f j.fst.fst)
⊢ IsLimit ((Over.forget (D.obj A.i')).mapCone ((Over.conePost D A.i').obj A.c))

Tactic:
exact (Functor.Initial.isLimitWhiskerEquiv (Over.forget A.i') A.c).symm A.hc

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)
U : Set S
s : Set (Set S)
hs : ⋃ t ∈ s, t = U
hf : s.Finite
H : ∀ t ∈ s, IsCompactOpenCovered f t
⊢ IsCompactOpenCovered f U

Tactic:
have := hf.to_subtype
  exact of_iUnion_eq_of_finite (fun i : s ↦ i.1) (by simpa) (by simpa)

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

Goal state before:
pp: R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
deg_bound₂ : c'.degBound < c.degBound
⊢ c.degBound * c.degBound ^ c'.degBound = c.degBound ^ (c'.degBound + 1)

Tactic:
rw [pow_succ']

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:
c₄,

Goal state after:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.b₂ ^ 2 - 24 * W.b₄ = W.a₁ ^ 4
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1) ^ numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1) *
      ((k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n) =
    (k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1)

Tactic:
numBound_succ,

Goal state after:
k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
          ((k₀ * k) ^ (k₀ * k) • D) n) ^
        (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
          ((k₀ * k) ^ (k₀ * k) • D) n) *
      ((k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n) =
    (k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound k₀ (fun x ↦ Nat.casesOn x k D) (n + 1) *
      Nat.casesOn (n + 1) k D =
    numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1)

Tactic:
numBound_succ,

Goal state after:
k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound k₀ (fun x ↦ Nat.casesOn x k D) (n + 1) *
      Nat.casesOn (n + 1) k D =
    numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
      ((k₀ * k) ^ (k₀ * k) • D) n
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ numBound k₁ D₁ (n + 1) ≤ numBound k₂ D₂ (n + 1)

Tactic:
numBound_succ,

Goal state after:
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ numBound k₁ D₁ n * degBound k₁ D₁ n * D₁ n ≤ numBound k₂ D₂ (n + 1)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.Equation x (W'.negY x y) ↔ W'.Equation x y

Tactic:
equation_iff,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.negY x y ^ 2 + W'.a₁ * x * W'.negY x y + W'.a₃ * W'.negY x y = x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆ ↔
    W'.Equation x y
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.negY x y ^ 2 + W'.a₁ * x * W'.negY x y + W'.a₃ * W'.negY x y = x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆ ↔
    W'.Equation x y

Tactic:
equation_iff,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.negY x y ^ 2 + W'.a₁ * x * W'.negY x y + W'.a₃ * W'.negY x y = x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆ ↔
    y ^ 2 + W'.a₁ * x * y + W'.a₃ * y = x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆
Module: Mathlib.LinearAlgebra.FreeModule.Norm

Goal state before:
pp: S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
⊢ finrank F (S ⧸ span {f}) = (∏ i, smithCoeffs b (span {f}) ⋯ i).natDegree

Tactic:
natDegree_prod _ _ fun i _ => smithCoeffs_ne_zero b _ h i,

Goal state after:
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
⊢ finrank F (S ⧸ span {f}) = ∑ i, (smithCoeffs b (span {f}) h i).natDegree
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case pos
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₂)
hx : x₁ = x₂
⊢ y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
have hy : y₁ ≠ W.negY x₂ y₂ := fun h => hxy ⟨hx, h⟩
      rcases hx, Y_eq_of_Y_ne h₁ h₂ hx hy with ⟨rfl, rfl⟩
      simp [linePolynomial]

Goal state after:
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
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ C (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) =
    -(C (X - C x₁) * C (X - C x₂) * C (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))

Tactic:
rw [addPolynomial_slope h₁ h₂ hxy]
  simp

Goal state after:
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:
simp_rw [slope_of_X_ne hx, addX, negY, ← neg_sub x₁, neg_sq]

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ -(x₁ - (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂)) - x₂ =
    -(x₁ -
            (((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) -
              W.a₂)) -
        x₂ -
      (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂) ^ 2
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
⊢ ∃ i, (D.obj i).IsQuasiAffine

Tactic:
obtain ⟨j, fj⟩ := IsCofiltered.inf_objs_exists (σ.image i)

Goal state after:
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 : ∀ {X : I}, X ∈ Finset.image i σ → Nonempty (j ⟶ X)
⊢ ∃ i, (D.obj i).IsQuasiAffine
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case mpr
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
P : W.Point
⊢ P = 0 → toClass P = 0

Tactic:
· exact congr_arg toClass

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.c₄ = 16 * W.a₂ ^ 2 - 48 * W.a₄

Tactic:
c₄,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.b₂ ^ 2 - 24 * W.b₄ = 16 * W.a₂ ^ 2 - 48 * W.a₄
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.c₄ = 16 * W.a₂ ^ 2 - 48 * W.a₄

Tactic:
rw [c₄, b₂_of_isCharNeTwoNF, b₄_of_isCharNeTwoNF]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ (4 * W.a₂) ^ 2 - 24 * (2 * W.a₄) = 16 * W.a₂ ^ 2 - 48 * W.a₄
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.c₄ = W.b₂ ^ 2

Tactic:
c₄,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.b₂ ^ 2 - 24 * W.b₄ = W.b₂ ^ 2