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

Goal state before:
pp: X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this✝¹ : Algebra ↑R ↑A := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset ↑A
hs : Algebra.adjoin ↑R ↑s = ⊤
W : ↑A → TopologicalSpace.Opens ↥X
hxW : ∀ (t : ↑A), x ∈ W t
f : (t : ↑A) → ToType (X.presheaf.obj (Opposite.op (W t)))
hf : ∀ (t : ↑A), (ConcreteCategory.hom (X.presheaf.germ (W t) x ⋯)) (f t) = (ConcreteCategory.hom φ) t
H : x ∈ s.inf W ⊓ U
this✝ : Algebra ↑R ↑Γ(X, U) := (CommRingCat.Hom.hom φRX).toAlgebra
this : Algebra ↑R ↑(X.presheaf.stalk x) := (CommRingCat.Hom.hom (φRX ≫ X.presheaf.germ U x hxU)).toAlgebra
⊢ (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H)).range

Tactic:
let := (φRX ≫ X.presheaf.map (homOfLE (inf_le_right (a := s.inf W))).op).hom.toAlgebra

Goal state after:
X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this✝² : Algebra ↑R ↑A := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset ↑A
hs : Algebra.adjoin ↑R ↑s = ⊤
W : ↑A → TopologicalSpace.Opens ↥X
hxW : ∀ (t : ↑A), x ∈ W t
f : (t : ↑A) → ToType (X.presheaf.obj (Opposite.op (W t)))
hf : ∀ (t : ↑A), (ConcreteCategory.hom (X.presheaf.germ (W t) x ⋯)) (f t) = (ConcreteCategory.hom φ) t
H : x ∈ s.inf W ⊓ U
this✝¹ : Algebra ↑R ↑Γ(X, U) := (CommRingCat.Hom.hom φRX).toAlgebra
this✝ : Algebra ↑R ↑(X.presheaf.stalk x) := (CommRingCat.Hom.hom (φRX ≫ X.presheaf.germ U x hxU)).toAlgebra
this : Algebra ↑R ↑(X.presheaf.obj (Opposite.op (s.inf W ⊓ U))) :=
  (CommRingCat.Hom.hom (φRX ≫ X.presheaf.map (homOfLE ⋯).op)).toAlgebra
⊢ (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H)).range
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
⊢ Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU

Tactic:
Scheme.Hom.appLE,

Goal state after:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
⊢ (Scheme.Hom.app sY U ≫ Y.presheaf.map (homOfLE iVU).op) ≫ Y.presheaf.germ V y hyV ≫ φ =
    Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: R : CommRingCat
inst✝ : IsDomain ↑R
⊢ genericPoint ↥(Spec R) = ⊥

Tactic:
apply (genericPoint_spec (Spec R)).eq

Goal state after:
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ IsGenericPoint ⊥ Set.univ
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z : Scheme
f : X.PartialMap Y
g : Y ⟶ Z
x : ↥X
hx : x ∈ (f.compHom g).domain
⊢ (f.compHom g).fromSpecStalkOfMem hx = f.fromSpecStalkOfMem hx ≫ g

Tactic:
simp [fromSpecStalkOfMem]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ (Hom.toPartialMap f).fromSpecStalkOfMem trivial = X.fromSpecStalk x ≫ f

Tactic:
simp [fromSpecStalkOfMem]

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

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
sZ : Z ⟶ S
f : X.PartialIso Y
g : Y.PartialIso Z
e : f.target = g.source
hf : IsOver sX sY f
hg : IsOver sY sZ g
⊢ IsOver sX sZ (f.trans' g e)

Tactic:
simp [IsOver, ← hf, hg]

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

Goal state before:
pp: X Y : Scheme
f g : X.PartialMap Y
h : f.equiv g
⊢ IsDominant f.hom ↔ IsDominant g.hom

Tactic:
obtain ⟨W, hW, hWl, hWr, h⟩ := h
  have e₁ := isDominant_hom_iff_isDominant_restrict_hom f W hW hWl
  have e₂ := isDominant_hom_iff_isDominant_restrict_hom g W hW hWr
  dsimp only [restrict_domain, restrict_hom] at ⊢ e₁ e₂ h
  rw [e₁, h, ← e₂]

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

Goal state before:
pp: case H
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ ((PartialMap.id X).comp f).hom = (X.isoOfEq ⋯).hom ≫ f.hom

Tactic:
simp_rw [comp_hom, Hom.toPartialMap_hom, Hom.toPartialMap_domain, morphismRestrict_comp,
      morphismRestrict_id, ← X.topIso_hom, Hom.comp_preimage, Hom.id_preimage,
      Category.comp_id, ← X.topIso.hom.isoImage_preimage_hom_homOfLE, Category.assoc,
      Iso.inv_hom_id_assoc]
    rfl

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
⊢ { I₀ := ↑X.affineOpens, X := fun U ↦ ↑↑U, f := fun U ↦ (↑U).ι }.presieve₀ ∈ (precoverage IsOpenImmersion).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, inferInstance⟩
    use ⟨(isBasis_iff_nbhd.mp X.isBasis_affineOpens (mem_top x)).choose,
      (isBasis_iff_nbhd.mp X.isBasis_affineOpens (mem_top x)).choose_spec.1⟩
    simpa using (isBasis_iff_nbhd.mp X.isBasis_affineOpens (mem_top x)).choose_spec.2.1

Goal state after:
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: P : MorphismProperty Scheme
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝² : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝¹ : Category.{v_2, u_2} 𝒰.I₀
inst✝ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
i j k : 𝒰.I₀
hij : i ⟶ j
hjk : j ⟶ k
⊢ d.transitionMap (hij ≫ hjk) =
    (MorphismProperty.Over.mapComp ⊤ ⋯ ⋯ (Cover.trans 𝒰 (hij ≫ hjk)) ⋯).hom.app (d.cocone i).pt ≫
      (MorphismProperty.Over.map ⊤ ⋯).map (d.transitionMap hij) ≫ d.transitionMap hjk

Tactic:
by
  apply (isColimitOfPreserves (Over.map ⊤ <| d.prop_trans _) (d.isColimit i)).hom_ext
  intro
  ext
  simp [← Functor.map_comp_assoc, cocone_ι_transitionMap, pullback.map_comp_assoc]

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
κ : Type u_4
inst✝ : Finite κ
s : κ → Set S
hs : ⋃ i, s i = U
H : ∀ (i : κ), IsCompactOpenCovered f (s i)
⊢ IsCompactOpenCovered f U

Tactic:
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.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hab.refine_2
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
k : Fin n
⊢ coeff(c'.val k) ⊆ ↑(coeffSubmodule R₀ c)

Tactic:
simp only [update_apply, hi', modByMonic_one, c']

Goal state after:
case hab.refine_2
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
k : Fin n
⊢ coeff(if k = j then 0 else c.val k) ⊆ ↑(coeffSubmodule R₀ c)
Module: Mathlib.AlgebraicGeometry.ColimitsOver

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

Tactic:
apply pullback.hom_ext <;> simp

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

Goal state before:
pp: S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
⊢ QuasiCompactCover (PreZeroHypercover.pullback₁ f 𝒰)

Tactic:
refine ⟨fun {U'} hU' ↦ ?_⟩
  wlog h : ∃ (U : S.Opens), IsAffineOpen U ∧ f '' U' ⊆ U generalizing U'
  · refine .of_isCompact_of_forall_exists_isCompactOpenCovered hU'.isCompact fun x hxU ↦ ?_
    obtain ⟨W, hW, hx, _⟩ := isBasis_iff_nbhd.mp S.isBasis_affineOpens (mem_top (f x))
    obtain ⟨W', hW', hx', hle⟩ := isBasis_iff_nbhd.mp T.isBasis_affineOpens
      (show x ∈ f ⁻¹ᵁ W ⊓ U' from ⟨hx, hxU⟩)
    exact ⟨W', le_trans hle inf_le_right, by simpa [hx], W'.2,
      this hW' ⟨W, hW, by simpa using! le_trans hle inf_le_left⟩⟩
  obtain ⟨U, hU, hsub⟩ := h
  obtain ⟨s, hf, V, hc, (heq : _ = (U : Set S))⟩ := hU.isCompactOpenCovered 𝒰
  refine ⟨s, hf, fun i hi ↦ pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ (V i hi),
      fun i hi ↦ ?_, ?_⟩
  · 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 _ _))
  · refine subset_antisymm (by simp) (fun x hx ↦ ?_)
    have : f x ∈ (U : Set S) := hsub ⟨x, hx, rfl⟩
    simp_rw [← heq, Set.mem_iUnion] at this
    obtain ⟨i, hi, y, hy, heq⟩ := this
    simp_rw [Set.mem_iUnion]
    obtain ⟨z, hzl, hzr⟩ := Scheme.Pullback.exists_preimage_pullback x y heq.symm
    exact ⟨i, hi, z, ⟨by simpa [hzl], by simpa [hzr]⟩, hzl⟩

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

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : UnivLE.{v, u}
𝒰 : Cover (precoverage P) S
s : ↥S
⊢ ∃ i, s ∈ Set.range ⇑({ I₀ := PUnit.{v + 1}, X := fun x ↦ ∐ 𝒰.X, f := fun x ↦ Sigma.desc 𝒰.f }.f i)

Tactic:
obtain ⟨i, y, rfl⟩ := 𝒰.exists_eq s

Goal state after:
P : MorphismProperty Scheme
S : Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : UnivLE.{v, u}
𝒰 : Cover (precoverage P) S
i : 𝒰.I₀
y : ↥(𝒰.X i)
⊢ ∃ i_1, (𝒰.f i) y ∈ Set.range ⇑({ I₀ := PUnit.{v + 1}, X := fun x ↦ ∐ 𝒰.X, f := fun x ↦ Sigma.desc 𝒰.f }.f i_1)
Module: Mathlib.AlgebraicGeometry.Cover.Sigma

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : UnivLE.{v, u}
inst✝ : P.IsMultiplicative
𝒰✝ 𝒱 𝒰 : Cover (precoverage P) S
⊢ (Hom.sigma (𝟙 𝒰)).h₀ = (𝟙 𝒰.sigma).h₀

Tactic:
ext j : 1

Goal state after:
P : MorphismProperty Scheme
S : Scheme
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : UnivLE.{v, u}
inst✝ : P.IsMultiplicative
𝒰✝ 𝒱 𝒰 : Cover (precoverage P) S
j : 𝒰.sigma.I₀
⊢ (Hom.sigma (𝟙 𝒰)).h₀ j = (𝟙 𝒰.sigma).h₀ j
Module: Mathlib.AlgebraicGeometry.Cover.Sigma

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : UnivLE.{v, u}
inst✝ : P.IsMultiplicative
𝒰 𝒱 X✝ Y✝ Z✝ : Cover (precoverage P) S
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (Hom.sigma (f ≫ g)).h₀ = (Hom.sigma f ≫ Hom.sigma g).h₀

Tactic:
ext j : 1

Goal state after:
P : MorphismProperty Scheme
S : Scheme
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : UnivLE.{v, u}
inst✝ : P.IsMultiplicative
𝒰 𝒱 X✝ Y✝ Z✝ : Cover (precoverage P) S
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
j : X✝.sigma.I₀
⊢ (Hom.sigma (f ≫ g)).h₀ j = (Hom.sigma f ≫ Hom.sigma g).h₀ j
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

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

Tactic:
obtain ⟨b, hfac⟩ : ∃ (u : Y.carrier ⟶ S.carrier), π.base ≫ u = f.base := by
    apply IsRegularEpi.exists_of_isKernelPair _ (IsPullback.of_hasPullback _ _)
    have := congr(Scheme.forgetToTop.map $hf)
    rwa [Functor.map_comp, Functor.map_comp, ← pullbackComparison_comp_fst_assoc,
      ← pullbackComparison_comp_snd_assoc, cancel_epi] at this

Goal state after:
X Y S : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
f : X ⟶ S
hf : fst π π ≫ f = snd π π ≫ f
b : ↑Y.toPresheafedSpace ⟶ ↑S.toPresheafedSpace
hfac : π.base ≫ b = f.base
⊢ ∃ 𝒰, ∀ (i : 𝒰.I₀), ∃ u, fst π (𝒰.f i) ≫ f = snd π (𝒰.f i) ≫ u
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
hΔ : Δ W ≠ 0
⊢ Δ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)) ≠ 0

Tactic:
by
      rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]

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) ⋯
x y : ↥c.pt
j : I
fjx : j ⟶ i x
fjy : j ⟶ i y
⊢ (ConcreteCategory.hom
        (Scheme.Hom.appLE (c.π.app (i x)) (U x) (c.π.app j ⁻¹ᵁ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) ⋯))
      (t x) =
    (ConcreteCategory.hom
        (Scheme.Hom.appLE (c.π.app (i y)) (U y) (c.π.app j ⁻¹ᵁ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) ⋯))
      (t y)

Tactic:
Scheme.Hom.appLE,

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) ⋯
x y : ↥c.pt
j : I
fjx : j ⟶ i x
fjy : j ⟶ i y
⊢ (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x) ≫ c.pt.presheaf.map (homOfLE ⋯).op)) (t x) =
    (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i y)) (U y) ≫ c.pt.presheaf.map (homOfLE ⋯).op)) (t y)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst✝ : W.IsElliptic
⊢ (C • W).j = W.j

Tactic:
rw [j, coe_inv_variableChange_Δ', variableChange_c₄, j, mul_pow, ← pow_mul, ← mul_assoc,
    mul_right_comm (C.u.val ^ 12), ← mul_pow, C.u.mul_inv, one_pow, one_mul]

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:
by
  rw [← map_negPolynomial, map_baseChange]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ normEDS b c d 4 = d * b

Tactic:
by
  simp [normEDS, show ¬Odd (4 : ℤ) by decide]

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
x y : F
h : W.Nonsingular x y
⊢ ↑(XYIdeal W x (C y)) * (↑(XYIdeal W x (C (W.negY x y))) * (↑(XIdeal W x))⁻¹) = 1

Tactic:
by
    rw [← mul_assoc, ← coeIdeal_mul, mul_comm <| XYIdeal W .., XYIdeal_neg_mul h, XIdeal,
      FractionalIdeal.coe_ideal_span_singleton_mul_inv W.FunctionField <| XClass_ne_zero x]

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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ 2 • dp < (fun x1 x2 ↦ x1 + x2) (2 • dq) ↑3

Tactic:
by dsimp; linarith only [hpq]

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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ (fun x1 x2 ↦ x1 + x2) ((fun x1 x2 ↦ x1 + x2) dp dq) 1 < (fun x1 x2 ↦ x1 + x2) (2 • dq) ↑3

Tactic:
by dsimp; linarith only [hpq]

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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ (fun x1 x2 ↦ x1 + x2) ((fun x1 x2 ↦ x1 + x2) dp dq) 1 < 2 • dp

Tactic:
by dsimp; linarith only [hpq]

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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ (fun x1 x2 ↦ x1 + x2) (2 • dq) ↑3 < 2 • dp

Tactic:
by dsimp; linarith only [hpq]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (X * W.ΨSq ↑(n + 1) - W.preΨ ↑(n + 1 + 1) * W.preΨ ↑n * if Even (n + 1) then 1 else W.Ψ₂Sq) =
    (X * W.preΨ' (n + 1) ^ 2 * if Even n then 1 else W.Ψ₂Sq) -
      W.preΨ' (n + 2) * W.preΨ' n * if Even n then W.Ψ₂Sq else 1

Tactic:
ΨSq_ofNat,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (X * (W.preΨ' (n + 1) ^ 2 * if Even (n + 1) then W.Ψ₂Sq else 1) -
      W.preΨ ↑(n + 1 + 1) * W.preΨ ↑n * if Even (n + 1) then 1 else W.Ψ₂Sq) =
    (X * W.preΨ' (n + 1) ^ 2 * if Even n then 1 else W.Ψ₂Sq) -
      W.preΨ' (n + 2) * W.preΨ' n * if Even n then W.Ψ₂Sq else 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ C X * W.ψ (-n) ^ 2 - W.ψ (-n + 1) * W.ψ (-n - 1) = C X * W.ψ n ^ 2 - W.ψ (n + 1) * W.ψ (n - 1)

Tactic:
ψ_neg,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ C X * (-W.ψ n) ^ 2 - W.ψ (-n + 1) * W.ψ (-n - 1) = C X * W.ψ n ^ 2 - W.ψ (n + 1) * W.ψ (n - 1)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case zero
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
⊢ zero.xRep ≠ 0

Tactic:
simp [xRep]

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

Goal state before:
pp: case some
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝ y✝ h✝).xRep ≠ 0

Tactic:
simp [xRep]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ C X * W.ψ n ^ 2 - W.ψ (-(n - 1)) * W.ψ (-(n + 1)) = C X * W.ψ n ^ 2 - W.ψ (n + 1) * W.ψ (n - 1)

Tactic:
ψ_neg,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ C X * W.ψ n ^ 2 - -W.ψ (n - 1) * -W.ψ (n + 1) = C X * W.ψ n ^ 2 - W.ψ (n + 1) * W.ψ (n - 1)