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

Goal state before:
pp: case insert
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
⊢ A.det = B.det

Tactic:
@ih (updateRow B i (A i)) (Function.update c i 0),

Goal state after:
case insert
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
⊢ (B.updateRow i (A i)).det = B.det

case insert.x
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_1 ∉ s, update c i 0 i_1 = 0

case insert.k
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
⊢ n

case insert.x
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
⊢ ?insert.k ∉ s

case insert.x
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_1 j : n), A i_1 j = B.updateRow i (A i) i_1 j + update c i 0 i_1 * B.updateRow i (A i) ?insert.k j
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
i j : Fin n.succ
⊢ M i j = N i j

Tactic:
refine Fin.cases (h0 j) (fun i => ?_) i

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
i : Fin n
⊢ M i.succ j = N i.succ j
Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : PreservesFilteredColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsFiltered J
⊢ PreservesColimitsOfShape J F

Tactic:
let e := ((ShrinkHoms.equivalence.{w'} J).trans <| Shrink.equivalence _).symm

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : PreservesFilteredColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsFiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
⊢ PreservesColimitsOfShape J F
Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : ReflectsFilteredColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsFiltered J
⊢ ReflectsColimitsOfShape J F

Tactic:
let e := ((ShrinkHoms.equivalence.{w'} J).trans <| Shrink.equivalence _).symm

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : ReflectsFilteredColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsFiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
⊢ ReflectsColimitsOfShape J F
Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : PreservesCofilteredLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsCofiltered J
⊢ PreservesLimitsOfShape J F

Tactic:
let e := ((ShrinkHoms.equivalence.{w'} J).trans <| Shrink.equivalence _).symm

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : PreservesCofilteredLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsCofiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
⊢ PreservesLimitsOfShape J F
Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : ReflectsCofilteredLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsCofiltered J
⊢ ReflectsLimitsOfShape J F

Tactic:
let e := ((ShrinkHoms.equivalence.{w'} J).trans <| Shrink.equivalence _).symm

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : ReflectsCofilteredLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsCofiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
⊢ ReflectsLimitsOfShape J F
Module: Mathlib.CategoryTheory.Limits.Types.Colimits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
hc : c.IsColimit
s : Cocone F
m : (F.coconeTypesEquiv c).pt ⟶ s.pt
hm : ∀ (j : J), (F.coconeTypesEquiv c).ι.app j ≫ m = s.ι.app j
⊢ m = ↾fun x ↦ hc.desc (F.coconeTypesEquiv.symm s) x

Tactic:
ext x
          exact congr_fun (hc.funext fun j ↦ funext fun y ↦ by simp [← hm j]) x

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
T : Type w₂
f g : c.pt → T
h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j
⊢ f = g

Tactic:
suffices Equiv.ulift.{w₃}.invFun.comp f =
        Equiv.ulift.invFun.comp g by
      ext x
      simpa using congr_fun this x
    exact hc.funext (fun j ↦ by simp [Function.comp_assoc, h])

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

Goal state before:
pp: case refine_2._hc
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.castSucc < ↑i.succ
⊢ update c k 0 i = 0

Tactic:
Fin.val_castSucc,

Goal state after:
case refine_2._hc
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.succ
⊢ update c k 0 i = 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case neg
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
j : Fin n.succ
hik : ¬i = k
hik2 : ¬k < i
⊢ ↑i.castSucc < ↑k.succ

Tactic:
Fin.val_castSucc,

Goal state after:
case neg
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
j : Fin n.succ
hik : ¬i = k
hik2 : ¬k < i
⊢ ↑i < ↑k.succ
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
⊢ 1 = M.mk F ⟨j, 1⟩

Tactic:
apply M.mk_eq

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) ⟨⋯.some, 1⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨j, 1⟩.snd
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x' y : (j : J) × ↑(F.obj j)
j₁ : J
x : ↑(F.obj j₁)
hxx' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) ⟨j₁, x⟩ x'
⊢ colimitMulAux F ⟨j₁, x⟩ y = colimitMulAux F x' y

Tactic:
obtain ⟨j₂, y⟩ := y

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x' : (j : J) × ↑(F.obj j)
j₁ : J
x : ↑(F.obj j₁)
hxx' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) ⟨j₁, x⟩ x'
j₂ : J
y : ↑(F.obj j₂)
⊢ colimitMulAux F ⟨j₁, x⟩ ⟨j₂, y⟩ = colimitMulAux F x' ⟨j₂, y⟩
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
x : ↑(F.obj j₁)
j₂ : J
y : ↑(F.obj j₂)
j₃ : J
x' : ↑(F.obj j₃)
l : J
f : ⟨j₁, x⟩.fst ⟶ l
g : ⟨j₃, x'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x'
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₃ j₂ ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ
h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β
⊢ colimitMulAux F ⟨j₁, x⟩ ⟨j₂, y⟩ = colimitMulAux F ⟨j₃, x'⟩ ⟨j₂, y⟩

Tactic:
apply M.mk_eq

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
x : ↑(F.obj j₁)
j₂ : J
y : ↑(F.obj j₂)
j₃ : J
x' : ↑(F.obj j₃)
l : J
f : ⟨j₁, x⟩.fst ⟶ l
g : ⟨j₃, x'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x'
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₃ j₂ ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ
h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β
⊢ ∃ k f g,
    (ConcreteCategory.hom (F.map f))
        ⟨IsFiltered.max ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst,
            (ConcreteCategory.hom (F.map (IsFiltered.leftToMax ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst))) ⟨j₁, x⟩.snd *
              (ConcreteCategory.hom (F.map (IsFiltered.rightToMax ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst))) ⟨j₂, y⟩.snd⟩.snd =
      (ConcreteCategory.hom (F.map g))
        ⟨IsFiltered.max ⟨j₃, x'⟩.fst ⟨j₂, y⟩.fst,
            (ConcreteCategory.hom (F.map (IsFiltered.leftToMax ⟨j₃, x'⟩.fst ⟨j₂, y⟩.fst))) ⟨j₃, x'⟩.snd *
              (ConcreteCategory.hom (F.map (IsFiltered.rightToMax ⟨j₃, x'⟩.fst ⟨j₂, y⟩.fst))) ⟨j₂, y⟩.snd⟩.snd
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✝⁹ : CommSemiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝² : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹ : (i : ι) → Module R (M₁' i)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
z : (i : { a // a ∉ s }) → M₁ ↑i
⊢ ∀ [inst : DecidableEq α] (m : α → (i : ι) → M₁ i) (i : α) (x y : (i : ι) → M₁ i),
    (((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i (x + y) (e.symm i_1) ↑i_1) =
      (((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i x (e.symm i_1) ↑i_1) +
        ((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i y (e.symm i_1) ↑i_1

Tactic:
by classical simp [iteratedFDeriv_aux]

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✝⁹ : CommSemiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝² : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹ : (i : ι) → Module R (M₁' i)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
z : (i : { a // a ∉ s }) → M₁ ↑i
⊢ ∀ [inst : DecidableEq α] (m : α → (i : ι) → M₁ i) (i : α) (c : R) (x : (i : ι) → M₁ i),
    (((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i (c • x) (e.symm i_1) ↑i_1) =
      c • ((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i x (e.symm i_1) ↑i_1

Tactic:
by classical simp [iteratedFDeriv_aux]

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
y : ↑(F.obj j₁)
j₂ : J
x : ↑(F.obj j₂)
j₃ : J
y' : ↑(F.obj j₃)
l : J
f : ⟨j₁, y⟩.fst ⟶ l
g : ⟨j₃, y'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) y = (ConcreteCategory.hom (F.map g)) y'
s : J
α : IsFiltered.max j₂ j₁ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₂ j₃ ⟶ s
h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β
h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ
h₃ : IsFiltered.rightToMax j₂ j₃ ≫ γ = g ≫ β
⊢ colimitMulAux F ⟨j₂, x⟩ ⟨j₁, y⟩ = colimitMulAux F ⟨j₂, x⟩ ⟨j₃, y'⟩

Tactic:
apply M.mk_eq

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
y : ↑(F.obj j₁)
j₂ : J
x : ↑(F.obj j₂)
j₃ : J
y' : ↑(F.obj j₃)
l : J
f : ⟨j₁, y⟩.fst ⟶ l
g : ⟨j₃, y'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) y = (ConcreteCategory.hom (F.map g)) y'
s : J
α : IsFiltered.max j₂ j₁ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₂ j₃ ⟶ s
h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β
h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ
h₃ : IsFiltered.rightToMax j₂ j₃ ≫ γ = g ≫ β
⊢ ∃ k f g,
    (ConcreteCategory.hom (F.map f))
        ⟨IsFiltered.max ⟨j₂, x⟩.fst ⟨j₁, y⟩.fst,
            (ConcreteCategory.hom (F.map (IsFiltered.leftToMax ⟨j₂, x⟩.fst ⟨j₁, y⟩.fst))) ⟨j₂, x⟩.snd *
              (ConcreteCategory.hom (F.map (IsFiltered.rightToMax ⟨j₂, x⟩.fst ⟨j₁, y⟩.fst))) ⟨j₁, y⟩.snd⟩.snd =
      (ConcreteCategory.hom (F.map g))
        ⟨IsFiltered.max ⟨j₂, x⟩.fst ⟨j₃, y'⟩.fst,
            (ConcreteCategory.hom (F.map (IsFiltered.leftToMax ⟨j₂, x⟩.fst ⟨j₃, y'⟩.fst))) ⟨j₂, x⟩.snd *
              (ConcreteCategory.hom (F.map (IsFiltered.rightToMax ⟨j₂, x⟩.fst ⟨j₃, y'⟩.fst))) ⟨j₃, y'⟩.snd⟩.snd
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
y : (j : J) × ↑(F.obj j)
k : J
g : y.fst ⟶ k
j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
⊢ M.mk F ⟨j₁, x⟩ * M.mk F y =
    M.mk F ⟨k, (ConcreteCategory.hom (F.map f)) ⟨j₁, x⟩.snd * (ConcreteCategory.hom (F.map g)) y.snd⟩

Tactic:
obtain ⟨j₂, y⟩ := y

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
⊢ M.mk F ⟨j₁, x⟩ * M.mk F ⟨j₂, y⟩ =
    M.mk F ⟨k, (ConcreteCategory.hom (F.map f)) ⟨j₁, x⟩.snd * (ConcreteCategory.hom (F.map g)) ⟨j₂, y⟩.snd⟩
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x y z : ↑(R F)
⊢ ∀ (a b c : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j),
    Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a *
        (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b +
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c) =
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a *
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b +
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a *
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c

Tactic:
clear x y z

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
y z : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
j₁ : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₁
⊢ Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
      (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel y +
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel z) =
    Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel y +
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel z

Tactic:
obtain ⟨j₂, y⟩ := y

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
z : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
j₁ : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₂
⊢ Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
      (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₂, y⟩ +
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel z) =
    Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₂, y⟩ +
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel z
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e'_3.refine_4.e_a
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 σ₁) * ↑↑(sign σ₂) = ↑(↑(sign σ₁) * ↑(sign σ₂))

Tactic:
Int.cast_mul

Goal state after:
case e'_3.refine_4.e_a
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 σ₁) * ↑↑(sign σ₂) = ↑↑(sign σ₁) * ↑↑(sign σ₂)