mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
A_eq_BC : (fun i ↦ ∑ j ∈ A i, g i j) = update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)
Beq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i ↦ ∑ j ∈ B i, g i j
Ceq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i ↦ ∑ j ∈ C i, g i j
Brec : (f fun i ↦ ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i ↦ g i (r i)
Crec : (f fun i ↦ ∑ j ∈ C i, g i j) = ∑ r ∈ piFinset C, f fun i ↦ g i (r i)
D : Disjoint (piFinset B) (piFinset C)
r : (a : ι) → α a
hr : r ∈ piFinset A
hri₀ : r i₀ = j₂
i : ι
hi : i = i₀
⊢ r i₀ ∈ C i₀

Tactic:
by

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 (Cone F)
this : Nonempty C
⊢ IsCofilteredOrEmpty C

Tactic:
by

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 (Cone F)
⊢ IsCofiltered C

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ (IsFiltered.coeqHom f.unop g.unop).op ≫ f = (IsFiltered.coeqHom f.unop g.unop).op ≫ g

Tactic:
by

Goal state after:
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.det = N.det

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:
· congr
    ext i j
    refine Fin.cases (h0 j) (fun i => ?_) i
    rw [hsucc, hc i (Fin.succ_pos _), zero_mul, add_zero]

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.det = N.det
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ f ≫ (IsCofiltered.eqHom f.unop g.unop).op = g ≫ (IsCofiltered.eqHom f.unop g.unop).op

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type w
I : α → Type u₁
inst✝¹ : (i : α) → Category.{v₁, u₁} (I i)
inst✝ : ∀ (i : α), IsFilteredOrEmpty (I i)
k l : (i : α) → I i
f g : k ⟶ l
s : α
⊢ (f ≫ fun s ↦ coeqHom (f s) (g s)) s = (g ≫ fun s ↦ coeqHom (f s) (g s)) s

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type w
I : α → Type u₁
inst✝¹ : (i : α) → Category.{v₁, u₁} (I i)
inst✝ : ∀ (i : α), IsCofilteredOrEmpty (I i)
k l : (i : α) → I i
f g : k ⟶ l
s : α
⊢ ((fun s ↦ eqHom (f s) (g s)) ≫ f) s = ((fun s ↦ eqHom (f s) (g s)) ≫ g) s

Tactic:
by

Goal state after:
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

Goal state after:
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✝¹ : IsCofilteredOrEmpty C
inst✝ : IsCofilteredOrEmpty D
k l : C × D
f g : k ⟶ l
⊢ (eqHom f.1 g.1, eqHom f.2 g.2) ≫ f = (eqHom f.1 g.1, eqHom f.2 g.2) ≫ g

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

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
G : J ⥤ Type w₀'
app : (j : J) → G.obj j → F.obj j
naturality :
  ∀ {j j' : J} (f : j ⟶ j'), app j' ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ app j
j✝ j'✝ : J
f : j✝ ⟶ j'✝
⊢ (c.ι j'✝ ∘ app j'✝) ∘ ⇑(ConcreteCategory.hom (G.map f)) = c.ι j✝ ∘ app j✝

Tactic:
by

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₀
t : F.ColimitType
⊢ ∃ j x, F.ιColimitType j x = t

Tactic:
by

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
⊢ ∀ (a b : (j : J) × F.obj j),
    F.ColimitTypeRel a b →
      (match a with
        | ⟨j, x⟩ => c.ι j x) =
        match b with
        | ⟨j, x⟩ => c.ι j x

Tactic:
by

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
⊢ Function.Surjective (F.descColimitType c) ↔ ∀ (z : c.pt), ∃ i x, c.ι i x = z

Tactic:
by

Goal state after:
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
⊢ IsStablyFiniteRing R

Tactic:
by

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.IsColimit
j : J
x : F.obj j
⊢ hc.equiv (hc.equiv.symm (c.ι j x)) = hc.equiv (F.ιColimitType j x)

Tactic:
by

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.IsColimit
y : c.pt
⊢ ∃ j x, c.ι j x = y

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
j✝ j'✝ : J
f : j✝ ⟶ j'✝
⊢ ⇑(ConcreteCategory.hom (c.ι.app j'✝)) ∘ ⇑(ConcreteCategory.hom (F.map f)) = ⇑(ConcreteCategory.hom (c.ι.app j✝))

Tactic:
by

Goal state after:
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
j : J
⊢ ((F.coconeTypesEquiv c).ι.app j ≫ ↾fun x ↦ hc.desc (F.coconeTypesEquiv.symm s) x) = s.ι.app j

Tactic:
by

Goal state after:
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
x : (F.coconeTypesEquiv c).pt
j : J
y : F.obj j
⊢ ((ConcreteCategory.hom m).toFun ∘ c.ι j) y =
    ((ConcreteCategory.hom (↾fun x ↦ hc.desc (F.coconeTypesEquiv.symm s) x)).toFun ∘ c.ι j) y

Tactic:
by

Goal state after:
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:
by

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.IsColimit
c' : F.CoconeTypes
⊢ ∀ (j : J), (F.descColimitType c' ∘ ⇑hc.equiv.symm) ∘ c.ι j = c'.ι j

Tactic:
by

Goal state after:
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 : Limits.IsColimit (F.coconeTypesEquiv c)
x y : F.ColimitType
h : F.descColimitType c x = F.descColimitType c y
f : F.ColimitType → ULift.{u, 0} Bool := fun z ↦ { down := decide (x = z) }
this : f x = f y
⊢ x = y

Tactic:
by

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.IsColimit
c' : F.CoconeTypes
e : c.pt ≃ c'.pt
he : ∀ (j : J) (x : F.obj j), c'.ι j x = e (c.ι j x)
⊢ Function.Bijective (F.descColimitType c')

Tactic:
by

Goal state after:
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 : Limits.IsColimit (F.coconeTypesEquiv c)
x y : F.ColimitType
h : F.descColimitType c x = F.descColimitType c y
f : F.ColimitType → ULift.{u, 0} Bool := fun z ↦ { down := decide (x = z) }
this :
  ∀ (z : F.ColimitType),
    (ConcreteCategory.hom (hc.desc (F.coconeTypesEquiv (F.coconeTypes.postcomp f)))) (F.descColimitType c z) = f z
⊢ f x = f y

Tactic:
by

Goal state after:
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:
by

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.IsColimit
c' : F.CoconeTypes
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
⊢ c'.IsColimit ↔ Function.Bijective f

Tactic:
by

Goal state after:
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 : Limits.IsColimit (F.coconeTypesEquiv c)
x : c.pt
f₁ : (F.coconeTypesEquiv c).pt ⟶ ULift.{u, 0} Bool := ↾fun x ↦ { down := true }
f₂ : (F.coconeTypesEquiv c).pt ⟶ ULift.{u, 0} Bool := ↾fun x ↦ { down := decide (∃ a, F.descColimitType c a = x) }
this : f₁ = f₂
⊢ ∃ a, F.descColimitType c a = x

Tactic:
by

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 ∘ hc.desc (c'.postcomp ⇑Equiv.ulift.symm)) ∘ c.ι j = c'.ι j

Tactic:
by

Goal state after:
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 : Limits.IsColimit (F.coconeTypesEquiv c)
x✝ : c.pt
f₁ : (F.coconeTypesEquiv c).pt ⟶ ULift.{u, 0} Bool := ↾fun x ↦ { down := true }
f₂ : (F.coconeTypesEquiv c).pt ⟶ ULift.{u, 0} Bool := ↾fun x ↦ { down := decide (∃ a, F.descColimitType c a = x) }
j : J
x : F.obj j
⊢ F.descColimitType c (F.ιColimitType j x) = c.ι j x

Tactic:
by

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
this : Equiv.ulift.invFun ∘ f = Equiv.ulift.invFun ∘ g
⊢ f = g

Tactic:
by

Goal state after:
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
⊢ c.IsColimit ↔ Nonempty (Limits.IsColimit (F.coconeTypesEquiv c))

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
⊢ Nonempty (IsColimit c) ↔ (F.coconeTypesEquiv.symm c).IsColimit

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : Small.{u, max u v} F.ColimitType
⊢ ∀ (j : J) (x : F.obj j),
    (F.coconeTypesEquiv.symm (colimitCocone F)).ι j x = (equivShrink F.ColimitType) (F.coconeTypes.ι j x)

Tactic:
by

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
j : J
⊢ (Equiv.ulift.invFun ∘ f) ∘ c.ι j = (Equiv.ulift.invFun ∘ g) ∘ c.ι j

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j : J
x : F.obj j
⊢ (colimitEquivColimitType F) ((hom (colimit.ι F j)) x) = Quot.mk F.ColimitTypeRel ⟨j, x⟩

Tactic:
by

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:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j j' : J
x : F.obj j
f : j ⟶ j'
⊢ (hom (colimit.ι F j')) ((hom (F.map f)) x) = (hom (colimit.ι F j)) x

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
f : j ⟶ j'
w : (hom (F.map f)) x = x'
⊢ (hom (colimit.ι F j)) x = (hom (colimit.ι F j')) x'

Tactic:
by

Goal state after:
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 : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
A_eq_BC : (fun i ↦ ∑ j ∈ A i, g i j) = update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)
Beq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i ↦ ∑ j ∈ B i, g i j
Ceq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i ↦ ∑ j ∈ C i, g i j
Brec : (f fun i ↦ ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i ↦ g i (r i)
Crec : (f fun i ↦ ∑ j ∈ C i, g i j) = ∑ r ∈ piFinset C, f fun i ↦ g i (r i)
D : Disjoint (piFinset B) (piFinset C)
r : (a : ι) → α a
hr : r ∈ piFinset A
hri₀ : ¬r i₀ = j₂
i : ι
hi : i = i₀
⊢ r i₀ ∈ B i₀

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
j'' : J
f : j ⟶ j''
f' : j' ⟶ j''
w : (hom (F.map f)) x = (hom (F.map f')) x'
⊢ (hom (colimit.ι F j)) x = (hom (colimit.ι F j')) x'

Tactic:
by

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
G : J ⥤ Type w₀'
e : (j : J) → G.obj j ≃ F.obj j
naturality :
  ∀ {j j' : J} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)
c' : G.CoconeTypes
j : J
⊢ hc.desc (c'.precompose (fun {j'} ↦ ⇑(e j').symm) ⋯) ∘ (c.precompose (fun {j'} ↦ ⇑(e j')) ⋯).ι j = c'.ι j

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
w : (hom (colimit.ι F j)) x = (hom (colimit.ι F j')) x'
⊢ Relation.EqvGen F.ColimitTypeRel ⟨j, x⟩ ⟨j', x'⟩

Tactic:
by

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
G : J ⥤ Type w₀'
e : (j : J) → G.obj j ≃ F.obj j
naturality :
  ∀ {j j' : J} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)
T : Type w₂
f g : (c.precompose (fun {j'} ↦ ⇑(e j')) ⋯).pt → T
h : ∀ (j : J), f ∘ (c.precompose (fun {j'} ↦ ⇑(e j')) ⋯).ι j = g ∘ (c.precompose (fun {j'} ↦ ⇑(e j')) ⋯).ι j
j : J
⊢ f ∘ c.ι j = g ∘ c.ι j

Tactic:
by

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
y : F.ColimitType
⊢ hc.down.desc F.coconeTypes (F.descColimitType c y) = y

Tactic:
by

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
j : J
⊢ (F.descColimitType c ∘ hc.down.desc F.coconeTypes) ∘ c.ι j = id ∘ c.ι j

Tactic:
by

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
⊢ Function.RightInverse (hc.down.desc F.coconeTypes) (F.descColimitType c)

Tactic:
by

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
⊢ Function.Bijective (F.descColimitType c)

Tactic:
let e : F.ColimitType ≃ c.pt :=
      { toFun := F.descColimitType c
        invFun := (down.{max u w₁} hc).desc F.coconeTypes
        left_inv y := by
          obtain ⟨j, x, rfl⟩ := F.ιColimitType_jointly_surjective y
          simp
        right_inv := by
          have : (F.descColimitType c).comp
              ((down.{max u w₁} hc).desc F.coconeTypes) = id :=
            (down.{max u w₀} hc).funext (fun j ↦ by
              rw [Function.id_comp, Function.comp_assoc, fac,
                coconeTypes_ι, descColimitType_comp_ι])
          exact congr_fun this }
    exact e.bijective

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
⊢ Function.Bijective (F.descColimitType c)

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
⊢ ∃ j y, (hom (t.ι.app j)) y = x

Tactic:
by

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
G : J ⥤ Type w₀'
e : (j : J) → G.obj j ≃ F.obj j
naturality :
  ∀ {j j' : J} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)
hc : (c.precompose (fun {j'} ↦ ⇑(e j')) ⋯).IsColimit
⊢ ∀ (j : J) (x : F.obj j),
    c.ι j x =
      (Equiv.refl ((c.precompose (fun {j'} ↦ ⇑(e j')) ⋯).precompose (fun {j'} ↦ ⇑(e j').symm) ⋯).pt)
        (((c.precompose (fun {j'} ↦ ⇑(e j')) ⋯).precompose (fun {j'} ↦ ⇑(e j').symm) ⋯).ι j x)

Tactic:
by

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₀
⊢ Function.Bijective (F.descColimitType F.coconeTypes)

Tactic:
by

Goal state after: