mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
a : A
⊢ (Functor.commShiftIso (𝟭 C) a).hom ≫ Functor.whiskerRight adj.unit (shiftFunctor C a) =
    (shiftFunctor C a).whiskerLeft adj.unit ≫ (Functor.commShiftIso (F ⋙ G) a).hom

Tactic:
ext X

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
a : A
X : C
⊢ ((Functor.commShiftIso (𝟭 C) a).hom ≫ Functor.whiskerRight adj.unit (shiftFunctor C a)).app X =
    ((shiftFunctor C a).whiskerLeft adj.unit ≫ (Functor.commShiftIso (F ⋙ G) a).hom).app X
Module: Mathlib.CategoryTheory.Triangulated.Yoneda

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasShift C ℤ
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
A : Cᵒᵖ
T : Triangle C
hT : T ∈ distinguishedTriangles
x₂ : unop A ⟶ T.obj₂
⊢ (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).g) x₂ = 0 →
    ∃ x₁, (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).f) x₁ = x₂

Tactic:
(hx₂ : x₂ ≫ T.mor₂ = 0)

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasShift C ℤ
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
A : Cᵒᵖ
T : Triangle C
hT : T ∈ distinguishedTriangles
x₂ : unop A ⟶ T.obj₂
hx₂ : x₂ ≫ T.mor₂ = 0
⊢ ∃ x₁, (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).f) x₁ = x₂
Module: Mathlib.CategoryTheory.Center.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : CatCenter C
⊢ x * y = y * x

Tactic:
ext X

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x y : CatCenter C
X : C
⊢ (x * y).app X = (y * x).app X
Module: Mathlib.CategoryTheory.Center.Linear

Goal state before:
pp: R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
⊢ { app := fun X ↦ (a * b) • 𝟙 X, naturality := ⋯ } =
    { app := fun X ↦ b • 𝟙 X, naturality := ⋯ } * { app := fun X ↦ a • 𝟙 X, naturality := ⋯ }

Tactic:
ext X

Goal state after:
R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
X : C
⊢ CatCenter.app { app := fun X ↦ (a * b) • 𝟙 X, naturality := ⋯ } X =
    ({ app := fun X ↦ b • 𝟙 X, naturality := ⋯ } * { app := fun X ↦ a • 𝟙 X, naturality := ⋯ }).app X
Module: Mathlib.CategoryTheory.Center.Linear

Goal state before:
pp: R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
⊢ { app := fun X ↦ (a + b) • 𝟙 X, naturality := ⋯ } =
    { app := fun X ↦ a • 𝟙 X, naturality := ⋯ } + { app := fun X ↦ b • 𝟙 X, naturality := ⋯ }

Tactic:
ext X

Goal state after:
R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
X : C
⊢ CatCenter.app { app := fun X ↦ (a + b) • 𝟙 X, naturality := ⋯ } X =
    ({ app := fun X ↦ a • 𝟙 X, naturality := ⋯ } + { app := fun X ↦ b • 𝟙 X, naturality := ⋯ }).app X
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ solution.π.ker = Submodule.span A (Set.range relations.relation) → Function.Injective ⇑solution.fromQuotient

Tactic:
intro h
    rw [← LinearMap.ker_eq_bot, eq_bot_iff]
    intro x hx
    obtain ⟨x, rfl⟩ := relations.surjective_toQuotient x
    replace hx : x ∈ LinearMap.ker solution.π := by
      simpa only [LinearMap.mem_ker, fromQuotient_toQuotient] using hx
    rw [h, ← range_map] at hx
    obtain ⟨x, rfl⟩ := hx
    simp only [toQuotient_map_apply, Submodule.zero_mem]

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ⇑f
n : ℕ
hn : 0 < n
g₀ : G
⊢ #{g | g ^ n = g₀} ≤ (nthRoots n (f g₀)).card

Tactic:
by
  have : DecidableEq R := Classical.decEq _
  calc
    _ ≤ #(nthRoots n (f g₀)).toFinset :=
      card_le_card_of_injOn f (by aesop (add safe unfold Set.MapsTo)) hf.injOn
    _ ≤ _ := (nthRoots n (f g₀)).toFinset_card_le

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Bilinear

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
⊢ ((b₁.repr x).sum fun i xi ↦ (b₂.repr y).sum fun j yj ↦ ρ₁₂ xi • σ₁₂ yj • (B (b₁ i)) (b₂ j)) = (B x) y

Tactic:
by
  conv_rhs => rw [← b₁.linearCombination_repr x, ← b₂.linearCombination_repr y]
  simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum₂, map_sum, map_smulₛₗ₂, map_smulₛₗ]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type v
inst✝ : CommRing R
A : SL(2, R)
⊢ A⁻¹ = ⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩

Tactic:
ext
  have := Matrix.adjugate_fin_two A.1
  rw [coe_inv, this]
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
σ₁ σ₂ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : M₁
y : M₂
⊢ (B x) y = ⇑σ₁ ∘ ⇑(b₁.repr x) ⬝ᵥ (toMatrix₂ b₁ b₂) B *ᵥ ⇑σ₂ ∘ ⇑(b₂.repr y)

Tactic:
by
  nth_rw 1 [← b₁.sum_repr x, ← b₂.sum_repr y]
  suffices ∑ j, ∑ i, σ₂ (b₂.repr y j) * σ₁ (b₁.repr x i) * B (b₁ i) (b₂ j) =
           ∑ i, ∑ j, σ₁ (b₁.repr x i) * σ₂ (b₂.repr y j) * B (b₁ i) (b₂ j) by
    simpa [dotProduct, Matrix.mulVec_eq_sum, Finset.mul_sum, -Basis.sum_repr, ← mul_assoc]
  simp_rw [mul_comm (σ₂ _)]
  exact Finset.sum_comm

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
⊢ toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m) = toLinearMap₂' R

Tactic:
by
  ext M
  simp only [coe_comp, coe_single, Function.comp_apply, toLinearMap₂_apply, Pi.basisFun_repr,
    toLinearMap₂'_apply]

Goal state after:
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f : (i : ι) → A i →+ R
hone : (f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj
⊢ (toAddMonoid f) 1 = 1

Tactic:
change (toAddMonoid f) (of _ 0 _) = 1
      rw [toAddMonoid_of]
      exact hone

Goal state after:
Module: Mathlib.Algebra.DirectSum.Decomposition

Goal state before:
pp: ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid M
inst✝⁴ : SetLike σ M
inst✝³ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝² : Decomposition ℳ
P : Type u_5
inst✝¹ : SetLike P M
inst✝ : AddSubmonoidClass P M
p q : P
hp : SetLike.IsHomogeneous ℳ p
hq : SetLike.IsHomogeneous ℳ q
hpq : ∀ (i : ι), ∀ m ∈ ℳ i, m ∈ p ↔ m ∈ q
m : M
⊢ m ∈ p ↔ m ∈ q

Tactic:
rw [AddSubmonoidClass.IsHomogeneous.mem_iff ℳ p hp,
    AddSubmonoidClass.IsHomogeneous.mem_iff ℳ q hq]

Goal state after:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid M
inst✝⁴ : SetLike σ M
inst✝³ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝² : Decomposition ℳ
P : Type u_5
inst✝¹ : SetLike P M
inst✝ : AddSubmonoidClass P M
p q : P
hp : SetLike.IsHomogeneous ℳ p
hq : SetLike.IsHomogeneous ℳ q
hpq : ∀ (i : ι), ∀ m ∈ ℳ i, m ∈ p ↔ m ∈ q
m : M
⊢ (∀ (i : ι), ↑(((decompose ℳ) m) i) ∈ p) ↔ ∀ (i : ι), ↑(((decompose ℳ) m) i) ∈ q
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
c₁ : Basis n' R M₁
c₂ : Basis m' R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ (toMatrix₂ c₁ c₂) (B.compl₁₂ id id) = (toMatrix₂ c₁ c₂) B

Tactic:
LinearMap.compl₁₂_id_id

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
c₁ : Basis n' R M₁
c₂ : Basis m' R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ (toMatrix₂ c₁ c₂) B = (toMatrix₂ c₁ c₂) B
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case succ
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
n✝ : ℕ
n_ih : ↑n✝ ∈ A 0
⊢ ↑n✝ + 1 ∈ A 0

Tactic:
exact add_mem n_ih (SetLike.one_mem_graded _)

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
ι_mul : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((ι Q) m * x)
⊢ ∀ (x : CliffordAlgebra Q), P x

Tactic:
refine reverse_involutive.surjective.forall.2 ?_
  intro x
  induction x using CliffordAlgebra.right_induction with
  | algebraMap r => simpa only [reverse.commutes] using algebraMap r
  | add _ _ hx hy => simpa only [map_add] using add _ _ hx hy
  | mul_ι _ _ hx => simpa only [reverse.map_mul, reverse_ι] using ι_mul _ _ hx

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem_mul_mem.add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n✝ : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n✝ → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n✝.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n✝) (hy : y ∈ evenOdd Q n✝),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n✝), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ evenOdd Q n✝
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n✝.val
x y : CliffordAlgebra Q
n : ℕ
hx : x ∈ ((ι Q).range ^ 2) ^ n
hy : y ∈ ((ι Q).range ^ 2) ^ n
ihx : motive (x * b) ⋯
ihy : motive (y * b) ⋯
⊢ motive ((x + y) * b) ⋯

Tactic:
simp_rw [add_mul]
      apply add _ _ _ _ ihx ihy

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem_mul_mem.mem_mul.mem_mul_mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n✝ : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n✝ → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n✝.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n✝) (hy : y ∈ evenOdd Q n✝),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n✝), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n✝
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n✝.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ ((ι Q).range ^ 2) ^ n''
ihy : motive (y * b) ⋯
m : CliffordAlgebra Q
hm : m ∈ (ι Q).range
n : CliffordAlgebra Q
hn : n ∈ (ι Q).range
⊢ motive (m * n * y * b) ⋯

Tactic:
simp_rw [LinearMap.mem_range] at hm hn
        obtain ⟨m₁, rfl⟩ := hm; obtain ⟨m₂, rfl⟩ := hn
        simp_rw [mul_assoc _ y b]
        exact ι_mul_ι_mul _ _ _ _ ihy

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ExteriorAlgebra R M →ₗ[R] M

Tactic:
letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
  haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
  exact (TrivSqZeroExt.sndHom R M).comp toTrivSqZeroExt.toLinearMap

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ limMap (F.whiskerLeft (restriction R (f ≫ g))) ≫
      limit.π ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j =
    limMap (F.whiskerLeft (restriction R f)) ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (limMap (F.whiskerLeft (restriction R g))) ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
              (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)).inv ≫
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
                ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).map (limit.π (F ⋙ evaluation R Z) j)) ≫
              (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                  (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ ((F ⋙ evaluation R Z).obj j)).inv

Tactic:
← Functor.map_comp_assoc,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ limMap (F.whiskerLeft (restriction R (f ≫ g))) ≫
      limit.π ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j =
    limMap (F.whiskerLeft (restriction R f)) ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
            (limMap (F.whiskerLeft (restriction R g)) ≫
              (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)).inv) ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
              ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).map (limit.π (F ⋙ evaluation R Z) j)) ≫
            (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ ((F ⋙ evaluation R Z).obj j)).inv
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ limMap (F.whiskerLeft (restriction R (f ≫ g))) ≫
      limit.π ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j =
    limMap (F.whiskerLeft (restriction R f)) ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
            (limMap (F.whiskerLeft (restriction R g)) ≫
              (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)).inv) ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
              ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).map (limit.π (F ⋙ evaluation R Z) j)) ≫
            (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ ((F ⋙ evaluation R Z).obj j)).inv

Tactic:
← Functor.map_comp_assoc,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ limMap (F.whiskerLeft (restriction R (f ≫ g))) ≫
      limit.π ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j =
    limMap (F.whiskerLeft (restriction R f)) ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
            ((limMap (F.whiskerLeft (restriction R g)) ≫
                (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)).inv) ≫
              (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).map (limit.π (F ⋙ evaluation R Z) j)) ≫
          (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
              (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ ((F ⋙ evaluation R Z).obj j)).inv
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ (F.obj j).map (f ≫ g) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))).map (colimit.ι (F ⋙ evaluation R Z) j) =
    (F.whiskerLeft (restriction R f)).app j ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (colimit.ι (F ⋙ evaluation R Y) j) ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
            (colimMap (F.whiskerLeft (restriction R g)) ≫
              (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)).inv) ≫
          (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
              (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))).inv

Tactic:
← Functor.map_comp_assoc,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ (F.obj j).map (f ≫ g) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))).map (colimit.ι (F ⋙ evaluation R Z) j) =
    (F.whiskerLeft (restriction R f)).app j ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
          (colimit.ι (F ⋙ evaluation R Y) j ≫
            colimMap (F.whiskerLeft (restriction R g)) ≫
              (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)).inv) ≫
        (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
            (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))).inv
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : Closed A
I : C
t : IsInitial I
f : A ⟶ I
⊢ Mono f

Tactic:
rw [← lift_snd (𝟙 A) f, ← zeroMul_hom t]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : Closed A
I : C
t : IsInitial I
f : A ⟶ I
⊢ Mono (lift (𝟙 A) f ≫ (zeroMul t).hom)
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G H K : C ⥤ D
⊢ (α_ F G H).hom ▷ K ≫ (α_ F (G ⊗ H) K).hom ≫ F ◁ (α_ G H K).hom = (α_ (F ⊗ G) H K).hom ≫ (α_ F G (H ⊗ K)).hom

Tactic:
ext X

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G H K : C ⥤ D
X : C
⊢ ((α_ F G H).hom ▷ K ≫ (α_ F (G ⊗ H) K).hom ≫ F ◁ (α_ G H K).hom).app X =
    ((α_ (F ⊗ G) H K).hom ≫ (α_ F G (H ⊗ K)).hom).app X
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
⊢ (α_ F G H).hom ≫ (NatIso.ofComponents (fun x ↦ β_ (F.obj x) ((G ⊗ H).obj x)) ⋯).hom ≫ (α_ G H F).hom =
    (NatIso.ofComponents (fun x ↦ β_ (F.obj x) (G.obj x)) ⋯).hom ▷ H ≫
      (α_ G F H).hom ≫ G ◁ (NatIso.ofComponents (fun x ↦ β_ (F.obj x) (H.obj x)) ⋯).hom

Tactic:
ext X

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
X : C
⊢ ((α_ F G H).hom ≫ (NatIso.ofComponents (fun x ↦ β_ (F.obj x) ((G ⊗ H).obj x)) ⋯).hom ≫ (α_ G H F).hom).app X =
    ((NatIso.ofComponents (fun x ↦ β_ (F.obj x) (G.obj x)) ⋯).hom ▷ H ≫
          (α_ G F H).hom ≫ G ◁ (NatIso.ofComponents (fun x ↦ β_ (F.obj x) (H.obj x)) ⋯).hom).app
      X
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
⊢ (α_ F G H).inv ≫ (NatIso.ofComponents (fun x ↦ β_ ((F ⊗ G).obj x) (H.obj x)) ⋯).hom ≫ (α_ H F G).inv =
    F ◁ (NatIso.ofComponents (fun x ↦ β_ (G.obj x) (H.obj x)) ⋯).hom ≫
      (α_ F H G).inv ≫ (NatIso.ofComponents (fun x ↦ β_ (F.obj x) (H.obj x)) ⋯).hom ▷ G

Tactic:
ext X

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
X : C
⊢ ((α_ F G H).inv ≫ (NatIso.ofComponents (fun x ↦ β_ ((F ⊗ G).obj x) (H.obj x)) ⋯).hom ≫ (α_ H F G).inv).app X =
    (F ◁ (NatIso.ofComponents (fun x ↦ β_ (G.obj x) (H.obj x)) ⋯).hom ≫
          (α_ F H G).inv ≫ (NatIso.ofComponents (fun x ↦ β_ (F.obj x) (H.obj x)) ⋯).hom ▷ G).app
      X