awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ComposableArrows.One
Goal:
C : Type u
inst : Category.{v, u} C
i j i' j' n : ℕ
h : i ≤ j
h_1 : i' ≤ j'
h_2 : i ≤ i'
h_3 : j ≤ j'
h_4 : j' ≤ n
S : ComposableArrows.{v, u} C n
⊢ (Functor.obj (functorArrows C i j n ⋯ ⋯) S).map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ S.map' j j' h_3 h_4 =
    S.map' i i' h_2 ⋯ ≫ (Functor.obj (functorArrows C i' j' n ⋯ ⋯) S).map' 0 1 homMk₁._proof_4 homMk₁._proof_5

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Three
Goal:
C : Type u
inst : Category.{v, u} C
i j k l : C
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
⊢ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃).app 0 = 𝟙 ((mk₂ f₁ f₂).obj 0)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Three
Goal:
C : Type u
inst : Category.{v, u} C
i j k l : C
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
⊢ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃).app 1 = 𝟙 ((mk₂ f₁ f₂).obj 1)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Three
Goal:
C : Type u
inst : Category.{v, u} C
i j k l : C
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
⊢ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃).app 2 = f₃

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Three
Goal:
C : Type u
inst : Category.{v, u} C
i j k l : C
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
f₂₃ : j ⟶ l
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
⊢ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃).app 0 = 𝟙 ((mk₂ f₁ f₂₃).obj 0)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Three
Goal:
C : Type u
inst : Category.{v, u} C
i j k l : C
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
f₂₃ : j ⟶ l
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
⊢ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃).app 1 = f₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Three
Goal:
C : Type u
inst : Category.{v, u} C
i j k l : C
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
f₂₃ : j ⟶ l
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
⊢ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃).app 2 = 𝟙 ((mk₂ f₁ f₂₃).obj 2)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Three
Goal:
C : Type u
inst : Category.{v, u} C
i j k l : C
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
⊢ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂).app 0 = f₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Three
Goal:
C : Type u
inst : Category.{v, u} C
i j k l : C
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
⊢ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂).app 1 = 𝟙 ((mk₂ f₁₂ f₃).obj 1)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Three
Goal:
C : Type u
inst : Category.{v, u} C
i j k l : C
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
⊢ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂).app 2 = 𝟙 ((mk₂ f₁₂ f₃).obj 2)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Two
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
⊢ (twoδ₂Toδ₁ f g fg h).app 0 = 𝟙 ((mk₁ f).obj 0)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Two
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
⊢ (twoδ₂Toδ₁ f g fg h).app 1 = g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Two
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
⊢ (twoδ₁Toδ₀ f g fg h).app 0 = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Two
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
⊢ (twoδ₁Toδ₀ f g fg h).app 1 = 𝟙 ((mk₁ fg).obj 1)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Two
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst_1 : IsIso g
rw : IsIso (X := (mk₁ f).obj 0) ((twoδ₂Toδ₁ f g fg h).app 0) ∧ IsIso (X := (mk₁ f).obj 1) ((twoδ₂Toδ₁ f g fg h).app 1)
⊢ IsIso (twoδ₂Toδ₁ f g fg h)

Tactic:
rw [isIso_iff₁]

Premises used: CategoryTheory.ComposableArrows.isIso_iff₁
-- Module: Mathlib.CategoryTheory.ComposableArrows.Two
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst_1 : IsIso g
left : IsIso (X := (mk₁ f).obj 0) ((twoδ₂Toδ₁ f g fg h).app 0)
right : IsIso (X := (mk₁ f).obj 1) ((twoδ₂Toδ₁ f g fg h).app 1)
⊢ IsIso (X := (mk₁ f).obj 0) ((twoδ₂Toδ₁ f g fg h).app 0) ∧ IsIso (X := (mk₁ f).obj 1) ((twoδ₂Toδ₁ f g fg h).app 1)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.ComposableArrows.Two
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst_1 : IsIso g
left : IsIso.{v_1, u_1} (𝟙 i)
⊢ IsIso (X := (mk₁ f).obj 0) ((twoδ₂Toδ₁ f g fg h).app 0)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Two
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst_1 right : IsIso g
⊢ IsIso (X := (mk₁ f).obj 1) ((twoδ₂Toδ₁ f g fg h).app 1)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Two
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst_1 : IsIso g
⊢ IsIso.{v_1, u_1} (𝟙 i)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.ComposableArrows.Two
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst_1 : IsIso g
⊢ IsIso g

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.ComposableArrows.Two
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst_1 : IsIso f
rw : IsIso (X := (mk₁ fg).obj 0) ((twoδ₁Toδ₀ f g fg h).app 0) ∧ IsIso (X := (mk₁ fg).obj 1) ((twoδ₁Toδ₀ f g fg h).app 1)
⊢ IsIso (twoδ₁Toδ₀ f g fg h)

Tactic:
rw [isIso_iff₁]

Premises used: CategoryTheory.ComposableArrows.isIso_iff₁
-- Module: Mathlib.CategoryTheory.ComposableArrows.Two
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst_1 : IsIso f
left : IsIso (X := (mk₁ fg).obj 0) ((twoδ₁Toδ₀ f g fg h).app 0)
right : IsIso (X := (mk₁ fg).obj 1) ((twoδ₁Toδ₀ f g fg h).app 1)
⊢ IsIso (X := (mk₁ fg).obj 0) ((twoδ₁Toδ₀ f g fg h).app 0) ∧ IsIso (X := (mk₁ fg).obj 1) ((twoδ₁Toδ₀ f g fg h).app 1)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.ComposableArrows.Two
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst_1 left : IsIso f
⊢ IsIso (X := (mk₁ fg).obj 0) ((twoδ₁Toδ₀ f g fg h).app 0)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Two
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst_1 : IsIso f
right : IsIso.{v_1, u_1} (𝟙 k)
⊢ IsIso (X := (mk₁ fg).obj 1) ((twoδ₁Toδ₀ f g fg h).app 1)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Two
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst_1 : IsIso f
⊢ IsIso f

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.ComposableArrows.Two
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst_1 : IsIso f
⊢ IsIso.{v_1, u_1} (𝟙 k)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X Y : C
f g : X ⟶ Y
h :
  Eq.{w + 1} (α := (a : ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X) → ToType.{w, v, u, u_1} (FC := FC) (CC := CC) Y)
    ((fun (f : X ⟶ Y) ↦ ((⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y) : (a : CC X) → CC Y)) f)
    ((fun (f : X ⟶ Y) ↦ ((⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y) : (a : CC X) → CC Y)) g)
rw :
  Eq.{v + 1} (α := X ⟶ Y) (ofHom (FC := FC) (CC := CC) (hom (FC := FC) (CC := CC) f))
    (ofHom (FC := FC) (CC := CC) (hom (FC := FC) (CC := CC) g))
⊢ f = g

Tactic:
rw [← ofHom_hom f, ← ofHom_hom g]

Premises used: CategoryTheory.ConcreteCategory.ofHom_hom
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X Y : C
f g : X ⟶ Y
h :
  Eq.{w + 1} (α := (a : ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X) → ToType.{w, v, u, u_1} (FC := FC) (CC := CC) Y)
    ((fun (f : X ⟶ Y) ↦ ((⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y) : (a : CC X) → CC Y)) f)
    ((fun (f : X ⟶ Y) ↦ ((⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y) : (a : CC X) → CC Y)) g)
⊢ Eq.{v + 1} (α := X ⟶ Y) (ofHom (FC := FC) (CC := CC) (hom (FC := FC) (CC := CC) f))
    (ofHom (FC := FC) (CC := CC) (hom (FC := FC) (CC := CC) g))

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X Y : C
⊢ Function.Bijective.{v + 1, u_1 + 1} (α := X ⟶ Y) (hom (FC := ToHom.{w, v, u, u_1} (FC := FC) (CC := CC)) (CC := CC))

Tactic:
homEquiv.bijective

Premises used: Equiv.bijective, CategoryTheory.ConcreteCategory.homEquiv
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X Y : C
⊢ Function.Injective.{v + 1, u_1 + 1} (α := X ⟶ Y) (hom (FC := ToHom.{w, v, u, u_1} (FC := FC) (CC := CC)) (CC := CC))

Tactic:
hom_bijective.injective

Premises used: Function.Bijective.injective, CategoryTheory.ConcreteCategory.hom_bijective
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X Y : C
⊢ Function.Surjective.{v + 1, u_1 + 1} (α := X ⟶ Y) (hom (FC := ToHom.{w, v, u, u_1} (FC := FC) (CC := CC)) (CC := CC))

Tactic:
hom_bijective.surjective

Premises used: CategoryTheory.ConcreteCategory.hom_bijective, Function.Bijective.surjective
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X Y : C
f g : X ⟶ Y
h : hom (FC := FC) (CC := CC) f = hom (FC := FC) (CC := CC) g
⊢ f = g

Tactic:
hom_injective h

Premises used: CategoryTheory.ConcreteCategory.hom_injective
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X Y : C
f g : X ⟶ Y
h :
  Eq.{w + 1} (α := (a : CC X) → CC Y) (⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y)
    (⇑(hom (FC := FC) (CC := CC) g) : (a : CC X) → CC Y)
⊢ f = g

Tactic:
ext (DFunLike.coe_injective h)

Premises used: CategoryTheory.ConcreteCategory.ext, DFunLike.coe_injective
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X Y : C
f g : X ⟶ Y
h :
  ∀ (x : CC X),
    Eq (α := CC Y) ((hom (FC := FC) (CC := CC) f : (a : CC X) → CC Y) x : CC Y)
      ((hom (FC := FC) (CC := CC) g : (a : CC X) → CC Y) x : CC Y)
⊢ f = g

Tactic:
ext (DFunLike.ext _ _ h)

Premises used: DFunLike.ext, CategoryTheory.ConcreteCategory.ext
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X Y : C
f g : X ⟶ Y
w :
  ∀ (x : CC X),
    Eq (α := CC Y) ((hom (FC := FC) (CC := CC) f : (a : CC X) → CC Y) x : CC Y)
      ((hom (FC := FC) (CC := CC) g : (a : CC X) → CC Y) x : CC Y)
⊢ f = g

Tactic:
ext (DFunLike.ext _ _ w)

Premises used: DFunLike.ext, CategoryTheory.ConcreteCategory.ext
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X Y : C
f g : X ⟶ Y
h : f = g
x : ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X
⊢ Eq (α := CC Y) ((hom (FC := FC) (CC := CC) f : (a : CC X) → CC Y) x : CC Y)
    ((hom (FC := FC) (CC := CC) g : (a : CC X) → CC Y) x : CC Y)

Tactic:
congrFun (congrArg (fun k : X ⟶ Y => (k : ToType X → ToType Y)) h) x

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, congrFun, DFunLike.coe
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X : C
h : ∀ (x : CC X), (@hom.{w, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X) : (a : CC X) → CC X) x = id x
⊢ Eq.{w + 1} (α := (a : CC X) → CC X) (⇑(@hom.{w, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X)) : (a : CC X) → CC X) id

Tactic:
ext
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X : C
x : CC X
⊢ (@hom.{w, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X) : (a : CC X) → CC X) x = id x

Tactic:
simp [ConcreteCategory.id_apply]

Premises used: CategoryTheory.ConcreteCategory.id_apply
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h :
  ∀ (x : CC X),
    Eq (α := CC Z) ((hom (FC := FC) (CC := CC) (f ≫ g) : (a : CC X) → CC Z) x : CC Z)
      (Function.comp (β := CC Y) (⇑(hom (FC := FC) (CC := CC) g) : (a : CC Y) → CC Z)
          (⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y) x :
        CC Z)
⊢ Eq.{w + 1} (α := (a : CC X) → CC Z) (⇑(hom (FC := FC) (CC := CC) (f ≫ g)) : (a : CC X) → CC Z)
    (Function.comp (β := CC Y) (⇑(hom (FC := FC) (CC := CC) g) : (a : CC Y) → CC Z)
      (⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x : CC X
⊢ Eq (α := CC Z) ((hom (FC := FC) (CC := CC) (f ≫ g) : (a : CC X) → CC Z) x : CC Z)
    (Function.comp (β := CC Y) (⇑(hom (FC := FC) (CC := CC) g) : (a : CC Y) → CC Z)
        (⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y) x :
      CC Z)

Tactic:
simp [ConcreteCategory.comp_apply]

Premises used: CategoryTheory.ConcreteCategory.comp_apply
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X : C
x : ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X
⊢ (@hom.{w, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X) : (a : CC X) → CC X) x = x

Tactic:
simp [ConcreteCategory.id_apply _]

Premises used: CategoryTheory.ConcreteCategory.id_apply
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x : ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X
⊢ Eq (α := CC Z) ((hom (FC := FC) (CC := CC) (f ≫ g) : (a : CC X) → CC Z) x : CC Z)
    ((hom (FC := FC) (CC := CC) g : (a : CC Y) → CC Z) ((hom (FC := FC) (CC := CC) f : (a : CC X) → CC Y) x : CC Y) :
      CC Z)

Tactic:
simp [ConcreteCategory.comp_apply]

Premises used: CategoryTheory.ConcreteCategory.comp_apply
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X Y : C
f : X ⟶ Y
x x' : ToType.{w, v, u, u_1} (FC := FC) (CC := CC) X
h : x = x'
⊢ Eq (α := CC Y) ((hom (FC := FC) (CC := CC) f : (a : CC X) → CC Y) x : CC Y)
    ((hom (FC := FC) (CC := CC) f : (a : CC X) → CC Y) x' : CC Y)

Tactic:
congrArg (f : ToType X → ToType Y) h

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X : C
h : ∀ (x : CC X), (@ConcreteCategory.hom.{w, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X) : (a : CC X) → CC X) x = id x
⊢ Eq.{w + 1} (α := (a : CC X) → CC X)
    (⇑(@ConcreteCategory.hom.{w, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X)) : (a : CC X) → CC X) id

Tactic:
ext
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X : C
x : CC X
⊢ (@ConcreteCategory.hom.{w, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X) : (a : CC X) → CC X) x = id x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h :
  ∀ (x : CC X),
    Eq (α := CC Z) ((ConcreteCategory.hom (FC := FC) (CC := CC) (f ≫ g) : (a : CC X) → CC Z) x : CC Z)
      (Function.comp (β := CC Y) (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) g) : (a : CC Y) → CC Z)
          (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y) x :
        CC Z)
⊢ Eq.{w + 1} (α := (a : CC X) → CC Z) (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (f ≫ g)) : (a : CC X) → CC Z)
    (Function.comp (β := CC Y) (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) g) : (a : CC Y) → CC Z)
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x : CC X
⊢ Eq (α := CC Z) ((ConcreteCategory.hom (FC := FC) (CC := CC) (f ≫ g) : (a : CC X) → CC Z) x : CC Z)
    (Function.comp (β := CC Y) (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) g) : (a : CC Y) → CC Z)
        (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y) x :
      CC Z)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
FC : C_1 → C_1 → Type u_1
CC : C_1 → Type w
inst_1 : (X Y : C_1) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C_1 FC (CC := CC)
C : Type u
D : Type u'
inst_3 : Category.{v', u'} D
FD : D → D → Type u_2
CD : D → Type w
inst_4 : (X Y : D) → FunLike.{u_2 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory.{w, v', u', u_2} D FD (CC := CD)
f : C → D
X Y : InducedCategory D f
x : X ⟶ Y
h :
  @hom.{w, v', u', u_2} _ inst_3 FD CD _ _ _ _
      (Hom.hom (homMk (ofHom (FC := FD) (CC := CD) (hom (FC := FD) (CC := CD) x.hom)))) =
    hom (FC := FD) (CC := CD) x.hom
⊢ homMk (ofHom (FC := FD) (CC := CD) (hom (FC := FD) (CC := CD) x.hom)) = x

Tactic:
ext
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
FC : C_1 → C_1 → Type u_1
CC : C_1 → Type w
inst_1 : (X Y : C_1) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C_1 FC (CC := CC)
C : Type u
D : Type u'
inst_3 : Category.{v', u'} D
FD : D → D → Type u_2
CD : D → Type w
inst_4 : (X Y : D) → FunLike.{u_2 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory.{w, v', u', u_2} D FD (CC := CD)
f : C → D
X Y : InducedCategory D f
x : X ⟶ Y
⊢ @hom.{w, v', u', u_2} _ inst_3 FD CD _ _ _ _
      (Hom.hom (homMk (ofHom (FC := FD) (CC := CD) (hom (FC := FD) (CC := CD) x.hom)))) =
    hom (FC := FD) (CC := CD) x.hom

Tactic:
simp [ofHom_hom]

Premises used: CategoryTheory.ConcreteCategory.ofHom_hom
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
FC_1 : C_1 → C_1 → Type u_1
CC_1 : C_1 → Type w
inst_1 : (X Y : C_1) → FunLike.{u_1 + 1, w + 1, w + 1} (FC_1 X Y) (CC_1 X) (CC_1 Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C_1 FC_1 (CC := CC_1)
C : Type u
inst_3 : Category.{v, u} C
FC : C → C → Type u_2
CC : C → Type w
inst_4 : (X Y : C) → FunLike.{u_2 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_5 : ConcreteCategory.{w, v, u, u_2} C FC (CC := CC)
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
x : X ⟶ Y
h :
  hom (FC := FC) (CC := CC) (homMk (P := P) (ofHom (FC := FC) (CC := CC) (hom (FC := FC) (CC := CC) x.hom))).hom =
    hom (FC := FC) (CC := CC) x.hom
⊢ homMk (P := P) (ofHom (FC := FC) (CC := CC) (hom (FC := FC) (CC := CC) x.hom)) = x

Tactic:
ext
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
FC_1 : C_1 → C_1 → Type u_1
CC_1 : C_1 → Type w
inst_1 : (X Y : C_1) → FunLike.{u_1 + 1, w + 1, w + 1} (FC_1 X Y) (CC_1 X) (CC_1 Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C_1 FC_1 (CC := CC_1)
C : Type u
inst_3 : Category.{v, u} C
FC : C → C → Type u_2
CC : C → Type w
inst_4 : (X Y : C) → FunLike.{u_2 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_5 : ConcreteCategory.{w, v, u, u_2} C FC (CC := CC)
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
x : X ⟶ Y
⊢ hom (FC := FC) (CC := CC) (homMk (P := P) (ofHom (FC := FC) (CC := CC) (hom (FC := FC) (CC := CC) x.hom))).hom =
    hom (FC := FC) (CC := CC) x.hom

Tactic:
simp [ofHom_hom]

Premises used: CategoryTheory.ConcreteCategory.ofHom_hom