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

Goal state before:
pp: X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
⊢ IsOver S f ↔ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)

Tactic:
constructor
  · intro h
    obtain ⟨g, hg, e⟩ := f.exists_partialMap_over S
    rw [← e, Hom.toRationalMap, ← compHom_toRationalMap, PartialMap.isOver_iff_eq_restrict.mp hg,
      PartialMap.restrict_toRationalMap]
  · intro e
    obtain ⟨f, rfl⟩ := PartialMap.toRationalMap_surjective f
    obtain ⟨U, hU, hUl, hUr, e⟩ := PartialMap.toRationalMap_eq_iff.mp e
    exact ⟨⟨f.restrict U hU hUl, by simpa using! e, by simp⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
⊢ D.map j.hom ⁻¹ᵁ U ≤ D.map (Over.Hom.left f ≫ k.hom) ⁻¹ᵁ U

Tactic:
Over.w f

Goal state after:
I : Type u
inst✝ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
⊢ D.map j.hom ⁻¹ᵁ U ≤ D.map j.hom ⁻¹ᵁ U
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_2.refine_1
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
x : ↥((opensDiagram D i U).obj j)
h : ((opensDiagram D i U).map f) x ∈ V
⊢ (D.map (Over.Hom.left f ≫ k.hom)) ↑x ∈ U

Tactic:
Over.w f

Goal state after:
case e'_2.refine_1
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
x : ↥((opensDiagram D i U).obj j)
h : ((opensDiagram D i U).map f) x ∈ V
⊢ (D.map j.hom) ↑x ∈ U
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
x : ↥(D.obj j.left)
h₁✝ : (D.map k.hom) ((D.map (Over.Hom.left f)) x) ∈ U
h₁ : (D.map (Over.Hom.left f ≫ k.hom)) x ∈ U
h₂ : ⟨(D.map (Over.Hom.left f)) x, h₁✝⟩ ∈ ↑V
e :
  (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom.base)
      ⟨(D.map (Over.Hom.left f)) x, h₁✝⟩ =
    (D.map (Over.Hom.left f)) x
⊢ x ∈ D.map j.hom ⁻¹ᵁ U

Tactic:
Over.w f

Goal state after:
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
x : ↥(D.obj j.left)
h₁✝ : (D.map k.hom) ((D.map (Over.Hom.left f)) x) ∈ U
h₁ : (D.map j.hom) x ∈ U
h₂ : ⟨(D.map (Over.Hom.left f)) x, h₁✝⟩ ∈ ↑V
e :
  (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom.base)
      ⟨(D.map (Over.Hom.left f)) x, h₁✝⟩ =
    (D.map (Over.Hom.left f)) x
⊢ x ∈ D.map j.hom ⁻¹ᵁ U
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)
i : I
U V : (D.obj i).Opens
hU : IsCompact ↑U
H : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
⊢ ∃ j fji, D.map fji ⁻¹ᵁ U ≤ D.map fji ⁻¹ᵁ V

Tactic:
have (j : Over i) : CompactSpace ↥((opensDiagram D i U).obj j) :=
    isCompact_iff_compactSpace.mp (QuasiCompact.isCompact_preimage (f := (D.map j.hom)) _ U.2 hU)
  have H : ((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V = ⊤ := by
    rw [Scheme.Hom.comp_preimage, ← top_le_iff]
    exact .trans (by simp) (Scheme.Hom.preimage_mono _ H)
  obtain ⟨j, fji, hj⟩ := exists_map_eq_top _ _ (isLimitOpensCone D c hc i U) (i := .mk (𝟙 i))
    (((Scheme.isoOfEq _ (by simp)).hom ≫ U.ι) ⁻¹ᵁ V)
    (by simpa [← Scheme.Hom.comp_preimage, -Scheme.Hom.comp_base])
  refine ⟨j.left, j.hom, ?_⟩
  replace hj : (D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map fji.left ⁻¹ᵁ V = ⊤ := by
    simpa [← Scheme.Hom.comp_preimage, -Scheme.Hom.comp_base] using hj
  replace hj : (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ D.map fji.left ⁻¹ᵁ V := Set.image_subset_iff.mpr hj.ge
  simpa [show fji.left = j.hom by simpa using fji.w] using hj

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰✝ : X.OpenCover
inst✝³ : Category.{v_1, ?u.14} 𝒰✝.I₀
inst✝² : Cover.LocallyDirected 𝒰✝
𝒰 : X.OpenCover
inst✝¹ : Category.{v_2, ?u.64} 𝒰.I₀
inst✝ : Cover.LocallyDirected 𝒰
Y : Scheme
g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y
h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), Cover.trans 𝒰 hij ≫ g j = g i
i j : 𝒰.I₀
k : (Cover.intersectionOfLocallyDirected 𝒰 i j).I₀
⊢ (Cover.intersectionOfLocallyDirected 𝒰 i j).f k ≫ pullback.fst (𝒰.f i) (𝒰.f j) ≫ g i =
    (Cover.intersectionOfLocallyDirected 𝒰 i j).f k ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ g j

Tactic:
simp [h]

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✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : ∀ (i : I), IsAffine (D.obj i)
inst✝³ : IsAffine c.pt
i j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝² : IsAffine (Spec R)
X : Scheme
inst✝¹ : IsAffine X
a : D.obj i ⟶ X
b : D.obj j ⟶ X
hab : c.π.app i ≫ a = c.π.app j ≫ b
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
hX : ∃ S, X = Spec S
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b

Tactic:
obtain ⟨S, rfl⟩ := hX

Goal state after:
I : Type u
inst✝⁷ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : ∀ (i : I), IsAffine (D.obj i)
inst✝³ : IsAffine c.pt
i j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝² : IsAffine (Spec R)
S : CommRingCat
inst✝¹ : IsAffine (Spec S)
a : D.obj i ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i ≫ a = c.π.app j ≫ b
f : Spec S ⟶ Spec R
inst✝ : LocallyOfFiniteType f
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: case refine_2
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₀
x : ↥d.glued
⊢ x ∈ Set.range ⇑(colimit.ι d.functor i) → x ∈ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i)

Tactic:
rintro ⟨y, rfl⟩

Goal state after:
case refine_2
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₀
y : ↥(d.functor.obj i)
⊢ (colimit.ι d.functor i) y ∈ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i)
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case neg
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
i : ι
h : i ∉ s
⊢ IsOpen (Sigma.mk i ⁻¹' s.sigma fun i ↦ if h : i ∈ s then ↑(V i h) else ∅)

Tactic:
simp [h]

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

Goal state before:
pp: S : Scheme
𝒰 : PreZeroHypercover S
inst✝ : QuasiCompactCover 𝒰
U : S.Opens
hU : IsCompact ↑U
⊢ ∃ n f V, (∀ (i : Fin n), IsAffineOpen (V i)) ∧ ⋃ i, ⇑(𝒰.f (f i)) '' ↑(V i) = ↑U

Tactic:
by
  obtain ⟨n, a, V, ha, heq⟩ := (isCompactOpenCovered_of_isCompact 𝒰 hU).exists_mem_of_isBasis
    (fun i ↦ (𝒰.X i).isBasis_affineOpens) (fun _ _ h ↦ h.isCompact)
  exact ⟨n, a, V, ha, heq⟩

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

Goal state before:
pp: case ht
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
⊢ c.degBound ≠ 0

Tactic:
← Nat.pos_iff_ne_zero,

Goal state after:
case ht
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
⊢ 0 < c.degBound
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: S : Scheme
𝒰✝¹ 𝒰✝ : PreZeroHypercover S
K : Precoverage Scheme
X : Scheme
𝒰 : PreZeroHypercover X
inst✝¹ : QuasiCompactCover 𝒰
f : (x : 𝒰.I₀) → PreZeroHypercover (𝒰.X x)
inst✝ : ∀ (x : 𝒰.I₀), QuasiCompactCover (f x)
U : X.Opens
hU✝ : IsAffineOpen U
s : Set 𝒰.I₀
hs : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hcV : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
this : ∀ (i : 𝒰.I₀) (hi : i ∈ s), IsCompactOpenCovered (fun x ↦ ⇑((f i).f x)) ↑(V i hi)
⊢ IsCompactOpenCovered (fun x ↦ ⇑((𝒰.bind f).f x)) ↑U

Tactic:
choose t ht W hcW hV using this

Goal state after:
S : Scheme
𝒰✝¹ 𝒰✝ : PreZeroHypercover S
K : Precoverage Scheme
X : Scheme
𝒰 : PreZeroHypercover X
inst✝¹ : QuasiCompactCover 𝒰
f : (x : 𝒰.I₀) → PreZeroHypercover (𝒰.X x)
inst✝ : ∀ (x : 𝒰.I₀), QuasiCompactCover (f x)
U : X.Opens
hU✝ : IsAffineOpen U
s : Set 𝒰.I₀
hs : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hcV : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
t : (i : 𝒰.I₀) → i ∈ s → Set (f i).I₀
ht : ∀ (i : 𝒰.I₀) (hi : i ∈ s), (t i hi).Finite
W : (i : 𝒰.I₀) → (hi : i ∈ s) → (i_1 : (f i).I₀) → i_1 ∈ t i hi → TopologicalSpace.Opens ((fun x ↦ ↥((f i).X x)) i_1)
hcW : ∀ (i : 𝒰.I₀) (hi : i ∈ s) (i_1 : (f i).I₀) (h : i_1 ∈ t i hi), IsCompact (W i hi i_1 h).carrier
hV : ∀ (i : 𝒰.I₀) (hi : i ∈ s), ⋃ i_1, ⋃ (h : i_1 ∈ t i hi), (fun x ↦ ⇑((f i).f x)) i_1 '' ↑(W i hi i_1 h) = ↑(V i hi)
⊢ IsCompactOpenCovered (fun x ↦ ⇑((𝒰.bind f).f x)) ↑U
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case pos
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
l : Fin n
m : ℕ
hlj : l = j
⊢ (c.val j %ₘ c.val i).coeff m ∈ coeffSubmodule R₀ c ^ (c.val j).degree.succ

Tactic:
convert!
          coeff_modByMonic_mem_pow_natDegree_mul _ _ _ (fun _ ↦ coeff_mem_coeffSubmodule)
            one_mem_coeffSubmodule _ (fun _ ↦ coeff_mem_coeffSubmodule) one_mem_coeffSubmodule _
          rw [← pow_succ, Polynomial.degree_eq_natDegree, WithBot.succ_natCast, Nat.cast_id]
          intro e
          simp [show c.val i = 0 by simpa [e] using hle] at hi

Goal state after:
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: case refine_1
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this✝ : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
i j : 𝒰.I₀
this : Epi (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
⊢ (pullback.congrHom ⋯ ⋯).hom ≫
      pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≫ pullback.fst (𝒰.f i) (𝒰.f j) ≫ u i =
    pullback.snd π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j

Tactic:
← pullbackLeftPullbackSndIso_inv_snd_snd,

Goal state after:
case refine_1
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this✝ : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
i j : 𝒰.I₀
this : Epi (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
⊢ (pullback.congrHom ⋯ ⋯).hom ≫
      ((pullbackLeftPullbackSndIso π (𝒰.f i) (pullback.fst (𝒰.f i) (𝒰.f j))).inv ≫
          pullback.snd (pullback.snd π (𝒰.f i)) (pullback.fst (𝒰.f i) (𝒰.f j))) ≫
        pullback.fst (𝒰.f i) (𝒰.f j) ≫ u i =
    pullback.snd π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: case refine_1
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this✝ : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
i j : 𝒰.I₀
this : Epi (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
⊢ (pullback.congrHom ⋯ ⋯).hom ≫
      (pullbackLeftPullbackSndIso π (𝒰.f i) (pullback.fst (𝒰.f i) (𝒰.f j))).inv ≫
        pullback.snd (pullback.snd π (𝒰.f i)) (pullback.fst (𝒰.f i) (𝒰.f j)) ≫ pullback.fst (𝒰.f i) (𝒰.f j) ≫ u i =
    pullback.snd π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j

Tactic:
← pullbackLeftPullbackSndIso_inv_snd_snd,

Goal state after:
case refine_1
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this✝ : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
i j : 𝒰.I₀
this : Epi (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
⊢ (pullback.congrHom ⋯ ⋯).hom ≫
      (pullbackLeftPullbackSndIso π (𝒰.f i) (pullback.fst (𝒰.f i) (𝒰.f j))).inv ≫
        pullback.snd (pullback.snd π (𝒰.f i)) (pullback.fst (𝒰.f i) (𝒰.f j)) ≫ pullback.fst (𝒰.f i) (𝒰.f j) ≫ u i =
    ((pullbackLeftPullbackSndIso π (𝒰.f j) (pullback.snd (𝒰.f i) (𝒰.f j))).inv ≫
        pullback.snd (pullback.snd π (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j))) ≫
      pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Nonsingular x y ↔ W.Equation x y ∧ (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)

Tactic:
Nonsingular,

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Equation x y ∧ (evalEval x y W.polynomialX ≠ 0 ∨ evalEval x y W.polynomialY ≠ 0) ↔
    W.Equation x y ∧ (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

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

Tactic:
Nonsingular,

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.Equation x y ∧
      (W'.a₁ * W'.negY x y ≠ 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄ ∨ W'.negY x y ≠ -W'.negY x y - W'.a₁ * x - W'.a₃) ↔
    W'.Nonsingular x y

Tactic:
← negY,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.Equation x y ∧ (W'.a₁ * W'.negY x y ≠ 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄ ∨ W'.negY x y ≠ W'.negY x (W'.negY x y)) ↔
    W'.Nonsingular x y
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
hx : eval (W'.addX x₁ x₂ ℓ) (derivative (W'.addPolynomial x₁ y₁ ℓ)) ≠ 0
⊢ W'.Nonsingular (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)

Tactic:
Nonsingular,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
hx : eval (W'.addX x₁ x₂ ℓ) (derivative (W'.addPolynomial x₁ y₁ ℓ)) ≠ 0
⊢ W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ) ∧
    (evalEval (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ) W'.polynomialX ≠ 0 ∨
      evalEval (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ) W'.polynomialY ≠ 0)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case refine_3
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)
hσ' : ∀ (x : MvPolynomial (Fin m) R), g (σ x) = x
hg' : Surjective ⇑g
S' : ConstructibleSetData (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Finset.image
    (fun x ↦
      match x with
      | { f := fk, n := k, g := gk } =>
        { f := σ fk, n := k + n,
          g := fun s ↦
            Sum.elim (⇑σ ∘ gk) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i)))
              (finSumFinEquiv.symm s) })
    S
s₀ : Set (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Set.range fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))
hs : zeroLocus s₀ = Set.range (comap g)
t : Set (PrimeSpectrum (MvPolynomial (Fin m) R))
⊢ t = comap g ⁻¹' comap σ ⁻¹' t ∩ comap g ⁻¹' Set.range (comap g)

Tactic:
Set.preimage_range,

Goal state after:
case refine_3
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)
hσ' : ∀ (x : MvPolynomial (Fin m) R), g (σ x) = x
hg' : Surjective ⇑g
S' : ConstructibleSetData (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Finset.image
    (fun x ↦
      match x with
      | { f := fk, n := k, g := gk } =>
        { f := σ fk, n := k + n,
          g := fun s ↦
            Sum.elim (⇑σ ∘ gk) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i)))
              (finSumFinEquiv.symm s) })
    S
s₀ : Set (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Set.range fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))
hs : zeroLocus s₀ = Set.range (comap g)
t : Set (PrimeSpectrum (MvPolynomial (Fin m) R))
⊢ t = comap g ⁻¹' comap σ ⁻¹' t ∩ Set.univ