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

Goal state before:
pp: P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
inst✝ : P.IsClosedUnderIsomorphisms
⊢ geometrically P f ↔ ∀ (K : Type u) [inst : Field K] (y : Spec (of K) ⟶ Y), P (pullback f y)

Tactic:
by
  refine ⟨fun h K _ _ ↦ pullback_of_geometrically h _ _, fun H K _ _ Y fst snd h ↦ ?_⟩
  exact P.prop_of_iso h.isoPullback.symm (H _ _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
y : ↥Y
⊢ Set.range ⇑(fiberι f y) = ⇑f ⁻¹' {y}

Tactic:
by
  simp [fiber, fiberι, Scheme.Pullback.range_fst, Scheme.range_fromSpecResidueField]

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

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
⊢ DenseRange ⇑f

Tactic:
DenseRange,

Goal state after:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
⊢ Dense (Set.range ⇑f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f

Tactic:
by
  wlog hY : IsAffine Y
  · rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsFinite) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := @IsIntegralHom) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := @LocallyOfFiniteType) Y.affineCover]
    simp_rw [this, forall_and]
  rw [HasAffineProperty.iff_of_isAffine (P := @IsFinite),
    HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom),
    RingHom.finite_iff_isIntegral_and_finiteType, ← and_assoc]
  refine and_congr_right fun ⟨_, _⟩ ↦
    (HasRingHomProperty.iff_of_isAffine (P := @LocallyOfFiniteType)).symm

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ Flat f ∧ Surjective f ↔ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).FaithfullyFlat

Tactic:
by
  rw [RingHom.FaithfullyFlat.iff_flat_and_comap_surjective,
    MorphismProperty.arrow_mk_iso_iff @Surjective (arrowIsoSpecΓOfIsAffine f),
    MorphismProperty.arrow_mk_iso_iff @Flat (arrowIsoSpecΓOfIsAffine f),
    ← HasRingHomProperty.Spec_iff (P := @Flat), surjective_iff]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
⊢ ∃ U, x ∈ U ∧ U.ι ≫ f = U.ι ≫ g

Tactic:
by
  obtain ⟨_, ⟨V : Y.Opens, hV, rfl⟩, hxV, -⟩ :=
    Y.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ (f x)) isOpen_univ
  have hxV' : g x ∈ V := e ▸ hxV
  obtain ⟨U, hxU, _, hUV, HU⟩ := X.exists_le_and_germ_injective x (f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V) ⟨hxV, hxV'⟩
  refine ⟨U, hxU, ?_⟩
  rw [← Scheme.Hom.resLE_comp_ι _ (hUV.trans inf_le_left),
    ← Scheme.Hom.resLE_comp_ι _ (hUV.trans inf_le_right)]
  congr 1
  have : IsAffine V := hV
  suffices ∀ (U₀ V₀) (eU : U = U₀) (eV : V = V₀),
      f.appLE V₀ U₀ (eU ▸ eV ▸ hUV.trans inf_le_left) =
        g.appLE V₀ U₀ (eU ▸ eV ▸ hUV.trans inf_le_right) by
    rw [← cancel_mono V.toScheme.isoSpec.hom]
    simp only [Scheme.isoSpec, asIso_hom, Scheme.toSpecΓ_naturality,
      Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE]
    congr 2
    apply this <;> simp
  rintro U V rfl rfl
  have := ConcreteCategory.mono_of_injective _ HU
  rw [← cancel_mono (X.presheaf.germ U x hxU)]
  simp only [Scheme.Hom.appLE, Category.assoc, X.presheaf.germ_res', ← Scheme.Hom.germ_stalkMap, H]
  simp only [TopCat.Presheaf.germ_stalkSpecializes_assoc, Scheme.Hom.germ_stalkMap]

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

Goal state before:
pp: X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f₁ : X₁ ⤏ X₂
inst✝¹ : f₁.IsDominant
f₂ : X₂ ⤏ X₃
inst✝ : f₂.IsDominant
f₃ : X₃ ⤏ Y
⊢ f₂.representative.equiv f₂.representative.toRationalMap.representative

Tactic:
rw [toRationalMap_representative]

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Category.{v_1, ?u.54} 𝒰.I₀
inst✝ : Cover.LocallyDirected 𝒰
s : Cocone (Cover.functorOfLocallyDirected 𝒰)
m : (Cover.coconeOfLocallyDirected 𝒰).pt ⟶ s.pt
hm : ∀ (j : 𝒰.I₀), (Cover.coconeOfLocallyDirected 𝒰).ι.app j ≫ m = s.ι.app j
j : 𝒰.I₀
⊢ 𝒰.f j ≫ m = 𝒰.f j ≫ 𝒰.glueMorphismsOfLocallyDirected s.ι.app ⋯

Tactic:
by simpa using hm j

Goal state after:
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: case refine_4
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) (m : s.pt ⟶ d.functor.obj i),
    m ≫ d.natTrans.app i = s.fst →
      m ≫ colimit.ι d.functor i = s.snd → m = IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯

Tactic:
· intro s m h1 h2
    simpa [← cancel_mono (colimit.ι d.functor i)]

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 { val := 0 }.val) \ zeroLocus {f} = ↑(basicOpen f)

Tactic:
simp only [basicOpen_eq_zeroLocus_compl, Set.compl_eq_univ_sdiff]

Goal state after:
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}
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₃.inr.refine_1
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
⊢ comap Polynomial.C '' (zeroLocus ↑(Ideal.span (Set.range c.val)) \ zeroLocus {f}) =
    comap Polynomial.C ''
      (zeroLocus ↑(Ideal.span (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val)) \ zeroLocus {f})

Tactic:
idealSpan_range_update_divByMonic hne

Goal state after:
case hP₃.inr.refine_1
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
⊢ comap Polynomial.C '' (zeroLocus ↑(Ideal.span (Set.range c.val)) \ zeroLocus {f}) =
    comap Polynomial.C '' (zeroLocus ↑(Ideal.span (Set.range c.val)) \ zeroLocus {f})
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
⊢ IsPullback (d.transitionMap hij).left (d.cocone i).pt.hom (d.cocone j).pt.hom (Cover.trans 𝒰 hij)

Tactic:
let iso1 : (d.cocone i).pt ≅ _ :=
    (d.isColimit i).coconePointsIsoOfNatIso
      (isColimitOfPreserves (Over.pullback P ⊤ (𝒰.trans hij)) (d.isColimit j)) <|
      D.isoWhiskerLeft (Over.pullbackComp _ _ _) ≪≫ (Functor.associator _ _ _).symm
  have heq : (Over.map _ (d.prop_trans hij)).map iso1.hom ≫
        (Over.mapPullbackAdj _ _ _ (d.prop_trans hij) trivial).counit.app _ =
      d.transitionMap hij := by
    apply (isColimitOfPreserves (Over.map _ (d.prop_trans hij)) (d.isColimit i)).hom_ext
    intro a
    dsimp only [Functor.comp_obj, Functor.id_obj, Functor.mapCocone_pt, Functor.const_obj_obj,
      Functor.mapCocone_ι_app, Iso.trans_hom, Functor.isoWhiskerLeft_hom, Iso.symm_hom]
    rw [IsColimit.coconePointsIsoOfNatIso_hom, ← Functor.map_comp_assoc, IsColimit.ι_map,
      Functor.mapCocone_ι_app, Functor.map_comp, Category.assoc,
      Adjunction.counit_naturality, cocone_ι_transitionMap]
    ext
    dsimp
    rw [Category.comp_id, ← Category.assoc]
    congr 1
    apply pullback.hom_ext <;> simp
  let iso2 : (d.cocone i).pt.left ≅ pullback (d.cocone j).pt.hom (𝒰.trans hij) :=
    (MorphismProperty.Over.forget _ _ _ ⋙ Over.forget _).mapIso iso1
  refine .of_iso (IsPullback.of_hasPullback _ _) iso2.symm (.refl _) (.refl _) (.refl _) ?_ ?_
      (by simp) (by simp)
  · simpa [← cancel_epi iso2.hom] using! congr($(heq).left)
  · exact (Over.w iso1.inv).symm

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
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' ↑U' ⊆ ↑U
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq✝ : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
x : ↥T
hx : x ∈ ↑U'
i : 𝒰.I₀
hi : i ∈ s
y : ↥(𝒰.X i)
hy : y ∈ ↑(V i ⋯)
heq : (fun a ↦ (𝒰.f i) a) y = f x
z : ↥(pullback f (𝒰.f i))
hzl : (pullback.fst f (𝒰.f i)) z = x
hzr : (pullback.snd f (𝒰.f i)) z = y
⊢ z ∈ ↑(pullback.snd f (𝒰.f i) ⁻¹ᵁ V i ⋯)

Tactic:
by simpa [hzr]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y - (Y - W'.polynomialY) = W'.polynomialY

Tactic:
sub_sub_cancel

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ W'.polynomialY = W'.polynomialY
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

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

Tactic:
rw [hx]

Goal state after:
case a
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
h₂ : y₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ = x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆
hx : x₁ = x₂
⊢ (y₁ - y₂) * (y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) +
        (x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆ + (y₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂)) -
      (0 + (y₁ ^ 2 + W.a₁ * x₂ * y₁ + W.a₃ * y₁ + (x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆))) =
    0
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_3
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
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : (c.π.app i) x ∈ ↑U
this : ∀ (j : Over i), IsAffine ((opensDiagram D i U).obj j)
j : Over i
t : ↑Γ((opensDiagram D i U).obj j, ⊤)
hj :
  (ConcreteCategory.hom (Scheme.Hom.appTop ((opensCone D c i U).π.app j))) t =
    (s |_ ⋯.functor.obj (Opposite.unop (Opposite.op ⊤))) ⋯
H : c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ (c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤
e_1✝ :
  ↑Γ(((Functor.const I).obj c.pt).obj j.left, c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) =
    ↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤)))
⊢ (ConcreteCategory.hom (c.pt.presheaf.map (homOfLE ⋯).op)) s =
    (ConcreteCategory.hom (c.pt.presheaf.map (homOfLE ⋯).op ≫ c.pt.presheaf.map (homOfLE H).op)) s

Tactic:
rw [← Functor.map_comp]

Goal state after:
case e'_3
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
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : (c.π.app i) x ∈ ↑U
this : ∀ (j : Over i), IsAffine ((opensDiagram D i U).obj j)
j : Over i
t : ↑Γ((opensDiagram D i U).obj j, ⊤)
hj :
  (ConcreteCategory.hom (Scheme.Hom.appTop ((opensCone D c i U).π.app j))) t =
    (s |_ ⋯.functor.obj (Opposite.unop (Opposite.op ⊤))) ⋯
H : c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ (c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤
e_1✝ :
  ↑Γ(((Functor.const I).obj c.pt).obj j.left, c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) =
    ↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤)))
⊢ (ConcreteCategory.hom (c.pt.presheaf.map (homOfLE ⋯).op)) s =
    (ConcreteCategory.hom (c.pt.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE H).op))) s
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))
⊢ ∃ T,
    comap ↑f '' S.toSet = T.toSet ∧
      ∀ C ∈ T, C.n ≤ numBound k m n d ∧ ∀ (i : Fin C.n) (j : Fin n), degreeOf j (C.g i) ≤ degBound k m n d

Tactic:
have hσ : g.comp σ = .id _ := by ext : 2 <;> simp [g, σ]

Goal state after:
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)
⊢ ∃ T,
    comap ↑f '' S.toSet = T.toSet ∧
      ∀ C ∈ T, C.n ≤ numBound k m n d ∧ ∀ (i : Fin C.n) (j : Fin n), degreeOf j (C.g i) ≤ degBound k m n d
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atom W a (-b) * atom W c d - atom W a c * atom W (-b) d + atom W a d * atom W (-b) c =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c

Tactic:
atom_neg_left odd,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atom W a (-b) * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atom W a b * atom W (-c) d - atom W a (-c) * atom W b d + atom W a d * atom W b (-c) =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c

Tactic:
atom_neg_left odd,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atom W a b * atom W c d - atom W a (-c) * atom W b d + atom W a d * atom W b (-c) =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c
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), QuasiSeparatedSpace ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU' : IsCompact ↑U
hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U)
this✝¹ : ∀ (j : Over i), CompactSpace ↥((opensDiagram D i U).obj j)
this✝ : ∀ (j : Over i), QuasiSeparatedSpace ↥((opensDiagram D i U).obj j)
this : IsAffine (opensCone D c i U).pt
⊢ ∃ i_1 V, IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U

Tactic:
obtain ⟨j, hj⟩ := Scheme.exists_isAffine_of_isLimit _ _ (isLimitOpensCone D c hc i U)

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), QuasiSeparatedSpace ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU' : IsCompact ↑U
hU : IsAffineOpen (c.π.app i ⁻¹ᵁ U)
this✝¹ : ∀ (j : Over i), CompactSpace ↥((opensDiagram D i U).obj j)
this✝ : ∀ (j : Over i), QuasiSeparatedSpace ↥((opensDiagram D i U).obj j)
this : IsAffine (opensCone D c i U).pt
j : Over i
hj : IsAffine ((opensDiagram D i U).obj j)
⊢ ∃ i_1 V, IsAffineOpen V ∧ c.π.app i_1 ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ U
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 3), f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ f (preNormEDS' b c d (m✝ + 2)) ^ 2 * f (preNormEDS' b c d (m✝ + 3)) * f (preNormEDS' b c d (m✝ + 5)) -
      f (preNormEDS' b c d (m✝ + 1)) * f (preNormEDS' b c d (m✝ + 3)) * f (preNormEDS' b c d (m✝ + 4)) ^ 2 =
    preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 4) ^ 2

Tactic:
rw [ih _ <| by linarith only]

Goal state after:
case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 3), f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * f (preNormEDS' b c d (m✝ + 3)) * f (preNormEDS' b c d (m✝ + 5)) -
      f (preNormEDS' b c d (m✝ + 1)) * f (preNormEDS' b c d (m✝ + 3)) * f (preNormEDS' b c d (m✝ + 4)) ^ 2 =
    preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 4) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 3), f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * f (preNormEDS' b c d (m✝ + 3)) * f (preNormEDS' b c d (m✝ + 5)) -
      f (preNormEDS' b c d (m✝ + 1)) * f (preNormEDS' b c d (m✝ + 3)) * f (preNormEDS' b c d (m✝ + 4)) ^ 2 =
    preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 4) ^ 2

Tactic:
rw [ih _ <| by linarith only]

Goal state after:
case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 3), f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) * f (preNormEDS' b c d (m✝ + 5)) -
      f (preNormEDS' b c d (m✝ + 1)) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) * f (preNormEDS' b c d (m✝ + 4)) ^ 2 =
    preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 4) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 3), f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) * f (preNormEDS' b c d (m✝ + 5)) -
      f (preNormEDS' b c d (m✝ + 1)) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) * f (preNormEDS' b c d (m✝ + 4)) ^ 2 =
    preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 4) ^ 2

Tactic:
rw [ih _ <| by linarith only]

Goal state after:
case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 3), f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      f (preNormEDS' b c d (m✝ + 1)) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) * f (preNormEDS' b c d (m✝ + 4)) ^ 2 =
    preNormEDS' (f b) (f c) (f d) (m✝ + 2) ^ 2 * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 5) -
      preNormEDS' (f b) (f c) (f d) (m✝ + 1) * preNormEDS' (f b) (f c) (f d) (m✝ + 3) *
        preNormEDS' (f b) (f c) (f d) (m✝ + 4) ^ 2