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

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
⊢ ⨅ i, (ker (𝒰.f i ≫ f)).ideal U = f.ker.ideal U

Tactic:
refine le_antisymm ?_ (le_iInf fun i ↦ (𝒰.f i).le_ker_comp f U)
  intro s hs
  simp only [Hom.ker_apply, RingHom.mem_ker]
  apply X.IsSheaf.section_ext
  rintro x hxU
  obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
  simp only [homOfLE_leOfHom, map_zero, exists_and_left]
  refine ⟨𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ U.1, ⟨_, hxU, rfl⟩,
    Set.image_preimage_subset (𝒰.f i) (f ⁻¹ᵁ U), ?_⟩
  apply ((𝒰.f i).appIso _).commRingCatIsoToRingEquiv.injective
  rw [map_zero, ← RingEquiv.coe_toRingHom, Iso.commRingCatIsoToRingEquiv_toRingHom,
    Scheme.Hom.appIso_hom']
  simp only [homOfLE_leOfHom, Scheme.Hom.app_eq_appLE, ← RingHom.comp_apply,
    ← CommRingCat.hom_comp, Scheme.Hom.appLE_map, Scheme.Hom.appLE_comp_appLE]
  simpa [Scheme.Hom.appLE] using! ideal_ker_le _ _ (Ideal.mem_iInf.mp hs i)

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ I.glueDataObjPullback U V ⟶ I.glueDataObjPullback V U

Tactic:
by
  letI F := pullback.snd (I.glueDataObjι U) (X.homOfLE (inf_le_left (b := V.1)))
  refine pullback.lift ((F ≫ X.homOfLE inf_le_right ≫
    V.2.isoSpec.hom).liftQuotient _ ?_) (F ≫ X.homOfLE (by simp)) ?_
  · intro x hx
    simp only [Hom.comp_app, Hom.comp_base, TopologicalSpace.Opens.map_comp_obj,
      TopologicalSpace.Opens.map_top, homOfLE_app, homOfLE_leOfHom, Category.assoc, RingHom.mem_ker]
    convert_to (U.1.ι.app V.1 ≫ (F ≫ X.homOfLE inf_le_left).appLE (U.1.ι ⁻¹ᵁ V.1) ⊤
      (by rw [← Scheme.Hom.comp_preimage, Category.assoc, X.homOfLE_ι]
          exact fun x _ ↦ by simpa using (F x).2.2)).hom x = 0 using 3
    · simp only [homOfLE_leOfHom, Opens.ι_app, Hom.comp_appLE, homOfLE_app]
      have H : ⊤ ≤ X.homOfLE (inf_le_left (b := V.1)) ⁻¹ᵁ U.1.ι ⁻¹ᵁ V.1 := by
        rw [← Scheme.Hom.comp_preimage, X.homOfLE_ι]; exact fun x _ ↦ by simpa using x.2.2
      rw [← F.map_appLE (show ⊤ ≤ F ⁻¹ᵁ ⊤ from le_rfl) (homOfLE H).op]
      simp only [homOfLE_leOfHom, Opens.toScheme_presheaf_map, Quiver.Hom.unop_op,
        Hom.opensFunctor_map_homOfLE, ← Functor.map_comp_assoc, IsAffineOpen.isoSpec_hom_appTop,
        Opens.topIso_inv, eqToHom_op, homOfLE_leOfHom, Category.assoc,
        Iso.inv_hom_id_assoc, F.app_eq_appLE]
      rfl
    · have : (U.1.ι.app V.1 ≫ (I.glueDataObjι U).app (U.1.ι ⁻¹ᵁ V.1)).hom x = 0 :=
        I.ideal_le_ker_glueDataObjι U V hx
      simp_rw [F, ← pullback.condition]
      simp only [Scheme.Opens.ι_app, CommRingCat.hom_comp, RingHom.coe_comp,
        Function.comp_apply, Scheme.Hom.appLE, Scheme.Hom.comp_app, Category.assoc] at this ⊢
      simp only [this, map_zero]
  · conv_lhs => enter [2]; rw [glueDataObjι]
    rw [Scheme.Hom.liftQuotient_comp_assoc, Category.assoc, Category.assoc, Iso.hom_inv_id,
      Category.comp_id, Category.assoc, X.homOfLE_homOfLE]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (pullback.fst f g) (T.SpecTensorTo p) = T.x

Tactic:
by
  simp only [SpecTensorTo]
  rw [← Scheme.Hom.comp_apply]
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (pullback.snd f g) (T.SpecTensorTo p) = T.y

Tactic:
by
  simp only [SpecTensorTo]
  rw [← Scheme.Hom.comp_apply]
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (Hom.ker f).map g = Hom.ker (f ≫ g)

Tactic:
by
  simp [← map_bot]

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ (vanishingIdeal Z).map f = vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' ↑Z))

Tactic:
by
  apply le_antisymm
  · rw [map, ← le_support_iff_le_vanishingIdeal, TopologicalSpace.Closeds.closure_le]
    refine .trans ?_ (Hom.range_subset_ker_support _)
    rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
      range_subschemeι, coe_support_vanishingIdeal]
  · simp [le_map_iff_comap_le, ← le_support_iff_le_vanishingIdeal, ← Set.image_subset_iff,
      subset_closure, ← SetLike.coe_subset_coe]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒱 i).I₀), IsAffine ((𝒱 i).X j)
U : (i : 𝒰.I₀) × (𝒱 i).I₀ → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i ↦ (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩)
hU :
  ∀ (i : (i : 𝒰.I₀) × (𝒱 i).I₀),
    (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i = Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩)
hf : iSup U = ⊤
i : (i : 𝒰.I₀) × (𝒱 i).I₀
⊢ IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱 ∣_ U i)

Tactic:
MorphismProperty.arrow_mk_iso_iff (P := @IsClosedImmersion) (morphismRestrictRestrict _ _ _),

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒱 i).I₀), IsAffine ((𝒱 i).X j)
U : (i : 𝒰.I₀) × (𝒱 i).I₀ → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i ↦ (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩)
hU :
  ∀ (i : (i : 𝒰.I₀) × (𝒱 i).I₀),
    (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i = Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩)
hf : iSup U = ⊤
i : (i : 𝒰.I₀) × (𝒱 i).I₀
⊢ IsClosedImmersion (pullback.diagonal f ∣_ (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i)
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hf : affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f

Tactic:
refine affineLocally_le (fun hf ↦ ?_) f hf

Goal state after:
X✝ Y✝ : Scheme
f✝¹ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hf✝ : affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
f✝ : R✝ →+* S✝
hf : f✝.FinitePresentation
⊢ f✝.FiniteType
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
hU : IsAffineOpen U
⊢ (ker f).ideal ⟨U, hU⟩ = ⊥

Tactic:
f.ker_eq_bot

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
hU : IsAffineOpen U
⊢ ⊥.ideal ⟨U, hU⟩ = ⊥
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Subsingleton ↥X
inst✝¹ : IsReduced X
inst✝ : JacobsonSpace ↥Y
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [Subsingleton ↥X] [IsReduced X] [JacobsonSpace ↥Y],
    (∃ S, Y = Spec S) → (IsFinite f ↔ LocallyOfFiniteType f)
hY : ¬∃ S, Y = Spec S
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    ∀ (i : Y.affineCover.toPreZeroHypercover.1), LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
have inst (i) := ((Y.affineCover.pullback₁ f).f i).isOpenEmbedding.injective.subsingleton

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Subsingleton ↥X
inst✝¹ : IsReduced X
inst✝ : JacobsonSpace ↥Y
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [Subsingleton ↥X] [IsReduced X] [JacobsonSpace ↥Y],
    (∃ S, Y = Spec S) → (IsFinite f ↔ LocallyOfFiniteType f)
hY : ¬∃ S, Y = Spec S
inst :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    Subsingleton ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    ∀ (i : Y.affineCover.toPreZeroHypercover.1), LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
f g : X ⟶ 𝔸(n; S)
h₁ : f ≫ 𝔸(n; S) ↘ S = g ≫ 𝔸(n; S) ↘ S
h₂ :
  ∀ (i : n),
    (ConcreteCategory.hom (Scheme.Hom.appTop f)) (coord S i) = (ConcreteCategory.hom (Scheme.Hom.appTop g)) (coord S i)
i : n
⊢ (toSpecMvPolyIntEquiv n) (f ≫ toSpecMvPoly n S) i = (toSpecMvPolyIntEquiv n) (g ≫ toSpecMvPoly n S) i

Tactic:
toSpecMvPolyIntEquiv_comp,

Goal state after:
n : Type u
S X : Scheme
f g : X ⟶ 𝔸(n; S)
h₁ : f ≫ 𝔸(n; S) ↘ S = g ≫ 𝔸(n; S) ↘ S
h₂ :
  ∀ (i : n),
    (ConcreteCategory.hom (Scheme.Hom.appTop f)) (coord S i) = (ConcreteCategory.hom (Scheme.Hom.appTop g)) (coord S i)
i : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop f)) ((toSpecMvPolyIntEquiv n) (toSpecMvPoly n S) i) =
    (toSpecMvPolyIntEquiv n) (g ≫ toSpecMvPoly n S) i
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S T : Scheme
f : S ⟶ T
i : n
⊢ (toSpecMvPolyIntEquiv n) (map n f ≫ toSpecMvPoly n T) i = (toSpecMvPolyIntEquiv n) (toSpecMvPoly n S) i

Tactic:
toSpecMvPolyIntEquiv_comp,

Goal state after:
n : Type u
S T : Scheme
f : S ⟶ T
i : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (map n f))) ((toSpecMvPolyIntEquiv n) (toSpecMvPoly n T) i) =
    (toSpecMvPolyIntEquiv n) (toSpecMvPoly n S) i
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
j : J
x y : F.obj j
⊢ (∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) y) →
    ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) y

Tactic:
rintro ⟨k, f, h⟩
    exact ⟨k, f, f, h⟩

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

Goal state before:
pp: R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n :=
  { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom ↑q₁) ∘ e.val }
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := { val := ⇑(mapRingHom ↑q₂) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
⊢ Statement R₀ (R ⧸ Ideal.span {c}) n { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } →
    Statement R₀ R n e

Tactic:
(H₂ : Statement R₀ _ _ e₂)

Goal state after:
R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n :=
  { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom ↑q₁) ∘ e.val }
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := { val := ⇑(mapRingHom ↑q₂) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
H₂ : Statement R₀ (R ⧸ Ideal.span {c}) n e₂
⊢ Statement R₀ R n e
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case right
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
z : X
hz : z ∈ V
t : Set X
ht : t ∈ 𝓝 z ∧ (t ∩ D.support).Finite
⊢ (t ∩ Function.support fun z ↦ if hz : z ∈ V then D z else 0) ⊆ t ∩ D.support

Tactic:
intro _ _

Goal state after:
case right
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
z : X
hz : z ∈ V
t : Set X
ht : t ∈ 𝓝 z ∧ (t ∩ D.support).Finite
a✝¹ : X
a✝ : a✝¹ ∈ t ∩ Function.support fun z ↦ if hz : z ∈ V then D z else 0
⊢ a✝¹ ∈ t ∩ D.support
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
⊢ EqOn (⇑(D.restrict h)) (⇑D) V

Tactic:
intro _ _

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
x✝ : X
a✝ : x✝ ∈ V
⊢ (D.restrict h) x✝ = D x✝
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
⊢ EqOn (⇑(D.restrict h)) 0 Vᶜ

Tactic:
intro _ hx
  simp_all

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case inr
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)
h✝ : Nonempty I
i : I
this✝² : IsCofiltered I
𝒰 : (D.obj i).OpenCover := (D.obj i).affineCover.finiteSubcover
this✝¹ : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
j : 𝒰.I₀
H : ∀ {i' : I} (f : i' ⟶ i), Nonempty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map f) 𝒰).X j)
F : Over i ⥤ Scheme := Over.post D ⋙ Over.pullback (𝒰.f j) ⋙ Over.forget (𝒰.X j)
this✝ : ∀ (i' : Over i), IsAffine (F.obj i')
this : ∀ (i' : Over i), Nonempty ↥(F.obj i')
⊢ Nonempty ↥c.pt

Tactic:
let e : F ⟶ (F ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := Functor.whiskerLeft F ΓSpec.adjunction.unit

Goal state after:
case inr
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)
h✝ : Nonempty I
i : I
this✝² : IsCofiltered I
𝒰 : (D.obj i).OpenCover := (D.obj i).affineCover.finiteSubcover
this✝¹ : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
j : 𝒰.I₀
H : ∀ {i' : I} (f : i' ⟶ i), Nonempty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map f) 𝒰).X j)
F : Over i ⥤ Scheme := Over.post D ⋙ Over.pullback (𝒰.f j) ⋙ Over.forget (𝒰.X j)
this✝ : ∀ (i' : Over i), IsAffine (F.obj i')
this : ∀ (i' : Over i), Nonempty ↥(F.obj i')
e : F ⟶ (F ⋙ Γ.rightOp) ⋙ Scheme.Spec := F.whiskerLeft ΓSpec.adjunction.unit
⊢ Nonempty ↥c.pt
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'
this : ∀ (i : I), vanishingIdeal { carrier := Z i, isClosed' := ⋯ } ≤ Scheme.Hom.ker (s.π.app i ≫ ι.app i)
⊢ Scheme.Hom.ker (⨆ i, (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).comap (c.π.app i)).subschemeι ≤
    Scheme.Hom.ker (hc.lift ((Cone.postcompose ι).obj s))

Tactic:
by
        simpa [← le_map_iff_comap_le, ← Scheme.Hom.ker_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_2
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
⊢ (ConcreteCategory.hom (Scheme.Hom.app (D.map (Over.Hom.left f)) U)) s =
    (ConcreteCategory.hom ((D.obj j.left).presheaf.map (homOfLE ⋯).op))
      ((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))

Tactic:
dsimp [Scheme.Opens.toScheme_presheaf_obj]
    rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply]
    congr! 2
    simp [Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE]

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

Goal state before:
pp: 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₀
⊢ ⋃ i ∈ S, comap g '' zeroLocus (Set.range i.g) \ comap g '' zeroLocus {i.f} =
    ⋃ y ∈ S,
      (zeroLocus (⇑σ '' Set.range y.g) ∩
          zeroLocus (Set.range fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i)))) \
        zeroLocus {σ y.f}

Tactic:
simp [hg'', ← Set.inter_sdiff_distrib_right, Set.sdiff_inter_right_comm, s₀]

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.norm R[X]) (p • 1 + q • (mk W') Y) =
    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:
simp_rw [Algebra.norm_eq_matrix_det <| CoordinateRing.basis W', Matrix.det_fin_two,
    Algebra.leftMulMatrix_eq_repr_mul, basis_zero, mul_one, basis_one, smul_basis_mul_Y, map_add,
    Finsupp.add_apply, map_smul, Finsupp.smul_apply, ← basis_zero, ← basis_one,
    Basis.repr_self_apply, if_pos, one_ne_zero, if_false, smul_eq_mul]
  ring1

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

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
⊢ ∀ (x y : W.Point),
    (match x + y with
      | zero => 0
      | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) =
      (match x with
        | zero => 0
        | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) +
        match y with
        | zero => 0
        | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)

Tactic:
rintro (_ | ⟨x₁, y₁, h₁⟩) (_ | ⟨x₂, y₂, h₂⟩)
    any_goals simp only [← zero_def, zero_add, add_zero]
    by_cases hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
    · simp only [hxy.left, hxy.right, add_of_Y_eq rfl rfl]
      exact (CoordinateRing.mk_XYIdeal'_neg_mul h₂).symm
    · simp only [add_some hxy]
      exact (CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal' h₁ h₂ hxy).symm

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆).natDegree ≤ 3

Tactic:
compute_degree

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈).natDegree ≤ 4

Tactic:
compute_degree

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (2 * X ^ 6 + C W.b₂ * X ^ 5 + 5 * C W.b₄ * X ^ 4 + 10 * C W.b₆ * X ^ 3 + 10 * C W.b₈ * X ^ 2 +
          C (W.b₂ * W.b₈ - W.b₄ * W.b₆) * X +
        C (W.b₄ * W.b₈ - W.b₆ ^ 2)).natDegree ≤
    6

Tactic:
compute_degree

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.preΨ₄.coeff 6 = 2

Tactic:
by
  rw [preΨ₄]
  compute_degree!

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.b₈ = 4 * W.a₂ * W.a₆ - W.a₄ ^ 2

Tactic:
b₈,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2 = 4 * W.a₂ * W.a₆ - W.a₄ ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.b₈ = W.a₆ + 4 * W.a₂ * W.a₆

Tactic:
b₈,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2 = W.a₆ + 4 * W.a₂ * W.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ W.b₈ = -W.a₄ ^ 2

Tactic:
b₈,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2 = -W.a₄ ^ 2