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

Goal state before:
pp: n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A + (detp 1 A • (B * adjp (-1) B + detp (-1) B • 1) + detp (-1) A • (B * adjp 1 B + detp 1 B • 1)) =
    detp 1 A • (B * adjp 1 B + detp (-1) B • 1) + detp (-1) A • (B * adjp (-1) B + detp 1 B • 1)
⊢ B * A = 1

Tactic:
smul_add,

Goal state after:
n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A + (detp 1 A • (B * adjp (-1) B) + detp 1 A • detp (-1) B • 1 + detp (-1) A • (B * adjp 1 B + detp 1 B • 1)) =
    detp 1 A • (B * adjp 1 B + detp (-1) B • 1) + detp (-1) A • (B * adjp (-1) B + detp 1 B • 1)
⊢ B * A = 1
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A + (detp 1 A • (B * adjp (-1) B) + detp 1 A • detp (-1) B • 1 + detp (-1) A • (B * adjp 1 B + detp 1 B • 1)) =
    detp 1 A • (B * adjp 1 B + detp (-1) B • 1) + detp (-1) A • (B * adjp (-1) B + detp 1 B • 1)
⊢ B * A = 1

Tactic:
smul_add,

Goal state after:
n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A +
      (detp 1 A • (B * adjp (-1) B) + detp 1 A • detp (-1) B • 1 +
        (detp (-1) A • (B * adjp 1 B) + detp (-1) A • detp 1 B • 1)) =
    detp 1 A • (B * adjp 1 B + detp (-1) B • 1) + detp (-1) A • (B * adjp (-1) B + detp 1 B • 1)
⊢ B * A = 1
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A +
      (detp 1 A • (B * adjp (-1) B) + detp 1 A • detp (-1) B • 1 +
        (detp (-1) A • (B * adjp 1 B) + detp (-1) A • detp 1 B • 1)) =
    detp 1 A • (B * adjp (-1) B + detp 1 B • 1) + detp (-1) A • (B * adjp (-1) B + detp 1 B • 1)
⊢ B * A = 1

Tactic:
smul_add,

Goal state after:
n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A +
      (detp 1 A • (B * adjp (-1) B) + detp 1 A • detp (-1) B • 1 +
        (detp (-1) A • (B * adjp 1 B) + detp (-1) A • detp 1 B • 1)) =
    detp 1 A • (B * adjp (-1) B) + detp 1 A • detp 1 B • 1 + detp (-1) A • (B * adjp (-1) B + detp 1 B • 1)
⊢ B * A = 1
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A +
      (detp 1 A • (B * adjp (-1) B) + detp 1 A • detp (-1) B • 1 +
        (detp (-1) A • (B * adjp 1 B) + detp (-1) A • detp 1 B • 1)) =
    detp 1 A • (B * adjp (-1) B) + detp 1 A • detp 1 B • 1 + detp (-1) A • (B * adjp 1 B + detp (-1) B • 1)
⊢ B * A = 1

Tactic:
smul_add,

Goal state after:
n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A +
      (detp 1 A • (B * adjp (-1) B) + detp 1 A • detp (-1) B • 1 +
        (detp (-1) A • (B * adjp 1 B) + detp (-1) A • detp 1 B • 1)) =
    detp 1 A • (B * adjp (-1) B) + detp 1 A • detp 1 B • 1 +
      (detp (-1) A • (B * adjp 1 B) + detp (-1) A • detp (-1) B • 1)
⊢ B * A = 1
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
⊢ IsCofiltered C

Tactic:
have : Nonempty C := by
    obtain ⟨c⟩ := h (Functor.empty _)
    exact ⟨c.pt⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
⊢ IsCofiltered C
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_1
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
⊢ M = N

Tactic:
ext i j

Goal state after:
case refine_1
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
i j : Fin n.succ
⊢ M i j = N i j
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A + (detp 1 A • (B * adjp (-1) B + detp (-1) B • 1) + detp (-1) A • (B * adjp 1 B + detp 1 B • 1)) =
    1 +
      (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B) +
        (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • 1)
⊢ B * A = 1

Tactic:
smul_add,

Goal state after:
n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A + (detp 1 A • (B * adjp (-1) B) + detp 1 A • detp (-1) B • 1 + detp (-1) A • (B * adjp 1 B + detp 1 B • 1)) =
    1 +
      (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B) +
        (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • 1)
⊢ B * A = 1
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A + (detp 1 A • (B * adjp (-1) B) + detp 1 A • detp (-1) B • 1 + detp (-1) A • (B * adjp 1 B + detp 1 B • 1)) =
    1 +
      (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B) +
        (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • 1)
⊢ B * A = 1

Tactic:
smul_add,

Goal state after:
n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A +
      (detp 1 A • (B * adjp (-1) B) + detp 1 A • detp (-1) B • 1 +
        (detp (-1) A • (B * adjp 1 B) + detp (-1) A • detp 1 B • 1)) =
    1 +
      (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B) +
        (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • 1)
⊢ B * A = 1
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
⊢ M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)

Tactic:
ext i j

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
i j : Fin n.succ
⊢ M i j = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc) i j
Module: Mathlib.Algebra.Category.Grp.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
x : ↑(G F)
⊢ x⁻¹ * x = 1

Tactic:
refine Quot.inductionOn x ?_

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
x : ↑(G F)
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).obj j),
    (Quot.mk ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel a)⁻¹ *
        Quot.mk ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel a =
      1
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x : ↑(R F)
⊢ 0 * x = 0

Tactic:
refine Quot.inductionOn x ?_

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x : ↑(R F)
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j),
    0 * Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a = 0
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x : ↑(R F)
⊢ x * 0 = 0

Tactic:
refine Quot.inductionOn x ?_

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x : ↑(R F)
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j),
    Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a * 0 = 0
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x : M F
⊢ 1 * x = x

Tactic:
obtain ⟨j, x, rfl⟩ := x.mk_surjective

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
x : ↑(F.obj j)
⊢ 1 * M.mk F ⟨j, x⟩ = M.mk F ⟨j, x⟩
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x : M F
⊢ x * 1 = x

Tactic:
obtain ⟨j, x, rfl⟩ := x.mk_surjective

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
x : ↑(F.obj j)
⊢ M.mk F ⟨j, x⟩ * 1 = M.mk F ⟨j, x⟩
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
t : Cocone F
m : (colimitCocone F).pt ⟶ t.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = t.ι.app j
x✝ : ↑(colimitCocone F).pt
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ (Hom.hom m) (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j, x⟩) =
    (Hom.hom
        (ofHom
          (let __src := descAddMonoidHom t;
          { toFun := (↑__src).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })))
      (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j, x⟩)

Tactic:
exact (ConcreteCategory.congr_hom ((forget SemiRingCat).congr_map (hm j)) x).trans
      (descAddMonoidHom_quotMk t x).symm

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
m : (colimitCocone X).pt ⟶ s.pt
w : ∀ (j : C), (colimitCocone X).ι.app j ≫ m = s.ι.app j
⊢ m = ↾fun x ↦ (hom (s.ι.app (unop X))) (𝟙 (unop X))

Tactic:
ext ⟨⟩
    simp [← w]

Goal state after:
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
F : J ⥤ K ⥤ C
c : Cocone F
t : (k : K) → IsColimit (((evaluation K C).obj k).mapCocone c)
s : Cocone F
X Y : K
f : X ⟶ Y
j : J
⊢ (((evaluation K C).obj X).mapCocone c).ι.app j ≫
      c.pt.map f ≫ (t Y).desc { pt := s.pt.obj Y, ι := whiskerRight s.ι ((evaluation K C).obj Y) } =
    (((evaluation K C).obj X).mapCocone c).ι.app j ≫
      (t X).desc { pt := s.pt.obj X, ι := whiskerRight s.ι ((evaluation K C).obj X) } ≫ s.pt.map f

Tactic:
by
          rw [(t X).fac_assoc _ j]
          erw [← (c.ι.app j).naturality_assoc f]
          erw [(t Y).fac ⟨s.pt.obj _, whiskerRight s.ι _⟩ j]
          simp

Goal state after:
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
F : J ⥤ K ⥤ C
G : D ⥤ K
inst✝ : HasColimitsOfShape J C
j : J
⊢ G.whiskerLeft (colimit.ι F j) ≫ (colimitCompWhiskeringLeftIsoCompColimit F G).inv =
    colimit.ι (F ⋙ (whiskeringLeft D K C).obj G) j

Tactic:
simp [Iso.comp_inv_eq]

Goal state after:
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✝ : HasColimitsOfShape J C
F G : K ⥤ J ⥤ C
η : F ⟶ G
⊢ (flipFunctor K J C ⋙ colim).map η ≫ (colimitFlipIsoCompColim G).hom =
    (colimitFlipIsoCompColim F).hom ≫ ((whiskeringRight K (J ⥤ C) C).obj colim).map η

Tactic:
ext k
    apply colimit_obj_ext
    intro j
    simp [comp_evaluation, ← NatTrans.comp_app_assoc _ (colimMap _)]

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
P : C ⥤ Type w
s : P.obj (unop X)
Y : Cᵒᵖ
f : Y ⟶ X
⊢ (ConcreteCategory.hom ((shrinkCoyonedaEquiv.symm s).app (unop Y))) (shrinkCoyonedaObjObjEquiv.symm f.unop) =
    (ConcreteCategory.hom (P.map f.unop)) s

Tactic:
by
  obtain ⟨g, rfl⟩ := shrinkCoyonedaEquiv.surjective s
  simp [map_shrinkCoyonedaEquiv]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ C
inst✝ : HasLimit F
j : J
⊢ (limit.π F j).op ≫ (colimitOpIsoOpLimit F).inv = colimit.ι F.op (op j)

Tactic:
simp [Iso.comp_inv_eq]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
inst✝ : HasLimit F
j : J
⊢ (limit.π F j).unop ≫ (colimitLeftOpIsoUnopLimit F).inv = colimit.ι F.leftOp (op j)

Tactic:
simp [Iso.comp_inv_eq]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
inst✝ : HasLimit F
j : Jᵒᵖ
⊢ (limit.π F j).op ≫ (colimitRightOpIsoUnopLimit F).inv = colimit.ι F.rightOp (unop j)

Tactic:
simp [Iso.comp_inv_eq]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
inst✝ : HasLimit F
j : Jᵒᵖ
⊢ (limit.π F j).unop ≫ (colimitUnopIsoOpLimit F).inv = colimit.ι F.unop (unop j)

Tactic:
simp [Iso.comp_inv_eq]

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

Goal state before:
pp: case f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ IsColimit c → IsLimit c.unop

Tactic:
intro h
    exact ((IsColimit.precomposeHomEquiv _ _).invFun
      ((IsColimit.whiskerEquivalenceEquiv _).toFun h)).unop

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

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
j : J
x : ↑(F.obj j)
⊢ (Quot.desc F s) ((AddEquiv.ofBijective (Quot.desc F c) h).symm ((Hom.hom (c.ι.app j)) x)) = (Hom.hom (s.ι.app j)) x

Tactic:
conv_lhs => erw [← Quot.ι_desc F c j x]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
j : J
x : ↑(F.obj j)
⊢ (Quot.desc F s) ((AddEquiv.ofBijective (Quot.desc F c) h).symm ((Quot.desc F c) ((Quot.ι F j) x))) =
    (Hom.hom (s.ι.app j)) x
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x₁ x₂ x₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x₁.1 •> (x₂.2 + x₃.2) + x₁.2 <• (x₂.1 + x₃.1) = x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)

Tactic:
smul_add,

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x₁ x₂ x₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x₁.1 •> x₂.2 + x₁.1 •> x₃.2 + x₁.2 <• (x₂.1 + x₃.1) = x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x₁ x₂ x₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x₁.1 •> x₃.2 + x₂.1 •> x₃.2 + (x₁.2 + x₂.2) <• x₃.1 = x₁.1 •> x₃.2 + x₁.2 <• x₃.1 + (x₂.1 •> x₃.2 + x₂.2 <• x₃.1)

Tactic:
smul_add,

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x₁ x₂ x₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x₁.1 •> x₃.2 + x₂.1 •> x₃.2 + (x₁.2 <• x₃.1 + x₂.2 <• x₃.1) =
    x₁.1 •> x₃.2 + x₁.2 <• x₃.1 + (x₂.1 •> x₃.2 + x₂.2 <• x₃.1)
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x y z : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (x.1 * y.1) •> z.2 + (x.1 •> y.2 + x.2 <• y.1) <• z.1 = x.1 •> (y.1 •> z.2 + y.2 <• z.1) + x.2 <• (y.1 * z.1)

Tactic:
smul_add,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x y z : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (x.1 * y.1) •> z.2 + (x.1 •> y.2 <• z.1 + x.2 <• y.1 <• z.1) =
    x.1 •> y.1 •> z.2 + x.1 •> (y.2 <• z.1) + x.2 <• (y.1 * z.1)
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
⊢ -0 = 0

Tactic:
neg_zero

Goal state after:
case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
⊢ 0 = 0
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ -0 = 0

Tactic:
neg_zero

Goal state after:
case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ 0 = 0
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hl
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 : A
⊢ (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 x) +
          (TensorProduct.map (inr R A B) (inr R A B)) (comul 0))) =
    (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 x) + (TensorProduct.map (inr R A B) (inr R A B)) (comul 0))

Tactic:
simp only [map_zero, add_zero]
      simp_rw [← comp_apply, ← comp_assoc, rTensor_comp_map, lTensor_comp_map, coprod_inl,
        ← 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.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
⊢ rTensor ((i : n) → A i) counit ∘ₗ comul = (TensorProduct.mk R R ((i : n) → A i)) 1

Tactic:
ext : 1
    rw [comp_assoc, comul_comp_single, ← comp_assoc, rTensor_comp_map, counit_comp_single,
      ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]

Goal state after: