mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monad.Algebra

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : C
Y : T.Algebra
f : X ⟶ T.forget.obj Y
⊢ T.map (T.map f ≫ Y.a) ≫ Y.a = (T.free.obj X).a ≫ T.map f ≫ Y.a

Tactic:
by simp [← Y.assoc, ← T.μ.naturality_assoc]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g✝ g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
m✝ : LocalizedModule S M
x✝² x✝¹ : M × ↥S
m : M
s : ↥S
m' : M
s' : ↥S
x✝ : (m, s) ≈ (m', s')
c : ↥S
eq1 : ↑c • ↑s' • m = ↑c • ↑s • m'
this✝ : c • s • g m' = c • s' • g m
this : Function.Injective ⇑⋯.unit.inv
⊢ ⋯.unit.inv (↑(m, s).2 • g m') = ⋯.unit.inv (↑(m', s').2 • g m)

Tactic:
Units.inv_eq_val_inv,

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g✝ g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
m✝ : LocalizedModule S M
x✝² x✝¹ : M × ↥S
m : M
s : ↥S
m' : M
s' : ↥S
x✝ : (m, s) ≈ (m', s')
c : ↥S
eq1 : ↑c • ↑s' • m = ↑c • ↑s • m'
this✝ : c • s • g m' = c • s' • g m
this : Function.Injective ⇑⋯.unit.inv
⊢ ↑⋯.unit⁻¹ (↑(m, s).2 • g m') = ↑⋯.unit⁻¹ (↑(m', s').2 • g m)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g✝ g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
m✝ : LocalizedModule S M
x✝² x✝¹ : M × ↥S
m : M
s : ↥S
m' : M
s' : ↥S
x✝ : (m, s) ≈ (m', s')
c : ↥S
eq1 : ↑c • ↑s' • m = ↑c • ↑s • m'
this✝ : c • s • g m' = c • s' • g m
this : Function.Injective ⇑⋯.unit.inv
⊢ g (↑c • ↑(m', s').2 • m) = g (↑c • ↑(m, s).2 • m')

Tactic:
eq1

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g✝ g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
m✝ : LocalizedModule S M
x✝² x✝¹ : M × ↥S
m : M
s : ↥S
m' : M
s' : ↥S
x✝ : (m, s) ≈ (m', s')
c : ↥S
eq1 : ↑c • ↑s' • m = ↑c • ↑s • m'
this✝ : c • s • g m' = c • s' • g m
this : Function.Injective ⇑⋯.unit.inv
⊢ g (↑c • ↑s • m') = g (↑c • ↑(m, s).2 • m')
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
A : Type u_5
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M
inst✝⁵ : Module A M
N : Type u_6
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module A N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
r : R
f : M →ₗ[A] N
h : IsLocalizedModule (Submonoid.powers ((algebraMap R A) r)) f
⊢ IsLocalizedModule (Submonoid.powers r) (↑R f)

Tactic:
rw [← Algebra.algebraMapSubmonoid_powers] at h
  exact IsLocalizedModule.restrictScalars _ f

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
M : Type u_2
inst✝¹⁰ : AddCommMonoid M
A : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
inst✝⁷ : Module R M
S : Submonoid R
N : Type u_6
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Module A M
inst✝³ : Module A N
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R A N
f : M →ₗ[A] N
inst✝ : IsLocalizedModule S (↑R f)
x : ↥(Algebra.algebraMapSubmonoid A S)
⊢ IsUnit ((algebraMap A (End A N)) ↑x)

Tactic:
obtain ⟨_, x, hx, rfl⟩ := x

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Type u_2
inst✝¹⁰ : AddCommMonoid M
A : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
inst✝⁷ : Module R M
S : Submonoid R
N : Type u_6
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Module A M
inst✝³ : Module A N
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R A N
f : M →ₗ[A] N
inst✝ : IsLocalizedModule S (↑R f)
x : R
hx : x ∈ ↑S
⊢ IsUnit ((algebraMap A (End A N)) ↑⟨(algebraMap R A) x, ⋯⟩)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case property.right.right
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝ : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
f' : A →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R ↑(pushoutCocone R A B).pt :=
  have this := inferInstance;
  this
h : (pushoutCocone R A B).pt ⟶ s.pt
⊢ ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h = s.inl →
    ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ h = s.inr →
      h = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom

Tactic:
eq1

Goal state after:
case property.right.right
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝ : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
f' : A →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R ↑(pushoutCocone R A B).pt :=
  have this := inferInstance;
  this
h : (pushoutCocone R A B).pt ⟶ s.pt
eq1 : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h = s.inl
⊢ ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ h = s.inr →
    h = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
a : M
b : ↥S
a' : M
b' : ↥S
eq1 : ↑b • f a' = ↑b' • f a
⊢ ↑b' • f a = ↑b • f a'

Tactic:
eq1

Goal state after:
case h.h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
a : M
b : ↥S
a' : M
b' : ↥S
eq1 : ↑b • f a' = ↑b' • f a
⊢ ↑b' • f a = ↑b' • f a
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M'
a : M
b : ↥S
eq1 : b • m = f a
⊢ ⋯.choose.2 • b • m = ⋯.choose.2 • f a

Tactic:
eq1

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M'
a : M
b : ↥S
eq1 : b • m = f a
⊢ ⋯.choose.2 • f a = ⋯.choose.2 • f a
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R S : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
R' S' : Type u
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' := (⋯.isoPushout ≪≫ h.isoPushout.symm).commRingCatIsoToRingEquiv
h2 :
  ∀ (r : R'),
    (ConcreteCategory.hom ⋯.isoPushout.hom) (r ⊗ₜ[R] 1) =
      (ConcreteCategory.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) r
h3 :
  ∀ (x : R'),
    (Hom.hom h.isoPushout.inv) ((Hom.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) x) =
      (algebraMap R' S') x
e' : R' ⊗[R] S ≃ₐ[R'] S' :=
  let __spread.0 := e;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ e'.toRingEquiv.toRingHom.comp (algebraMap S (R' ⊗[R] S)) = algebraMap S S'

Tactic:
ext s

Goal state after:
R S : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
R' S' : Type u
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' := (⋯.isoPushout ≪≫ h.isoPushout.symm).commRingCatIsoToRingEquiv
h2 :
  ∀ (r : R'),
    (ConcreteCategory.hom ⋯.isoPushout.hom) (r ⊗ₜ[R] 1) =
      (ConcreteCategory.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) r
h3 :
  ∀ (x : R'),
    (Hom.hom h.isoPushout.inv) ((Hom.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) x) =
      (algebraMap R' S') x
e' : R' ⊗[R] S ≃ₐ[R'] S' :=
  let __spread.0 := e;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
s : S
⊢ (e'.toRingEquiv.toRingHom.comp (algebraMap S (R' ⊗[R] S))) s = (algebraMap S S') s
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₁ : Type u_7
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
m : M
s : ↥S₁
⊢ (liftOfLE S₁ S₂ h f₁ f₂) (mk' f₁ m s) = mk' f₂ m ⟨↑s, ⋯⟩

Tactic:
apply ((Module.End.isUnit_iff _).mp (map_units f₂ ⟨s, h s.2⟩)).1

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₁ : Type u_7
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
m : M
s : ↥S₁
⊢ ((algebraMap R (End R M₂)) ↑⟨↑s, ⋯⟩) ((liftOfLE S₁ S₂ h f₁ f₂) (mk' f₁ m s)) =
    ((algebraMap R (End R M₂)) ↑⟨↑s, ⋯⟩) (mk' f₂ m ⟨↑s, ⋯⟩)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 → ∃ m, m • x = 0
x : S
x✝ : ∃ m, m • x = 0
m : R
hm : m ∈ M
e : ⟨m, hm⟩ • x = 0
⊢ m • f x = (algebraMap R S') m * 0

Tactic:
simpa [Submonoid.smul_def] using f.congr_arg e

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
α : Type u₁
F : J → α
⊢ (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : J), F j = F j'

Tactic:
hF

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ ∀ (j j' : J), F j = F j'
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: A : Type u_1
inst✝³ : Category.{v_1, u_1} A
B : Type u_2
inst✝² : Category.{v_2, u_2} B
T : Type u_3
inst✝¹ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
W : MorphismProperty T
X✝ : T
inst✝ : W.RespectsIso
X Y : Comma L R
e : X ≅ Y
h : commaObj L R W X
⊢ commaObj L R W Y

Tactic:
rwa [commaObj_iff, ← W.cancel_left_of_respectsIso (L.map e.hom.left), e.hom.w,
      W.cancel_right_of_respectsIso]

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_1
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
⊢ ∀ (x : B), x ∈ adjoin A ↑(Subalgebra.map f (adjoin R (Set.range MvPolynomial.X)))

Tactic:
adjoin_range_X,

Goal state after:
case refine_1
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
⊢ ∀ (x : B), x ∈ adjoin A ↑(Subalgebra.map f ⊤)
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
⊢ Subalgebra.restrictScalars R (adjoin A (Set.range MvPolynomial.X)) = Subalgebra.restrictScalars R ⊤

Tactic:
adjoin_range_X,

Goal state after:
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
⊢ Subalgebra.restrictScalars R ⊤ = Subalgebra.restrictScalars R ⊤
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case inr
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : A
hx : x ∈ t
⊢ (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) (MvPolynomial.C ↑⟨x, hx⟩) -
      (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) ((MvPolynomial.map (algebraMap R A)) (t' ⟨x, hx⟩)) =
    0

Tactic:
MvPolynomial.aeval_map_algebraMap,

Goal state after:
case inr
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : A
hx : x ∈ t
⊢ (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) (MvPolynomial.C ↑⟨x, hx⟩) -
      (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) (t' ⟨x, hx⟩) =
    0
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
d : ↑(F.obj X)
| colimit.ι (Grothendieck.ι F X ⋙ G) d

Tactic:
rw [← colimit.eqToHom_comp_ι (Grothendieck.ι F X ⋙ G)
      (j := (F.map (𝟙 X)).toFunctor.obj d) (by simp)]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
d : ↑(F.obj X)
| eqToHom ⋯ ≫ colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone G
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
⊢ (fiberwiseColimit G).map f ≫ colimit.desc (Grothendieck.ι F x✝ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝) c) =
    colimit.desc (Grothendieck.ι F x✝¹ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝¹) c) ≫ ((const C).obj c.pt).map f

Tactic:
dsimp; ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c✝ : Cocone G
hc : IsColimit c✝
s : Cocone (fiberwiseColimit G)
c : C
⊢ (coconeFiberwiseColimitOfCocone c✝).ι.app c ≫
      hc.desc { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι } =
    s.ι.app c

Tactic:
dsimp; ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : HasLimitsOfShape D E
inst✝ : HasLimitsOfShape C E
X✝ Y✝ : D ⥤ E
f : X✝ ⟶ Y✝
⊢ lim.map f ≫ (limitIso F Y✝).symm.hom = (limitIso F X✝).symm.hom ≫ ((whiskeringLeft C D E).obj F ⋙ lim).map f

Tactic:
simp only [comp_obj, whiskeringLeft_obj_obj, lim_obj, comp_map, whiskeringLeft_obj_map, lim_map,
      Iso.symm_hom, limitIso_inv]

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : HasLimitsOfShape D E
inst✝ : HasLimitsOfShape C E
X✝ Y✝ : D ⥤ E
f : X✝ ⟶ Y✝
⊢ limMap f ≫ limit.pre Y✝ F = limit.pre X✝ F ≫ limMap (F.whiskerLeft f)
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝¹ y✝ : (WithTerminal C)ᵒᵖ
f✝ : unop y✝ ⟶ unop x✝¹
x y : C
f : unop (op (of y)) ⟶ unop (op (of x))
x✝ : op (of x) ⟶ op (of y)
⊢ (𝟭 (WithTerminal C)ᵒᵖ).map (op f) ≫
      (match op (of y) with
        | op x =>
          match x with
          | of x => Iso.refl ((𝟭 (WithTerminal C)ᵒᵖ).obj (op (of x)))
          | star => Iso.refl ((𝟭 (WithTerminal C)ᵒᵖ).obj (op star))).hom =
    (match op (of x) with
        | op x =>
          match x with
          | of x => Iso.refl ((𝟭 (WithTerminal C)ᵒᵖ).obj (op (of x)))
          | star => Iso.refl ((𝟭 (WithTerminal C)ᵒᵖ).obj (op star))).hom ≫
      ({
              obj := fun x ↦
                match x with
                | op x =>
                  match x with
                  | of x => WithInitial.of (op x)
                  | star => WithInitial.star,
              map := fun {x y} x_1 ↦
                match x_1 with
                | op f =>
                  match x, y, f, x_1 with
                  | op (of x), op (of y), f, x_2 => (down f).op
                  | op star, op (of a), x, x_2 =>
                    WithInitial.starInitial.to
                      (match op (of a) with
                      | op x =>
                        match x with
                        | of x => WithInitial.of (op x)
                        | star => WithInitial.star)
                  | op star, op star, x, x_2 =>
                    𝟙
                      (match op star with
                      | op x =>
                        match x with
                        | of x => WithInitial.of (op x)
                        | star => WithInitial.star),
              map_id := ⋯, map_comp := ⋯ } ⋙
            {
              obj := fun x ↦
                match x with
                | WithInitial.of x => op (of (unop x))
                | WithInitial.star => op star,
              map := fun {x y} f ↦
                match x, y, f with
                | WithInitial.of (op x), WithInitial.of (op y), f => WithInitial.down f
                | WithInitial.star, WithInitial.of (op unop), x =>
                  op
                    (starTerminal.from
                      (Opposite.unop
                        (match WithInitial.of (op unop) with
                        | WithInitial.of x => op (of (Opposite.unop x))
                        | WithInitial.star => op star)))
                | WithInitial.star, WithInitial.star, x =>
                  𝟙
                    (match WithInitial.star with
                    | WithInitial.of x => op (of (unop x))
                    | WithInitial.star => op star),
              map_id := ⋯, map_comp := ⋯ }).map
        (op f)

Tactic:
simp only [Functor.id_obj, Functor.comp_obj,
              Functor.id_map, Iso.refl_hom, Category.comp_id, Functor.comp_map, Category.id_comp]
            rfl

Goal state after: