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

Goal state before:
pp: case hX
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
n m k : ℕ
hn : n = m + k
i✝ : Fin n
⊢ (Polynomial.map ((↑Algebra.TensorProduct.includeLeft).comp (map (algebraMap R S))) (freeMonic R m) *
          Polynomial.map ((↑Algebra.TensorProduct.includeRight).comp (map (algebraMap R S))) (freeMonic R k)).coeff
      ↑i✝ =
    (Polynomial.map
            ((↑(Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S)))
                    ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S)))
                    ⋯)).comp
              ↑Algebra.TensorProduct.includeLeft)
            (freeMonic R m) *
          Polynomial.map
            ((↑(Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S)))
                    ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S)))
                    ⋯)).comp
              ↑Algebra.TensorProduct.includeRight)
            (freeMonic R k)).coeff
      ↑i✝

Tactic:
congr 2

Goal state after:
case hX.e_a.e_a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
n m k : ℕ
hn : n = m + k
i✝ : Fin n
⊢ Polynomial.map ((↑Algebra.TensorProduct.includeLeft).comp (map (algebraMap R S))) (freeMonic R m) =
    Polynomial.map
      ((↑(Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S)))
              ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S)))
              ⋯)).comp
        ↑Algebra.TensorProduct.includeLeft)
      (freeMonic R m)

case hX.e_a.e_a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
n m k : ℕ
hn : n = m + k
i✝ : Fin n
⊢ Polynomial.map ((↑Algebra.TensorProduct.includeRight).comp (map (algebraMap R S))) (freeMonic R k) =
    Polynomial.map
      ((↑(Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S)))
              ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S)))
              ⋯)).comp
        ↑Algebra.TensorProduct.includeRight)
      (freeMonic R k)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.e_a
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
⊢ (Polynomial.map
          ((↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
            ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inl)))
          (freeMonic R m)).resultant
      (Polynomial.map
        ((↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
          ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr)))
        (freeMonic R k))
      m k =
    (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m)).resultant
      (Polynomial.map (↑Algebra.TensorProduct.includeRight) (freeMonic R k))

Tactic:
congr 2

Goal state after:
case inr.e_a.e_3.e_f
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
⊢ (↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
      ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inl)) =
    Algebra.TensorProduct.includeLeftRingHom

case inr.e_a.e_4.e_f
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
⊢ (↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
      ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr)) =
    ↑Algebra.TensorProduct.includeRight

case inr.e_a.e_5
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
⊢ m = (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m)).natDegree

case inr.e_a.e_6
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
⊢ k = (Polynomial.map (↑Algebra.TensorProduct.includeRight) (freeMonic R k)).natDegree
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
i : Fin m
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' :
  Polynomial.eval₂ ((universalFactorizationMap R n m k hn).comp (map (algebraMap ℤ R))) (F.toRingHom (X i ⊗ₜ[ℤ] 1)) p =
    F.toRingHom 0
⊢ Polynomial.eval₂ (universalFactorizationMap R n m k hn).toRingHom (X i ⊗ₜ[R] 1)
      (Polynomial.map (map (algebraMap ℤ R)) p) =
    0

Tactic:
simpa [← Polynomial.eval₂_map, F] using! hp'

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝⁴ : QuasiCompact f✝
inst✝³ : QuasiSeparated f✝
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : Smooth g
x : ↥(pullback (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : (pullback.snd (fromNormalization f) g ≫ g) x ∈ ↑U
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : (pullback.snd (fromNormalization f) g) x ∈ ↑V
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
this✝¹ : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
this✝ : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
algInst✝² : Algebra ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst✝¹ : Algebra ↑Γ(S, U) ↑Γ(Y, V) := (CommRingCat.Hom.hom (appLE g U V hVU)).toAlgebra
algInst✝ : Algebra ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) :=
  (CommRingCat.Hom.hom (app (pullback.snd f g) V)).toAlgebra
algebraizeInst✝ : Algebra.Smooth ↑Γ(S, U) ↑Γ(Y, V)
this : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
e₀ : CommRingCat.of
    (↑(Y.presheaf.1 (Opposite.op V)) ⊗[↑(S.presheaf.1 (Opposite.op U))] ↑(X.presheaf.1 (Opposite.op (f ⁻¹ᵁ U)))) ≅
  Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) :=
  ⋯.isoPushout ≪≫ pushout.congrHom ⋯ ⋯ ≪≫ asIso (pushoutSection ⋯ hVU ⋯ ⋯)
r : ↑Γ(Y, V)
⊢ (ConcreteCategory.hom (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ e₀.hom)) r =
    (ConcreteCategory.hom (app (pullback.snd f g) V)) r

Tactic:
congr 2

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝⁴ : QuasiCompact f✝
inst✝³ : QuasiSeparated f✝
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : Smooth g
x : ↥(pullback (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : (pullback.snd (fromNormalization f) g ≫ g) x ∈ ↑U
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : (pullback.snd (fromNormalization f) g) x ∈ ↑V
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
this✝¹ : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
this✝ : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
algInst✝² : Algebra ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst✝¹ : Algebra ↑Γ(S, U) ↑Γ(Y, V) := (CommRingCat.Hom.hom (appLE g U V hVU)).toAlgebra
algInst✝ : Algebra ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) :=
  (CommRingCat.Hom.hom (app (pullback.snd f g) V)).toAlgebra
algebraizeInst✝ : Algebra.Smooth ↑Γ(S, U) ↑Γ(Y, V)
this : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
e₀ : CommRingCat.of
    (↑(Y.presheaf.1 (Opposite.op V)) ⊗[↑(S.presheaf.1 (Opposite.op U))] ↑(X.presheaf.1 (Opposite.op (f ⁻¹ᵁ U)))) ≅
  Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) :=
  ⋯.isoPushout ≪≫ pushout.congrHom ⋯ ⋯ ≪≫ asIso (pushoutSection ⋯ hVU ⋯ ⋯)
r : ↑Γ(Y, V)
⊢ CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ e₀.hom = app (pullback.snd f g) V
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
H₁ : ∀ (i : Fin m), (universalFactorizationMap R n m k hn).IsIntegralElem (X i ⊗ₜ[R] 1)
i : Fin k
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' :
  Polynomial.eval₂ ((universalFactorizationMap R n m k hn).comp (map (algebraMap ℤ R))) (F.toRingHom (1 ⊗ₜ[ℤ] X i)) p =
    F.toRingHom 0
⊢ Polynomial.eval₂ (universalFactorizationMap R n m k hn).toRingHom (1 ⊗ₜ[R] X i)
      (Polynomial.map (map (algebraMap ℤ R)) p) =
    0

Tactic:
simpa [← Polynomial.eval₂_map, F] using! hp'

Goal state after:
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]
g : R[X]
r : R
x y : R[X]
hx : x ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hy : y ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hx' : ((taylor r) x).resultant ((taylor r) g) = x.resultant g
hy' : ((taylor r) y).resultant ((taylor r) g) = y.resultant g
hx0 : ¬x = 0
hy0 : y = 0
⊢ ((taylor r) (x * y)).resultant ((taylor r) g) = (x * y).resultant g

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

Tactic:
· simp [hy0]

Goal state after:
case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
g : R[X]
r : R
x y : R[X]
hx : x ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hy : y ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hx' : ((taylor r) x).resultant ((taylor r) g) = x.resultant g
hy' : ((taylor r) y).resultant ((taylor r) g) = y.resultant g
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ((taylor r) (x * y)).resultant ((taylor r) g) = (x * y).resultant 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
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p ∧ IsCoprime ↑q.1 ↑q.2 }
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
congr 2

Goal state after:
case e_6
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
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p ∧ IsCoprime ↑q.1 ↑q.2 }
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

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

Tactic:
· rw [← resultant_add_mul_right _ _ a _ _ _ le_rfl, add_comm, mul_comm, e, ← C.map_one] at this
      · simpa [hf.leadingCoeff] using this
      · by_contra! H
        replace H := natDegree_mul_le.trans_lt H
        rw [add_comm, ← hf.natDegree_mul' hb0, mul_comm f] at H
        have := natDegree_add_eq_left_of_natDegree_lt H
        simp only [e, natDegree_one] at this
        lia

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
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 ⋯
x✝ : ↥↑U'
x : ↥(normalization f)
a : ↥(normalization (pullback.snd f fT))
ha : a ∈ U.carrier
e : fTn a = x
⊢ ↑(fTnU ⟨a, ha⟩) = ↑⟨x, ⋯⟩

Tactic:
simpa [fTnU] using e

Goal state after:
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✝
P : Extension R S
T : Type u_4
inst✝¹ : CommRing T
inst✝ : Algebra R T
this✝⁴ : Algebra P.Ring P.baseChange.Ring := P.algebraBaseChange T
this✝³ : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
this✝² : Algebra P.Ring (T ⊗[R] S) := compHom (T ⊗[R] S) (algebraMap P.Ring S)
this✝¹ : IsScalarTower R P.Ring (T ⊗[R] S)
PT : Extension T (T ⊗[R] S) := P.baseChange
this✝ : IsPushout R T P.Ring PT.Ring
this : IsScalarTower P.Ring PT.Ring (T ⊗[R] S)
⊢ ∀ (s : P.Ring) (x : T) (y : S), ((TensorProduct.mk R T S) x) (s • y) = s • ((TensorProduct.mk R T S) x) y

Tactic:
by simp [Algebra.smul_def, RingHom.algebraMap_toAlgebra]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
S : StrictPseudofunctorCore B C
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
f : b✝ ⟶ c✝
⊢ S.map₂ (η ▷ f) = (eqToIso ⋯).hom ≫ S.map₂ η ▷ S.map f ≫ (eqToIso ⋯).inv

Tactic:
by
    simpa using S.map₂_whisker_right η f

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

Goal state before:
pp: B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
inst✝¹ : Strict B
inst✝ : Strict C
S : StrictPseudofunctorPreCore B C
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
f : b✝ ⟶ c✝
⊢ S.map₂ (η ▷ f) = (eqToIso ⋯).hom ≫ S.map₂ η ▷ S.map f ≫ (eqToIso ⋯).inv

Tactic:
by
    simpa using S.map₂_whisker_right η f

Goal state after:
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
S : StrictlyUnitaryPseudofunctorCore B C
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
f : b✝ ⟶ c✝
⊢ S.map₂ (η ▷ f) = (S.mapComp f✝ f).hom ≫ S.map₂ η ▷ S.map f ≫ (S.mapComp g✝ f).inv

Tactic:
by
    simpa using S.map₂_whisker_right η f

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

Goal state before:
pp: R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f g : WithConv (S →ₐ[R] T)
⊢ Hom.asOver (map (CommRingCat.ofHom (f * g).ofConv.toRingHom)) (Spec (CommRingCat.of R)) =
    Hom.asOver (map (CommRingCat.ofHom f.ofConv.toRingHom)) (Spec (CommRingCat.of R)) *
      Hom.asOver (map (CommRingCat.ofHom g.ofConv.toRingHom)) (Spec (CommRingCat.of R))

Tactic:
by
    ext1
    dsimp [AlgHom.convMul_def, AlgHom.comp_toRingHom, Hom.mul_def]
    simp only [← Category.assoc, Spec.map_comp, mul_spec_asOver_spec_left]
    congr 1
    rw [← Iso.comp_inv_eq]
    ext
    all_goals
    · simp only [specOverSpec_over, ← Spec.map_comp, ← CommRingCat.ofHom_comp,
      ← AlgHom.comp_toRingHom, Category.assoc, pullbackSpecIso_inv_fst, pullbackSpecIso_inv_snd,
      limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]
      congr 3
      ext; simp

Goal state after:
Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation

Goal state before:
pp: R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Algebra.FinitePresentation R S
R' : Type u
w✝⁴ : CommRing R'
w✝³ : Algebra R R'
w✝² : Module.Finite R R'
w✝¹ : Free R R'
w✝ : Algebra.FinitePresentation R R'
f : R' →ₐ[R] S
hf : Function.Surjective ⇑f
this✝² : Algebra R' S := f.toAlgebra
this✝¹ : IsScalarTower R R' S
this✝ : FinitePresentation R R'
this : FinitePresentation R' S
⊢ FinitePresentation R S

Tactic:
exact .trans R S R'

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case refine_1
X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst✝² : IsAffine T
t : ↥T
inst✝¹ : Flat f
inst✝ : IsFinite f
i : Spec (S.affineOpenCover.X (S.affineOpenCover.idx (g t))) ⟶ S := S.affineOpenCover.f (S.affineOpenCover.idx (g t))
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl : (pullback.fst (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = Exists.choose ⋯
hyr : (pullback.snd (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = t
⊢ pullback (pullback.snd f g) (u ≫ pullback.snd i g) ⟶ pullback f (S.affineOpenCover.f (S.affineOpenCover.idx (g t)))

Tactic:
exact pullback.map _ _ _ _ (pullback.fst f g) (u ≫ pullback.fst _ _) g
        pullback.condition.symm (by simp [← pullback.condition]; rfl)

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : Ideal.span {r} = ⊤
⊢ ringKrullDim (R ⧸ Ideal.span {r}) + 1 ≤ ringKrullDim R

Tactic:
hr',

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : Ideal.span {r} = ⊤
⊢ ringKrullDim (R ⧸ ⊤) + 1 ≤ ringKrullDim R
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx : coheight x = 1
hx' : x ∈ U
this : Ring.KrullDimLE 1 ↑(X.presheaf.stalk x)
⊢ (ordHom x hx) ((ConcreteCategory.hom (X.germToFunctionField U)) f) = 1

Tactic:
rw [← algebraMap_germ_eq_germToFunctionField _ hx']

Goal state after:
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx : coheight x = 1
hx' : x ∈ U
this : Ring.KrullDimLE 1 ↑(X.presheaf.stalk x)
⊢ (ordHom x hx)
      ((algebraMap ↑(X.presheaf.stalk x) ↑X.functionField) ((ConcreteCategory.hom (X.presheaf.germ U x hx')) f)) =
    1
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
⊢ vanishingIdeal t ⊔ vanishingIdeal t' ≤ vanishingIdeal (t ∩ t')

Tactic:
intro r
  rw [← HomogeneousIdeal.mem_iff, HomogeneousIdeal.toIdeal_sup, mem_vanishingIdeal,
    Submodule.mem_sup]
  rintro ⟨f, hf, g, hg, rfl⟩ x ⟨hxt, hxt'⟩
  rw [HomogeneousIdeal.mem_iff, mem_vanishingIdeal] at hf hg
  apply Submodule.add_mem <;> solve_by_elim

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

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g : A
⊢ basicOpen 𝒜 (f * g) ≤ basicOpen 𝒜 f

Tactic:
basicOpen_mul 𝒜 f g

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g : A
⊢ basicOpen 𝒜 f ⊓ basicOpen 𝒜 g ≤ basicOpen 𝒜 f
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g : A
⊢ basicOpen 𝒜 (f * g) ≤ basicOpen 𝒜 g

Tactic:
basicOpen_mul 𝒜 f g

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g : A
⊢ basicOpen 𝒜 f ⊓ basicOpen 𝒜 g ≤ basicOpen 𝒜 g
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
𝒜 : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq0 : IsLocalization.mk' (at 𝔭.primeCompl) ↑f.num ⟨↑f.den, ⋯⟩ * IsLocalization.mk' (at 𝔭.primeCompl) b s = 1
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)

Tactic:
← IsLocalization.mk'_mul,

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
𝒜 : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq0 : IsLocalization.mk' (at 𝔭.primeCompl) (↑f.num * b) (⟨↑f.den, ⋯⟩ * s) = 1
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec R).Modules
f : modulesSpecToSheaf.obj M ⟶ modulesSpecToSheaf.obj N
X✝ Y✝ : (Opens ↥(Spec R))ᵒᵖ
i : X✝ ⟶ Y✝
x : ↑(M.val.obj X✝)
⊢ (ModuleCat.Hom.hom
        (M.val.map i ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom ((Spec R).ringCatSheaf.obj.map i))).map
            (ModuleCat.ofHom { toAddHom := (ModuleCat.Hom.hom (f.hom.app Y✝)).toAddHom, map_smul' := ⋯ })))
      x =
    (ModuleCat.Hom.hom
        (ModuleCat.ofHom { toAddHom := (ModuleCat.Hom.hom (f.hom.app X✝)).toAddHom, map_smul' := ⋯ } ≫ N.val.map i))
      x

Tactic:
exact congr($(f.1.naturality i).hom x)

Goal state after: