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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
s : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
⊢ ((AlgHom.restrictScalars R (aeval (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x))).comp
          (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R)))).comp
      ↑(tensorEquivSum R (Fin m) (Fin k) R) =
    AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : ↑j < ↑i
a b : ℕ
hab : a + b = ↑j
⊢ a ≠ ↑i

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h✝ : ↑i ≤ ↑j
a b : ℕ
e : a + b = ↑j
h : a = ↑i → ¬b = ↑j - ↑i
⊢ a ≠ ↑i

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin k
j : Fin n
h : ↑j < ↑i
⊢ ∀ (x : ℕ × ℕ),
    x.1 + x.2 = ↑j →
      (if x.2 < k then
          if h : x.1 < m then if x.2 = ↑i then X (Sum.inl ⟨x.1, h⟩) else 0 else if x.1 = m ∧ x.2 = ↑i then 1 else 0
        else 0) =
        0

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin k
j : Fin n
h : ↑i ≤ ↑j
a b : ℕ
a✝² : a + b = ↑j
a✝¹ : ¬(a = ↑j - ↑i ∧ b = ↑i)
a✝ : b < k
⊢ b ≠ ↑i

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
⊢ m + k = n

Tactic:
lia

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝⁴ : QuasiCompact f✝
inst✝³ : QuasiSeparated f✝
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : Smooth g
x : ↥(pullback (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : (pullback.snd (fromNormalization f) g ≫ g) x ∈ ↑U
⊢ ∃ U, x ∈ U ∧ MorphismProperty.isomorphisms Scheme (normalizationPullback f g ∣_ U)

Tactic:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU : V ≤ g ⁻¹ᵁ U⟩ :=
    Y.isBasis_affineOpens.exists_subset_of_mem_open (a := pullback.snd _ g x) hxU (g ⁻¹ᵁ U).2

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝⁴ : QuasiCompact f✝
inst✝³ : QuasiSeparated f✝
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : Smooth g
x : ↥(pullback (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : (pullback.snd (fromNormalization f) g ≫ g) x ∈ ↑U
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : (pullback.snd (fromNormalization f) g) x ∈ ↑V
hVU : V ≤ g ⁻¹ᵁ U
⊢ ∃ U, x ∈ U ∧ MorphismProperty.isomorphisms Scheme (normalizationPullback f g ∣_ U)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
h : f.natDegree = 0
⊢ f.resultant f = 0 ^ f.natDegree

pp: case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
h : ¬f.natDegree = 0
⊢ f.resultant f = 0 ^ f.natDegree

Tactic:
· obtain ⟨r, rfl⟩ := natDegree_eq_zero.mp h; simp

Goal state after:
case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
h : ¬f.natDegree = 0
⊢ f.resultant f = 0 ^ f.natDegree
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H✝ : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this✝ : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
H : (b * g).natDegree < (a * f).natDegree
this : 0 = (a * f).natDegree
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ 1 ≤ g.natDegree

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case Splits.mul
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
g : R[X]
r : R
x y : R[X]
hx : x ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hy : y ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hx' : ((taylor r) x).resultant ((taylor r) g) = x.resultant g
hy' : ((taylor r) y).resultant ((taylor r) g) = y.resultant g
⊢ ((taylor r) (x * y)).resultant ((taylor r) g) = (x * y).resultant g

Tactic:
by_cases hx0 : x = 0

Goal state after:
case pos
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
g : R[X]
r : R
x y : R[X]
hx : x ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hy : y ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hx' : ((taylor r) x).resultant ((taylor r) g) = x.resultant g
hy' : ((taylor r) y).resultant ((taylor r) g) = y.resultant g
hx0 : x = 0
⊢ ((taylor r) (x * y)).resultant ((taylor r) g) = (x * y).resultant g

case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
g : R[X]
r : R
x y : R[X]
hx : x ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hy : y ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hx' : ((taylor r) x).resultant ((taylor r) g) = x.resultant g
hy' : ((taylor r) y).resultant ((taylor r) g) = y.resultant g
hx0 : ¬x = 0
⊢ ((taylor r) (x * y)).resultant ((taylor r) g) = (x * y).resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
h₁ : ↑j ≤ ↑i
h₂ : ¬↑i ≤ ↑j + n
⊢ g.natDegree < ↑i - ↑j

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
h₁ : ↑j ≤ ↑i
h₂ : ¬↑i ≤ ↑j + m
⊢ f.natDegree < ↑i - ↑j

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this✝ : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
H : (b * g).natDegree < (a * f).natDegree
this : 0 = (a * f).natDegree
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 1
⊢ f.natDegree - 1 + f.natDegree = 1

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
⊢ f.natDegree - 1 + f.natDegree ≠ 0

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
this : NeZero (f.natDegree - 1 + f.natDegree)
i : ℕ
hi : i < 1
j : ℕ
hj : j < 1
⊢ i = 0

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
this : NeZero (f.natDegree - 1 + f.natDegree)
j : ℕ
hj : j < 1
hi : 0 < 1
⊢ j = 0

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
⊢ f.natDegree - 1 + f.natDegree = 3

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : 0 < f.natDegree
⊢ f.natDegree = f.natDegree - 1 + 1

Tactic:
lia

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁹ : Nonempty ↥G.left
this✝⁸ : IsProper (G ⊗ G).hom
this✝⁷ : JacobsonSpace ↥(G ⊗ G).left
this✝⁶ : Surjective G.hom
this✝⁵ : IsProper (Over.Hom.left (fst G G))
this✝⁴ : Surjective (Over.Hom.left (fst G G))
this✝³ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
H : ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
⊢ (⇑(pullback.lift (pullback.fst G.hom G.hom) (Over.Hom.left (GrpObj.commutator G)) ⋯) ''
      ⇑(pullback.fst G.hom G.hom) ⁻¹' {(Over.Hom.left η) point}).Finite

Tactic:
exact (Set.finite_singleton _).subset H

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
hVW' : ↑W = (↑V)ᶜ
this✝ : IsClosedImmersion V.ι
this : IsClosedImmersion W.ι
H : IsColimit (BinaryCofan.mk V.ι W.ι)
e : normalization (pullback.snd f fT) ≅ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) :=
  (normalizationCoprodIso (pullback.snd f fT) H).symm ≪≫
    coprod.mapIso (asIso (toNormalization (V.ι ≫ pullback.snd f fT))).symm
      (Iso.refl (normalization (W.ι ≫ pullback.snd f fT)))
ι : ↑V ⟶ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) := coprod.inl
⊢ IsIso ((toNormalization (pullback.snd f fT) ≫ e.hom) ∣_ opensRange ι ≫ (isoOpensRange ι).inv)

Tactic:
have Heq : (pullback.snd f fT).toNormalization ⁻¹ᵁ e.hom ⁻¹ᵁ Scheme.Hom.opensRange ι = V := by
      apply le_antisymm
      · rintro a ⟨b, hab⟩
        by_contra h
        lift a to W using hVW'.ge h
        replace hab : ι b = ((W.ι ≫ pullback.snd f fT).toNormalization ≫ coprod.inr) a := by
          have : W.ι ≫ (H.coconePointUniqueUpToIso (colimit.isColimit _)).hom = coprod.inr :=
            H.comp_coconePointUniqueUpToIso_hom _ ⟨.right⟩
          simp only [← W.ι_apply, ← Scheme.Hom.comp_apply, Category.assoc, e] at hab
          simpa [-Scheme.Hom.comp_base, Scheme.Hom.normalizationCoprodIso,
            reassoc_of% this] using hab
        exact Set.disjoint_iff_forall_ne.mp
          (isCompl_range_inl_inr V (W.ι ≫ pullback.snd f fT).normalization).1 ⟨_, rfl⟩ ⟨_, rfl⟩ hab
      · rw [← Scheme.Hom.inv_image, ← SetLike.coe_subset_coe]
        simpa [← Scheme.Hom.opensRange_comp, ι, e, Scheme.Hom.normalizationCoprodIso,
          Set.range_comp] using Set.subset_preimage_image _ _

Goal state after:
case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
hVW' : ↑W = (↑V)ᶜ
this✝ : IsClosedImmersion V.ι
this : IsClosedImmersion W.ι
H : IsColimit (BinaryCofan.mk V.ι W.ι)
e : normalization (pullback.snd f fT) ≅ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) :=
  (normalizationCoprodIso (pullback.snd f fT) H).symm ≪≫
    coprod.mapIso (asIso (toNormalization (V.ι ≫ pullback.snd f fT))).symm
      (Iso.refl (normalization (W.ι ≫ pullback.snd f fT)))
ι : ↑V ⟶ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) := coprod.inl
Heq : toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι = V
⊢ IsIso ((toNormalization (pullback.snd f fT) ≫ e.hom) ∣_ opensRange ι ≫ (isoOpensRange ι).inv)
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: case refine_3.refine_2
K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁹ : Nonempty ↥G.left
this✝⁸ : IsProper (G ⊗ G).hom
this✝⁷ : JacobsonSpace ↥(G ⊗ G).left
this✝⁶ : Surjective G.hom
this✝⁵ : IsProper (Over.Hom.left (fst G G))
this✝⁴ : Surjective (Over.Hom.left (fst G G))
this✝³ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
H✝¹ :
  ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H✝ : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
H : ∀ (x : ↥U), (⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ)).Finite
y : ↥(G ⊗ G).left
hyU : y ∈ ↑(Over.Hom.left (fst G G) ⁻¹ᵁ U)
hy : IsClosed {y}
hx : IsClosed {(Over.Hom.left (fst G G)) y}
x : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ G := Over.homMk (pointOfClosedPoint G.hom ((Over.Hom.left (fst G G)) y) hx) ⋯
xe : ↥(G ⊗ G).left := (Over.Hom.left (fst G G ≫ (ρ_ G).inv ≫ G ◁ η)) y
⊢ (fst G G ≫ (ρ_ G).inv ≫ G ◁ η) ≫ lift (fst G G) (GrpObj.commutator G) = fst G G ≫ (ρ_ G).inv ≫ G ◁ η

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R✝ R A : CommRingCat
inst✝¹ : Algebra ↑R ↑A
inst✝ : Algebra.FiniteType ↑R ↑A
⊢ LocallyOfFiniteType (Spec A ↘ Spec R)

Tactic:
by
  rw [specOverSpec_over, HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)]
  simpa [RingHom.finiteType_algebraMap]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom ≫
      Spec (of (S ⊗[R] T)) ↘ Spec (of S) =
    pullback (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ↘ Spec (of S)

Tactic:
rw [← cancel_epi (pullbackSymmetry .. ≪≫ pullbackSpecIso' ..).inv,
      Scheme.canonicallyOverPullback_over, Iso.inv_hom_id_assoc, Iso.trans_inv, Category.assoc,
      pullbackSymmetry_inv_comp_snd]

Goal state after:
R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ Spec (of (S ⊗[R] T)) ↘ Spec (of S) =
    (pullbackSpecIso' R S T).inv ≫ pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ Over.Hom.left
        (LaxMonoidal.μ (Over.pullback (Spec.map (ofHom (algebraMap R S)))) (Over.mk (Spec.map (ofHom (algebraMap R T))))
          (Over.mk (Spec.map (ofHom (algebraMap R T))))) ≫
      pullback.fst
        (pullback.fst (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R T))) ≫
          Spec.map (ofHom (algebraMap R T)))
        (Spec.map (ofHom (algebraMap R S))) =
    Over.Hom.left
        (Hom.asOver
            ((pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S)) ⊗ₘ
          Hom.asOver
            ((pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S))) ≫
      (pullbackSpecIso S (S ⊗[R] T) (S ⊗[R] T)).hom ≫
        Spec.map (ofHom (mapRingHom (algebraMap R S) ↑includeRight ↑includeRight ⋯ ⋯)) ≫ (pullbackSpecIso R T T).inv

Tactic:
ext <;> simp

Goal state after:
case h₀
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ pullback.fst (pullback.snd (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))))
        (pullback.snd (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S)))) ≫
      pullback.fst (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))) =
    Over.Hom.left
        (Hom.asOver
            ((pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S)) ⊗ₘ
          Hom.asOver
            ((pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S))) ≫
      (pullbackSpecIso S (S ⊗[R] T) (S ⊗[R] T)).hom ≫
        Spec.map (ofHom (mapRingHom (algebraMap R S) ↑includeRight ↑includeRight ⋯ ⋯)) ≫
          Spec.map (ofHom includeLeftRingHom)

case h₁
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ pullback.snd (pullback.snd (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))))
        (pullback.snd (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S)))) ≫
      pullback.fst (Spec.map (ofHom (algebraMap R T))) (Spec.map (ofHom (algebraMap R S))) =
    Over.Hom.left
        (Hom.asOver
            ((pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S)) ⊗ₘ
          Hom.asOver
            ((pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
              (pullbackSpecIso' R S T).hom)
            (Spec (of S))) ≫
      (pullbackSpecIso S (S ⊗[R] T) (S ⊗[R] T)).hom ≫
        Spec.map (ofHom (mapRingHom (algebraMap R S) ↑includeRight ↑includeRight ⋯ ⋯)) ≫ Spec.map (ofHom ↑includeRight)
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case h.zero.refine_1
R : Type u
S : Type (max u v)
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsPrime
this✝ : IsArtinianRing (p.ResidueField ⊗[R] S)
hpSfin : (p.primesOver S).Finite
IH :
  ∀ m < 0,
    ∀ {R : Type u} {S : Type (max u v)} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
      [Module.Finite R S] (p : Ideal R) [inst_4 : p.IsPrime],
      (p.primesOver S).ncard = m →
        ∃ R' x x_1,
          ∃ (_ : Etale R R'),
            ∃ P,
              ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
                ∃ n e,
                  ∃ (_ : CompleteOrthogonalIdempotents e),
                    ∃ P',
                      ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                        Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                          (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                            ∀ (P'' : Ideal (R' ⊗[R] S)),
                              P''.IsPrime →
                                P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i
h : (p.primesOver S).ncard = 0
this : p.primesOver S = ∅
⊢ Function.Bijective ⇑(Ideal.ResidueField.mapₐ p p (ofId R R) ⋯)

Tactic:
rw! [ofId_self, Ideal.ResidueField.mapₐ_id]

Goal state after:
case h.zero.refine_1
R : Type u
S : Type (max u v)
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsPrime
this✝ : IsArtinianRing (p.ResidueField ⊗[R] S)
hpSfin : (p.primesOver S).Finite
IH :
  ∀ m < 0,
    ∀ {R : Type u} {S : Type (max u v)} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
      [Module.Finite R S] (p : Ideal R) [inst_4 : p.IsPrime],
      (p.primesOver S).ncard = m →
        ∃ R' x x_1,
          ∃ (_ : Etale R R'),
            ∃ P,
              ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
                ∃ n e,
                  ∃ (_ : CompleteOrthogonalIdempotents e),
                    ∃ P',
                      ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                        Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                          (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                            ∀ (P'' : Ideal (R' ⊗[R] S)),
                              P''.IsPrime →
                                P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i
h : (p.primesOver S).ncard = 0
this : p.primesOver S = ∅
⊢ Function.Bijective ⇑(AlgHom.id R p.ResidueField)
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type (max u v)
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsPrime
this✝ : IsArtinianRing (p.ResidueField ⊗[R] S)
hpSfin : (p.primesOver S).Finite
IH :
  ∀ m < 0,
    ∀ {R : Type u} {S : Type (max u v)} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
      [Module.Finite R S] (p : Ideal R) [inst_4 : p.IsPrime],
      (p.primesOver S).ncard = m →
        ∃ R' x x_1,
          ∃ (_ : Etale R R'),
            ∃ P,
              ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
                ∃ n e,
                  ∃ (_ : CompleteOrthogonalIdempotents e),
                    ∃ P',
                      ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                        Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                          (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                            ∀ (P'' : Ideal (R' ⊗[R] S)),
                              P''.IsPrime →
                                P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i
h : (p.primesOver S).ncard = 0
this : p.primesOver S = ∅
P : Ideal (R ⊗[R] S)
h₁ : P.IsPrime
h₂ : P.LiesOver p
⊢ p = Ideal.under R (Ideal.comap TensorProduct.includeRight.toRingHom P)

Tactic:
by simp [P.over_def p, Ideal.under, Ideal.comap_comap]

Goal state after: