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

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 0 < 5
⊢ (if 0 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 0 ∧ 0 ≤ j + 3 then f.coeff (0 - j) else 0
      else if j ≤ 0 + 2 ∧ 0 ≤ j - 2 + 2 then f.coeff (0 - (j - 2) + 1) * (↑(0 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨0, hi⟩

Tactic:
·

Goal state after:
case «0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 0 < 5
⊢ (if 0 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 0 ∧ 0 ≤ j + 3 then f.coeff (0 - j) else 0
      else if j ≤ 0 + 2 ∧ 0 ≤ j - 2 + 2 then f.coeff (0 - (j - 2) + 1) * (↑(0 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨0, hi⟩
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 1 < 5
⊢ (if 1 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 1 ∧ 1 ≤ j + 3 then f.coeff (1 - j) else 0
      else if j ≤ 1 + 2 ∧ 1 ≤ j - 2 + 2 then f.coeff (1 - (j - 2) + 1) * (↑(1 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨1, hi⟩

Tactic:
·

Goal state after:
case «1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 1 < 5
⊢ (if 1 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 1 ∧ 1 ≤ j + 3 then f.coeff (1 - j) else 0
      else if j ≤ 1 + 2 ∧ 1 ≤ j - 2 + 2 then f.coeff (1 - (j - 2) + 1) * (↑(1 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨1, hi⟩
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 2 < 5
⊢ (if 2 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 2 ∧ 2 ≤ j + 3 then f.coeff (2 - j) else 0
      else if j ≤ 2 + 2 ∧ 2 ≤ j - 2 + 2 then f.coeff (2 - (j - 2) + 1) * (↑(2 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨2, hi⟩

Tactic:
·

Goal state after:
case «2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 2 < 5
⊢ (if 2 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 2 ∧ 2 ≤ j + 3 then f.coeff (2 - j) else 0
      else if j ≤ 2 + 2 ∧ 2 ≤ j - 2 + 2 then f.coeff (2 - (j - 2) + 1) * (↑(2 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨2, hi⟩
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 3 < 5
⊢ (if 3 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 3 ∧ 3 ≤ j + 3 then f.coeff (3 - j) else 0
      else if j ≤ 3 + 2 ∧ 3 ≤ j - 2 + 2 then f.coeff (3 - (j - 2) + 1) * (↑(3 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨3, hi⟩

Tactic:
·

Goal state after:
case «3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 3 < 5
⊢ (if 3 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 3 ∧ 3 ≤ j + 3 then f.coeff (3 - j) else 0
      else if j ≤ 3 + 2 ∧ 3 ≤ j - 2 + 2 then f.coeff (3 - (j - 2) + 1) * (↑(3 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨3, hi⟩
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 4 < 5
⊢ (if 4 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 4 ∧ 4 ≤ j + 3 then f.coeff (4 - j) else 0
      else if j ≤ 4 + 2 ∧ 4 ≤ j - 2 + 2 then f.coeff (4 - (j - 2) + 1) * (↑(4 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨4, hi⟩

Tactic:
·

Goal state after:
case «4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 4 < 5
⊢ (if 4 = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ 4 ∧ 4 ≤ j + 3 then f.coeff (4 - j) else 0
      else if j ≤ 4 + 2 ∧ 4 ≤ j - 2 + 2 then f.coeff (4 - (j - 2) + 1) * (↑(4 - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨4, hi⟩
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
F : Cᵒᵖ ⥤ GrpCat
⊢ yonedaGrp.essImage F → (F ⋙ forget GrpCat).IsRepresentable

pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
F : Cᵒᵖ ⥤ GrpCat
⊢ (F ⋙ forget GrpCat).IsRepresentable → yonedaGrp.essImage F

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
F : Cᵒᵖ ⥤ GrpCat
⊢ yonedaGrp.essImage F → (F ⋙ forget GrpCat).IsRepresentable
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
F : Cᵒᵖ ⥤ GrpCat
⊢ (F ⋙ forget GrpCat).IsRepresentable → yonedaGrp.essImage F

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
F : Cᵒᵖ ⥤ GrpCat
⊢ (F ⋙ forget GrpCat).IsRepresentable → yonedaGrp.essImage F
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
G : C
inst✝¹ : GrpObj G
inst✝ : BraidedCategory C
h : ∀ (X : C), IsMulCommutative (X ⟶ G)
⊢ GrpObj.commutator G = toUnit (G ⊗ G) ≫ η

pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
G : C
inst✝¹ : GrpObj G
inst✝ : BraidedCategory C
heq : GrpObj.commutator G = toUnit (G ⊗ G) ≫ η
X : C
f g : X ⟶ G
⊢ f * g = g * f

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
G : C
inst✝¹ : GrpObj G
inst✝ : BraidedCategory C
h : ∀ (X : C), IsMulCommutative (X ⟶ G)
⊢ GrpObj.commutator G = toUnit (G ⊗ G) ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
G : C
inst✝¹ : GrpObj G
inst✝ : BraidedCategory C
heq : GrpObj.commutator G = toUnit (G ⊗ G) ≫ η
X : C
f g : X ⟶ G
⊢ f * g = g * f

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
G : C
inst✝¹ : GrpObj G
inst✝ : BraidedCategory C
heq : GrpObj.commutator G = toUnit (G ⊗ G) ≫ η
X : C
f g : X ⟶ G
⊢ f * g = g * f
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: case 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 (fst G G)) ⁻¹' {(Over.Hom.left η) point} \
      ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}).Nonempty
⊢ IsClosed (⇑(Over.Hom.left (fst G G)) ⁻¹' ⇑(Over.Hom.left η) '' {point})

Tactic:
·

Goal state after:
case 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 (fst G G)) ⁻¹' {(Over.Hom.left η) point} \
      ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}).Nonempty
⊢ IsClosed (⇑(Over.Hom.left (fst G G)) ⁻¹' ⇑(Over.Hom.left η) '' {point})
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case refine_1
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
⊢ ι v = e.hom ((toNormalization (pullback.snd f fT)) ↑v)

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 ι)

Tactic:
·

Goal state after:
case refine_1
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
⊢ ι v = e.hom ((toNormalization (pullback.snd f fT)) ↑v)
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case a
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) := ⋯
ι : ↑V ⟶ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) := ⋯
⊢ toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι ≤ V

pp: case a
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) := ⋯
ι : ↑V ⟶ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) := ⋯
⊢ V ≤ toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι

Tactic:
·

Goal state after:
case a
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) := ⋯
ι : ↑V ⟶ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) := ⋯
⊢ toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι ≤ V
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case a
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) := ⋯
ι : ↑V ⟶ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) := ⋯
⊢ V ≤ toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι

Tactic:
·

Goal state after:
case a
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) := ⋯
ι : ↑V ⟶ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) := ⋯
⊢ V ≤ toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι
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
U : (normalization (pullback.snd f fT)).Opens
hU : (toNormalization (pullback.snd f fT)) ↑v ∈ U
right✝ : IsIso (toNormalization (pullback.snd f fT) ∣_ U)
fTn : normalization (pullback.snd f fT) ⟶ normalization f :=
  normalizationPullback f fT ≫ pullback.fst (fromNormalization f) fT
U' : (normalization f).Opens := { carrier := ⇑fTn '' U.carrier, is_open' := ⋯ }
fTnU : ↑U ⟶ ↑U' := resLE fTn U' U ⋯
this : Surjective fTnU
H : toNormalization (pullback.snd f fT) ⁻¹ᵁ U ≤ pullback.fst f fT ⁻¹ᵁ toNormalization f ⁻¹ᵁ U'
⊢ toNormalization (pullback.snd f fT) ∣_ U ≫ fTnU =
    resLE (pullback.fst f fT) (toNormalization f ⁻¹ᵁ U') (toNormalization (pullback.snd f fT) ⁻¹ᵁ U) H ≫
      toNormalization f ∣_ U'

Tactic:
·

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
U : (normalization (pullback.snd f fT)).Opens
hU : (toNormalization (pullback.snd f fT)) ↑v ∈ U
right✝ : IsIso (toNormalization (pullback.snd f fT) ∣_ U)
fTn : normalization (pullback.snd f fT) ⟶ normalization f :=
  normalizationPullback f fT ≫ pullback.fst (fromNormalization f) fT
U' : (normalization f).Opens := { carrier := ⇑fTn '' U.carrier, is_open' := ⋯ }
fTnU : ↑U ⟶ ↑U' := resLE fTn U' U ⋯
this : Surjective fTnU
H : toNormalization (pullback.snd f fT) ⁻¹ᵁ U ≤ pullback.fst f fT ⁻¹ᵁ toNormalization f ⁻¹ᵁ U'
⊢ toNormalization (pullback.snd f fT) ∣_ U ≫ fTnU =
    resLE (pullback.fst f fT) (toNormalization f ⁻¹ᵁ U') (toNormalization (pullback.snd f fT) ⁻¹ᵁ U) H ≫
      toNormalization f ∣_ U'
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
W : TopologicalSpace.Opens ↥X
hW : W ∈ X.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ toNormalization f ⁻¹ᵁ V y
this : IsAffine ↑W
⊢ ∃ U r,
    IsAffineOpen U ∧
      IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r) ∧
        x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r ∧ (normalization f).basicOpen r ≤ V y

Tactic:
let V' := (X.homOfLE hWV ≫ f.toNormalization ∣_ V y ≫ (V y).ι).opensRange

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
W : TopologicalSpace.Opens ↥X
hW : W ∈ X.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ toNormalization f ⁻¹ᵁ V y
this : IsAffine ↑W
V' : (normalization f).Opens := opensRange (X.homOfLE hWV ≫ toNormalization f ∣_ V y ≫ (V y).ι)
⊢ ∃ U r,
    IsAffineOpen U ∧
      IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r) ∧
        x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r ∧ (normalization f).basicOpen r ≤ V y