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

Goal state before:
pp: case inl.right
R : Type u_1
inst✝ : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i : Fin m
i✝ : Fin k
⊢ (pderiv ((universalFactorizationMapPresentation R (m + k) m k ⋯).map (finSumFinEquiv (Sum.inl i))))
      ((universalFactorizationMapPresentation R (m + k) m k ⋯).relation (Fin.natAdd m i✝)) =
    -Fin.addCases
        (fun j₁ ↦
          if ↑(Fin.natAdd m i✝) ∈ Set.Icc (↑j₁) (↑j₁ + k) then
            (Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))).comp (rename Sum.inr)))
                  (freeMonic R k)).coeff
              (↑(Fin.natAdd m i✝) - ↑j₁)
          else 0)
        (fun j₁ ↦
          if ↑(Fin.natAdd m i✝) ∈ Set.Icc (↑j₁) (↑j₁ + m) then
            (Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))).comp (rename Sum.inl)))
                  (freeMonic R m)).coeff
              (↑(Fin.natAdd m i✝) - ↑j₁)
          else 0)
        ((finCongr ⋯) (finSumFinEquiv (Sum.inl i)))

Tactic:
simp [pderiv_map, coeff_freeMonic, apply_dite (DFunLike.coe _), apply_ite (DFunLike.coe _),
        pderiv_inl_universalFactorizationMap_X, pderiv_inr_universalFactorizationMap_X]

Goal state after:
case inl.right
R : Type u_1
inst✝ : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i : Fin m
i✝ : Fin k
⊢ (if m + ↑i✝ < ↑i then 0
    else if h : m + ↑i✝ - ↑i < k then X (Sum.inr ⟨m + ↑i✝ - ↑i, ⋯⟩) else if m + ↑i✝ - ↑i = k then 1 else 0) =
    if ↑i ≤ m + ↑i✝ ∧ m + ↑i✝ ≤ ↑i + k then
      if h : m + ↑i✝ - ↑i < k then X (Sum.inr ⟨m + ↑i✝ - ↑i, h⟩) else if m + ↑i✝ - ↑i = k then 1 else 0
    else 0
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.left
R : Type u_1
inst✝ : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i : Fin k
i✝ : Fin m
⊢ (pderiv ((universalFactorizationMapPresentation R (m + k) m k ⋯).map (finSumFinEquiv (Sum.inr i))))
      ((universalFactorizationMapPresentation R (m + k) m k ⋯).relation (Fin.castAdd k i✝)) =
    -Fin.addCases
        (fun j₁ ↦
          if ↑(Fin.castAdd k i✝) ∈ Set.Icc (↑j₁) (↑j₁ + k) then
            (Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))).comp (rename Sum.inr)))
                  (freeMonic R k)).coeff
              (↑(Fin.castAdd k i✝) - ↑j₁)
          else 0)
        (fun j₁ ↦
          if ↑(Fin.castAdd k i✝) ∈ Set.Icc (↑j₁) (↑j₁ + m) then
            (Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))).comp (rename Sum.inl)))
                  (freeMonic R m)).coeff
              (↑(Fin.castAdd k i✝) - ↑j₁)
          else 0)
        ((finCongr ⋯) (finSumFinEquiv (Sum.inr i)))

Tactic:
simp [pderiv_map, coeff_freeMonic, apply_dite (DFunLike.coe _), apply_ite (DFunLike.coe _),
        pderiv_inl_universalFactorizationMap_X, pderiv_inr_universalFactorizationMap_X]

Goal state after:
case inr.left
R : Type u_1
inst✝ : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i : Fin k
i✝ : Fin m
⊢ (if ↑i✝ < ↑i then 0 else if h : ↑i✝ - ↑i < m then X (Sum.inl ⟨↑i✝ - ↑i, ⋯⟩) else if ↑i✝ - ↑i = m then 1 else 0) =
    if ↑i ≤ ↑i✝ ∧ ↑i✝ ≤ ↑i + m then
      if h : ↑i✝ - ↑i < m then X (Sum.inl ⟨↑i✝ - ↑i, h⟩) else if ↑i✝ - ↑i = m then 1 else 0
    else 0
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.right
R : Type u_1
inst✝ : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i i✝ : Fin k
⊢ (pderiv ((universalFactorizationMapPresentation R (m + k) m k ⋯).map (finSumFinEquiv (Sum.inr i))))
      ((universalFactorizationMapPresentation R (m + k) m k ⋯).relation (Fin.natAdd m i✝)) =
    -Fin.addCases
        (fun j₁ ↦
          if ↑(Fin.natAdd m i✝) ∈ Set.Icc (↑j₁) (↑j₁ + k) then
            (Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))).comp (rename Sum.inr)))
                  (freeMonic R k)).coeff
              (↑(Fin.natAdd m i✝) - ↑j₁)
          else 0)
        (fun j₁ ↦
          if ↑(Fin.natAdd m i✝) ∈ Set.Icc (↑j₁) (↑j₁ + m) then
            (Polynomial.map (↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))).comp (rename Sum.inl)))
                  (freeMonic R m)).coeff
              (↑(Fin.natAdd m i✝) - ↑j₁)
          else 0)
        ((finCongr ⋯) (finSumFinEquiv (Sum.inr i)))

Tactic:
simp [pderiv_map, coeff_freeMonic, apply_dite (DFunLike.coe _), apply_ite (DFunLike.coe _),
        pderiv_inl_universalFactorizationMap_X, pderiv_inr_universalFactorizationMap_X]

Goal state after:
case inr.right
R : Type u_1
inst✝ : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i i✝ : Fin k
⊢ (if m + ↑i✝ < ↑i then 0
    else if h : m + ↑i✝ - ↑i < m then X (Sum.inl ⟨m + ↑i✝ - ↑i, ⋯⟩) else if m + ↑i✝ - ↑i = m then 1 else 0) =
    if ↑i ≤ m + ↑i✝ ∧ m + ↑i✝ ≤ ↑i + m then
      if h : m + ↑i✝ - ↑i < m then X (Sum.inl ⟨m + ↑i✝ - ↑i, h⟩) else if m + ↑i✝ - ↑i = m then 1 else 0
    else 0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g₁ g₂ : R[X]), q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂
g₁ g₂ : S[X]
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
g₁' : R[X]
hg₁ : map φ g₁' = g₁
e₁ : g₁'.degree = g₁.degree
g₂' : R[X]
hg₂ : map φ g₂' = g₂
e₂ : g₂'.degree = g₂.degree
⊢ φ (f'.resultant (g₁' * g₂') (map φ f').natDegree (g₁.natDegree + g₂.natDegree)) =
    φ (f'.resultant g₁' (map φ f').natDegree g₁.natDegree) * φ (f'.resultant g₂' (map φ f').natDegree g₂.natDegree)

Tactic:
hf',

Goal state after:
case surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g₁ g₂ : R[X]), q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂
g₁ g₂ : S[X]
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
g₁' : R[X]
hg₁ : map φ g₁' = g₁
e₁ : g₁'.degree = g₁.degree
g₂' : R[X]
hg₂ : map φ g₂' = g₂
e₂ : g₂'.degree = g₂.degree
⊢ φ (f'.resultant (g₁' * g₂') f.natDegree (g₁.natDegree + g₂.natDegree)) =
    φ (f'.resultant g₁' f.natDegree g₁.natDegree) * φ (f'.resultant g₂' f.natDegree g₂.natDegree)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH : ∀ (q : R[X]), q.resultant q = 0 ^ q.natDegree
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
⊢ φ (f'.resultant f' (map φ f').natDegree (map φ f').natDegree) = 0 ^ (map φ f').natDegree

Tactic:
hf',

Goal state after:
case surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH : ∀ (q : R[X]), q.resultant q = 0 ^ q.natDegree
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
⊢ φ (f'.resultant f' f.natDegree f.natDegree) = 0 ^ f.natDegree
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inr.inr.inr
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 1 f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

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
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree

Tactic:
resultant_one_right

Goal state after:
case inr.inr.inr.inr
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.coeff f.natDegree ^ (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

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
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inr.surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g : R[X]) (r : R),
    q ≠ 0 →
      g ≠ 0 →
        (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
          r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
hf : f ≠ 0
hg : g ≠ 0
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : R[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
r : R
hfl : f.leadingCoeff = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ (map φ (f'.scaleRoots r)).resultant (map φ (g'.scaleRoots r)) (map φ f').natDegree (map φ g').natDegree =
    φ r ^ ((map φ f').natDegree * (map φ g').natDegree) * (map φ f').resultant (map φ g')

Tactic:
hf',

Goal state after:
case inr.inr.surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g : R[X]) (r : R),
    q ≠ 0 →
      g ≠ 0 →
        (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
          r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
hf : f ≠ 0
hg : g ≠ 0
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : R[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
r : R
hfl : f.leadingCoeff = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ (map φ (f'.scaleRoots r)).resultant (map φ (g'.scaleRoots r)) f.natDegree (map φ g').natDegree =
    φ r ^ (f.natDegree * (map φ g').natDegree) * f.resultant (map φ g')
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 R n
⊢ Algebra.Etale R 𝓡'

Tactic:
let Δ : 𝓡 := (presentation m k hn p).jacobian
  have hΔ : IsUnit (algebraMap 𝓡 (Localization.Away Δ) Δ) :=
    IsLocalization.Away.algebraMap_isUnit _
  let P : Algebra.SubmersivePresentation R (Localization.Away Δ) _ _ :=
    { toPreSubmersivePresentation :=
        .comp (.localizationAway (Localization.Away Δ) Δ) (presentation m k hn p),
      jacobian_isUnit := by simpa [Algebra.smul_def, -isUnit_map_iff, hΔ] }
  have : Algebra.IsStandardSmoothOfRelativeDimension 0 R (Localization.Away Δ) :=
    ⟨_, _, _, inferInstance, P, by
      simp only [Algebra.PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension, P]
      simp [Algebra.Presentation.dimension, hn]⟩
  infer_instance

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

Goal state before:
pp: case surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH : ∀ (q g : R[X]) (r : R), ((taylor r) q).resultant ((taylor r) g) = q.resultant g
g : S[X]
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : R[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
r : R
hfl : f.leadingCoeff = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ φ (((taylor r) f').resultant ((taylor r) g') (map φ f').natDegree (map φ g').natDegree) =
    φ (f'.resultant g' (map φ f').natDegree (map φ g').natDegree)

Tactic:
hf',

Goal state after:
case surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH : ∀ (q g : R[X]) (r : R), ((taylor r) q).resultant ((taylor r) g) = q.resultant g
g : S[X]
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : R[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
r : R
hfl : f.leadingCoeff = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ φ (((taylor r) f').resultant ((taylor r) g') f.natDegree (map φ g').natDegree) =
    φ (f'.resultant g' f.natDegree (map φ g').natDegree)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
P : Ideal R
inst✝ : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H✝ : map (algebraMap R P.ResidueField) ↑p = ↑f * ↑g
Hpq : IsCoprime ↑f ↑g
φ : 𝓡' →ₐ[R] P.ResidueField := ⋯
Q : Ideal 𝓡' := ⋯
this✝ : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ f.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯).toRingHom =
    (↑((homEquiv Q.ResidueField m k hn p) (φi.comp φ))).1

Tactic:
simp [homEquiv_comp_fst, φ, φi]

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

Goal state before:
pp: case neg.refine_2.inl
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
b : R[X]
this : f.resultant 1 f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
e : 0 * f + b * g = 1
⊢ 1 = f.resultant b * f.resultant g

Tactic:
resultant_one_right

Goal state after:
case neg.refine_2.inl
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
b : R[X]
this : f.coeff f.natDegree ^ (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
e : 0 * f + b * g = 1
⊢ 1 = f.resultant b * f.resultant g
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : StrictlyUnitaryLaxFunctor B C
x : B
⊢ IsIso (F.mapId x)

Tactic:
mapId_eq_eqToHom

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : StrictlyUnitaryLaxFunctor B C
x : B
⊢ IsIso (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: case h₀
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
this : (↑(Algebra.TensorProduct.comm R S T)).comp includeLeftRingHom = ↑includeRight
⊢ (pullbackSpecIso' R T S).inv ≫
      (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
        pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R)) =
    (Spec.map (ofHom ↑(Algebra.TensorProduct.comm R S T)) ≫ (pullbackSpecIso' R S T).inv) ≫
      pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))

Tactic:
pullbackSymmetry_hom_comp_fst

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
this : (↑(Algebra.TensorProduct.comm R S T)).comp includeLeftRingHom = ↑includeRight
⊢ (pullbackSpecIso' R T S).inv ≫ pullback.snd (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) =
    (Spec.map (ofHom ↑(Algebra.TensorProduct.comm R S T)) ≫ (pullbackSpecIso' R S T).inv) ≫
      pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))
Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation

Goal state before:
pp: case empty
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
⊢ ∃ S' x x_1, ∃ (_ : Module.Finite R S') (_ : Free R S') (_ : Algebra.FinitePresentation R S'), ∃ f, ↑∅ ⊆ ↑f.range

Tactic:
exact ⟨R, _, _, inferInstance, inferInstance, inferInstance, Algebra.ofId R S, by simp⟩

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₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ β ▷ r₃ ⊗≫
          (r₁ ≫ g₁) ◁ leftZigzag adj₂.unit adj₂.counit ▷ (h₂ ≫ r₃) ⊗≫
            r₁ ◁ α ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ (g₁ ≫ g₂) ◁ adj₃.unit ⊗≫
        r₁ ◁ ((α_ g₁ g₂ l₃).hom ≫ g₁ ◁ β ≫ (α_ g₁ l₂ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ r₃ ⊗≫
          adj₁.counit ▷ (h₁ ≫ h₂) ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)

Tactic:
by
      rw [adj₂.left_triangle]
      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 : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
⊢ (mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄)) (leftAdjointSquare.hcomp α β) =
    rightAdjointSquare.hcomp ((mateEquiv adj₁ adj₂) α) ((mateEquiv adj₃ adj₄) β)

Tactic:
simp only [mateEquiv_apply']

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      (r₃ ≫ r₁) ◁ g ◁ (adj₂.comp adj₄).unit ⊗≫
        (r₃ ≫ r₁) ◁ leftAdjointSquare.hcomp α β ▷ (r₄ ≫ r₂) ⊗≫
          (adj₁.comp adj₃).counit ▷ k ▷ (r₄ ≫ r₂) ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    rightAdjointSquare.hcomp (𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂))
      (𝟙 (r₃ ≫ h) ⊗≫ r₃ ◁ h ◁ adj₄.unit ⊗≫ r₃ ◁ β ▷ r₄ ⊗≫ adj₃.counit ▷ k ▷ r₄ ⊗≫ 𝟙 (k ≫ r₄))
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : r₁ ⟶ r₂
⊢ (conjugateEquiv adj₁ adj₂).symm α =
    (λ_ l₂).inv ≫ adj₁.unit ▷ l₂ ≫ (α_ l₁ r₁ l₂).hom ≫ l₁ ◁ α ▷ l₂ ≫ l₁ ◁ adj₂.counit ≫ (ρ_ l₁).hom

Tactic:
rw [conjugateEquiv_symm_apply, mateEquiv_symm_apply']
  bicategory

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
inst✝¹ : CompactSpace ↥V
I : Ideal ↑(CommRingCat.of ((i : ι) → ↑(R i)))
e : V ≅ Spec (CommRingCat.of (↑(CommRingCat.of ((i : ι) → ↑(R i))) ⧸ I))
inst✝ : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
this✝ : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
⊢ IsIso (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))

Tactic:
obtain rfl := eq_bot_of_comp_quotientMk_eq_sigmaSpec R I (f ≫ e.hom) (by rwa [Category.assoc])

Goal state after:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
inst✝¹ : CompactSpace ↥V
e : V ≅ Spec (CommRingCat.of (↑(CommRingCat.of ((i : ι) → ↑(R i))) ⧸ ⊥))
inst✝ : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)) = sigmaSpec R
this✝ : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
⊢ IsIso (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : QuasiSeparatedSpace ↥X
⊢ Function.Injective (pointsPi R X)

Tactic:
by
  rintro f g e
  have := isIso_of_comp_eq_sigmaSpec R (V := equalizer f g)
    (equalizer.lift (sigmaSpec R) (by ext1 i; simpa using! congr_fun e i))
    (equalizer.ι f g) (by simp)
  rw [← cancel_epi (equalizer.ι f g), equalizer.condition]

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

Goal state before:

Tactic:
_ = 𝟙 _ ⊗≫
          rightAdjointSquare.vcomp
            (mateEquiv adj₁ adj₂ ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
            (mateEquiv adj₂ adj₃ β) ⊗≫ 𝟙 _ := by
      dsimp only [conjugateEquiv_apply, rightAdjointConjugateSquare.vcomp, rightAdjointSquare.vcomp]
      bicategory
    _ = _ := by
      rw [← mateEquiv_vcomp]
      simp only [leftAdjointSquare.vcomp, mateEquiv_apply', leftAdjointConjugateSquare.vcomp]
      bicategory

Goal state after:
Module: Mathlib.Data.FunLike.Graded

Goal state before:
pp: E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝¹ : EquivLike E A B
inst✝ : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
y : ↥(ℬ i)
⊢ e (EquivLike.inv e ↑y) ∈ ℬ i

Tactic:
rw [EquivLike.apply_inv_apply]; exact y.2

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.RingHom

Goal state before:
pp: ι : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_6
τ : Type u_7
inst✝¹² : Semiring A
inst✝¹¹ : Semiring B
inst✝¹⁰ : SetLike σ A
inst✝⁹ : SetLike τ B
inst✝⁸ : DecidableEq ι
inst✝⁷ : AddMonoid ι
inst✝⁶ : AddSubmonoidClass σ A
inst✝⁵ : AddSubmonoidClass τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝⁴ : GradedRing 𝒜
inst✝³ : GradedRing ℬ
F : Type u_10
inst✝² : FunLike F A B
inst✝¹ : GradedFunLike F 𝒜 ℬ
inst✝ : RingHomClass F A B
f : F
x : A
⊢ (decompose ℬ) (f (∑ i ∈ DFinsupp.support ((decompose 𝒜) x), ↑(((decompose 𝒜) x) i))) =
    (map (↑f).gradedAddHom) ((decompose 𝒜) (∑ i ∈ DFinsupp.support ((decompose 𝒜) x), ↑(((decompose 𝒜) x) i)))

Tactic:
map_sum,

Goal state after:
ι : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_6
τ : Type u_7
inst✝¹² : Semiring A
inst✝¹¹ : Semiring B
inst✝¹⁰ : SetLike σ A
inst✝⁹ : SetLike τ B
inst✝⁸ : DecidableEq ι
inst✝⁷ : AddMonoid ι
inst✝⁶ : AddSubmonoidClass σ A
inst✝⁵ : AddSubmonoidClass τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝⁴ : GradedRing 𝒜
inst✝³ : GradedRing ℬ
F : Type u_10
inst✝² : FunLike F A B
inst✝¹ : GradedFunLike F 𝒜 ℬ
inst✝ : RingHomClass F A B
f : F
x : A
⊢ (decompose ℬ) (∑ x_1 ∈ DFinsupp.support ((decompose 𝒜) x), f ↑(((decompose 𝒜) x) x_1)) =
    (map (↑f).gradedAddHom) ((decompose 𝒜) (∑ i ∈ DFinsupp.support ((decompose 𝒜) x), ↑(((decompose 𝒜) x) i)))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f✝ g✝ : A
m✝ : ℕ
f_deg✝ : f✝ ∈ 𝒜 m✝
hm✝ : 0 < m✝
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x✝ : A
hx : x✝ = f✝ * g
ι : Type u_2
f : ι → A
m : ι → ℕ
f_deg : ∀ (i : ι), f i ∈ 𝒜 (m i)
hm : ∀ (i : ι), 0 < m i
hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)
x : ↥(Proj 𝒜)
⊢ x ∈ Set.range ⇑(awayι 𝒜 (f ⋯.choose) ⋯ ⋯)

Tactic:
by
    change x ∈ (awayι 𝒜 _ _ _).opensRange
    rw [opensRange_awayι]
    exact (mem_iSup.mp ((iSup_basicOpen_eq_top 𝒜 f hf).ge (Set.mem_univ x))).choose_spec

Goal state after: