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

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ ∑ i ∈ (ofSign 1).disjUnion (ofSign (-1)) ⋯,
      sign ((Equiv.inv (Perm n)) i) • ∏ i_1, M (((Equiv.inv (Perm n)) i) i_1) i_1 =
    detp 1 M - detp (-1) M

Tactic:
sum_disjUnion

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ ∑ x ∈ ofSign 1, sign ((Equiv.inv (Perm n)) x) • ∏ i, M (((Equiv.inv (Perm n)) x) i) i +
      ∑ x ∈ ofSign (-1), sign ((Equiv.inv (Perm n)) x) • ∏ i, M (((Equiv.inv (Perm n)) x) i) i =
    detp 1 M - detp (-1) M
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
p : n → n
H : ¬Bijective p
i j : n
hpij : p i = p j
hij : i ≠ j
σ : Perm n
x✝ : σ ∈ univ
⊢ ↑↑(sign σ) * ∏ x, M (σ x) (p x) * N (p x) x +
      ↑↑(sign (σ * Equiv.swap i j)) * ∏ x, M ((σ * Equiv.swap i j) x) (p x) * N (p x) x =
    0

Tactic:
by
        have : (∏ x, M (σ x) (p x)) = ∏ x, M ((σ * Equiv.swap i j) x) (p x) :=
          Fintype.prod_equiv (swap i j) _ _ (by simp [apply_swap_eq_self hpij])
        simp [this, sign_swap hij, -sign_swap', prod_mul_distrib]

Goal state after:
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 (Cocone F)
this✝ : Nonempty C
this : IsFilteredOrEmpty C
⊢ IsFiltered C

Tactic:
apply IsFiltered.mk

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e e' : m ≃ n
M : Matrix m m R
⊢ ↑↑(sign (e.trans e'.symm).symm) * M.det = ↑↑(sign (e'.trans e.symm)) * M.det

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
i j : n
i_ne_j : i ≠ j
hij : ∀ (k : n), M k i = M k j
⊢ Mᵀ i = Mᵀ j

Tactic:
exact funext hij

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFilteredOrEmpty C
ι✝ : Type u_1
inst✝¹ : Finite ι✝
k₁ k₂ : C
ι : Type u_1
inst✝ : Fintype ι
IH : ∀ (j : ι → C) (f : (i : ι) → j i ⟶ k₁) (g : (i : ι) → j i ⟶ k₂), ∃ s α β, ∀ (i : ι), f i ≫ α = g i ≫ β
j : Option ι → C
f : (i : Option ι) → j i ⟶ k₁
g : (i : Option ι) → j i ⟶ k₂
s₁ : C
α₁ : k₁ ⟶ s₁
β₁ : k₂ ⟶ s₁
H₁ : ∀ (i : ι), f (some i) ≫ α₁ = g (some i) ≫ β₁
s₂ : C
α₂ : k₁ ⟶ s₂
β₂ : k₂ ⟶ s₂
H₂ : f none ≫ α₂ = g none ≫ β₂
t : C
α : s₁ ⟶ t
β : s₂ ⟶ t
h₁ : α₁ ≫ α = α₂ ≫ β
h₂ : β₁ ≫ α = β₂ ≫ β
⊢ f none ≫ α₁ ≫ α = g none ≫ β₁ ≫ α

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFilteredOrEmpty C
ι✝ : Type u_1
inst✝¹ : Finite ι✝
k₁ k₂ : C
ι : Type u_1
inst✝ : Fintype ι
IH : ∀ (j : ι → C) (f : (i : ι) → j i ⟶ k₁) (g : (i : ι) → j i ⟶ k₂), ∃ s α β, ∀ (i : ι), f i ≫ α = g i ≫ β
j : Option ι → C
f : (i : Option ι) → j i ⟶ k₁
g : (i : Option ι) → j i ⟶ k₂
s₁ : C
α₁ : k₁ ⟶ s₁
β₁ : k₂ ⟶ s₁
H₁ : ∀ (i : ι), f (some i) ≫ α₁ = g (some i) ≫ β₁
s₂ : C
α₂ : k₁ ⟶ s₂
β₂ : k₂ ⟶ s₂
H₂ : f none ≫ α₂ = g none ≫ β₂
t : C
α : s₁ ⟶ t
β : s₂ ⟶ t
h₁ : α₁ ≫ α = α₂ ≫ β
h₂ : β₁ ≫ α = β₂ ≫ β
⊢ ∀ (val : ι), f (some val) ≫ α₁ ≫ α = g (some val) ≫ β₁ ≫ α

Tactic:
grind

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ i ∉ ∅, c i = 0
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
⊢ ∀ (i : n), c i = 0

Tactic:
grind

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case pos
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
i' : n
hi' : i' ∉ s
hi'i : i' = i
⊢ 0 = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
⊢ ∀ (c : Fin n → R),
    (∀ (i : Fin n), k < 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

Tactic:
refine Fin.induction ?_ (fun k ih => ?_) k <;> intro c hc M N h0 hsucc

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
⊢ M.det = N.det

case refine_2
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.det = N.det
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2
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.det = N.det

Tactic:
set M' := updateRow M k.succ (N k.succ) with hM'

Goal state after:
case refine_2
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.det = N.det
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : IsFilteredOrEmpty D
k l : C × D
f g : k ⟶ l
⊢ f ≫ (coeqHom f.1 g.1, coeqHom f.2 g.2) = g ≫ (coeqHom f.1 g.1, coeqHom f.2 g.2)

Tactic:
by simp [coeq_condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimitCore
c' : F.CoconeTypes
j : J
⊢ Equiv.ulift.toFun ∘ (c'.postcomp ⇑Equiv.ulift.symm).ι j = c'.ι j

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
j : J
x : F.obj j
⊢ F.descColimitType F.coconeTypes (F.ιColimitType j x) = id (F.ιColimitType j x)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case pos
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)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
hi : ↑k ≤ ↑i
hik : i = k
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
⊢ (fun j ↦ if h : P j then update x i c ⟨j, h⟩ else z ⟨j, h⟩) =
    update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) c

Tactic:
grind

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ.symm x).2 = x.2
mk_apply_eq : ∀ (k : o) (x : n), ((σ (x, k)).1, k) = σ (x, k)
⊢ ∀ (k : o) (x : n), ((σ.symm (x, k)).1, k) = σ.symm (x, k)

Tactic:
grind

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_3
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ.symm x).2 = x.2
mk_apply_eq : ∀ (k : o) (x : n), ((σ (x, k)).1, k) = σ (x, k)
⊢ ∃ a, ∃ (_ : a ∈ univ), (prodCongrLeft fun k ↦ a k ⋯) = σ

Tactic:
have mk_inv_apply_eq : ∀ k x, ((σ.symm (x, k)).fst, k) = σ.symm (x, k) := by grind

Goal state after:
case refine_3
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ.symm x).2 = x.2
mk_apply_eq : ∀ (k : o) (x : n), ((σ (x, k)).1, k) = σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((σ.symm (x, k)).1, k) = σ.symm (x, k)
⊢ ∃ a, ∃ (_ : a ∈ univ), (prodCongrLeft fun k ↦ a k ⋯) = σ
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat) ⟨j, 0⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e'_3.refine_4
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m
σ₂ : Perm n
⊢ (↑↑(sign σ₁) * ∏ x, A (σ₁ x) x) * (↑↑(sign σ₂) * ∏ x, D (σ₂ x) x) =
    ↑↑(sign (σ₁.sumCongr σ₂)) *
      ((∏ a₁, fromBlocks A B 0 D ((σ₁.sumCongr σ₂) (Sum.inl a₁)) (Sum.inl a₁)) *
        ∏ a₂, fromBlocks A B 0 D ((σ₁.sumCongr σ₂) (Sum.inr a₂)) (Sum.inr a₂))

Tactic:
Equiv.sumCongr_apply,

Goal state after:
case e'_3.refine_4
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m
σ₂ : Perm n
⊢ (↑↑(sign σ₁) * ∏ x, A (σ₁ x) x) * (↑↑(sign σ₂) * ∏ x, D (σ₂ x) x) =
    ↑↑(sign (σ₁.sumCongr σ₂)) *
      ((∏ x, fromBlocks A B 0 D (Sum.map (⇑σ₁) (⇑σ₂) (Sum.inl x)) (Sum.inl x)) *
        ∏ x, fromBlocks A B 0 D (Sum.map (⇑σ₁) (⇑σ₂) (Sum.inr x)) (Sum.inr x))
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
⊢ ∑ y, sign (decomposeFin.symm (i.succ, y)) • ∏ x, A ((decomposeFin.symm (i.succ, y)) x) x =
    ∑ i_1,
      -1 *
        (A i.succ 0 *
          sign i_1 • ∏ i_2, (of fun i_3 j ↦ A (i.succ.succAbove i_3) j.succ).submatrix (⇑i.cycleRange) id (i_1 i_2) i_2)

Tactic:
refine Finset.sum_congr rfl fun σ _ => ?_

Goal state after:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝¹ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
σ : Perm (Fin n)
x✝ : σ ∈ univ
⊢ sign (decomposeFin.symm (i.succ, σ)) • ∏ x, A ((decomposeFin.symm (i.succ, σ)) x) x =
    -1 *
      (A i.succ 0 *
        sign σ • ∏ i_1, (of fun i_2 j ↦ A (i.succ.succAbove i_2) j.succ).submatrix (⇑i.cycleRange) id (σ i_1) i_1)
Module: Mathlib.CategoryTheory.Limits.Types.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
t : IsLimit c
x : ↑F.sections
j : J
⊢ (hom (c.π.app j)) ((isLimitEquivSections t).symm x) =
    ↑((isLimitEquivSections t).toFun ((isLimitEquivSections t).invFun x)) j

Tactic:
rfl

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j₁ : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₃
k : J := IsFiltered.max₃ j₁ j₂ j₃
f : j₁ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.firstToMax₃ j₁ j₂ j₃
g : j₂ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.secondToMax₃ j₁ j₂ j₃
h : j₃ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.thirdToMax₃ j₁ j₂ j₃
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat)
      ⟨k,
        (ConcreteCategory.hom (F.map f)) x * (ConcreteCategory.hom (F.map g)) y +
          (ConcreteCategory.hom (F.map f)) x * (ConcreteCategory.hom (F.map h)) z⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
      ⟨k,
        (ConcreteCategory.hom (𝟙 (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).obj k)))
            ((ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map f)) x *
              (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map g)) y) +
          (ConcreteCategory.hom (𝟙 (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).obj k)))
            ((ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map f)) x *
              (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map h)) z)⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Images

Goal state before:
pp: α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
x : Image f
⊢ ↑x = (ConcreteCategory.hom (ι f)).toFun x

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:

Tactic:
det A = ↑((-1 : ℤˣ) ^ (i : ℕ) * (-1 : ℤˣ) ^ (i : ℕ) : ℤˣ) * det A := by simp
      _ = (-1 : R) ^ (i : ℕ) * (Perm.sign i.cycleRange⁻¹) * det A := by simp [-Int.units_mul_self]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Images

Goal state before:
pp: case step
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
a : F.obj (Opposite.op 0)
n m p : ℕ
h : m.le p
ih :
  (ConcreteCategory.hom (F.map (Opposite.op { down := { down := h } })))
      ((fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op p)) =
    (fun x ↦
        match x with
        | Opposite.op n => preimage hF a n)
      (Opposite.op m)
h' : m ≤ p
⊢ (ConcreteCategory.hom (F.map (homOfLE h').op)) (preimage hF a p) =
    (ConcreteCategory.hom (F.map (Opposite.op { down := { down := h } })))
      ((fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op p))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Images

Goal state before:
pp: F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
⊢ c.π.app (Opposite.op 0) = (hc.conePointUniqueUpToIso (limitConeIsLimit F)).hom ≫ ↾fun u ↦ ↑u (Opposite.op 0)

Tactic:
rfl

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

Goal state before:
pp: case insert.e_a
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
⊢ f (update (s.piecewise b a) k (s.piecewise b a k - b k)) =
    f fun j ↦ if j = k ∨ j ∈ s → j < k then a j else if k = j then a j - b j else b j

pp: case insert.e_a
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
⊢ (∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j) =
    ∑ x ∈ s, f fun j ↦ if j = k ∨ j ∈ s → j < x then a j else if x = j then a j - b j else b j

Tactic:
· congr; ext i; split_ifs with h₁ h₂
    · rw [update_of_ne, Finset.piecewise_eq_of_notMem]
      · exact fun h ↦ (hk i h).not_gt (h₁ <| .inr h)
      · exact fun h ↦ (h₁ <| .inl h).ne h
    · cases h₂
      rw [update_self, s.piecewise_eq_of_notMem _ _ (lt_irrefl _ <| hk k ·)]
    · push Not at h₁
      rw [update_of_ne (Ne.symm h₂), s.piecewise_eq_of_mem _ _ (h₁.1.resolve_left <| Ne.symm h₂)]

Goal state after:
case insert.e_a
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
⊢ (∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j) =
    ∑ x ∈ s, f fun j ↦ if j = k ∨ j ∈ s → j < x then a j else if x = j then a j - b j else b j
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case insert.e_a
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
⊢ ∀ x ∈ s,
    (f fun j ↦ if j ∈ s → j < x then a j else if x = j then a j - b j else b j) =
      f fun j ↦ if j = k ∨ j ∈ s → j < x then a j else if x = j then a j - b j else b j

Tactic:
grind

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j₁ : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₃
k : J := IsFiltered.max₃ j₁ j₂ j₃
f : j₁ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.firstToMax₃ j₁ j₂ j₃
g : j₂ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.secondToMax₃ j₁ j₂ j₃
h : j₃ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.thirdToMax₃ j₁ j₂ j₃
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat)
      ⟨k,
        (ConcreteCategory.hom (F.map f)) x * (ConcreteCategory.hom (F.map h)) z +
          (ConcreteCategory.hom (F.map g)) y * (ConcreteCategory.hom (F.map h)) z⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
      ⟨k,
        (ConcreteCategory.hom (𝟙 (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).obj k)))
            ((ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map f)) x *
              (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map h)) z) +
          (ConcreteCategory.hom (𝟙 (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).obj k)))
            ((ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map g)) y *
              (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map h)) z)⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
j : J
⊢ ↑1 j = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
j : J
x✝¹ x✝ : (Types.Small.limitCone (F ⋙ forget MonCat)).pt
⊢ ↑((equivShrink ↑(F ⋙ forget MonCat).sections).symm x✝¹ * (equivShrink ↑(F ⋙ forget MonCat).sections).symm x✝) j =
    ↑((equivShrink ↑(F ⋙ forget MonCat).sections).symm x✝¹) j * ↑((equivShrink ↑(F ⋙ forget MonCat).sections).symm x✝) j

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: case refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s : Cone F
⊢ (equivShrink ↑(F ⋙ forget MonCat).sections) ⟨fun j ↦ 1, ⋯⟩ = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: case refine_2
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s : Cone F
x y : ↑s.1
⊢ ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) x * (ConcreteCategory.hom (s.π.app j)) y, ⋯⟩ =
    ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) x, ⋯⟩ * ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) y, ⋯⟩

Tactic:
rfl

Goal state after: