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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
j₁ : Fin (m + n)
i : Fin n
IH : ↑(Fin.natAdd m i) ≤ m → (M ↑(Fin.natAdd m i)).det = M₂.det
hi : m + ↑i + 1 ≤ m
⊢ m + ↑i + (k + m) = m + (↑i + (k + m))

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
j₁ : Fin (m + n)
i : Fin n
IH : ↑(Fin.natAdd m i) ≤ m → (M ↑(Fin.natAdd m i)).det = M₂.det
hi : m + ↑i + 1 ≤ m
⊢ m + ↑i + (k + m) = m + (↑i + (k + m))
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (C r * g) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
hi : 0 ≤ m
⊢ (Matrix.of fun j₁ j₂ ↦ M₂ j₁ j₂).det = M₂.det

Tactic:
;

Goal state after:
case zero
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (C r * g) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
hi : 0 ≤ m
⊢ (Matrix.of fun j₁ j₂ ↦ M₂ j₁ j₂).det = M₂.det
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ (f.sylvester g (m + 1) (n + 1)).det = (-1) ^ (n + 1) * g.coeff (n + 1) * f.resultant g m (n + 1)

Tactic:
Matrix.det_succ_row (i := .last _),

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ ∑ j,
      (-1) ^ (↑(Fin.last ((m + 1).add n)) + ↑j) * f.sylvester g (m + 1) (n + 1) (Fin.last ((m + 1).add n)) j *
        ((f.sylvester g (m + 1) (n + 1)).submatrix (Fin.last ((m + 1).add n)).succAbove j.succAbove).det =
    (-1) ^ (n + 1) * g.coeff (n + 1) * f.resultant g m (n + 1)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ m + 1 + n + m = 2 * m + (n + 1)

Tactic:
;

Goal state after:
case e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ m + 1 + n + m = 2 * m + (n + 1)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin m
⊢ ↑((Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.castAdd (n + 1) j))) =
    ↑(Fin.castAdd (n + 1) j.castSucc)

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin m
⊢ ↑((Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.castAdd (n + 1) j))) =
    ↑(Fin.castAdd (n + 1) j.castSucc)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin (n + 1)
⊢ ↑((Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j))) = ↑(Fin.natAdd (m + 1) j)

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin (n + 1)
⊢ ↑((Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j))) = ↑(Fin.natAdd (m + 1) j)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n k✝ : ℕ
hf : f.natDegree ≤ m
k : ℕ
IH : f.resultant g (m + k) n = (-1) ^ (n * k) * g.coeff n ^ k * f.resultant g m n
⊢ (-1) ^ n * g.coeff n * ((-1) ^ (n * k) * g.coeff n ^ k * f.resultant g m n) =
    (-1) ^ (n * (k + 1)) * g.coeff n ^ (k + 1) * f.resultant g m n

Tactic:
;

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n k✝ : ℕ
hf : f.natDegree ≤ m
k : ℕ
IH : f.resultant g (m + k) n = (-1) ^ (n * k) * g.coeff n ^ k * f.resultant g m n
⊢ (-1) ^ n * g.coeff n * ((-1) ^ (n * k) * g.coeff n ^ k * f.resultant g m n) =
    (-1) ^ (n * (k + 1)) * g.coeff n ^ (k + 1) * f.resultant g m n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
f g : R[X]
n : ℕ
hg : g.natDegree < n
hf : f.natDegree < 0
⊢ f.resultant g 0 n = 0

pp: case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
n : ℕ
hg : g.natDegree < n
m : ℕ
hf : f.natDegree < m + 1
⊢ f.resultant g (m + 1) n = 0

Tactic:
;

Goal state after:
case zero
R : Type u_1
inst✝ : CommRing R
f g : R[X]
n : ℕ
hg : g.natDegree < n
hf : f.natDegree < 0
⊢ f.resultant g 0 n = 0

case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
n : ℕ
hg : g.natDegree < n
m : ℕ
hf : f.natDegree < m + 1
⊢ f.resultant g (m + 1) n = 0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree < m + 1
hg : g.natDegree < 0
⊢ f.resultant g (m + 1) 0 = 0

pp: case succ.succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree < m + 1
n : ℕ
hg : g.natDegree < n + 1
⊢ f.resultant g (m + 1) (n + 1) = 0

Tactic:
;

Goal state after:
case succ.zero
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree < m + 1
hg : g.natDegree < 0
⊢ f.resultant g (m + 1) 0 = 0

case succ.succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree < m + 1
n : ℕ
hg : g.natDegree < n + 1
⊢ f.resultant g (m + 1) (n + 1) = 0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree < m + 1
n : ℕ
hg : g.natDegree < n + 1
⊢ (-1) ^ ((n + 1) * 1) * g.coeff (n + 1) ^ 1 * f.resultant g m (n + 1) = 0

Tactic:
resultant_add_right_deg _ _ _ _ _ (by lia)

Goal state after:
case succ.succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree < m + 1
n : ℕ
hg : g.natDegree < n + 1
⊢ (-1) ^ ((n + 1) * 1) * g.coeff (n + 1) ^ 1 * (f.coeff m ^ 1 * f.resultant g m n) = 0
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
this✝ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this : IsIso (app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U))
⊢ ⊤ = (Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑⟨U, hU⟩)) ≫ IsAffineOpen.fromSpec ⋯) ⁻¹ᵁ U

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
this✝ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this : IsIso (app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U))
⊢ ⊤ = (Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑⟨U, hU⟩)) ≫ IsAffineOpen.fromSpec ⋯) ⁻¹ᵁ U
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
H : ¬g.natDegree = 0
⊢ 0 ^ g.natDegree * g.coeff 0 ^ (g * r).natDegree =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)).prod

Tactic:
simp only [zero_pow H]

Goal state after:
case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
H : ¬g.natDegree = 0
⊢ 0 * g.coeff 0 ^ (g * r).natDegree = (Multiset.map (fun ij ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)).prod
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr✝ : ¬g ∣ f
r : K[X] := C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
⊢ g.natDegree + r.natDegree < n

Tactic:
;

Goal state after:
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr✝ : ¬g ∣ f
r : K[X] := C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
⊢ g.natDegree + r.natDegree < n
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case refine_2.inl
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
m : S → ℕ
a : S
hrp : a ∉ p
hr : IsIntegral R a
hm : ∀ (x : S), IsIntegral R (a ^ m x * x)
t : Set S := insert a {x | ∃ x_1 ∈ s, a ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨a, ⋯⟩
⊢ IsIntegral R a

pp: case refine_2.inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
x : S
hx : x ∈ s
⊢ IsIntegral R (r ^ m x * x)

Tactic:
;

Goal state after:
case refine_2.inl
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
m : S → ℕ
a : S
hrp : a ∉ p
hr : IsIntegral R a
hm : ∀ (x : S), IsIntegral R (a ^ m x * x)
t : Set S := insert a {x | ∃ x_1 ∈ s, a ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨a, ⋯⟩
⊢ IsIntegral R a

case refine_2.inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
x : S
hx : x ∈ s
⊢ IsIntegral R (r ^ m x * x)
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case refine_2.inl
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
m : S → ℕ
a : S
hrp : a ∉ p
hr : IsIntegral R a
hm : ∀ (x : S), IsIntegral R (a ^ m x * x)
t : Set S := insert a {x | ∃ x_1 ∈ s, a ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨a, ⋯⟩
⊢ IsIntegral R a

pp: case refine_2.inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
x : S
hx : x ∈ s
⊢ IsIntegral R (r ^ m x * x)

Tactic:
exacts [hr, hm _]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Over

Goal state before:
pp: case refine_2
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
f : S →ₐ[R] T
Hf : Function.Surjective ⇑f
P : Ideal R
H : (P.primesOver S).Finite
q : Ideal T
left✝ : q.IsPrime
right✝ : q.LiesOver P
inst✝¹ : (comap f q).IsPrime
inst✝ : (comap f q).LiesOver P
hkP' : ¬RingHom.ker f.toRingHom ≤ comap f q
⊢ False

Tactic:
;

Goal state after:
case refine_2
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
f : S →ₐ[R] T
Hf : Function.Surjective ⇑f
P : Ideal R
H : (P.primesOver S).Finite
q : Ideal T
left✝ : q.IsPrime
right✝ : q.LiesOver P
inst✝¹ : (comap f q).IsPrime
inst✝ : (comap f q).LiesOver P
hkP' : ¬RingHom.ker f.toRingHom ≤ comap f q
⊢ False
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
⊢ IsIntegralHom (fromNormalization f)

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
⊢ IsIntegralHom (fromNormalization f)
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝¹ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝ : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
⊢ (Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑U)) ≫ IsAffineOpen.fromSpec ⋯) ⁻¹ᵁ ↑U = ⊤

Tactic:
;

Goal state after:
case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝¹ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝ : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
⊢ (Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑U)) ≫ IsAffineOpen.fromSpec ⋯) ⁻¹ᵁ ↑U = ⊤
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝¹ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝ : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
⊢ (Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑U)) ≫ IsAffineOpen.fromSpec ⋯) ⁻¹ᵁ ↑U = ⊤

Tactic:
;

Goal state after:
case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝¹ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝ : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
⊢ (Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑U)) ≫ IsAffineOpen.fromSpec ⋯) ⁻¹ᵁ ↑U = ⊤
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝¹ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝ : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
⊢ f ⁻¹ᵁ ↑U ≤ f ⁻¹ᵁ ↑U

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝¹ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝ : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
⊢ f ⁻¹ᵁ ↑U ≤ f ⁻¹ᵁ ↑U
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case mk
R : Type u_1
inst✝ : CommRing R
n k : ℕ
h : ¬k < n
val✝ : ℕ
isLt✝ : val✝ < n
x✝ : ⟨val✝, isLt✝⟩ ∈ Finset.univ
⊢ ¬k = ↑⟨val✝, isLt✝⟩

Tactic:
;

Goal state after:
case mk
R : Type u_1
inst✝ : CommRing R
n k : ℕ
h : ¬k < n
val✝ : ℕ
isLt✝ : val✝ < n
x✝ : ⟨val✝, isLt✝⟩ ∈ Finset.univ
⊢ ¬k = ↑⟨val✝, isLt✝⟩
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
f : MvPolynomial (Fin n) R →ₐ[R] S
i : Fin n
⊢ ((fun p ↦ aeval fun x ↦ (↑p).coeff ↑x) ((fun f ↦ (MonicDegreeEq.freeMonic R n).map f.toRingHom) f)) (X i) = f (X i)

Tactic:
;

Goal state after:
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
f : MvPolynomial (Fin n) R →ₐ[R] S
i : Fin n
⊢ ((fun p ↦ aeval fun x ↦ (↑p).coeff ↑x) ((fun f ↦ (MonicDegreeEq.freeMonic R n).map f.toRingHom) f)) (X i) = f (X i)
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
p : MonicDegreeEq S n
this : ∀ i ≥ n, (if i = n then 1 else 0) = (↑p).coeff i
i : ℕ
⊢ (↑((fun f ↦ (MonicDegreeEq.freeMonic R n).map f.toRingHom) ((fun p ↦ aeval fun x ↦ (↑p).coeff ↑x) p))).coeff i =
    (↑p).coeff i

Tactic:
;

Goal state after:
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
p : MonicDegreeEq S n
this : ∀ i ≥ n, (if i = n then 1 else 0) = (↑p).coeff i
i : ℕ
⊢ (↑((fun f ↦ (MonicDegreeEq.freeMonic R n).map f.toRingHom) ((fun p ↦ aeval fun x ↦ (↑p).coeff ↑x) p))).coeff i =
    (↑p).coeff i
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case a.convert_2.add
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom (↑(universalFactorizationMap R n m k hn)) (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x)
H : ∀ (i : Fin m ⊕ Fin k), (tensorEquivSum R (Fin m) (Fin k) R) (f (X i)) = X i
p q : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)
a✝¹ :
  p - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f p)) ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))
a✝ :
  q - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f q)) ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))
⊢ p - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f p)) +
      (q - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f q))) ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))

Tactic:
;

Goal state after:
case a.convert_2.add
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom (↑(universalFactorizationMap R n m k hn)) (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x)
H : ∀ (i : Fin m ⊕ Fin k), (tensorEquivSum R (Fin m) (Fin k) R) (f (X i)) = X i
p q : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)
a✝¹ :
  p - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f p)) ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))
a✝ :
  q - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f q)) ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))
⊢ p - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f p)) +
      (q - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f q))) ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))