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

Goal state before:
pp: case succ.e_a.e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ f.sylvester g (m + 1) (n + 1) (Fin.last (m + 1 + n)) (Fin.castAdd (n + 1) (Fin.last m)) = g.coeff (n + 1)

Tactic:
simp only [sylvester, Set.mem_Icc, Matrix.of_apply, Fin.val_last, Fin.addCases_left]

Goal state after:
case succ.e_a.e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ (if m ≤ m + 1 + n ∧ m + 1 + n ≤ m + (n + 1) then g.coeff (m + 1 + n - m) else 0) = g.coeff (n + 1)
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
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
this :
  (algebraMap K L) ((f %ₘ g).leadingCoeff⁻¹ ^ g.natDegree) *
      (algebraMap K L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)).prod
⊢ f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod

Tactic:
inv_pow,

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
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
this :
  (algebraMap K L) ((f %ₘ g).leadingCoeff ^ g.natDegree)⁻¹ *
      (algebraMap K L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)).prod
⊢ f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
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₂
U : (directedCover Y).I₀
⊢ colimit.ι (normalizationGlueData f).functor U ≫
      colimit.desc (normalizationGlueData f).functor
          { pt := T,
            ι :=
              {
                app := fun U ↦
                  Spec.map
                      (CommRingCat.ofHom
                        ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ U.toOpens) ⋯)).codRestrict
                          (integralClosure ↑Γ(Y, U.toOpens) ↑Γ(X, f ⁻¹ᵁ U.toOpens)) ⋯)) ≫
                    ⋯.fromSpec,
                naturality := ⋯ } } ≫
        f₂ =
    colimit.ι (normalizationGlueData f).functor U ≫ (normalizationGlueData f).toBase

Tactic:
colimit.ι_desc_assoc,

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₂
U : (directedCover Y).I₀
⊢ { pt := T,
              ι :=
                {
                  app := fun U ↦
                    Spec.map
                        (CommRingCat.ofHom
                          ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ U.toOpens) ⋯)).codRestrict
                            (integralClosure ↑Γ(Y, U.toOpens) ↑Γ(X, f ⁻¹ᵁ U.toOpens)) ⋯)) ≫
                      ⋯.fromSpec,
                  naturality := ⋯ } }.ι.app
        U ≫
      f₂ =
    colimit.ι (normalizationGlueData f).functor U ≫ (normalizationGlueData f).toBase
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:
exact hkP' (Ideal.ker_le_comap _)

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

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
this✝ :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (f g : R[X]) (n : ℕ),
    g.natDegree ≤ n →
      f.Splits →
        IsField R →
          f.Monic → ¬g = 0 → g.Monic → f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod
hgm : ¬g.Monic
inst : Field R := hR.toField
this :
  g.leadingCoeff⁻¹ ^ f.natDegree * f.resultant g f.natDegree n =
    (Multiset.map (fun x ↦ eval x (C g.leadingCoeff⁻¹ * g)) f.roots).prod
⊢ f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod

Tactic:
inv_pow,

Goal state after:
case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
this✝ :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (f g : R[X]) (n : ℕ),
    g.natDegree ≤ n →
      f.Splits →
        IsField R →
          f.Monic → ¬g = 0 → g.Monic → f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod
hgm : ¬g.Monic
inst : Field R := hR.toField
this :
  (g.leadingCoeff ^ f.natDegree)⁻¹ * f.resultant g f.natDegree n =
    (Multiset.map (fun x ↦ eval x (C g.leadingCoeff⁻¹ * g)) f.roots).prod
⊢ f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

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

pp: case inr.h₀
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : ↑i ≤ ↑j
⊢ ∀ b ∈ Finset.antidiagonal ↑j,
    b ≠ (↑i, ↑j - ↑i) →
      (if h : b.2 < k then if b.1 < m ∧ b.1 = ↑i then X (Sum.inr ⟨b.2, h⟩) else 0
        else if b.2 = k ∧ b.1 < m ∧ b.1 = ↑i then 1 else 0) =
        0

pp: case inr.h₁
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : ↑i ≤ ↑j
⊢ (↑i, ↑j - ↑i) ∉ Finset.antidiagonal ↑j →
    (if h : (↑i, ↑j - ↑i).2 < k then
        if (↑i, ↑j - ↑i).1 < m ∧ (↑i, ↑j - ↑i).1 = ↑i then X (Sum.inr ⟨(↑i, ↑j - ↑i).2, h⟩) else 0
      else if (↑i, ↑j - ↑i).2 = k ∧ (↑i, ↑j - ↑i).1 < m ∧ (↑i, ↑j - ↑i).1 = ↑i then 1 else 0) =
      0

Tactic:
if_neg h.not_gt

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : ↑i ≤ ↑j
⊢ (if h : (↑i, ↑j - ↑i).2 < k then
      if (↑i, ↑j - ↑i).1 < m ∧ (↑i, ↑j - ↑i).1 = ↑i then X (Sum.inr ⟨(↑i, ↑j - ↑i).2, h⟩) else 0
    else if (↑i, ↑j - ↑i).2 = k ∧ (↑i, ↑j - ↑i).1 < m ∧ (↑i, ↑j - ↑i).1 = ↑i then 1 else 0) =
    if h : ↑j - ↑i < k then X (Sum.inr ⟨↑j - ↑i, h⟩) else if ↑j - ↑i = k then 1 else 0

case inr.h₀
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : ↑i ≤ ↑j
⊢ ∀ b ∈ Finset.antidiagonal ↑j,
    b ≠ (↑i, ↑j - ↑i) →
      (if h : b.2 < k then if b.1 < m ∧ b.1 = ↑i then X (Sum.inr ⟨b.2, h⟩) else 0
        else if b.2 = k ∧ b.1 < m ∧ b.1 = ↑i then 1 else 0) =
        0

case inr.h₁
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : ↑i ≤ ↑j
⊢ (↑i, ↑j - ↑i) ∉ Finset.antidiagonal ↑j →
    (if h : (↑i, ↑j - ↑i).2 < k then
        if (↑i, ↑j - ↑i).1 < m ∧ (↑i, ↑j - ↑i).1 = ↑i then X (Sum.inr ⟨(↑i, ↑j - ↑i).2, h⟩) else 0
      else if (↑i, ↑j - ↑i).2 = k ∧ (↑i, ↑j - ↑i).1 < m ∧ (↑i, ↑j - ↑i).1 = ↑i then 1 else 0) =
      0
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

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

pp: case inr.h₀
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin k
j : Fin n
h : ↑i ≤ ↑j
⊢ ∀ b ∈ Finset.antidiagonal ↑j,
    b ≠ (↑j - ↑i, ↑i) →
      (if b.2 < k then
          if h : b.1 < m then if b.2 = ↑i then X (Sum.inl ⟨b.1, h⟩) else 0 else if b.1 = m ∧ b.2 = ↑i then 1 else 0
        else 0) =
        0

pp: case inr.h₁
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin k
j : Fin n
h : ↑i ≤ ↑j
⊢ (↑j - ↑i, ↑i) ∉ Finset.antidiagonal ↑j →
    (if (↑j - ↑i, ↑i).2 < k then
        if h : (↑j - ↑i, ↑i).1 < m then if (↑j - ↑i, ↑i).2 = ↑i then X (Sum.inl ⟨(↑j - ↑i, ↑i).1, h⟩) else 0
        else if (↑j - ↑i, ↑i).1 = m ∧ (↑j - ↑i, ↑i).2 = ↑i then 1 else 0
      else 0) =
      0

Tactic:
if_neg h.not_gt

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

case inr.h₀
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin k
j : Fin n
h : ↑i ≤ ↑j
⊢ ∀ b ∈ Finset.antidiagonal ↑j,
    b ≠ (↑j - ↑i, ↑i) →
      (if b.2 < k then
          if h : b.1 < m then if b.2 = ↑i then X (Sum.inl ⟨b.1, h⟩) else 0 else if b.1 = m ∧ b.2 = ↑i then 1 else 0
        else 0) =
        0

case inr.h₁
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin k
j : Fin n
h : ↑i ≤ ↑j
⊢ (↑j - ↑i, ↑i) ∉ Finset.antidiagonal ↑j →
    (if (↑j - ↑i, ↑i).2 < k then
        if h : (↑j - ↑i, ↑i).1 < m then if (↑j - ↑i, ↑i).2 = ↑i then X (Sum.inl ⟨(↑j - ↑i, ↑i).1, h⟩) else 0
        else if (↑j - ↑i, ↑i).1 = m ∧ (↑j - ↑i, ↑i).2 = ↑i then 1 else 0
      else 0) =
      0
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
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : g.natDegree = 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

pp: case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
· obtain ⟨a, rfl⟩ := natDegree_eq_zero.mp hg0; 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
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.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
⊢ f.sylvesterMap g hf hg ∘ₗ f.adjSylvester g = f.resultant g m n • LinearMap.id

Tactic:
let b₁ := ((degreeLT.basis R m).prod (degreeLT.basis R n)).reindex finSumFinEquiv

Goal state after:
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
b₁ : Module.Basis (Fin (m + n)) R (↥R[X]_m × ↥R[X]_n) :=
  ((degreeLT.basis R m).prod (degreeLT.basis R n)).reindex finSumFinEquiv
⊢ f.sylvesterMap g hf hg ∘ₗ f.adjSylvester g = f.resultant g m n • LinearMap.id
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
⊢ f.adjSylvester g ∘ₗ f.sylvesterMap g hf hg = f.resultant g m n • LinearMap.id

Tactic:
let b₁ := ((degreeLT.basis R m).prod (degreeLT.basis R n)).reindex finSumFinEquiv

Goal state after:
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
b₁ : Module.Basis (Fin (m + n)) R (↥R[X]_m × ↥R[X]_n) :=
  ((degreeLT.basis R m).prod (degreeLT.basis R n)).reindex finSumFinEquiv
⊢ f.adjSylvester g ∘ₗ f.sylvesterMap g hf hg = f.resultant g m n • LinearMap.id
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f g : K[X]
⊢ f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g

Tactic:
obtain rfl | hf := eq_or_ne f 0
  · obtain rfl | hg := eq_or_ne g 0; · simp
    simpa [isCoprime_zero_left, isUnit_iff, hg, natDegree_eq_zero] using
      show (∀ x, C x ≠ g) ↔ ∀ x ≠ 0, C x ≠ g by aesop
  have H : (C f.leadingCoeff⁻¹ * f).Monic := by
    rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simpa), coeff_C_mul]; simp [hf]
  have := isUnit_resultant_iff_isCoprime (f := C f.leadingCoeff⁻¹ * f) (g := g) H
  rw [resultant_C_mul_left, IsUnit.mul_iff, natDegree_C_mul (by simp [hf]),
    isCoprime_mul_unit_left_left (isUnit_C.mpr (by simp [hf]))] at this
  simp [← this, hf]

Goal state after:
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
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

Tactic:
have hV' : IsAffineOpen V' := isAffineOpen_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).ι)
hV' : IsAffineOpen V'
⊢ ∃ U r,
    IsAffineOpen U ∧
      IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r) ∧
        x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r ∧ (normalization f).basicOpen r ≤ V y
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Extension R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
t : T
s : S
x : Ω[P.Ring⁄R]
⊢ (AlgebraTensorModule.congr (LinearEquiv.refl P.baseChange.Ring (T ⊗[R] S))
        (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring P.baseChange.Ring))
      ((AlgebraTensorModule.cancelBaseChange P.Ring P.baseChange.Ring P.baseChange.Ring (T ⊗[R] S) Ω[P.Ring⁄R]).symm
        (((TensorProduct.mk R T S) t) s ⊗ₜ[P.Ring] x)) =
    t ⊗ₜ[R] s ⊗ₜ[P.baseChange.Ring] (KaehlerDifferential.map R T P.Ring P.baseChange.Ring) x

Tactic:
simp only [mk_apply, AlgebraTensorModule.cancelBaseChange_symm_tmul,
    AlgebraTensorModule.congr_tmul, LinearEquiv.refl_apply]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Extension R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
t : T
s : S
x : Ω[P.Ring⁄R]
⊢ t ⊗ₜ[R] s ⊗ₜ[P.baseChange.Ring]
      (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring P.baseChange.Ring) (1 ⊗ₜ[P.Ring] x) =
    t ⊗ₜ[R] s ⊗ₜ[P.baseChange.Ring] (KaehlerDifferential.map R T P.Ring P.baseChange.Ring) x
Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent

Goal state before:
pp: X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝ : IsNoetherian X
⊢ Z = closure ↑(X.irreducibleComponentOpen Z)

Tactic:
exact (closure_sUnion_irreducibleComponents_sdiff_singleton
      TopologicalSpace.NoetherianSpace.finite_irreducibleComponents Z hZ).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: X : Scheme
P✝ : MorphismProperty Scheme
inst✝⁹ : IsZariskiLocalAtSource P✝
S : Scheme
J : Type u_1
inst✝⁸ : Category.{v_1, u_1} J
F : J ⥤ P✝.Over ⊤ S
inst✝⁷ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝⁶ : (F ⋙ MorphismProperty.Over.forget P✝ ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝⁵ : Quiver.IsThin J
inst✝⁴ : Small.{u, u_1} J
P : MorphismProperty Scheme
inst✝³ : IsZariskiLocalAtSource P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.HasOfPostcompProperty P
inst✝ : P.IsMultiplicative
n : ℕ
⊢ HasColimitsOfShape (Discrete (Fin n)) (P.CostructuredArrow ⊤ Scheme.Spec S)

Tactic:
by
    have : (MorphismProperty.commaObj Scheme.Spec (.fromPUnit S) P).IsClosedUnderColimitsOfShape
        (Discrete (Fin n)) :=
      IsZariskiLocalAtSource.isClosedUnderColimitsOfShape_discrete _ _
    apply MorphismProperty.Comma.hasColimitsOfShape_of_closedUnderColimitsOfShape

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
η₁ : f ⟶ 𝟙 a ≫ g
η₂ : 𝟙 a ≫ f ⟶ 𝟙 a ≫ g
e_η₁ : η ≫ (λ_ g).inv = η₁
e_η₂ : (λ_ f).hom ≫ η₁ = η₂
⊢ 𝟙 a ◁ η = η₂

Tactic:
by
  simp [e_η₁, e_η₂]

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

Goal state before:
pp: R✝ R A : CommRingCat
X M G : Scheme
inst✝² : M.Over (Spec R)
inst✝¹ : MonObj (M.asOver (Spec R))
inst✝ : IsAffine M
this✝ : MonObj ((algSpec R).obj (op (CommAlgCat.of ↑R ↑Γ(M, ⊤))))
this : MonObj (op (CommAlgCat.of ↑R ↑Γ(M, ⊤)))
⊢ Bialgebra ↑R ↑Γ(M, ⊤)

Tactic:
exact ((commBialgCatEquivComonCommAlgCat R).inverse.obj <|
    .op <| .mk <| .op <| .of R Γ(M, ⊤)).bialgebra

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
η₁ : f ⟶ g ≫ 𝟙 b
η₂ : f ≫ 𝟙 b ⟶ g ≫ 𝟙 b
e_η₁ : η ≫ (ρ_ g).inv = η₁
e_η₂ : (ρ_ f).hom ≫ η₁ = η₂
⊢ η ▷ 𝟙 b = η₂

Tactic:
by
  simp [e_η₁, e_η₂]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ α ▷ r₂ ▷ g₂ ⊗≫
          (adj₁.counit ▷ (h₁ ≫ r₂ ≫ g₂ ≫ 𝟙 e) ≫ 𝟙 b ◁ h₁ ◁ r₂ ◁ g₂ ◁ adj₃.unit) ⊗≫
            h₁ ◁ r₂ ◁ β ▷ r₃ ⊗≫ h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ 𝟙 e) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ g₂ ◁ adj₃.unit) ⊗≫
          (adj₁.counit ▷ (h₁ ≫ r₂) ▷ (g₂ ≫ l₃) ≫ (𝟙 b ≫ h₁ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
            h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)

Tactic:
by
      rw [← whisker_exchange]
      bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
r₁ : b ⟶ a
r₂ : c ⟶ b
r₃ : e ⟶ d
r₄ : f ⟶ e
r₅ : y ⟶ x
r₆ : z ⟶ y
α : r₁ ≫ g₁ ⟶ h₁ ≫ r₃
β : r₂ ≫ h₁ ⟶ k₁ ≫ r₄
γ : r₃ ≫ g₂ ⟶ h₂ ≫ r₅
δ : r₄ ≫ h₂ ⟶ k₂ ≫ r₆
⊢ 𝟙 ((r₂ ≫ r₁) ≫ g₁ ≫ g₂) ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ (β ▷ (r₃ ≫ g₂) ≫ (k₁ ≫ r₄) ◁ γ) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 ((k₁ ≫ k₂) ≫ r₆ ≫ r₅) =
    (α_ r₂ r₁ (g₁ ≫ g₂)).hom ≫
      r₂ ◁ ((α_ r₁ g₁ g₂).inv ≫ α ▷ g₂ ≫ (α_ h₁ r₃ g₂).hom ≫ h₁ ◁ γ ≫ (α_ h₁ h₂ r₅).inv) ≫
        (α_ r₂ (h₁ ≫ h₂) r₅).inv ≫
          ((α_ r₂ h₁ h₂).inv ≫ β ▷ h₂ ≫ (α_ k₁ r₄ h₂).hom ≫ k₁ ◁ δ ≫ (α_ k₁ k₂ r₆).inv) ▷ r₅ ≫ (α_ (k₁ ≫ k₂) r₆ r₅).hom

Tactic:
by
      rw [← whisker_exchange]
      bicategory

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case convert_4.mem
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ n, f i ∈ 𝒜 n
hf : Algebra.adjoin (↥(𝒜 0)) (Set.range f) = ⊤
x : A
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
⊢ f i - (GradedRing.projZeroRingHom 𝒜) (f i) ∈ Ideal.span (Set.range f)

Tactic:
GradedRing.projZeroRingHom_apply

Goal state after:
case convert_4.mem
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ n, f i ∈ 𝒜 n
hf : Algebra.adjoin (↥(𝒜 0)) (Set.range f) = ⊤
x : A
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
⊢ f i - ↑(((DirectSum.decompose 𝒜) (f i)) 0) ∈ Ideal.span (Set.range f)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case exists_of_eq
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
k : ℕ
hc : ↑⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ * (x ^ m * (a * g ^ n)) = ↑⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ * (x ^ n * (b * g ^ m))
⊢ ∃ c, ↑c * Away.mk 𝒜 hf n a ha = ↑c * Away.mk 𝒜 hf m b hb

Tactic:
refine ⟨⟨_, k + m + n, rfl⟩, ?_⟩

Goal state after:
case exists_of_eq
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
k : ℕ
hc : ↑⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ * (x ^ m * (a * g ^ n)) = ↑⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ * (x ^ n * (b * g ^ m))
⊢ ↑⟨(fun x ↦ isLocalizationElem hf hg ^ x) (k + m + n), ⋯⟩ * Away.mk 𝒜 hf n a ha =
    ↑⟨(fun x ↦ isLocalizationElem hf hg ^ x) (k + m + n), ⋯⟩ * Away.mk 𝒜 hf m b hb