mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R
c : Fin n → R
A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0
A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc
⊢ A.det = B.det

Tactic:
rw [← det_transpose A, ← det_transpose B]
  exact det_eq_of_forall_row_eq_smul_add_pred c A_zero fun i j => A_succ j i

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

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₂
inst✝⁵ : SMulCommClass R S M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module S M₃
inst✝² : Module R M₃
inst✝¹ : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι'
m : (i : ι') → M₁ (σ.symm i)
i : ι'
c : R
⊢ ∀ (x : M₁ (σ.symm i)),
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m i (c • x)) =
      c • (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m i x)

Tactic:
by
        let := σ.decidableEq
        rw [← σ.apply_symm_apply i]
        intro x
        simp only [Function.comp, piCongrLeft'_symm_update, f.map_update_smul]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
inst✝² : HasLimit F
inst✝¹ : HasLimit (F ⋙ G)
inst✝ : IsIso (limit.post F G)
⊢ IsLimit (G.mapCone (limit.cone F))

Tactic:
by
    convert! IsLimit.ofPointIso (limit.isLimit (F ⋙ G))
    assumption

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s : Cone F
j : J
⊢ (hom ((hc (op s.pt)).lift ((coyoneda.obj (op s.pt)).mapCone s))) (𝟙 (unop (op s.pt))) ≫ c.π.app j = s.π.app j

Tactic:
by simpa using congr_hom ((hc (op s.pt)).fac
    ((coyoneda.obj (op s.pt)).mapCone s) j) (𝟙 s.pt)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Cᵒᵖ
⊢ PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (yoneda ⋙ (evaluation Cᵒᵖ (Type v)).obj K)

Tactic:
change PreservesLimitsOfSize (coyoneda.obj K)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Cᵒᵖ
⊢ PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (coyoneda.obj K)
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F G : K ⥤ J ⥤ C
η : F ⟶ G
k : K
j : J
⊢ (((whiskeringRight K (J ⥤ C) C).obj lim).map η ≫ (limitFlipIsoCompLim G).symm.hom).app k ≫
      (limit.π ((flipFunctor K J C).obj G) j).app k =
    ((limitFlipIsoCompLim F).symm.hom ≫ (flipFunctor K J C ⋙ lim).map η).app k ≫
      (limit.π ((flipFunctor K J C).obj G) j).app k

Tactic:
simp [comp_evaluation, ← NatTrans.comp_app (limMap _)]

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
J : Type u_1
inst✝² : Category.{v_1, u_1} J
F : J ⥤ AlgCat R
inst✝¹ : PreservesColimitsOfShape J (forget RingCat)
c : Cocone (F ⋙ forget₂ (AlgCat R) RingCat)
inst✝ : IsFilteredOrEmpty J
hc : IsColimit c
j k : J
⊢ F.obj k ⟶ ((Functor.const J).obj (of R ↑c.pt)).obj k

Tactic:
by
    letI : Algebra R c.pt := algebraOfIsFiltered hc j
    refine AlgCat.ofHom { __ := (c.ι.app k).hom, commutes' r := ?_ }
    simp [RingHom.algebraMap_toAlgebra', ← c.w (IsFiltered.leftToMax j k),
      ← c.w (IsFiltered.rightToMax j k)]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
T : D
⊢ T ◁ ε F ≫ T ◁ η F = 𝟙 (T ⊗ 𝟙_ D)

Tactic:
rw [← MonoidalCategory.whiskerLeft_comp, ε_η, MonoidalCategory.whiskerLeft_id]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
x✝ : C
⊢ 𝟙 (𝟙_ D ⊗ F.obj x✝) = (λ_ (F.obj x✝)).hom ≫ F.map (λ_ x✝).inv ≫ (h.μIso (𝟙_ C) x✝).inv ≫ h.εIso.inv ▷ F.obj x✝

Tactic:
h.left_unitality,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
x✝ : C
⊢ 𝟙 (𝟙_ D ⊗ F.obj x✝) =
    (h.εIso.hom ▷ F.obj x✝ ≫ (h.μIso (𝟙_ C) x✝).hom ≫ F.map (λ_ x✝).hom) ≫
      F.map (λ_ x✝).inv ≫ (h.μIso (𝟙_ C) x✝).inv ≫ h.εIso.inv ▷ F.obj x✝
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : Y ⊗ X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
⊢ F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      δ F (G.obj X) (G.obj Y ⊗ G.obj Z) ≫
        F.obj (G.obj X) ◁ δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y ⊗ₘ adj.counit.app Z) =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      F.map (G.obj X ◁ adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (Y ⊗ Z)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))

Tactic:
rw [← δ_natural_right_assoc, ← δ_natural_right_assoc, ← δ_natural_right_assoc]

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : Y ⊗ X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
⊢ F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      δ F (G.obj X) (G.obj Y ⊗ G.obj Z) ≫
        F.obj (G.obj X) ◁ δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y ⊗ₘ adj.counit.app Z) =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      δ F (G.obj X) (G.obj Y ⊗ G.obj Z) ≫
        F.obj (G.obj X) ◁ F.map (adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
          F.obj (G.obj X) ◁ F.map (G.map (δ F (G.obj Y) (G.obj Z))) ≫
            F.obj (G.obj X) ◁ F.map (G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
              (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : PreservesLimit (cospan f g) G
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
⊢ (iso G f g).hom ≫ pullback.fst (G.map f) (G.map g) = G.map (pullback.fst f g)

Tactic:
simp [PreservesPullback.iso]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : PreservesLimit (cospan f g) G
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
⊢ (iso G f g).hom ≫ pullback.snd (G.map f) (G.map g) = G.map (pullback.snd f g)

Tactic:
simp [PreservesPullback.iso]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.ContainsIdentities
x : C
⊢ W (𝟙 x)

Tactic:
exact id_mem x

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
⊢ ∀ ⦃X Y : Arrow (Type u)⦄ (f : X ⟶ Y),
    ({ obj := fun f ↦ ↑(Set.range ⇑(TypeCat.Hom.hom f.hom)),
              map := fun {X Y} φ ↦ ↾fun y ↦ ⟨(hom (Arrow.Hom.right φ)) ↑y, ⋯⟩,
              map_id := functorialSurjectiveInjectiveFactorizationData._proof_2,
              map_comp := @functorialSurjectiveInjectiveFactorizationData._proof_3 }.map
          f ≫
        ↾fun y ↦ ↑y) =
      (↾fun y ↦ ↑y) ≫ Arrow.rightFunc.map f

Tactic:
intros; rfl;

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
⊢ (adj.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫
      μ G (F.obj (X ⊗ Y)) (F.obj Z) ≫
        G.map
          ((adj.homEquiv (X ⊗ Y) (F.obj X ⊗ F.obj Y)).symm
                ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)) ▷
              F.obj Z ≫
            (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom) =
    (α_ X Y Z).hom ≫
      (adj.unit.app X ⊗ₘ adj.unit.app (Y ⊗ Z)) ≫
        μ G (F.obj X) (F.obj (Y ⊗ Z)) ≫
          G.map
            (F.obj X ◁
              (adj.homEquiv (Y ⊗ Z) (F.obj Y ⊗ F.obj Z)).symm
                ((adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj Y) (F.obj Z)))

Tactic:
conv_lhs =>
      rw [homEquiv_counit, map_comp_assoc, map_comp,
        ← μ_natural_left_assoc, map_comp, map_comp, tensorHom_def'_assoc]
      dsimp
      rw [← comp_whiskerRight_assoc]

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
⊢ (X ⊗ Y) ◁ adj.unit.app Z ≫
      (adj.unit.app (X ⊗ Y) ≫
            G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
              G.map (F.map (μ G (F.obj X) (F.obj Y))) ≫ G.map (adj.counit.app (F.obj X ⊗ F.obj Y))) ▷
          G.obj (F.obj Z) ≫
        μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
    (α_ X Y Z).hom ≫
      (adj.unit.app X ⊗ₘ adj.unit.app (Y ⊗ Z)) ≫
        μ G (F.obj X) (F.obj (Y ⊗ Z)) ≫
          G.map
            (F.obj X ◁
              (adj.homEquiv (Y ⊗ Z) (F.obj Y ⊗ F.obj Z)).symm
                ((adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj Y) (F.obj Z)))
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: case a
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : BraidedCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : BraidedCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
inst✝² : BraidedCategory E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxBraided
inst✝ : G.LaxBraided
X Y : C
| G.map (μ F X Y ≫ F.map (β_ X Y).hom)

pp: case a
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : BraidedCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : BraidedCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
inst✝² : BraidedCategory E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxBraided
inst✝ : G.LaxBraided
X Y : C
| μ G (F.obj X) (F.obj Y)

Tactic:
braided,

Goal state after:
case a
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : BraidedCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : BraidedCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
inst✝² : BraidedCategory E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxBraided
inst✝ : G.LaxBraided
X Y : C
| G.map ((β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X)

case a
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : BraidedCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : BraidedCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
inst✝² : BraidedCategory E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxBraided
inst✝ : G.LaxBraided
X Y : C
| μ G (F.obj X) (F.obj Y)
Module: Mathlib.CategoryTheory.Functor.TwoSquare

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Category.{v₂, u₂} C₂
inst✝⁶ : Category.{v₃, u₃} C₃
inst✝⁵ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
C₅ : Type u₅
C₆ : Type u₆
C₇ : Type u₇
C₈ : Type u₈
inst✝⁴ : Category.{v₅, u₅} C₅
inst✝³ : Category.{v₆, u₆} C₆
inst✝² : Category.{v₇, u₇} C₇
inst✝¹ : Category.{v₈, u₈} C₈
T' : C₂ ⥤ C₅
R' : C₅ ⥤ C₆
B' : C₄ ⥤ C₆
L' : C₃ ⥤ C₇
R'' : C₄ ⥤ C₈
B'' : C₇ ⥤ C₈
C₉ : Type u₉
inst✝ : Category.{v₉, u₉} C₉
R₃ : C₆ ⥤ C₉
B₃ : C₈ ⥤ C₉
w₁ : TwoSquare T L R B
w₂ : TwoSquare T' R R' B'
w₃ : TwoSquare B L' R'' B''
w₄ : TwoSquare B' R'' R₃ B₃
⊢ (w₁ ≫ₕ w₂) ≫ᵥ w₃ ≫ₕ w₄ = (w₁ ≫ᵥ w₃) ≫ₕ w₂ ≫ᵥ w₄

Tactic:
by
  unfold hComp vComp whiskerLeft whiskerRight
  ext c
  simp only [comp_obj, NatTrans.comp_app, associator_hom_app, associator_inv_app, comp_id, id_comp,
    map_comp, assoc]
  slice_rhs 2 3 =>
    rw [← Functor.comp_map _ B₃, ← w₄.naturality]
  simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (quotToQuotUlift F) ((Quot.ι F j) x) = (Quot.ι (F ⋙ uliftFunctor) j) { down := x }

Tactic:
dsimp [quotToQuotUlift, Quot.ι]
  conv_lhs => erw [AddMonoidHom.comp_apply (QuotientAddGroup.mk' (Relations F))
    (DFinsupp.singleAddHom _ j), QuotientAddGroup.lift_mk']
  simp only [DFinsupp.singleAddHom_apply, DFinsupp.sumAddHom_single]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : F.LaxBraided
W X Y Z : C
⊢ (α_ (F.obj W) (F.obj X) (F.obj Y ⊗ F.obj Z)).hom ≫
      F.obj W ◁ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫
        F.obj W ◁ (β_ (F.obj X) (F.obj Y)).hom ▷ F.obj Z ≫
          F.obj W ◁ (α_ (F.obj Y) (F.obj X) (F.obj Z)).hom ≫
            (α_ (F.obj W) (F.obj Y) (F.obj X ⊗ F.obj Z)).inv ≫
              μ F W Y ▷ (F.obj X ⊗ F.obj Z) ≫
                (α_ (F.obj (W ⊗ Y)) (F.obj X) (F.obj Z)).inv ≫
                  μ F (W ⊗ Y) X ▷ F.obj Z ≫ μ F ((W ⊗ Y) ⊗ X) Z ≫ F.map (α_ (W ⊗ Y) X Z).hom =
    (μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (W ⊗ X) (Y ⊗ Z) ≫
        F.map
          ((α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ W ◁ (β_ X Y).hom ▷ Z ≫ W ◁ (α_ Y X Z).hom ≫ (α_ W Y (X ⊗ Z)).inv)

Tactic:
associator_inv_naturality_left_assoc,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : F.LaxBraided
W X Y Z : C
⊢ (α_ (F.obj W) (F.obj X) (F.obj Y ⊗ F.obj Z)).hom ≫
      F.obj W ◁ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫
        F.obj W ◁ (β_ (F.obj X) (F.obj Y)).hom ▷ F.obj Z ≫
          F.obj W ◁ (α_ (F.obj Y) (F.obj X) (F.obj Z)).hom ≫
            (α_ (F.obj W) (F.obj Y) (F.obj X ⊗ F.obj Z)).inv ≫
              (α_ (F.obj W ⊗ F.obj Y) (F.obj X) (F.obj Z)).inv ≫
                μ F W Y ▷ F.obj X ▷ F.obj Z ≫
                  μ F (W ⊗ Y) X ▷ F.obj Z ≫ μ F ((W ⊗ Y) ⊗ X) Z ≫ F.map (α_ (W ⊗ Y) X Z).hom =
    (μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (W ⊗ X) (Y ⊗ Z) ≫
        F.map
          ((α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ W ◁ (β_ X Y).hom ▷ Z ≫ W ◁ (α_ Y X Z).hom ≫ (α_ W Y (X ⊗ Z)).inv)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : F.LaxBraided
W X Y Z : C
⊢ tensorμ (F.obj W) (F.obj X) (F.obj Y) (F.obj Z) ≫ (μ F W Y ⊗ₘ μ F X Z) ≫ μ F (W ⊗ Y) (X ⊗ Z) =
    (μ F W X ⊗ₘ μ F Y Z) ≫ μ F (W ⊗ X) (Y ⊗ Z) ≫ F.map (tensorμ W X Y Z)

Tactic:
by
  rw [tensorHom_def]
  simp only [tensorμ, Category.assoc]
  rw [whiskerLeft_μ_comp_μ,
    associator_inv_naturality_left_assoc, ← pentagon_inv_assoc,
    ← comp_whiskerRight_assoc, ← comp_whiskerRight_assoc, Category.assoc, μ_whiskerRight_comp_μ,
    whiskerLeft_hom_inv_assoc, Iso.inv_hom_id_assoc, comp_whiskerRight_assoc,
    comp_whiskerRight_assoc, μ_natural_left_assoc, associator_inv_naturality_middle_assoc,
    ← comp_whiskerRight_assoc, ← comp_whiskerRight_assoc, ← MonoidalCategory.whiskerLeft_comp,
    ← Functor.LaxBraided.braided,
    MonoidalCategory.whiskerLeft_comp_assoc, μ_natural_right, whiskerLeft_μ_comp_μ_assoc,
    comp_whiskerRight_assoc, comp_whiskerRight_assoc, comp_whiskerRight_assoc,
    comp_whiskerRight_assoc, pentagon_inv_assoc, μ_natural_left_assoc, μ_natural_left_assoc,
    Iso.hom_inv_id_assoc, ← associator_inv_naturality_left_assoc, μ_whiskerRight_comp_μ_assoc,
    Iso.inv_hom_id_assoc, ← tensorHom_def_assoc]
  simp only [← Functor.map_comp, whisker_assoc, Category.assoc, pentagon_inv_inv_hom_hom_inv,
    pentagon_inv_hom_hom_hom_inv_assoc]

Goal state after:
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d✝ c : RingCon M
d : RingCon c.Quotient
y : c.Quotient
x : M
⊢ (mapGen ⇑c.mk') (c.mk' x) y ↔ d (c.mk' x) y

Tactic:
obtain ⟨y, rfl⟩ := c.mk'_surjective y

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d✝ c : RingCon M
d : RingCon c.Quotient
x y : M
⊢ (mapGen ⇑c.mk') (c.mk' x) (c.mk' y) ↔ d (c.mk' x) (c.mk' y)
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d✝ c : RingCon M
d : RingCon c.Quotient
x y : M
⊢ (mapGen ⇑c.mk') (c.mk' x) (c.mk' y) ↔ d (c.mk' x) (c.mk' y)

Tactic:
mapGen_apply_apply_of_surjective _ (comap_bot c.mk' ▸ comap_mono bot_le) c.mk'_surjective,

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d✝ c : RingCon M
d : RingCon c.Quotient
x y : M
⊢ (d.comap c.mk') x y ↔ d (c.mk' x) (c.mk' y)
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case cons
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map (fun x ↦ (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ (List.map
          ((fun x_1 ↦ x.fst •> x_1) ∘ fun x ↦
            (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
          xs.zipIdx).sum +
      x.snd <• (List.map fst xs).prod =
    x.snd <• (List.map fst xs).prod +
      (List.map
          (fun x_1 ↦
            x.fst •> (List.take x_1.2 (List.map fst xs)).prod •> x_1.1.snd <•
              (List.drop (x_1.2 + 1) (List.map fst xs)).prod)
          xs.zipIdx).sum

Tactic:
← smul_comm (_ : R) (_ : Rᵐᵒᵖ)

Goal state after:
case cons
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map (fun x ↦ (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ (List.map
          ((fun x_1 ↦ x.fst •> x_1) ∘ fun x ↦
            (List.take x.2 (List.map fst xs)).prod •> (x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod))
          xs.zipIdx).sum +
      x.snd <• (List.map fst xs).prod =
    x.snd <• (List.map fst xs).prod +
      (List.map
          (fun x_1 ↦
            x.fst •>
              (List.take x_1.2 (List.map fst xs)).prod •> (x_1.1.snd <• (List.drop (x_1.2 + 1) (List.map fst xs)).prod))
          xs.zipIdx).sum
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring R
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
m : M
⊢ IsUnit 0 ↔ Subsingleton R

Tactic:
isUnit_zero_iff,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring R
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
m : M
⊢ 0 = 1 ↔ Subsingleton R
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x : B
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((rTensor (A × B)
          ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
        ((TensorProduct.map (inl R A B) (inl R A B)) (comul 0) +
          (TensorProduct.map (inr R A B) (inr R A B)) (comul x))) =
    (lTensor (A × B)
        ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
      ((TensorProduct.map (inl R A B) (inl R A B)) (comul 0) + (TensorProduct.map (inr R A B) (inr R A B)) (comul x))

Tactic:
simp only [map_zero, zero_add]
      simp_rw [← comp_apply, ← comp_assoc, rTensor_comp_map, lTensor_comp_map, coprod_inr,
        ← map_comp_rTensor, ← map_comp_lTensor, comp_assoc, ← coassoc, ← comp_assoc,
        TensorProduct.map_map_comp_assoc_eq, comp_apply, LinearEquiv.coe_coe]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
⊢ α = β

Tactic:
by
  apply (restrictScalars f).map_injective
  let := f.toAlgebra
  ext : 1
  apply TensorProduct.ext'
  intro (s : S) m
  change α (s ⊗ₜ m) = β (s ⊗ₜ m)
  have : s ⊗ₜ[R] (m : M) = s • (1 : S) ⊗ₜ[R] m := by
    rw [ExtendScalars.smul_tmul, mul_one]
  simp only [this, map_smul, h]

Goal state after: