awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 5
app₀ : f.obj' 0 _proof_83 ≅ g.obj' 0 _proof_83
app₁ : f.obj' 1 _proof_84 ≅ g.obj' 1 _proof_84
app₂ : f.obj' 2 _proof_85 ≅ g.obj' 2 _proof_85
app₃ : f.obj' 3 _proof_86 ≅ g.obj' 3 _proof_86
app₄ : f.obj' 4 _proof_87 ≅ g.obj' 4 _proof_87
app₅ : f.obj' 5 _proof_88 ≅ g.obj' 5 _proof_88
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_84
w₁ : f.map' 1 2 _proof_8 _proof_85 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_85
w₂ : f.map' 2 3 _proof_25 _proof_86 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_86
w₃ : f.map' 3 4 _proof_50 _proof_87 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_87
w₄ : f.map' 4 5 _proof_87 _proof_88 ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_87 _proof_88
⊢ g.map' 3 4 _proof_50 _proof_87 ≫ app₄.inv = app₃.inv ≫ f.map' 3 4 _proof_50 _proof_87
have rw : app₃.inv ≫ f.map' 3 (HAdd.hAdd (α := ℕ) 3 1) sorry sorry = app₃.inv ≫ f.map' 3 4 _proof_50 _proof_87
Tactic: rw [map'_inv_eq_inv_map' (by valid) app₃ app₄ w₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 5
app₀ : f.obj' 0 _proof_83 ≅ g.obj' 0 _proof_83
app₁ : f.obj' 1 _proof_84 ≅ g.obj' 1 _proof_84
app₂ : f.obj' 2 _proof_85 ≅ g.obj' 2 _proof_85
app₃ : f.obj' 3 _proof_86 ≅ g.obj' 3 _proof_86
app₄ : f.obj' 4 _proof_87 ≅ g.obj' 4 _proof_87
app₅ : f.obj' 5 _proof_88 ≅ g.obj' 5 _proof_88
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_84
w₁ : f.map' 1 2 _proof_8 _proof_85 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_85
w₂ : f.map' 2 3 _proof_25 _proof_86 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_86
w₃ : f.map' 3 4 _proof_50 _proof_87 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_87
w₄ : f.map' 4 5 _proof_87 _proof_88 ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_87 _proof_88
⊢ g.map' 4 5 _proof_87 _proof_88 ≫ app₅.inv = app₄.inv ≫ f.map' 4 5 _proof_87 _proof_88
have rw : app₄.inv ≫ f.map' 4 (HAdd.hAdd (α := ℕ) 4 1) sorry sorry = app₄.inv ≫ f.map' 4 5 _proof_87 _proof_88
Tactic: rw [map'_inv_eq_inv_map' (by valid) app₄ app₅ w₄]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
hn :
  ∀ (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ),
    ∃ (F : ComposableArrows.{v_1, u_1} C n) (e : (i : Fin (n + 1)) → F.obj i ≅ obj i),
      ∀ (i : ℕ) (hi : i < n),
        mapSucc ⟨i, hi⟩ =
          Iso.inv (e (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi ≫ Iso.hom (e (⟨i + 1, ⋯⟩ : Fin (n + 1)))
obj : Fin (n + 1 + 1) → C
mapSucc : (i : Fin (n + 1)) → obj i.castSucc ⟶ obj i.succ
⊢ ∃ (F : ComposableArrows.{v_1, u_1} C (n + 1)) (e : (i : Fin (n + 1 + 1)) → F.obj i ≅ obj i),
    ∀ (i : ℕ) (hi : i < n + 1),
      mapSucc ⟨i, hi⟩ =
        Iso.inv (e (⟨i, ⋯⟩ : Fin (n + 1 + 1))) ≫ F.map' i (i + 1) ⋯ hi ≫ Iso.hom (e (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)))
have succ : ∀ (F : ComposableArrows.{v_1, u_1} C n) (e : (i : Fin (n + 1)) → F.obj i ≅ obj i.succ)
  (h :
    ∀ (i : ℕ) (hi : i < n),
      mapSucc ⟨i, hi⟩.succ =
        Iso.inv (e (⟨i, sorry⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) sorry hi ≫ Iso.hom (e (⟨i + 1, sorry⟩ : Fin (n + 1)))),
  ∃ (F : ComposableArrows.{v_1, u_1} C (n + 1)) (e : (i : Fin (n + 1 + 1)) → F.obj i ≅ obj i),
    ∀ (i : ℕ) (hi : i < n + 1),
      mapSucc ⟨i, hi⟩ =
        Iso.inv (e (⟨i, sorry⟩ : Fin (n + 1 + 1))) ≫ F.map' i (i + 1) sorry hi ≫ Iso.hom (e (⟨i + 1, sorry⟩ : Fin (n + 1 + 1)))
Tactic: obtain ⟨F, e, h⟩ := hn (fun i => obj i.succ) (fun i => mapSucc i.succ)
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
hn :
  ∀ (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ),
    ∃ (F : ComposableArrows.{v_1, u_1} C n) (e : (i : Fin (n + 1)) → F.obj i ≅ obj i),
      ∀ (i : ℕ) (hi : i < n),
        mapSucc ⟨i, hi⟩ =
          Iso.inv (e (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi ≫ Iso.hom (e (⟨i + 1, ⋯⟩ : Fin (n + 1)))
obj : Fin (n + 1 + 1) → C
mapSucc : (i : Fin (n + 1)) → obj i.castSucc ⟶ obj i.succ
F : ComposableArrows.{v_1, u_1} C n
e : (i : Fin (n + 1)) → F.obj i ≅ obj i.succ
h :
  ∀ (i : ℕ) (hi : i < n),
    mapSucc ⟨i, hi⟩.succ =
      Iso.inv (e (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi ≫ Iso.hom (e (⟨i + 1, ⋯⟩ : Fin (n + 1)))
⊢ ∃ (F : ComposableArrows.{v_1, u_1} C (n + 1)) (e : (i : Fin (n + 1 + 1)) → F.obj i ≅ obj i),
    ∀ (i : ℕ) (hi : i < n + 1),
      mapSucc ⟨i, hi⟩ =
        Iso.inv (e (⟨i, ⋯⟩ : Fin (n + 1 + 1))) ≫ F.map' i (i + 1) ⋯ hi ≫ Iso.hom (e (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)))
have succ : ∀ (i : ℕ) (hi : i < n + 1),
  Eq (α := obj (⟨i, hi⟩ : Fin (n + 1)).castSucc ⟶ obj ⟨i, hi⟩.succ) (mapSucc ⟨i, hi⟩)
    (Iso.inv
        ((fun (i : Fin (n + 1 + 1)) ↦
            (match (motive := (i : Fin (n + 1 + 1)) → (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj i ≅ obj i) i with
              | ⟨0, sorry⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj 0)
              | ⟨i.succ, hi⟩ => e ⟨i, sorry⟩ :
              (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj i ≅ obj i))
          ⟨i, sorry⟩) ≫
      (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).map' i (i + 1) sorry hi ≫
        Iso.hom
          ((fun (i : Fin (n + 1 + 1)) ↦
              (match (motive := (i : Fin (n + 1 + 1)) → (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj i ≅ obj i) i with
                | ⟨0, sorry⟩ => Iso.refl ((F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj 0)
                | ⟨i.succ, hi⟩ => e (⟨i, sorry⟩ : Fin (n + 1)) :
                (F.precomp (mapSucc 0 ≫ Iso.inv (e 0))).obj i ≅ obj i))
            (⟨i + 1, sorry⟩ : Fin (n + 1 + 1))))
Tactic: refine ⟨F.precomp (mapSucc 0 ≫ (e 0).inv), fun i => match i with
      | 0 => Iso.refl _
      | ⟨i + 1, hi⟩ => e _, fun i hi => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
obj : Fin (n + 1) → C
mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ
⊢ ∃ (F : ComposableArrows.{v_1, u_1} C n) (e : (i : Fin (n + 1)) → F.obj i ≅ obj i),
    ∀ (i : ℕ) (hi : i < n),
      mapSucc ⟨i, hi⟩ =
        Iso.inv (e (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi ≫ Iso.hom (e (⟨i + 1, ⋯⟩ : Fin (n + 1)))
have zero : ∀ (obj : Fin (HAdd.hAdd (α := ℕ) 0 1) → C) (mapSucc : (i : Fin 0) → obj i.castSucc ⟶ obj i.succ),
  ∃ (F : ComposableArrows.{v_1, u_1} C 0) (e : (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) → F.obj i ≅ obj i),
    ∀ (i : ℕ) (hi : i < 0),
      mapSucc ⟨i, hi⟩ =
        Iso.inv (e (⟨i, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1))) ≫
          F.map' i (i + 1) sorry hi ≫ Iso.hom (e (⟨i + 1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)))
Tactic: induction n with
  | zero => exact ⟨mk₀ (obj 0), fun 0 => Iso.refl _, fun i hi => by simp at hi⟩
  | succ n hn =>
    obtain ⟨F, e, h⟩ := hn (fun i => obj i.succ) (fun i => mapSucc i.succ)
    refine ⟨F.precomp (mapSucc 0 ≫ (e 0).inv), fun i => match i with
      | 0 => Iso.refl _
      | ⟨i + 1, hi⟩ => e _, fun i hi => ?_⟩
    obtain _ | i := i
    · simp
    · exact h i (by valid)
Cleared hypotheses: n, obj, mapSucc
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
obj : Fin (n + 1) → C
mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ
zero :
  ∀ (obj : Fin (HAdd.hAdd (α := ℕ) 0 1) → C) (mapSucc : (i : Fin 0) → obj i.castSucc ⟶ obj i.succ),
    ∃ (F : ComposableArrows.{v_1, u_1} C 0) (e : (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) → F.obj i ≅ obj i),
      ∀ (i : ℕ) (hi : i < 0),
        mapSucc ⟨i, hi⟩ =
          Iso.inv (e (⟨i, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1))) ≫
            F.map' i (i + 1) ⋯ hi ≫ Iso.hom (e (⟨i + 1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)))
⊢ ∃ (F : ComposableArrows.{v_1, u_1} C n) (e : (i : Fin (n + 1)) → F.obj i ≅ obj i),
    ∀ (i : ℕ) (hi : i < n),
      mapSucc ⟨i, hi⟩ =
        Iso.inv (e (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi ≫ Iso.hom (e (⟨i + 1, ⋯⟩ : Fin (n + 1)))
have succ : ∀ (n : ℕ)
  (hn :
    ∀ (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ),
      ∃ (F : ComposableArrows.{v_1, u_1} C n) (e : (i : Fin (n + 1)) → F.obj i ≅ obj i),
        ∀ (i : ℕ) (hi : i < n),
          mapSucc ⟨i, hi⟩ =
            Iso.inv (e (⟨i, sorry⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) sorry hi ≫ Iso.hom (e (⟨i + 1, sorry⟩ : Fin (n + 1))))
  (obj : Fin (n + 1 + 1) → C) (mapSucc : (i : Fin (n + 1)) → obj i.castSucc ⟶ obj i.succ),
  ∃ (F : ComposableArrows.{v_1, u_1} C (n + 1)) (e : (i : Fin (n + 1 + 1)) → F.obj i ≅ obj i),
    ∀ (i : ℕ) (hi : i < n + 1),
      mapSucc ⟨i, hi⟩ =
        Iso.inv (e (⟨i, sorry⟩ : Fin (n + 1 + 1))) ≫ F.map' i (i + 1) sorry hi ≫ Iso.hom (e (⟨i + 1, sorry⟩ : Fin (n + 1 + 1)))
Tactic: induction n with
  | zero => exact ⟨mk₀ (obj 0), fun 0 => Iso.refl _, fun i hi => by simp at hi⟩
  | succ n hn =>
    obtain ⟨F, e, h⟩ := hn (fun i => obj i.succ) (fun i => mapSucc i.succ)
    refine ⟨F.precomp (mapSucc 0 ≫ (e 0).inv), fun i => match i with
      | 0 => Iso.refl _
      | ⟨i + 1, hi⟩ => e _, fun i hi => ?_⟩
    obtain _ | i := i
    · simp
    · exact h i (by valid)
Cleared hypotheses: n, obj, mapSucc
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Two (goal)
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 (twoδ₂Toδ₁ f g fg h)
have 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)
Tactic: rw [isIso_iff₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Two (goal)
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 (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)
have left : IsIso (X := (mk₁ f).obj 0) ((twoδ₂Toδ₁ f g fg h).app 0)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Two (goal)
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)
⊢ 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)
have right : IsIso (X := (mk₁ f).obj 1) ((twoδ₂Toδ₁ f g fg h).app 1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Two (goal)
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 (X := (mk₁ f).obj 0) ((twoδ₂Toδ₁ f g fg h).app 0)
have left : IsIso.{v_1, u_1} (𝟙 i)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Two (goal)
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 (twoδ₁Toδ₀ f g fg h)
have 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)
Tactic: rw [isIso_iff₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Two (goal)
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 (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)
have left : IsIso (X := (mk₁ fg).obj 0) ((twoδ₁Toδ₀ f g fg h).app 0)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Two (goal)
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)
⊢ 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)
have right : IsIso (X := (mk₁ fg).obj 1) ((twoδ₁Toδ₀ f g fg h).app 1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Two (goal)
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 (X := (mk₁ fg).obj 1) ((twoδ₁Toδ₀ f g fg h).app 1)
have right : IsIso.{v_1, u_1} (𝟙 k)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.Basic (goal)
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)
⊢ f = g
have 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))
Tactic: rw [← ofHom_hom f, ← ofHom_hom g]
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.Basic (goal)
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
⊢ Eq.{w + 1} (α := (a : CC X) → CC X) (⇑(@hom.{w, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X)) : (a : CC X) → CC X) id
have h : ∀ (x : CC X), (@hom.{w, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X) : (a : CC X) → CC X) x = id x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.Basic (goal)
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
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.Basic (goal)
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
⊢ 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
have h : ∀ (x : CC X), (@ConcreteCategory.hom.{w, v, u, u_1} _ inst FC CC _ _ _ _ (𝟙 X) : (a : CC X) → CC X) x = id x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.Basic (goal)
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
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.Basic (goal)
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
⊢ homMk (ofHom (FC := FD) (CC := CD) (hom (FC := FD) (CC := CD) x.hom)) = x
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.Basic (goal)
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
⊢ homMk (P := P) (ofHom (FC := FC) (CC := CC) (hom (FC := FC) (CC := CC) x.hom)) = x
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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)
⊢ Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C) ↔
    Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
have mp : Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C) →
  Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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)
mp :
  Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C) →
    Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
⊢ Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C) ↔
    Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
have mpr : Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) →
  Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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)
h : Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C)
⊢ Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
have mp : ∀ {X Y : C} (f : X ⟶ Y) [Epi f],
  Epi (X := Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X)
    (Functor.map (forget C (FC := FC) (CC := CC)) f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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)
h : Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C)
X Y : C
f : X ⟶ Y
hf : epimorphisms C f
⊢ Epi (X := Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X)
    (Functor.map (forget C (FC := FC) (CC := CC)) f)
have mp : Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X))
  (β := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) Y))
  (⇑(hom (FC := TypeCat.Fun) (Functor.map (forget C (FC := FC) (CC := CC)) f)) :
    (a : (fun (X : Type w) ↦ X) ((forget C).obj X)) → (fun (X : Type w) ↦ X) ((forget C).obj Y))
Tactic: rw [epi_iff_surjective]
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (hypothesis)
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)
h : Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C)
X Y : C
f : X ⟶ Y
hf : epimorphisms C f
⊢ Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X))
    (β := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) Y))
    (⇑(hom (FC := TypeCat.Fun) (Functor.map (forget C (FC := FC) (CC := CC)) f)) :
      (a : (fun (X : Type w) ↦ X) ((forget C).obj X)) → (fun (X : Type w) ↦ X) ((forget C).obj Y))
have hf₁ : MorphismProperty.surjective C (FC := FC) (CC := CC) f
Tactic: rw [← h] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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)
h : Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
⊢ Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C)
have mpr : LE.le (α := MorphismProperty.{v, u} C) (epimorphisms C) (MorphismProperty.surjective C (FC := FC) (CC := CC))
Tactic: apply le_antisymm (surjective_le_epimorphisms C)
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (hypothesis)
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)
h : Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
hf : epimorphisms C f
⊢ MorphismProperty.surjective C (FC := FC) (CC := CC) f
have this : Epi f
Tactic: have : Epi f := hf
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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)
h : Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
hf : epimorphisms C f
this : Epi f
⊢ MorphismProperty.surjective C (FC := FC) (CC := CC) f
have mpr : Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X))
  (β := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) Y))
  (⇑(hom (FC := TypeCat.Fun) (Functor.map (forget C (FC := FC) (CC := CC)) f)) :
    (a : (fun (X : Type w) ↦ X) ((forget C).obj X)) → (fun (X : Type w) ↦ X) ((forget C).obj Y))
Tactic: change Function.Surjective ((forget C).map f)