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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
let φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := f.appTop
  let 𝒰 : X.OpenCover := X.affineCover.finiteSubcover
  let res (i : 𝒰.I₀) : Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := (𝒰.f i).appTop
  refine stalkMap_injective_of_isAffine _ _ (fun (g : Γ(Y, ⊤)) h ↦ ?_)
  rw [TopCat.Presheaf.Γgerm, Scheme.Hom.germ_stalkMap_apply] at h
  obtain ⟨U, w, (hx : x ∈ U), hg⟩ :=
    X.toRingedSpace.exists_res_eq_zero_of_germ_eq_zero ⊤ (φ g) ⟨x, trivial⟩ h
  obtain ⟨_, ⟨s, rfl⟩, hyv, bsle⟩ := Opens.isBasis_iff_nbhd.mp (isBasis_basicOpen Y)
    (show f x ∈ ⟨f '' U.carrier, hfopen U.carrier U.is_open'⟩ from ⟨x, by simpa⟩)
  let W (i : 𝒰.I₀) : TopologicalSpace.Opens (𝒰.X i) := (𝒰.X i).basicOpen ((res i) (φ s))
  have hwle (i : 𝒰.I₀) : W i ≤ (𝒰.f i) ⁻¹ᵁ U := by
    change (𝒰.X i).basicOpen ((𝒰.f i ≫ f).appTop s) ≤ _
    rw [← Scheme.preimage_basicOpen_top, Scheme.Hom.comp_base, Opens.map_comp_obj]
    refine Scheme.Hom.preimage_mono _
      (le_trans (f.preimage_mono bsle) (le_of_eq ?_))
    simp [Set.preimage_image_eq _ hfinj₁]
  have h0 (i : 𝒰.I₀) : (𝒰.f i).appLE _ (W i) (by simp) (φ g) = 0 := by
    rw [← Scheme.Hom.appLE_map _ ((Opens.map _).map w).le (homOfLE <| hwle i).op,
      ← Scheme.Hom.map_appLE _ le_rfl w.op]
    simp only [CommRingCat.comp_apply]
    rw [hg]
    simp only [map_zero]
  have h1 (i : 𝒰.I₀) : ∃ n, (res i) (φ (s ^ n * g)) = 0 := by
    obtain ⟨n, hn⟩ := exists_of_res_zero_of_qcqs_of_top (s := ((res i) (φ s))) (h0 i)
    exact ⟨n, by rwa [map_mul, map_mul, map_pow, map_pow]⟩
  have h2 : ∃ n, ∀ i, (res i) (φ (s ^ n * g)) = 0 := by
    choose fn hfn using h1
    refine ⟨Finset.sup Finset.univ fn, fun i ↦ ?_⟩
    rw [map_mul, map_pow, map_mul, map_pow]
    simp only [map_mul, map_pow, map_mul, map_pow] at hfn
    apply pow_mul_eq_zero_of_le (Finset.le_sup (Finset.mem_univ i)) (hfn i)
  obtain ⟨n, hn⟩ := h2
  apply germ_eq_zero_of_pow_mul_eq_zero (U := ⊤) ⟨f x, trivial⟩ hyv
  rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero] at hfinj₂
  exact hfinj₂ _ (Scheme.zero_of_zero_cover _ _ hn)

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

Goal state before:
pp: X Y Z : Scheme
⊢ AffineTargetMorphismProperty.IsStableUnderBaseChange fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))

Tactic:
have := HasAffineProperty.isLocal_affineProperty @IsClosedImmersion

Goal state after:
X Y Z : Scheme
this :
  AffineTargetMorphismProperty.IsLocal fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ AffineTargetMorphismProperty.IsStableUnderBaseChange fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this : ∀ {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X), g ≫ f = 𝟙 Y → (∃ R, X = Spec R) → IsClosedImmersion g
hX : ¬∃ R, X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : ¬Set.range ⇑g ⊆ ↑(Scheme.Hom.opensRange (X.affineCover.f i))
x : ↥Y
hx : g x ∈ Set.range ⇑(X.affineCover.f i)
⊢ Set.range ⇑g ⊆ ↑(Scheme.Hom.opensRange (X.affineCover.f i))

Tactic:
rintro _ ⟨y, rfl⟩

Goal state after:
X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this : ∀ {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X), g ≫ f = 𝟙 Y → (∃ R, X = Spec R) → IsClosedImmersion g
hX : ¬∃ R, X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : ¬Set.range ⇑g ⊆ ↑(Scheme.Hom.opensRange (X.affineCover.f i))
x : ↥Y
hx : g x ∈ Set.range ⇑(X.affineCover.f i)
y : ↥Y
⊢ g y ∈ ↑(Scheme.Hom.opensRange (X.affineCover.f i))
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: case refine_1
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
⊢ IsPullback
    (pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
        (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯ ≫
      pullback.fst f (Z.fromSpecResidueField (g y)))
    (Scheme.Hom.fiberToSpecResidueField snd y) f
    (Spec.map (Scheme.Hom.residueFieldMap g y) ≫ Z.fromSpecResidueField (g y))

Tactic:
simpa using! (IsPullback.of_hasPullback _ _).paste_horiz h

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
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
h𝒰 : TopologicalSpace.IsOpenCover fun V ↦ (↑V).1 :=
  TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le (Scheme.isBasis_affineOpens Y)
    (TopologicalSpace.IsOpenCover.comap (TopologicalSpace.Opens.IsBasis.isOpenCover (Scheme.isBasis_affineOpens S))
      (TopCat.Hom.hom g.base))
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, ⟨U, hU⟩).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
⊢ RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V)) ≤ ⊥

Tactic:
intro x hx

Goal state after:
X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
h𝒰 : TopologicalSpace.IsOpenCover fun V ↦ (↑V).1 :=
  TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le (Scheme.isBasis_affineOpens Y)
    (TopologicalSpace.IsOpenCover.comap (TopologicalSpace.Opens.IsBasis.isOpenCover (Scheme.isBasis_affineOpens S))
      (TopCat.Hom.hom g.base))
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, ⟨U, hU⟩).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : ↑Γ(Y, V)
hx : x ∈ RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V))
⊢ x ∈ ⊥
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : JacobsonSpace ↥Y
inst✝ : LocallyOfFiniteType f
⊢ closedPoints ↥X ⊆ ⇑f ⁻¹' closedPoints ↥Y

Tactic:
intro x hx

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : JacobsonSpace ↥Y
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : x ∈ closedPoints ↥X
⊢ x ∈ ⇑f ⁻¹' closedPoints ↥Y
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case refine_2
R : CommRingCat
s : Set ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst✝² : Flat (Spec.map φ)
inst✝¹ : QuasiCompact (Spec.map φ)
inst✝ : Surjective (Spec.map φ)
hs : IsOpen (⇑(Spec.map φ) ⁻¹' s)
⊢ GeneralizingMap (PrimeSpectrum.comap (CommRingCat.Hom.hom φ))

Tactic:
apply RingHom.Flat.generalizingMap_comap
    rwa [← HasRingHomProperty.Spec_iff (P := @Flat)]

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case left
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
f g : X → Y
hf : f ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
hg : g ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
⊢ Function.support (f + g) ⊆ U

Tactic:
intro x hx

Goal state after:
case left
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
f g : X → Y
hf : f ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
hg : g ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
x : X
hx : x ∈ Function.support (f + g)
⊢ x ∈ U
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✝ : AddMonoid Y
f g : X → Y
hf : f ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
hg : g ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ Function.support f).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ Function.support g).Finite
⊢ (t₁ ∩ t₂ ∩ Function.support (f + g)).Finite

Tactic:
apply Set.Finite.subset (s := (t₁ ∩ f.support) ∪ (t₂ ∩ g.support)) (ht₁.2.union ht₂.2)

Goal state after:
case right
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
f g : X → Y
hf : f ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
hg : g ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ Function.support f).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ Function.support g).Finite
⊢ t₁ ∩ t₂ ∩ Function.support (f + g) ⊆ t₁ ∩ Function.support f ∪ t₂ ∩ Function.support g
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 }
⊢ Statement R₀ (Localization.Away c) n
      {
        val :=
          Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Localization.Away c))) ∘ e.val } →
    Statement R₀ (R ⧸ Ideal.span {c}) n { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } →
      Statement R₀ R n e

Tactic:
set e₂ : InductionObj (R ⧸ Ideal.span {c}) n := ⟨mapRingHom q₂ ∘ 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 }
⊢ Statement R₀ (Localization.Away c) n
      {
        val :=
          Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Localization.Away c))) ∘ e.val } →
    Statement R₀ (R ⧸ Ideal.span {c}) n { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } →
      Statement R₀ R n e
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
⊢ (Function.support fun z ↦ if hz : z ∈ V then D z else 0) ⊆ V

Tactic:
intro x hx

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
hx : x ∈ Function.support fun z ↦ if hz : z ∈ V then D z else 0
⊢ x ∈ V
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
⊢ ∀ (x : ↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f)))),
    (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf)) x = 0 → x = 0

Tactic:
intro x hx

Goal state after:
case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f)))
hx : (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf)) x = 0
⊢ x = 0
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
⊢ f.restrict f.domain ⋯ ⋯ = f

Tactic:
ext1 <;> simp [restrict_domain]

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

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
V : X.Opens
hV : Dense ↑V
hV' : V ≤ U
⊢ (f.restrict U hU hU').restrict V hV hV' = f.restrict V hV ⋯

Tactic:
ext1 <;> simp [restrict_domain]

Goal state after:
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
    exact PartialMap.ext _ f rfl (by simpa using f.toPartialMap_toRationalMap_restrict)

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
⊢ f.toPartialMap.toRationalMap = f

Tactic:
obtain ⟨f, rfl⟩ := PartialMap.toRationalMap_surjective f
  trans (f.toRationalMap.toPartialMap.restrict _
    f.dense_domain f.le_domain_toRationalMap).toRationalMap
  · simp
  · congr 1
    exact PartialMap.ext _ f rfl (by simpa using f.toPartialMap_toRationalMap_restrict)

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

Goal state before:
pp: X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g₁ g₂ : Y.PartialMap Z
W : Y.Opens
hW : Dense ↑W
hW₁ : W ≤ g₁.domain
hW₂ : W ≤ g₂.domain
e : f.comp (g₁.restrict W hW hW₁) = f.comp (g₂.restrict W hW hW₂)
⊢ (f.comp g₁).equiv (f.comp g₂)

Tactic:
comp_restrict_right,

Goal state after:
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g₁ g₂ : Y.PartialMap Z
W : Y.Opens
hW : Dense ↑W
hW₁ : W ≤ g₁.domain
hW₂ : W ≤ g₂.domain
e : (f.comp g₁).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ W) ⋯ ⋯ = f.comp (g₂.restrict W hW hW₂)
⊢ (f.comp g₁).equiv (f.comp g₂)
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.190} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
hij : i ⟶ j
⊢ P (pullback.map f (𝒰.f i) f (𝒰.f j) (𝟙 Y) (𝒰.trans hij) (𝟙 X) ⋯ ⋯)

Tactic:
by
    let iso : pullback f (𝒰.f i) ≅ pullback (pullback.snd f (𝒰.f j)) (𝒰.trans hij) :=
      pullback.congrHom rfl (by simp) ≪≫ (pullbackLeftPullbackSndIso _ _ _).symm
    rw [← P.cancel_left_of_respectsIso iso.inv]
    simp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
      PreZeroHypercover.pullback₁_X, Iso.trans_inv, Iso.symm_inv, pullback.congrHom_inv,
      Category.assoc, iso]
    convert! P.pullback_fst (pullback.snd f (𝒰.f j)) _ (𝒰.property_trans hij)
    apply pullback.hom_ext <;> simp [pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C✝ : Type u_1
inst✝³ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝² : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst✝¹ : EffectiveEpiFamily Z fun i ↦ g i ≫ f i
inst✝ : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
i : I
⊢ (g i ≫ f i) ≫ EffectiveEpiFamily.desc Z (fun i ↦ g i ≫ f i) (fun i ↦ g i ≫ φ i) ⋯ = g i ≫ φ i

Tactic:
EffectiveEpiFamily.fac _ (fun i => g i ≫ f i)

Goal state after:
C✝ : Type u_1
inst✝³ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝² : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst✝¹ : EffectiveEpiFamily Z fun i ↦ g i ≫ f i
inst✝ : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
i : I
⊢ g i ≫ φ i = g i ≫ φ i
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hmn
R : Type u_6
inst✝ : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
f : BasicConstructibleSetData R[X] → ConstructibleSetData R
hf₁ :
  ∀ (C : BasicConstructibleSetData R[X]),
    comap Polynomial.C '' (zeroLocus (Set.range { val := C.g }.val) \ zeroLocus {C.f}) = (f C).toSet
hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g }.degBound
hf₃ :
  ∀ (C : BasicConstructibleSetData R[X]),
    ∀ C_1 ∈ f C, ∀ (i : Fin C_1.n), C_1.g i ∈ coeffSubmodule ℤ { val := C.g } ^ { val := C.g }.powBound
x : BasicConstructibleSetData R
y : BasicConstructibleSetData R[X]
hy : y ∈ S
hx : x ∈ f y
H : { val := y.g }.degBound ≤ S.degBound
i : Fin x.n
⊢ { val := y.g }.powBound ≤ S.degBound ^ S.degBound

Tactic:
· delta powBound
      by_cases h : S.degBound = 0
      · have : degBound ⟨y.g⟩ = 0 := by nlinarith
        rw [h, this]
      gcongr
      rwa [Nat.one_le_iff_ne_zero]

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

Goal state before:
pp: R : Type u_6
inst✝ : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
⊢ ∃ T,
    comap Polynomial.C '' S.toSet = T.toSet ∧
      ∀ C ∈ T, C.n ≤ S.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ M ^ S.degBound ^ S.degBound

Tactic:
choose f hf₁ hf₂ hf₃ using fun C : BasicConstructibleSetData R[X] ↦ statement (R₀ := ℤ) ⟨C.g⟩ C.f
  refine ⟨S.biUnion f, ?_, ?_⟩
  · simp only [BasicConstructibleSetData.toSet, ConstructibleSetData.toSet, Set.image_iUnion,
      Finset.set_biUnion_biUnion, hf₁]
  · simp only [Finset.mem_biUnion, forall_exists_index, and_imp]
    intro x y hy hx
    have H : degBound ⟨y.g⟩ ≤ S.degBound :=
      Finset.le_sup (f := fun e ↦ ∑ i, (e.g i).degree.succ) hy
    refine ⟨(hf₂ y x hx).trans H, fun i ↦ SetLike.le_def.mp ?_ (hf₃ y x hx i)⟩
    gcongr
    · simpa [Submodule.one_eq_span]
    · refine Submodule.span_le.mpr ?_
      simp [Set.subset_def, hM, forall_comm (α := R), hS y hy]
    · delta powBound
      by_cases h : S.degBound = 0
      · have : degBound ⟨y.g⟩ = 0 := by nlinarith
        rw [h, this]
      gcongr
      rwa [Nat.one_le_iff_ne_zero]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
⊢ W.a₆ = 0 ∧ (W.a₄ ≠ 0 ∨ evalEval 0 0 W.polynomialY ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)

Tactic:
evalEval_polynomialY_zero,

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
⊢ W.a₆ = 0 ∧ (W.a₄ ≠ 0 ∨ W.a₃ ≠ 0) ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W : Affine R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
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).polynomialY = Polynomial.map (mapRingHom ↑f) (W⁄A).polynomialY

Tactic:
rw [← map_polynomialY, map_baseChange]

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

Goal state before:
pp: case neg
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
hp : ¬p = 0
hq : ¬q = 0
⊢ (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₆)).degree =
    max (2 • p.degree) (2 • q.degree + 3)

Tactic:
· rw [← not_congr degree_eq_bot] at hp hq
      -- Porting note: BUG `cases` tactic does not modify assumptions in `hp'` and `hq'`
      rcases hp' : p.degree with _ | dp -- `hp' : ` should be redundant
      · exact (hp hp').elim -- `hp'` should be `rfl`
      · rw [hp'] at hdp hdpq -- line should be redundant
        rcases hq' : q.degree with _ | dq -- `hq' : ` should be redundant
        · exact (hq hq').elim -- `hq'` should be `rfl`
        · rw [hq'] at hdpq hdq -- line should be redundant
          rcases le_or_gt dp (dq + 1) with hpq | hpq
          · convert!
            (degree_sub_eq_right_of_degree_lt <|
                  (degree_sub_le _ _).trans_lt <|
                    max_lt_iff.mpr ⟨hdp.trans_lt _, hdpq.trans_lt _⟩).trans
              (max_eq_right_of_lt _).symm <;> rw [hdq] <;>
                exact WithBot.coe_lt_coe.mpr <| by dsimp; linarith only [hpq]
          · rw [sub_sub]
            convert!
              (degree_sub_eq_left_of_degree_lt <|
                    (degree_add_le _ _).trans_lt <|
                      max_lt_iff.mpr ⟨hdpq.trans_lt _, hdq.trans_lt _⟩).trans
                (max_eq_left_of_lt _).symm <;> rw [hdp] <;>
                exact WithBot.coe_lt_coe.mpr <| by dsimp; linarith only [hpq]

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

Goal state before:
pp: F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
⊢ W.j ≠ 0

Tactic:
j_of_isCharThreeJNeZeroNF_of_char_three,

Goal state after:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
⊢ -W.a₂ ^ 3 / W.a₆ ≠ 0