mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case inr.mpr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H : ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
⊢ Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f)) =
    X ^ ((LinearMap.mul R A) f).charpoly.natDegree

Tactic:
ext i

Goal state after:
case inr.mpr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H : ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
i : ℕ
⊢ (Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f))).coeff i =
    (X ^ ((LinearMap.mul R A) f).charpoly.natDegree).coeff i
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ IsOpenMap (comap C)

Tactic:
intro U

Goal state after:
R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
⊢ IsOpen U → IsOpen (comap C '' U)
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
this :
  ∀ {X : Scheme} {s : Set ↥X},
    IsLocallyConstructible s →
      ∀ (R : CommRingCat) (f : X ⟶ Spec R) [hf : LocallyOfFinitePresentation f] [QuasiCompact f],
        (∃ S, X = Spec S) → IsLocallyConstructible (⇑f '' s)
hX : ¬∃ S, X = Spec S
inst✝ : CompactSpace ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
inst : QuasiCompact (𝒰.f i ≫ f)
⊢ ⇑f '' (s ∩ ↑(opensRange (𝒰.f i))) = ⇑(𝒰.f i ≫ f) '' ⇑(𝒰.f i) ⁻¹' s

Tactic:
rw [Scheme.Hom.comp_base, ← TopCat.Hom.hom, ← TopCat.Hom.hom, TopCat.hom_comp,
      ContinuousMap.coe_comp, Set.image_comp, Set.image_preimage_eq_inter_range, coe_opensRange]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
⊢ ∀ (U : X.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)

Tactic:
intro U

Goal state after:
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
⊢ IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
⊢ ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

Tactic:
intro U

Goal state after:
X : Scheme
inst✝ : IsLocallyNoetherian X
U : ↑X.affineOpens
⊢ ∀ (V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
⊢ IsOpenMap (comap C)

Tactic:
intro U

Goal state after:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
U : Set (PrimeSpectrum (MvPolynomial σ R))
⊢ IsOpen U → IsOpen (comap C '' U)
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : Flat f
this :
  HasRingHomProperty (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    fun {R S} [CommRing R] [CommRing S] f ↦
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom f))
⊢ ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))))

Tactic:
intro U

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : Flat f
this :
  HasRingHomProperty (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    fun {R S} [CommRing R] [CommRing S] f ↦
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom f))
U : ↑Y.affineOpens
⊢ ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))))
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f)
hY : ¬IsAffine Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f

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

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

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
inst✝² : CommRing R₀
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
n : ℕ
e : InductionObj R n
⊢ 1 ≤ coeffSubmodule R₀ e

Tactic:
rw [Submodule.one_eq_span, Submodule.span_le, Set.singleton_subset_iff]

Goal state after:
R₀ : Type u_1
R : Type u_2
inst✝² : CommRing R₀
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
n : ℕ
e : InductionObj R n
⊢ 1 ∈ ↑(coeffSubmodule R₀ e)
Module: Mathlib.AlgebraicGeometry.AffineSpace

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

Tactic:
ext i

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

Goal state before:
pp: n : Type u
S X : Scheme
inst✝ : X.Over S
v : n → ↑Γ(X, ⊤)
⊢ (fun f i ↦ (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i)) ((fun v ↦ ⟨homOfVector (X ↘ S) v, ⋯⟩) v) = v

Tactic:
ext i

Goal state after:
n : Type u
S X : Scheme
inst✝ : X.Over S
v : n → ↑Γ(X, ⊤)
i : n
⊢ (fun f i ↦ (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i)) ((fun v ↦ ⟨homOfVector (X ↘ S) v, ⋯⟩) v) i = v i
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
⊢ Scheme.Hom.appTop (SpecIso n R).hom =
    (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).hom ≫
      CommRingCat.ofHom
        (eval₂Hom (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R)))
          (coord (Spec R)))

Tactic:
ext i

Goal state after:
n : Type u
R : CommRingCat
i : ↑Γ(Spec (CommRingCat.of (MvPolynomial n ↑R)), ⊤)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop (SpecIso n R).hom)) i =
    (CommRingCat.Hom.hom
        ((Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).hom ≫
          CommRingCat.ofHom
            (eval₂Hom (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop (𝔸(n; Spec R) ↘ Spec R)))
              (coord (Spec R)))))
      i
Module: Mathlib.AlgebraicGeometry.AffineSpace

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

Tactic:
ext i

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

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

Tactic:
obtain ⟨k, g, eq⟩ := h (max j j') (F.map (leftToMax _ _) x)
      (F.map (rightToMax _ _) x') (by simpa only [c.ι_naturality_apply])

Goal state after:
case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h :
  ∀ (j : J) (x x' : F.obj j),
    c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'
j j' : J
x : F.obj j
x' : F.obj j'
eq✝ : c.ι j x = c.ι j' x'
k : J
g : IsFiltered.max j j' ⟶ k
eq :
  (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (F.map (leftToMax j j'))) x) =
    (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (F.map (rightToMax j j'))) x')
⊢ ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
f✝ : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
J : Ideal ↑R := RingHom.ker (algebraMap (↑R) (Localization.AtPrime I))
hJ : ∀ (x : ↑R), x ∈ J ↔ ∃ y, ↑y * x = 0
f : (x : ↑R) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : ↑R) (a : x ∈ J), ↑(f x a) * x = 0
s : Finset ↑R
hs : Ideal.span ↑s = J
hs' : ↑s ⊆ ↑J
x y : ↑R
e : y * x = 0
hy : y ∉ I
⊢ J ≤ (↑R ∙ ↑(∏ x ∈ s.attach, f ↑x ⋯)).annihilator

Tactic:
rw [← hs, Ideal.span_le]

Goal state after:
X Y S : Scheme
f✝ : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
J : Ideal ↑R := RingHom.ker (algebraMap (↑R) (Localization.AtPrime I))
hJ : ∀ (x : ↑R), x ∈ J ↔ ∃ y, ↑y * x = 0
f : (x : ↑R) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : ↑R) (a : x ∈ J), ↑(f x a) * x = 0
s : Finset ↑R
hs : Ideal.span ↑s = J
hs' : ↑s ⊆ ↑J
x y : ↑R
e : y * x = 0
hy : y ∉ I
⊢ ↑s ⊆ ↑(↑R ∙ ↑(∏ x ∈ s.attach, f ↑x ⋯)).annihilator
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
i : I
this✝⁴ : IsCofiltered I
𝒰 : (D.obj i).OpenCover := ⋯
this✝³ : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
j : 𝒰.I₀
H : ∀ {i' : I} (f : i' ⟶ i), Nonempty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map f) 𝒰).X j)
F : Over i ⥤ Scheme := ⋯
this✝² : ∀ (i' : Over i), IsAffine (F.obj i')
this✝¹ : ∀ (i' : Over i), Nonempty ↥(F.obj i')
e : F ⟶ (F ⋙ Γ.rightOp) ⋙ Scheme.Spec := ⋯
this✝ : ∀ (i_1 : Over i), IsIso (e.app i_1)
this : IsIso e
c' : LimitCone F := ⋯
⊢ Nontrivial ↑(Opposite.unop (limit.cone (F ⋙ Γ.rightOp)).pt)

Tactic:
have (i' : _) : Nontrivial ((F ⋙ Scheme.Γ.rightOp).leftOp.obj i') := by
        apply +allowSynthFailures Scheme.component_nontrivial
        simp

Goal state after:
I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
i : I
this✝⁵ : IsCofiltered I
𝒰 : (D.obj i).OpenCover := (D.obj i).affineCover.finiteSubcover
this✝⁴ : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
j : 𝒰.I₀
H : ∀ {i' : I} (f : i' ⟶ i), Nonempty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map f) 𝒰).X j)
F : Over i ⥤ Scheme := Over.post D ⋙ Over.pullback (𝒰.f j) ⋙ Over.forget (𝒰.X j)
this✝³ : ∀ (i' : Over i), IsAffine (F.obj i')
this✝² : ∀ (i' : Over i), Nonempty ↥(F.obj i')
e : F ⟶ (F ⋙ Γ.rightOp) ⋙ Scheme.Spec := F.whiskerLeft ΓSpec.adjunction.unit
this✝¹ : ∀ (i_1 : Over i), IsIso (e.app i_1)
this✝ : IsIso e
c' : LimitCone F :=
  { cone := (Cone.postcompose (asIso e).inv).obj (Scheme.Spec.mapCone (limit.cone (F ⋙ Γ.rightOp))),
    isLimit :=
      (IsLimit.postcomposeInvEquiv (asIso e) (Scheme.Spec.mapCone (limit.cone (F ⋙ Γ.rightOp)))).symm
        (isLimitOfPreserves Scheme.Spec (limit.isLimit (F ⋙ Γ.rightOp))) }
this : ∀ (i' : (Over i)ᵒᵖ), Nontrivial ↑((F ⋙ Γ.rightOp).leftOp.obj i')
⊢ Nontrivial ↑(Opposite.unop (limit.cone (F ⋙ Γ.rightOp)).pt)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofilteredOrEmpty I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
X Y : I
f : X ⟶ Y
⊢ TopologicalSpace.Closeds.closure (⇑(D.map f) '' ↑{ carrier := Z X, isClosed' := ⋯ }) ≤
    (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }).support

Tactic:
simpa [(hZc _).closure_subset_iff] using (hmapsTo f).subset_preimage

Goal state after:
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 : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅ pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) :=
  pullbackRightPullbackFstIso f (𝒰.f j) (pullback.fst f (𝒰.f i)) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫ pullbackAssoc f (𝒰.f i) (𝒰.f i) (𝒰.f j)
this :
  ∀ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j),
    pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
        (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯ =
      pullback.map f (𝒰.f k) f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) (𝟙 Y)
          (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) (𝟙 X) ⋯ ⋯ ≫
        iso.inv
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
yk : ↥(𝒰.X k)
hyk :
  (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) yk = (iso.hom ≫ pullback.snd f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)) x
⊢ ∃ k hki hkj y,
    (pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
          (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯)
        y =
      x

Tactic:
refine ⟨k, hki, hkj, show x ∈ Set.range _ from ?_⟩

Goal state after:
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 : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅ pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) :=
  pullbackRightPullbackFstIso f (𝒰.f j) (pullback.fst f (𝒰.f i)) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫ pullbackAssoc f (𝒰.f i) (𝒰.f i) (𝒰.f j)
this :
  ∀ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j),
    pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
        (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯ =
      pullback.map f (𝒰.f k) f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) (𝟙 Y)
          (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) (𝟙 X) ⋯ ⋯ ≫
        iso.inv
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
yk : ↥(𝒰.X k)
hyk :
  (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) yk = (iso.hom ≫ pullback.snd f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)) x
⊢ x ∈
    Set.range
      ⇑(pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
          (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯)
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: case refine_3
P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this : (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x ∈ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
k : 𝒰.I₀
h : (fun i ↦ Hom.opensRange (𝒰.f i)) k ≤ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : (𝒰.f k) y = (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x
⊢ (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯ ≫
        pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
      y =
    (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x

Tactic:
pullback.lift_fst_assoc,

Goal state after:
case refine_3
P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this : (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x ∈ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
k : 𝒰.I₀
h : (fun i ↦ Hom.opensRange (𝒰.f i)) k ≤ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : (𝒰.f k) y = (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x
⊢ (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯ ≫ 𝒰.f i) y = (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x
Module: Mathlib.Topology.Category.TopCat.EffectiveEpi

Goal state before:
pp: B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
a✝ : ↑X
⊢ ↑(hπ.liftEquiv.symm (Hom.hom g)) a✝ = ↑⟨Hom.hom e, ⋯⟩ a✝

Tactic:
simp only [IsQuotientMap.liftEquiv_symm_apply_coe, ContinuousMap.comp_apply, ← hm]

Goal state after:
B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
a✝ : ↑X
⊢ (Hom.hom g) ((ConcreteCategory.hom π) a✝) = (Hom.hom (π ≫ g)) a✝
Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.PreservesEffectiveEpis
inst✝ : G.PreservesEffectiveEpis
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : EffectiveEpi x✝¹
⊢ EffectiveEpi ((F ⋙ G).map x✝¹)

Tactic:
dsimp; infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
inst✝² : F.PreservesFiniteEffectiveEpiFamilies
inst✝¹ : G.PreservesFiniteEffectiveEpiFamilies
α✝ : Type
inst✝ : Finite α✝
B✝ : C
x✝² : α✝ → C
x✝¹ : (a : α✝) → x✝² a ⟶ B✝
x✝ : EffectiveEpiFamily x✝² x✝¹
⊢ EffectiveEpiFamily (fun a ↦ (F ⋙ G).obj (x✝² a)) fun a ↦ (F ⋙ G).map (x✝¹ a)

Tactic:
dsimp; infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.PreservesEffectiveEpiFamilies
inst✝ : G.PreservesEffectiveEpiFamilies
α✝ : Type u
B✝ : C
x✝² : α✝ → C
x✝¹ : (a : α✝) → x✝² a ⟶ B✝
x✝ : EffectiveEpiFamily x✝² x✝¹
⊢ EffectiveEpiFamily (fun a ↦ (F ⋙ G).obj (x✝² a)) fun a ↦ (F ⋙ G).map (x✝¹ a)

Tactic:
dsimp; infer_instance

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆ =
    W.a₁ ^ 4 * W.b₈ + W.a₃ ^ 4 + W.a₁ ^ 3 * W.a₃ ^ 3

Tactic:
b₂_of_char_two,

Goal state after:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ -(W.a₁ ^ 2) ^ 2 * W.b₈ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.a₁ ^ 2 * W.b₄ * W.b₆ =
    W.a₁ ^ 4 * W.b₈ + W.a₃ ^ 4 + W.a₁ ^ 3 * W.a₃ ^ 3
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
f : R →+* S
hf : Function.Injective ⇑f
x y : R
⊢ (W.map f).Equation (f x) (f y) ↔ W.Equation x y

Tactic:
simp only [Equation, map_polynomial, map_mapRingHom_evalEval, map_eq_zero_iff f hf]

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

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : x₁ = x₂
⊢ { a := 1, b := -W.slope x₁ x₂ y₁ y₂ ^ 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
      c := 2 * x₁ * W.slope x₁ x₂ y₁ y₂ ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ + (-W.a₁ * y₁ + W.a₄),
      d :=
        -x₁ ^ 2 * W.slope x₁ x₂ y₁ y₂ ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
          (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) + x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂),
      d := -(x₁ * x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) }

pp: case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ = x₂
⊢ { a := 1, b := -W.slope x₁ x₂ y₁ y₂ ^ 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
      c := 2 * x₁ * W.slope x₁ x₂ y₁ y₂ ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ + (-W.a₁ * y₁ + W.a₄),
      d :=
        -x₁ ^ 2 * W.slope x₁ x₂ y₁ y₂ ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
          (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) + x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂),
      d := -(x₁ * x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) }

Tactic:
· have hy : y₁ ≠ W.negY x₂ y₂ := fun h => hxy ⟨hx, h⟩
    rcases hx, Y_eq_of_Y_ne h₁ h₂ hx hy with ⟨rfl, rfl⟩
    rw [equation_iff] at h₁ h₂
    rw [slope_of_Y_ne rfl hy]
    rw [negY, ← sub_ne_zero] at hy
    replace hy : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0 := by convert! hy using 1; ring
    ext
    · rfl
    · simp only [addX]
      ring1
    · simp [field]
      ring1
    · linear_combination (norm := (simp [field]; ring1)) -h₁

Goal state after:
case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ = x₂
⊢ { a := 1, b := -W.slope x₁ x₂ y₁ y₂ ^ 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
      c := 2 * x₁ * W.slope x₁ x₂ y₁ y₂ ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ + (-W.a₁ * y₁ + W.a₄),
      d :=
        -x₁ ^ 2 * W.slope x₁ x₂ y₁ y₂ ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
          (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) + x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂),
      d := -(x₁ * x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) }