mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.Colimits

Goal state before:
pp: case mpr.refine_2
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
⊢ (F.coconeTypesEquiv c).ι.app j ≫ f₁ = (F.coconeTypesEquiv c).ι.app j ≫ f₂

Tactic:
ext x

Goal state after:
case mpr.refine_2
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 := ⋯
f₂ : (F.coconeTypesEquiv c).pt ⟶ ULift.{u, 0} Bool := ⋯
j : J
x : F.obj j
⊢ ((ConcreteCategory.hom ((F.coconeTypesEquiv c).ι.app j ≫ f₁)).toFun x).down =
    ((ConcreteCategory.hom ((F.coconeTypesEquiv c).ι.app j ≫ f₂)).toFun x).down
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:
ext x

Goal state after:
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
x : c.pt
⊢ f x = g x
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:
ext x

Goal state after:
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
x : F.obj j
⊢ (f ∘ c.ι j) x = (g ∘ c.ι j) x
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
    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.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_2
inst✝ : DecidableEq ι
t : Finset α
i : ι
g : α → M₁ i
m : (i : ι) → M₁ i
⊢ f (update m i (∑ a ∈ t, g a)) = ∑ a ∈ t, f (update m i (g a))

Tactic:
induction t using Finset.induction with
    | empty => simp
    | insert _ _ has ih => simp [Finset.sum_insert has, ih]

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✝¹⁰ : Semiring R
inst✝⁹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap R (fun x ↦ M₂) M₃
x✝ : ι₁ → M₂
⊢ (domDomCongr σ.symm (domDomCongr σ m)) x✝ = m x✝

Tactic:
simp [domDomCongr]

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✝¹⁰ : Semiring R
inst✝⁹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap R (fun x ↦ M₂) M₃
x✝ : ι₂ → M₂
⊢ (domDomCongr σ (domDomCongr σ.symm m)) x✝ = m x✝

Tactic:
simp [domDomCongr]

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✝¹⁰ : Semiring R
inst✝⁹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
a b : MultilinearMap R (fun x ↦ M₂) M₃
x✝ : ι₂ → M₂
⊢ (domDomCongr σ (a + b)) x✝ = (domDomCongr σ a + domDomCongr σ b) x✝

Tactic:
simp [domDomCongr]

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = (hom (t.ι.app i)) xi
hinj :
  ∀ (i j : J) (xi : (fun X ↦ X) (F.obj i)) (xj : (fun X ↦ X) (F.obj j)),
    (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj → ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj
α : t.pt → J := fun x ↦ ⋯.choose
f : (x : t.pt) → F.obj (α x) := fun x ↦ ⋯.choose
hf : ∀ (x : t.pt), x = (hom (t.ι.app (α x))) (f x)
s : Cocone F
m : t.pt ⟶ s.pt
hm : ∀ (j : J), t.ι.app j ≫ m = s.ι.app j
⊢ m = ↾fun x ↦ (hom (s.ι.app (α x))) (f x)

Tactic:
ext x

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = (hom (t.ι.app i)) xi
hinj :
  ∀ (i j : J) (xi : (fun X ↦ X) (F.obj i)) (xj : (fun X ↦ X) (F.obj j)),
    (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj → ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj
α : t.pt → J := fun x ↦ ⋯.choose
f : (x : t.pt) → F.obj (α x) := fun x ↦ ⋯.choose
hf : ∀ (x : t.pt), x = (hom (t.ι.app (α x))) (f x)
s : Cocone F
m : t.pt ⟶ s.pt
hm : ∀ (j : J), t.ι.app j ≫ m = s.ι.app j
x : t.pt
⊢ (hom m).toFun x = (hom (↾fun x ↦ (hom (s.ι.app (α x))) (f x))).toFun 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 : Fin n.succ) → AddCommMonoid (M i)
inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M'
f✝ f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z✝ : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
z : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
c : R
a : M₁ ↑i
⊢ (f fun j ↦ if h : P j then update z i (c • a) ⟨j, h⟩ else z✝ ⟨j, h⟩) =
    c • f fun j ↦ if h : P j then update z i a ⟨j, h⟩ else z✝ ⟨j, h⟩

Tactic:
by
    classical
    repeat (rw [domDomRestrict_aux])
    simp only [MultilinearMap.map_update_smul]

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : (hom (F.map f)) x.snd = (hom (F.map g)) y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : (hom (F.map f')) y.snd = (hom (F.map g')) z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ (hom (F.map (fl ≫ n))) ((hom (F.map f)) x.snd) = (hom (F.map (fl ≫ n))) ((hom (F.map g)) y.snd)

Tactic:
by rw [h]

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

Goal state before:
pp: case e'_3.refine_2
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
a✝¹ : σ₁ ∈ ↑univ
σ₂ : Perm m × Perm n
a✝ : σ₂ ∈ ↑univ
h : σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2
h2 : (∀ (a : m), σ₁.1 a = σ₂.1 a) ∧ ∀ (b : n), σ₁.2 b = σ₂.2 b
⊢ σ₁ = σ₂

Tactic:
ext x

Goal state after:
case e'_3.refine_2.fst
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
a✝¹ : σ₁ ∈ ↑univ
σ₂ : Perm m × Perm n
a✝ : σ₂ ∈ ↑univ
h : σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2
h2 : (∀ (a : m), σ₁.1 a = σ₂.1 a) ∧ ∀ (b : n), σ₁.2 b = σ₂.2 b
x : m
⊢ σ₁.1 x = σ₂.1 x

case e'_3.refine_2.snd
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
a✝¹ : σ₁ ∈ ↑univ
σ₂ : Perm m × Perm n
a✝ : σ₂ ∈ ↑univ
h : σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2
h2 : (∀ (a : m), σ₁.1 a = σ₂.1 a) ∧ ∀ (b : n), σ₁.2 b = σ₂.2 b
x : n
⊢ σ₁.2 x = σ₂.2 x
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
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ (fromBlocks A B 0 D).det = A.det * D.det

Tactic:
classical
    simp_rw [det_apply']
    convert!
      Eq.symm <|
        sum_subset (M := R) (subset_univ ((sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset) ?_
    · simp_rw [sum_mul_sum, ← sum_product', univ_product_univ]
      refine sum_nbij (fun σ ↦ σ.fst.sumCongr σ.snd) ?_ ?_ ?_ ?_
      · intro σ₁₂ _
        simp
      · intro σ₁ _ σ₂ _
        dsimp only
        intro h
        have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x :=
          DFunLike.congr_fun h
        simp only [Sum.map_inr, Sum.map_inl, Perm.sumCongr_apply, Sum.forall, Sum.inl.injEq,
          Sum.inr.injEq] at h2
        ext x
        · exact h2.left x
        · exact h2.right x
      · intro σ hσ
        rw [mem_coe, Set.mem_toFinset] at hσ
        obtain ⟨σ₁₂, hσ₁₂⟩ := hσ
        use σ₁₂
        rw [← hσ₁₂]
        simp
      · simp only [forall_prop_of_true, Prod.forall, mem_univ]
        intro σ₁ σ₂
        rw [Fintype.prod_sum_type]
        simp_rw [Equiv.sumCongr_apply, Sum.map_inr, Sum.map_inl, fromBlocks_apply₁₁,
          fromBlocks_apply₂₂]
        rw [mul_mul_mul_comm]
        congr
        rw [sign_sumCongr, Units.val_mul, Int.cast_mul]
    · rintro σ - hσn
      have h1 : ¬∀ x, ∃ y, Sum.inl y = σ (Sum.inl x) := by
        rw [Set.mem_toFinset] at hσn
        simpa only [Set.MapsTo, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff] using
          mt mem_sumCongrHom_range_of_perm_mapsTo_inl hσn
      obtain ⟨a, ha⟩ := not_forall.mp h1
      rcases hx : σ (Sum.inl a) with a2 | b
      · have hn := (not_exists.mp ha) a2
        exact absurd hx.symm hn
      · rw [Finset.prod_eq_zero (Finset.mem_univ (Sum.inl a)), mul_zero]
        rw [hx, fromBlocks_apply₂₁, zero_apply]

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Finite ι
f g : MultilinearMap R (fun x ↦ R) M₂
h : (f fun x ↦ 1) = g fun x ↦ 1
⊢ f = g

Tactic:
ext x

Goal state after:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Finite ι
f g : MultilinearMap R (fun x ↦ R) M₂
h : (f fun x ↦ 1) = g fun x ↦ 1
x : ι → R
⊢ f x = g x
Module: Mathlib.CategoryTheory.Limits.Types.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type (max v u)
x✝¹ : Cone F
x✝ : x✝¹.pt ⟶ (limitCone F).pt
w : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = x✝¹.π.app j
⊢ x✝ = ↾fun v ↦ ⟨fun j ↦ (hom (x✝¹.π.app j)) v, ⋯⟩

Tactic:
ext x

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type (max v u)
x✝¹ : Cone F
x✝ : x✝¹.pt ⟶ (limitCone F).pt
w : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = x✝¹.π.app j
x : x✝¹.pt
⊢ (hom x✝).toFun x = (hom (↾fun v ↦ ⟨fun j ↦ (hom (x✝¹.π.app j)) v, ⋯⟩)).toFun x
Module: Mathlib.CategoryTheory.Limits.Types.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasLimit F
X✝ Y✝ : J ⥤ Type (max u v)
f : X✝ ⟶ Y✝
⊢ lim.map f ≫ (limitEquivSections Y✝).toIso.hom = (limitEquivSections X✝).toIso.hom ≫ (Functor.sectionsFunctor J).map f

Tactic:
ext x

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasLimit F
X✝ Y✝ : J ⥤ Type (max u v)
f : X✝ ⟶ Y✝
x : lim.obj X✝
⊢ (hom (lim.map f ≫ (limitEquivSections Y✝).toIso.hom)).toFun x =
    (hom ((limitEquivSections X✝).toIso.hom ≫ (Functor.sectionsFunctor J).map f)).toFun x
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
⊢ A.det = ∑ j, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

Tactic:
simp_rw [pow_add, mul_assoc, ← mul_sum]

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ A.det = (-1) ^ ↑i * ∑ i_1, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)
Module: Mathlib.CategoryTheory.Limits.Types.Images

Goal state before:
pp: α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
⊢ lift F' ≫ F'.m = ι f

Tactic:
ext x

Goal state after:
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
x : Image f
⊢ (ConcreteCategory.hom (lift F' ≫ F'.m)).toFun x = (ConcreteCategory.hom (ι f)).toFun x
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
t : Cocone F
j : J
⊢ (colimitCocone F).ι.app j ≫
      ofHom
        (let __src := descAddMonoidHom t;
        { toFun := (↑__src).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }) =
    t.ι.app j

Tactic:
ext x

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
t : Cocone F
j : J
x : ↑(F.obj j)
⊢ (Hom.hom
        ((colimitCocone F).ι.app j ≫
          ofHom
            (let __src := descAddMonoidHom t;
            { toFun := (↑__src).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })))
      x =
    (Hom.hom (t.ι.app j)) x
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cone F
t : (k : K) → IsLimit (((evaluation K C).obj k).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m =
    { app := fun k ↦ (t k).lift { pt := s.pt.obj k, π := whiskerRight s.π ((evaluation K C).obj k) }, naturality := ⋯ }

Tactic:
ext x

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cone F
t : (k : K) → IsLimit (((evaluation K C).obj k).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ c.π.app j = s.π.app j
x : K
⊢ m.app x =
    { app := fun k ↦ (t k).lift { pt := s.pt.obj k, π := whiskerRight s.π ((evaluation K C).obj k) },
          naturality := ⋯ }.app
      x
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cocone F
t : (k : K) → IsColimit (((evaluation K C).obj k).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
w : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m =
    { app := fun k ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι ((evaluation K C).obj k) }, naturality := ⋯ }

Tactic:
ext x

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cocone F
t : (k : K) → IsColimit (((evaluation K C).obj k).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
w : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : K
⊢ m.app x =
    { app := fun k ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι ((evaluation K C).obj k) },
          naturality := ⋯ }.app
      x
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
X Y : J
f : X ⟶ Y
⊢ F.map f ≫ { app := fun Y_1 ↦ colimit.ι (F.flip.obj Y_1) Y, naturality := ⋯ } =
    { app := fun Y ↦ colimit.ι (F.flip.obj Y) X, naturality := ⋯ } ≫ ((const J).obj (F.flip ⋙ colim)).map f

Tactic:
ext x

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
X Y : J
f : X ⟶ Y
x : K
⊢ (F.map f ≫ { app := fun Y_1 ↦ colimit.ι (F.flip.obj Y_1) Y, naturality := ⋯ }).app x =
    ({ app := fun Y ↦ colimit.ι (F.flip.obj Y) X, naturality := ⋯ } ≫ ((const J).obj (F.flip ⋙ colim)).map f).app x
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : Cᵒᵖ
f : shrinkCoyoneda.{w, v, u}.obj X✝ ⟶ shrinkCoyoneda.{w, v, u}.obj Y✝
⊢ shrinkCoyoneda.{w, v, u}.map (shrinkCoyonedaObjObjEquiv (shrinkCoyonedaEquiv f)).op = f

Tactic:
obtain ⟨f, rfl⟩ := shrinkCoyonedaEquiv.symm.surjective f
    cat_disch

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
a : (j : J) → ↑(F.obj j)
ah : a ∈ (F ⋙ forget GrpCat).sections
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (↾⇑(ConcreteCategory.hom (F.map f)))) (a j)⁻¹ = (a j')⁻¹

Tactic:
dsimp [Functor.sections] at ah ⊢

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
a : (j : J) → ↑(F.obj j)
ah : ∀ {j j' : J} (f : j ⟶ j'), (ConcreteCategory.hom (F.map f)) (a j) = a j'
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (F.map f)) (a j)⁻¹ = (a j')⁻¹
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ GrpCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget GrpCat).sections
this✝ : (forget₂ GrpCat MonCat).ReflectsIsomorphisms := reflectsIsomorphisms_forget₂ GrpCat MonCat
c' : Cone (F ⋙ forget₂ GrpCat MonCat)
t : IsLimit c'
this : HasLimit (F ⋙ forget₂ GrpCat MonCat)
⊢ Small.{u, max u v} ↑((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).sections

Tactic:
apply Concrete.small_sections_of_hasLimit (F ⋙ forget₂ GrpCat MonCat)

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
⊢ ofHom (Hom.hom f).ker.subtype ≫ f = 0

Tactic:
ext x

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
x : ↑(of ↥(Hom.hom f).ker)
⊢ (Hom.hom (ofHom (Hom.hom f).ker.subtype ≫ f)) x = (Hom.hom 0) x
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: case e'_3
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
E : Type u_1
inst✝² : Category.{v_1, u_1} E
T : C ⥤ E
S : E ⥤ D
X : C
adj2 : T ⊣ S ⋙ R
inst✝¹ : R.Faithful
inst✝ : R.Full
FF : R.FullyFaithful := ⋯
Y : E
e_1✝ : (T.obj ((L ⋙ R).obj X) ⟶ Y) = (T.obj (R.obj (L.obj X)) ⟶ Y)
e_2✝ : (T.obj ((𝟭 C).obj X) ⟶ Y) = (T.obj X ⟶ Y)
⊢ (fun x ↦ T.map (h.unit.app X) ≫ x) =
    ⇑((adj2.homEquiv (R.obj (L.obj X)) Y).trans
        (FF.homEquiv.symm.trans ((h.homEquiv X (S.obj Y)).trans (adj2.homEquiv X Y).symm)))

Tactic:
ext x

Goal state after:
case e'_3
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
E : Type u_1
inst✝² : Category.{v_1, u_1} E
T : C ⥤ E
S : E ⥤ D
X : C
adj2 : T ⊣ S ⋙ R
inst✝¹ : R.Faithful
inst✝ : R.Full
FF : R.FullyFaithful := FullyFaithful.ofFullyFaithful R
Y : E
e_1✝ : (T.obj ((L ⋙ R).obj X) ⟶ Y) = (T.obj (R.obj (L.obj X)) ⟶ Y)
e_2✝ : (T.obj ((𝟭 C).obj X) ⟶ Y) = (T.obj X ⟶ Y)
x : T.obj ((L ⋙ R).obj X) ⟶ Y
⊢ T.map (h.unit.app X) ≫ x =
    ((adj2.homEquiv (R.obj (L.obj X)) Y).trans
        (FF.homEquiv.symm.trans ((h.homEquiv X (S.obj Y)).trans (adj2.homEquiv X Y).symm)))
      x
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategoryStruct C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)
id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), 𝟙 X ⊗ₘ f = X ◁ f
tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), f ⊗ₘ 𝟙 Y = f ▷ Y
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)
leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ C) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f
rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f
pentagon :
  ∀ (W X Y Z : C),
    ((α_ W X Y).hom ⊗ₘ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom ≫ (𝟙 W ⊗ₘ (α_ X Y Z).hom) =
      (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom
triangle : ∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y
⊢ ∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
intros; simp [← id_tensorHom, ← tensorHom_id, triangle]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
X Y : D
⊢ F.map (𝟙 X ▷ Y) = F.map (𝟙 (X ⊗ Y))

Tactic:
by simp [fData.whiskerRight_eq]

Goal state after: