mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ι'
this : DecidableEq ι := σ.decidableEq
x : M₁ (σ.symm (σ (σ.symm i)))
⊢ ∀ (y : M₁ (σ.symm (σ (σ.symm i)))),
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) (x + y)) =
      (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) x) +
        (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) y)

Tactic:
y

Goal state after:
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 : ι'
this : DecidableEq ι := σ.decidableEq
x y : M₁ (σ.symm (σ (σ.symm i)))
⊢ (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) (x + y)) =
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) x) +
      (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) y)
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:
let := σ.decidableEq

Goal state after:
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
this : DecidableEq ι := σ.decidableEq
⊢ ∀ (x : M₁ (σ.symm i)),
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m i (c • x)) =
      c • (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m i x)
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 (fun i ↦ M₁ (σ.symm i)) M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
this : DecidableEq ι' := σ.symm.decidableEq
x : M₁ (σ.symm (σ i))
⊢ ∀ (y : M₁ (σ.symm (σ i))),
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) (x + y)) =
      (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) x) +
        (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) y)

Tactic:
y

Goal state after:
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 (fun i ↦ M₁ (σ.symm i)) M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
this : DecidableEq ι' := σ.symm.decidableEq
x y : M₁ (σ.symm (σ i))
⊢ (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) (x + y)) =
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) x) +
      (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) y)
Module: Mathlib.Algebra.Category.Grp.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
x y : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget GrpCat) x y
⊢ colimitInvAux F x = colimitInvAux F y

Tactic:
by
  apply G.mk_eq
  obtain ⟨k, f, g, hfg⟩ := h
  use k, f, g
  rw [map_inv, map_inv, inv_inj]
  exact hfg

Goal state after:
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 : (j : J) × ↑(F.obj j)
⊢ ∀ (b : (j : J) × ↑(F.obj j)),
    ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel x b → colimitInvAux F x = colimitInvAux F b

Tactic:
y

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
x✝ : ↑(G F)
x y : (j : J) × ↑(F.obj j)
⊢ ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel x y → colimitInvAux F x = colimitInvAux F y
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)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝ : DecidablePred P
h : DecidableEq { a // ¬P a }
m : (i : { a // ¬P a }) → M₁ ↑i
i : { a // ¬P a }
x : M₁ ↑i
⊢ ∀ (y : M₁ ↑i),
    f.domDomRestrict P (update m i (x + y)) = f.domDomRestrict P (update m i x) + f.domDomRestrict P (update m i y)

Tactic:
y

Goal state after:
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)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝ : DecidablePred P
h : DecidableEq { a // ¬P a }
m : (i : { a // ¬P a }) → M₁ ↑i
i : { a // ¬P a }
x y : M₁ ↑i
⊢ f.domDomRestrict P (update m i (x + y)) = f.domDomRestrict P (update m i x) + f.domDomRestrict P (update m i y)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case h
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
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : ¬∀ (x : n × o), (σ x).2 = x.2
k : n
x : o
hkx : ¬(σ (k, x)).2 = (k, x).2
⊢ (σ (k, x)).2 ≠ x

Tactic:
exact hkx

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

Goal state before:
pp: case refine_1
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x✝ y : M F
x : (j : J) × ↑(F.obj j)
⊢ ∀ (b₁ b₂ : (j : J) × ↑(F.obj j)),
    (F ⋙ forget MonCat).ColimitTypeRel b₁ b₂ → colimitMulAux F x b₁ = colimitMulAux F x b₂

Tactic:
y

Goal state after:
case refine_1
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x✝ y✝ : M F
x y : (j : J) × ↑(F.obj j)
⊢ ∀ (b₂ : (j : J) × ↑(F.obj j)), (F ⋙ forget MonCat).ColimitTypeRel y b₂ → colimitMulAux F x y = colimitMulAux F x b₂
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: case refine_2
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x✝ y : M F
x x' : (j : J) × ↑(F.obj j)
⊢ ∀ (b : (j : J) × ↑(F.obj j)), (F ⋙ forget MonCat).ColimitTypeRel x x' → colimitMulAux F x b = colimitMulAux F x' b

Tactic:
y

Goal state after:
case refine_2
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x✝ y✝ : M F
x x' y : (j : J) × ↑(F.obj j)
⊢ (F ⋙ forget MonCat).ColimitTypeRel x x' → colimitMulAux F x y = colimitMulAux F x' y
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ ∀ (b c : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j),
    Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel x *
        (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 x *
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b +
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel x *
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c

Tactic:
y

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x y : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ ∀ (c : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j),
    Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel x *
        (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel y +
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c) =
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel x *
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel y +
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel x *
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c
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 σ₁) * ↑↑(sign σ₂) * ((∏ x, A (σ₁ x) x) * ∏ x, D (σ₂ x) x) =
    ↑↑(sign (σ₁.sumCongr σ₂)) * ((∏ x, A (σ₁ x) x) * ∏ x, D (σ₂ x) x)

Tactic:
congr

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 (σ₁.sumCongr σ₂))
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: 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✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ f (update m i x) + f (update m i (-y)) = f (update m i x) + -f (update m i y)

Tactic:
map_update_neg

Goal state after:
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✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ f (update m i x) + -f (update m i y) = f (update m i x) + -f (update m i y)
Module: Mathlib.CategoryTheory.Limits.Types.Images

Goal state before:
pp: F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
a : F.obj (Opposite.op 0)
⊢ (fun x ↦
      match x with
      | Opposite.op n => preimage hF a n) ∈
    F.sections

Tactic:
intro ⟨n⟩ ⟨m⟩ ⟨⟨⟨(h : m ≤ n)⟩⟩⟩

Goal state after:
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
a : F.obj (Opposite.op 0)
n m : ℕ
h : m ≤ n
⊢ (ConcreteCategory.hom (F.map (Opposite.op { down := { down := h } })))
      ((fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op n)) =
    (fun x ↦
        match x with
        | Opposite.op n => preimage hF a n)
      (Opposite.op m)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
⊢ (-1) ^ ↑i * (↑↑(sign i.cycleRange⁻¹) * A.det) =
    (-1) ^ ↑i * ∑ i_1, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)

Tactic:
congr

Goal state after:
case e_a
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
⊢ ↑↑(sign i.cycleRange⁻¹) * A.det = ∑ i_1, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)
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

Tactic:
congr

Goal state after:
case insert.e_a.e_6
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
⊢ update (s.piecewise b a) k (s.piecewise b a k - b k) = fun j ↦
    if j = k ∨ j ∈ s → j < k then a j else if k = j then a j - b j else b j
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ ∀ (b c : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j),
    (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel x +
          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 x *
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c +
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b *
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c

Tactic:
y

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x y : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ ∀ (c : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j),
    (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel x +
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel y) *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c =
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel x *
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c +
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel y *
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F₁ F₂ : C × D ⥤ E
h : curry.obj F₁ = curry.obj F₂
⊢ uncurry.obj (curry.obj F₁) = F₂

Tactic:
← uncurry_obj_curry_obj F₂,

Goal state after:
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F₁ F₂ : C × D ⥤ E
h : curry.obj F₁ = curry.obj F₂
⊢ uncurry.obj (curry.obj F₁) = uncurry.obj (curry.obj F₂)
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:
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.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type r
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
x : E.pt
⊢ ∀ ⦃a₂ : ToType D.pt⦄,
    (fun x j ↦ (ConcreteCategory.hom (D.π.app j)) x) x = (fun x j ↦ (ConcreteCategory.hom (D.π.app j)) x) a₂ → x = a₂

Tactic:
y

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type r
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
x : E.pt
y : ToType D.pt
⊢ (fun x j ↦ (ConcreteCategory.hom (D.π.app j)) x) x = (fun x j ↦ (ConcreteCategory.hom (D.π.app j)) x) y → x = y
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasLimitsOfShape J C
k : K
W : C
f g : W ⟶ (limit H).obj k
w : ∀ (j : J), f ≫ (limit.π H j).app k = g ≫ (limit.π H j).app k
j : J
⊢ (f ≫ (limitObjIsoLimitCompEvaluation H k).hom) ≫ limit.π (H ⋙ (evaluation K C).obj k) j =
    (g ≫ (limitObjIsoLimitCompEvaluation H k).hom) ≫ limit.π (H ⋙ (evaluation K C).obj k) j

Tactic:
simpa using w j

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasColimitsOfShape J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g
j : J
⊢ colimit.ι (H ⋙ (evaluation K C).obj k) j ≫ (colimitObjIsoColimitCompEvaluation H k).inv ≫ f =
    colimit.ι (H ⋙ (evaluation K C).obj k) j ≫ (colimitObjIsoColimitCompEvaluation H k).inv ≫ g

Tactic:
simpa using w j

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 : ↑s.1
⊢ ∀ (y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget MonCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget MonCat).mapCone s).π.app j)) (x * y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget MonCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget MonCat).mapCone s).π.app j)) x, ⋯⟩ *
        EquivLike.coe (equivShrink ↑(F ⋙ forget MonCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget MonCat).mapCone s).π.app j)) y, ⋯⟩

Tactic:
y

Goal state after:
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
⊢ EquivLike.coe (equivShrink ↑(F ⋙ forget MonCat).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (((forget MonCat).mapCone s).π.app j)) (x * y), ⋯⟩ =
    EquivLike.coe (equivShrink ↑(F ⋙ forget MonCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget MonCat).mapCone s).π.app j)) x, ⋯⟩ *
      EquivLike.coe (equivShrink ↑(F ⋙ forget MonCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget MonCat).mapCone s).π.app j)) y, ⋯⟩
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: case refine_2.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s✝ : Cone F
x : ↑s✝.1
⊢ ∀ (y : ↑s✝.1),
    (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝)))
        (x * y) =
      (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) x *
        (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) y

Tactic:
y

Goal state after:
case refine_2.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s✝ : Cone F
x y : ↑s✝.1
⊢ (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝)))
      (x * y) =
    (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) x *
      (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) y