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

Goal state before:
pp: X Y : Scheme
inst✝ : IsIntegral X
f g : X.PartialMap Y
H : f.toRationalMap.fromFunctionField = g.toRationalMap.fromFunctionField
⊢ f.toRationalMap = g.toRationalMap

Tactic:
refine PartialMap.toRationalMap_eq_iff.mpr ?_

Goal state after:
X Y : Scheme
inst✝ : IsIntegral X
f g : X.PartialMap Y
H : f.toRationalMap.fromFunctionField = g.toRationalMap.fromFunctionField
⊢ f.equiv g
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case e'_2
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
e_1✝ : (↑((g x).domain ⊓ (g y).domain) ⟶ Y) = (↑((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).domain ⟶ Y)
⊢ (((X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯) ≫ (X.isoOfEq ⋯).inv) ≫ (g x).hom =
    ((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).hom

Tactic:
congr 1

Goal state after:
case e'_2.e_a
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
e_1✝ : (↑((g x).domain ⊓ (g y).domain) ⟶ Y) = (↑((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).domain ⟶ Y)
⊢ ((X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯) ≫ (X.isoOfEq ⋯).inv = X.homOfLE ⋯
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case e'_3
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
e_1✝ : (↑((g x).domain ⊓ (g y).domain) ⟶ Y) = (↑((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).domain ⟶ Y)
⊢ (((X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯) ≫ (X.isoOfEq ⋯).inv) ≫ (g y).hom =
    ((g y).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).hom

Tactic:
congr 1

Goal state after:
case e'_3.e_a
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
e_1✝ : (↑((g x).domain ⊓ (g y).domain) ⟶ Y) = (↑((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).domain ⟶ Y)
⊢ ((X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯) ≫ (X.isoOfEq ⋯).inv = X.homOfLE ⋯
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).toRationalMap = f.toRationalMap

Tactic:
congr 1

Goal state after:
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯ = f
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case H
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
⊢ ((Hom.isoImage (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain).ι
            ((TopologicalSpace.Opens.map (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv.base).obj
              ((TopologicalSpace.Opens.map (f.hom ∣_ g.domain).base).obj
                ((TopologicalSpace.Opens.map g.hom.base).obj h.domain)))).inv ≫
        (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv ∣_ (f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain) ≫
      f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain ≫ h.hom =
    ((((X₁.isoOfEq ⋯).hom ≫ (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)).inv) ≫
          (↑f.domain).homOfLE ⋯) ≫
        (Hom.isoImage (f.hom ⁻¹ᵁ g.domain).ι ((f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain)).inv) ≫
      f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain ≫ h.hom

Tactic:
congr 1

Goal state after:
case H.e_a
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
⊢ (Hom.isoImage (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain).ι
          ((TopologicalSpace.Opens.map (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv.base).obj
            ((TopologicalSpace.Opens.map (f.hom ∣_ g.domain).base).obj
              ((TopologicalSpace.Opens.map g.hom.base).obj h.domain)))).inv ≫
      (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv ∣_ (f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain =
    (((X₁.isoOfEq ⋯).hom ≫ (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)).inv) ≫
        (↑f.domain).homOfLE ⋯) ≫
      (Hom.isoImage (f.hom ⁻¹ᵁ g.domain).ι ((f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain)).inv
Module: Mathlib.RingTheory.RingHom.PurelyInseparable

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Field K
f : F →+* E
g : E →+* K
hf : f.IsPurelyInseparable
hg : g.IsPurelyInseparable
⊢ (g.comp f).IsPurelyInseparable

Tactic:
by
  algebraize [f, g, g.comp f]
  exact IsPurelyInseparable.trans F E K

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
h_inj : Injective ⇑f
hf : ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable
K : Type u
inst✝ : Field K
⊢ Injective fun g ↦ g ≫ f

Tactic:
g₁

Goal state after:
X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
h_inj : Injective ⇑f
hf : ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable
K : Type u
inst✝ : Field K
g₁ : Spec (CommRingCat.of K) ⟶ X
⊢ ∀ ⦃a₂ : Spec (CommRingCat.of K) ⟶ X⦄, (fun g ↦ g ≫ f) g₁ = (fun g ↦ g ≫ f) a₂ → g₁ = a₂
Module: Mathlib.AlgebraicGeometry.Cover.Over

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝³ : W.Over S
inst✝² : X.Over S
inst✝¹ : Cover.Over S 𝒰
inst✝ : Hom.IsOver f S
⊢ { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
        f := fun x ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }.presieve₀ ∈
    (precoverage P).coverings W

Tactic:
by
    rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, fun j ↦ ?_⟩
    · obtain ⟨i, hy⟩ := Cover.exists_eq (𝒰.pullback₁ f) x
      use i
      exact (mem_range_iff_of_surjective ((𝒰.pullback₁ f).f i) _
        ((PreservesPullback.iso (Over.forget S) (f.asOver S) ((𝒰.f _).asOver S)).inv)
        (PreservesPullback.iso_inv_fst _ _ _) x).mp hy
    · dsimp only
      rw [← Over.forget_map, ← PreservesPullback.iso_hom_fst, P.cancel_left_of_respectsIso]
      exact P.pullback_fst _ _ (𝒰.map_prop j)

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

Goal state before:
pp: case e'_2
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
⊢ zeroLocus (Set.range 0) \ zeroLocus {f} = Set.univ \ zeroLocus {f}

Tactic:
congr 1

Goal state after:
case e'_2.e_a
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
⊢ zeroLocus (Set.range 0) = Set.univ
Module: Mathlib.AlgebraicGeometry.Cover.Over

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝⁶ : W.Over S
inst✝⁵ : X.Over S
inst✝⁴ : Cover.Over S 𝒰
inst✝³ : Hom.IsOver f S
Q : MorphismProperty Scheme
inst✝² : Q.HasOfPostcompProperty Q
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
⊢ { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOverProp (𝒰.f x) S) (Hom.asOverProp f S)).left,
        f := fun x ↦ (pullback.snd (Hom.asOverProp (𝒰.f x) S) (Hom.asOverProp f S)).left }.presieve₀ ∈
    (precoverage P).coverings W

Tactic:
by
    rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, fun j ↦ ?_⟩
    · obtain ⟨i, hy⟩ := Cover.exists_eq (𝒰.pullback₂ f) x
      use i
      exact (mem_range_iff_of_surjective ((𝒰.pullback₂ f).f i) _
        ((PreservesPullback.iso (MorphismProperty.Over.forget Q _ _ ⋙ Over.forget S)
          ((𝒰.f _).asOverProp S) (f.asOverProp S)).inv)
        (PreservesPullback.iso_inv_snd _ _ _) x).mp hy
    · simp only [← CategoryTheory.Over.forget_map]
      rw [MorphismProperty.Comma.toCommaMorphism_eq_hom,
        ← MorphismProperty.Comma.forget_map, ← Functor.comp_map]
      rw [← PreservesPullback.iso_hom_snd, P.cancel_left_of_respectsIso]
      exact P.pullback_snd _ _ (𝒰.map_prop j)

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 𝒰
inst✝ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone i).pt ≅ ((MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)).mapCocone (d.cocone j)).pt :=
  (d.isColimit i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)) (d.isColimit j))
    (D.isoWhiskerLeft (MorphismProperty.Over.pullbackComp (Cover.trans 𝒰 hij) (𝒰.f j) (𝒰.f i) ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))).symm)
a : J
⊢ ((pullback.map (D.obj a).hom (𝒰.f i) (D.obj a).hom (Cover.trans 𝒰 hij ≫ 𝒰.f j) (𝟙 (D.obj a).left) (𝟙 (𝒰.X i)) (𝟙 S) ⋯
            ⋯ ≫
          (pullbackLeftPullbackSndIso (D.obj a).hom (𝒰.f j) (Cover.trans 𝒰 hij)).inv) ≫
        pullback.fst (pullback.snd (D.obj a).hom (𝒰.f j)) (Cover.trans 𝒰 hij)) ≫
      (Comma.Hom.hom ((d.cocone j).ι.app a)).left =
    pullback.map (D.obj a).hom (𝒰.f i) (D.obj a).hom (𝒰.f j) (𝟙 (D.obj a).left) (Cover.trans 𝒰 hij) (𝟙 S) ⋯ ⋯ ≫
      (Comma.Hom.hom ((d.cocone j).ι.app a)).left

Tactic:
congr 1

Goal state after:
case e_a
P : MorphismProperty Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝² : Category.{v_2, u_2} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone i).pt ≅ ((MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)).mapCocone (d.cocone j)).pt :=
  (d.isColimit i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)) (d.isColimit j))
    (D.isoWhiskerLeft (MorphismProperty.Over.pullbackComp (Cover.trans 𝒰 hij) (𝒰.f j) (𝒰.f i) ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))).symm)
a : J
⊢ (pullback.map (D.obj a).hom (𝒰.f i) (D.obj a).hom (Cover.trans 𝒰 hij ≫ 𝒰.f j) (𝟙 (D.obj a).left) (𝟙 (𝒰.X i)) (𝟙 S) ⋯
          ⋯ ≫
        (pullbackLeftPullbackSndIso (D.obj a).hom (𝒰.f j) (Cover.trans 𝒰 hij)).inv) ≫
      pullback.fst (pullback.snd (D.obj a).hom (𝒰.f j)) (Cover.trans 𝒰 hij) =
    pullback.map (D.obj a).hom (𝒰.f i) (D.obj a).hom (𝒰.f j) (𝟙 (D.obj a).left) (Cover.trans 𝒰 hij) (𝟙 S) ⋯ ⋯
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_1.refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.129} 𝒰.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.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
i j : (𝒱 a).I₀
hij : i ⟶ j
⊢ (Cover.trans (𝒱 a) hij ≫ ((d.cocone j).ι.app a).left) ≫ colimit.ι d.relativeGluingData.functor j =
    (((d.cocone i).ι.app a).left ≫ d.relativeGluingData.functor.map hij) ≫ colimit.ι d.relativeGluingData.functor j

Tactic:
congr 1

Goal state after:
case refine_1.refine_2.e_a
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.129} 𝒰.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.129} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a : J
i j : (𝒱 a).I₀
hij : i ⟶ j
⊢ Cover.trans (𝒱 a) hij ≫ ((d.cocone j).ι.app a).left =
    ((d.cocone i).ι.app a).left ≫ d.relativeGluingData.functor.map hij
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
⊢ ∃ u, π.base ≫ u = f.base

Tactic:
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

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✝¹ : IsCofiltered I
inst✝ : ∀ (i : I), IsAffine (D.obj i)
i : I
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
⊢ ∃ j f, (ConcreteCategory.hom (Scheme.Hom.appTop (D.map f))) s = 0

Tactic:
by
  have : ∀ i, IsAffine (D.op.obj i).unop := by dsimp; infer_instance
  obtain ⟨j, f, hj⟩ := (Types.FilteredColimit.isColimit_eq_iff'
    (isColimitOfPreserves (Scheme.Γ ⋙ forget _) hc.op) s (0 : Γ(D.obj i, ⊤))).mp
    (by dsimp at hs ⊢; simpa)
  dsimp at hj
  exact ⟨j.unop, f.unop, by simpa using hj⟩

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₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁) =
    (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / evalEval x₁ y₁ W.polynomialY

Tactic:
congr 1

Goal state after:
case e_a
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ y₁ - W.negY x₁ y₁ = evalEval x₁ y₁ W.polynomialY
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
n✝ n : ℕ
IH :
  ∀ {M : Submodule ℤ R},
    1 ∈ M →
      ∀ (k : ℕ) (d : Multiset (Fin n)) (S : ConstructibleSetData (MvPolynomial (Fin n) R)),
        (∀ C ∈ S, C.n ≤ k) →
          (∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) d)) →
            ∃ T,
              comap MvPolynomial.C '' S.toSet = T.toSet ∧
                ∀ C ∈ T,
                  C.n ≤ numBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n ∧
                    ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n
M : Submodule ℤ R
hM : 1 ∈ M
k✝ : ℕ
d : Multiset (Fin (n + 1))
S : ConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hSn : ∀ C ∈ S, C.n ≤ k✝
hS :
  ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin (n + 1)) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin (n + 1)) d)
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] (MvPolynomial (Fin n) R)[X] := MvPolynomial.finSuccEquiv R n
S' : ConstructibleSetData (MvPolynomial (Fin n) R)[X] := ConstructibleSetData.map e.toRingEquiv.toRingHom S
hS' : S'.degBound ≤ k✝ * (1 + Multiset.count 0 d)
B : Multiset (Fin n) := Finsupp.toMultiset (Finsupp.comapDomain Fin.succ (Multiset.toFinsupp d) ⋯)
x : BasicConstructibleSetData (MvPolynomial (Fin n) R)[X]
hxS : x ∈ S'
j : Fin x.n
k : ℕ
⊢ (x.g j).coeff k ∈ coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) B)

Tactic:
simp only [ConstructibleSetData.map,
          RingEquiv.toRingHom_eq_coe, AlgEquiv.toRingEquiv_toRingHom, Finset.mem_image,
          BasicConstructibleSetData.map, RingHom.coe_coe, S', e] at hxS
        obtain ⟨C, hxS, rfl⟩ := hxS
        simp only [comp_apply, Submodule.mem_inf, mem_coeffsIn, Submodule.restrictScalars_mem,
          mem_degreesLE]
        constructor
        · intro d
          simp only [finSuccEquiv_coeff_coeff]
          exact (hS _ hxS _).1 _
        · simp only [B]
          replace hS := (hS _ hxS j).2
          simp only [Submodule.coe_restrictScalars, SetLike.mem_coe, mem_degreesLE,
            Multiset.le_iff_count, Finsupp.count_toMultiset, Finsupp.comapDomain_apply,
            Multiset.toFinsupp_apply, ← degreeOf_def] at hS ⊢
          intro a
          exact (degreeOf_coeff_finSuccEquiv (C.g j) a k).trans (hS _)

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✝³ : IsCofiltered I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this : CompactSpace ↥c.pt
i : ↥c.pt → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ U x
t : (x : ↥c.pt) → ↑Γ(D.obj (i x), U x)
ht : ∀ (x : ↥c.pt), (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x))) (t x) = (s |_ c.π.app (i x) ⁻¹ᵁ U x) ⋯
j : ↥c.pt → ↥c.pt → I
fjx : (x y : ↥c.pt) → j x y ⟶ i x
fjy : (x y : ↥c.pt) → j x y ⟶ i y
hj :
  ∀ (x y : ↥c.pt),
    ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fjx x y)) (U x))) (t x) |_
          (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))
        ⋯ =
      ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fjy x y)) (U y))) (t y) |_
          (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))
        ⋯
σ : Finset ↥c.pt
hσ : ⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ U 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)) ⁻¹ᵁ U (σi x)).carrier
⊢ ∃ i t, s = (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) t

Tactic:
let S : Finset _ := σ.image i ∪ Finset.image₂ j σ σ

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)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this : CompactSpace ↥c.pt
i : ↥c.pt → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ U x
t : (x : ↥c.pt) → ↑Γ(D.obj (i x), U x)
ht : ∀ (x : ↥c.pt), (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x))) (t x) = (s |_ c.π.app (i x) ⁻¹ᵁ U x) ⋯
j : ↥c.pt → ↥c.pt → I
fjx : (x y : ↥c.pt) → j x y ⟶ i x
fjy : (x y : ↥c.pt) → j x y ⟶ i y
hj :
  ∀ (x y : ↥c.pt),
    ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fjx x y)) (U x))) (t x) |_
          (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))
        ⋯ =
      ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fjy x y)) (U y))) (t y) |_
          (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))
        ⋯
σ : Finset ↥c.pt
hσ : ⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ U 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)) ⁻¹ᵁ U (σi x)).carrier
S : Finset I := Finset.image i σ ∪ Finset.image₂ j σ σ
⊢ ∃ i t, s = (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) t
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
hpq : p • 1 + q • (mk W') Y = 0
⊢ p = 0 ∧ q = 0

Tactic:
by
  have h := Fintype.linearIndependent_iff.mp (CoordinateRing.basis W').linearIndependent ![p, q]
  rw [Fin.sum_univ_succ, basis_zero, Fin.sum_univ_one, Fin.succ_zero_eq_one, basis_one] at h
  exact ⟨h hpq 0, h hpq 1⟩

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
⊢ 0 + 0 = 0

Tactic:
add_zero

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x : R
⊢ (C (X - C x)).natDegree < W'.polynomial.natDegree

Tactic:
by rw [natDegree_polynomial, natDegree_C]; norm_num1

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

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

Tactic:
← map_negPolynomial,

Goal state after:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Affine R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W'⁄B).negPolynomial = ((W'⁄A).map ↑f).negPolynomial
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := (y₁ - W.negY x₁ y₁) ^ 2
hxy : (y₁ - W.negY x₁ y₁) ^ 2 ≠ 0
⊢ 1 + 0 = 1

Tactic:
add_zero

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := (y₁ - W.negY x₁ y₁) ^ 2
hxy : (y₁ - W.negY x₁ y₁) ^ 2 ≠ 0
⊢ 1 = 1
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
b c d : R
n : ℕ
hn : n = 0
⊢ preNormEDS b c d ↑n = preNormEDS' b c d n

pp: case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
n : ℕ
hn : ¬n = 0
⊢ preNormEDS b c d ↑n = preNormEDS' b c d n

Tactic:
· simp [hn, preNormEDS]

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
n : ℕ
hn : ¬n = 0
⊢ preNormEDS b c d ↑n = preNormEDS' b c d n