awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst_2 : EffectiveEpiFamily X π
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
m : e.functor.obj B ⟶ W
hm : ∀ (a : α), e.functor.map (π a) ≫ m = ε a
this :
  ∀ (m : B ⟶ e.inverse.obj W) (hm : ∀ (a : α), π a ≫ m = e.unit.app (X a) ≫ e.inverse.map (ε a)),
    m = EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯
⊢ m =
    e.functor.map (EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯) ≫
      e.counit.app W
have specialize : ∀ (a : α), π a ≫ e.unit.app B ≫ e.inverse.map m = e.unit.app (X a) ≫ e.inverse.map (ε a)
Tactic: specialize this (e.unit.app _ ≫ e.inverse.map m) fun a ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst_2 : EffectiveEpiFamily X π
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
m : e.functor.obj B ⟶ W
hm : ∀ (a : α), e.functor.map (π a) ≫ m = ε a
this :
  ∀ (m : B ⟶ e.inverse.obj W) (hm : ∀ (a : α), π a ≫ m = e.unit.app (X a) ≫ e.inverse.map (ε a)),
    m = EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯
specialize : ∀ (a : α), π a ≫ e.unit.app B ≫ e.inverse.map m = e.unit.app (X a) ≫ e.inverse.map (ε a)
⊢ m =
    e.functor.map (EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯) ≫
      e.counit.app W
have specialize₁ : ∀
  (this :
    e.unit.app B ≫ e.inverse.map m =
      EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) sorry),
  m =
    e.functor.map (EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) sorry) ≫
      e.counit.app W
Tactic: specialize this (e.unit.app _ ≫ e.inverse.map m) fun a ↦ ?_
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst_2 : EffectiveEpiFamily X π
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
m : e.functor.obj B ⟶ W
hm : ∀ (a : α), e.functor.map (π a) ≫ m = ε a
this :
  ∀ (m : B ⟶ e.inverse.obj W) (hm : ∀ (a : α), π a ≫ m = e.unit.app (X a) ≫ e.inverse.map (ε a)),
    m = EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯
a : α
⊢ π a ≫ e.unit.app B ≫ e.inverse.map m = e.unit.app (X a) ≫ e.inverse.map (ε a)
have rw : π a ≫ e.unit.app B ≫ e.inverse.map m = e.unit.app (X a) ≫ e.inverse.map (e.functor.map (π a) ≫ m)
Tactic: rw [← congrArg e.inverse.map (hm a)]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : IsRegularEpiCategory.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : F.PreservesEpimorphisms
inst_4 : HasPullbacks.{v_2, u_2} D
X Y : C
x : X ⟶ Y
h : EffectiveEpi x
⊢ EffectiveEpi (F.map x)
have rw : IsRegularEpi (F.map x)
Tactic: rw [← isRegularEpi_iff_effectiveEpi]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (goal)
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
D_1 : Type u_2
inst_1 : Category.{v_2, u_2} D_1
C : Type u_3
D : Type u_4
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst_4 : EffectiveEpi f
F : Functor.{v_3, v_4, u_3, u_4} C D
inst_5 : F.PreservesEffectiveEpis
inst_6 : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ F.map c.fst ≫ F.map f = F.map c.snd ≫ F.map f
have rw : F.map (c.snd ≫ f) = F.map c.snd ≫ F.map f
Tactic: rw [← F.map_comp, c.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (goal)
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
D_1 : Type u_2
inst_1 : Category.{v_2, u_2} D_1
C : Type u_3
D : Type u_4
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst_4 : EffectiveEpi f
F : Functor.{v_3, v_4, u_3, u_4} C D
inst_5 : F.PreservesEffectiveEpis
inst_6 : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ IsColimit (Cofork.ofπ (F.map f) ⋯)
have refine_1 : F.map c.fst ≫ F.map f = F.map c.snd ≫ F.map f
Tactic: refine isColimitCoforkOfEffectiveEpi (F.map f) (.mk (F.map c.fst) (F.map c.snd) ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (goal)
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
D_1 : Type u_2
inst_1 : Category.{v_2, u_2} D_1
C : Type u_3
D : Type u_4
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst_4 : EffectiveEpi f
F : Functor.{v_3, v_4, u_3, u_4} C D
inst_5 : F.PreservesEffectiveEpis
inst_6 : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
refine_1 : F.map c.fst ≫ F.map f = F.map c.snd ≫ F.map f
⊢ IsColimit (Cofork.ofπ (F.map f) ⋯)
have refine_2 : IsLimit (PullbackCone.mk (F.map c.fst) (F.map c.snd) sorry)
Tactic: refine isColimitCoforkOfEffectiveEpi (F.map f) (.mk (F.map c.fst) (F.map c.snd) ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (goal)
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
D_1 : Type u_2
inst_1 : Category.{v_2, u_2} D_1
C : Type u_3
D : Type u_4
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst_4 : EffectiveEpi f
F : Functor.{v_3, v_4, u_3, u_4} C D
inst_5 : F.PreservesEffectiveEpis
inst_6 : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ IsLimit (PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯)
have refine_2 : cospan f f ⋙ F ≅ cospan (F.map f) (F.map f)
Tactic: refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_ (isLimitOfPreserves F hc)
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (goal)
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
D_1 : Type u_2
inst_1 : Category.{v_2, u_2} D_1
C : Type u_3
D : Type u_4
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst_4 : EffectiveEpi f
F : Functor.{v_3, v_4, u_3, u_4} C D
inst_5 : F.PreservesEffectiveEpis
inst_6 : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
refine_2 : cospan f f ⋙ F ≅ cospan (F.map f) (F.map f)
⊢ IsLimit (PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯)
have refine_2₁ : (Cone.postcompose
        (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
            (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left)) (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right)) sorry
            sorry).hom).obj
    (F.mapCone c) ≅
  PullbackCone.mk (F.map c.fst) (F.map c.snd) sorry
Tactic: refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_ (isLimitOfPreserves F hc)
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.PreservesEffectiveEpis
inst_4 : G.PreservesEffectiveEpis
X Y : C
x : X ⟶ Y
h : EffectiveEpi x
⊢ EffectiveEpi ((F ⋙ G).map x)
have dsimp : EffectiveEpi (G.map (F.map x))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.PreservesFiniteEffectiveEpiFamilies
inst_4 : G.PreservesFiniteEffectiveEpiFamilies
α : Type
inst_5 : Finite α
B : C
x : α → C
x_1 : (a : α) → x a ⟶ B
h : EffectiveEpiFamily x x_1
⊢ EffectiveEpiFamily.{v_3, u_3, 0} (C := E) (B := (F ⋙ G).obj B) (fun (a : α) ↦ (F ⋙ G).obj (x a)) fun (a : α) ↦
    (F ⋙ G).map (x_1 a)
have dsimp : EffectiveEpiFamily.{v_3, u_3, 0} (C := E) (B := G.obj (F.obj B)) (fun (a : α) ↦ G.obj (F.obj (x a))) fun (a : α) ↦
  G.map (F.map (x_1 a))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.PreservesEffectiveEpiFamilies
inst_4 : G.PreservesEffectiveEpiFamilies
α : Type u
B : C
x : α → C
x_1 : (a : α) → x a ⟶ B
h : EffectiveEpiFamily x x_1
⊢ EffectiveEpiFamily.{v_3, u_3, u} (C := E) (B := (F ⋙ G).obj B) (fun (a : α) ↦ (F ⋙ G).obj (x a)) fun (a : α) ↦
    (F ⋙ G).map (x_1 a)
have dsimp : EffectiveEpiFamily.{v_3, u_3, u} (C := E) (B := G.obj (F.obj B)) (fun (a : α) ↦ G.obj (F.obj (x a))) fun (a : α) ↦
  G.map (F.map (x_1 a))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.ReflectsFiniteEffectiveEpiFamilies
X Y : C
x : X ⟶ Y
h : EffectiveEpi (F.map x)
⊢ EffectiveEpi x
have h₁ : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj Y) (fun (x : Unit) ↦ F.obj X) fun (x_1 : Unit) ↦
  match (motive := (x : Unit) → (fun (x : Unit) ↦ F.obj X) x ⟶ F.obj Y) x_1 with
  | PUnit.unit => F.map x
Tactic: rw [effectiveEpi_iff_effectiveEpiFamily] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.ReflectsFiniteEffectiveEpiFamilies
X Y : C
x : X ⟶ Y
h :
  EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj Y) (fun (x : Unit) ↦ F.obj X) fun (x_1 : Unit) ↦
    match (motive := (x : Unit) → (fun (x : Unit) ↦ F.obj X) x ⟶ F.obj Y) x_1 with
    | PUnit.unit => F.map x
⊢ EffectiveEpi x
have this : EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := Y) (fun (a : Unit) ↦ X) fun (a : Unit) ↦ x
Tactic: have := F.finite_effectiveEpiFamily_of_map _ _ h
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.IsEquivalence
α : Type u_3
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, u_3} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)
i : (a : α) → X a ⟶ F.inv.obj (F.obj (X a)) := fun (a : α) ↦ F.asEquivalence.unit.app (X a)
⊢ EffectiveEpiFamily X π
have this : EffectiveEpiFamily.{v_1, u_1, u_3} (B := F.inv.obj (F.obj B)) X fun (a : α) ↦ i a ≫ F.inv.map (F.map (π a))
Tactic: have : EffectiveEpiFamily X (fun a ↦ (i a) ≫ (inv F).map (F.map (π a))) := inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.IsEquivalence
α : Type u_3
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, u_3} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)
i : (a : α) → X a ⟶ F.inv.obj (F.obj (X a)) := fun (a : α) ↦ F.asEquivalence.unit.app (X a)
this : EffectiveEpiFamily.{v_1, u_1, u_3} (B := F.inv.obj (F.obj B)) X fun (a : α) ↦ i a ≫ F.inv.map (F.map (π a))
⊢ EffectiveEpiFamily X π
have this₁ : EffectiveEpiFamily.{v_1, u_1, u_3} (B := F.inv.obj (F.obj B)) X fun (a : α) ↦ π a ≫ F.asEquivalence.unit.app B
Tactic: simp only [inv_fun_map, Iso.hom_inv_id_app_assoc, i] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.IsEquivalence
α : Type u_3
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, u_3} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)
i : (a : α) → X a ⟶ F.inv.obj (F.obj (X a)) := fun (a : α) ↦ F.asEquivalence.unit.app (X a)
this : EffectiveEpiFamily.{v_1, u_1, u_3} (B := F.inv.obj (F.obj B)) X fun (a : α) ↦ π a ≫ F.asEquivalence.unit.app B
⊢ EffectiveEpiFamily X π
have this₁ : EffectiveEpiFamily.{v_1, u_1, u_3} (B := obj.{v_1, v_1, u_1, u_1} (𝟭 C) B) X fun (a : α) ↦
  (π a ≫ F.asEquivalence.unit.app B) ≫ F.asEquivalence.unitInv.app B
Tactic: have : EffectiveEpiFamily X (fun a ↦ (π a ≫ (asEquivalence F).unit.app B) ≫
        (asEquivalence F).unitInv.app _) := inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
x y : F.Elements
h₁ : x.fst (β := fun (c : C) ↦ F.obj c) = y.fst (β := fun (c : C) ↦ F.obj c)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom h₁)) :
        (a : (fun (X : Type w) ↦ X) (F.obj x.fst)) → (fun (X : Type w) ↦ X) (F.obj y.fst))
      (x.snd (β := fun (c : C) ↦ F.obj c)) =
    y.snd (β := fun (c : C) ↦ F.obj c)
⊢ x = y
have mk : ∀ (fst : C) (snd : F.obj fst)
  (h₁ :
    (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).fst (β := fun (c : C) ↦ F.obj c) =
      y.fst (β := fun (c : C) ↦ F.obj c))
  (h₂ :
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom h₁)) :
          (a : (fun (X : Type w) ↦ X) (F.obj ⟨fst, snd⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj y.fst))
        ((Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).snd (β := fun (c : C) ↦ F.obj c)) =
      y.snd (β := fun (c : C) ↦ F.obj c)),
  Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd = y
Tactic: cases x
Cleared hypotheses: x, h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
y : F.Elements
fst : C
snd : F.obj fst
h₁ :
  (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).fst (β := fun (c : C) ↦ F.obj c) = y.fst (β := fun (c : C) ↦ F.obj c)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom h₁)) :
        (a : (fun (X : Type w) ↦ X) (F.obj ⟨fst, snd⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj y.fst))
      ((Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).snd (β := fun (c : C) ↦ F.obj c)) =
    y.snd (β := fun (c : C) ↦ F.obj c)
⊢ Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd = y
have mk : ∀ (fst_1 : C) (snd_1 : F.obj fst_1)
  (h₁ :
    (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).fst (β := fun (c : C) ↦ F.obj c) =
      (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst_1 snd_1).fst (β := fun (c : C) ↦ F.obj c))
  (h₂ :
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom h₁)) :
          (a : (fun (X : Type w) ↦ X) (F.obj ⟨fst, snd⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj ⟨fst_1, snd_1⟩.fst))
        ((Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).snd (β := fun (c : C) ↦ F.obj c)) =
      (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst_1 snd_1).snd (β := fun (c : C) ↦ F.obj c)),
  Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd = Sigma.mk (β := fun (c : C) ↦ F.obj c) fst_1 snd_1
Tactic: cases y
Cleared hypotheses: y, h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
fst : C
snd : F.obj fst
fst_1 : C
snd_1 : F.obj fst_1
h₁ :
  (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).fst (β := fun (c : C) ↦ F.obj c) =
    (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst_1 snd_1).fst (β := fun (c : C) ↦ F.obj c)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom h₁)) :
        (a : (fun (X : Type w) ↦ X) (F.obj ⟨fst, snd⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj ⟨fst_1, snd_1⟩.fst))
      ((Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).snd (β := fun (c : C) ↦ F.obj c)) =
    (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst_1 snd_1).snd (β := fun (c : C) ↦ F.obj c)
⊢ Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd = Sigma.mk (β := fun (c : C) ↦ F.obj c) fst_1 snd_1
have mk : ∀ (snd_2 : F.obj fst)
  (h₂ :
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom sorry)) :
          (a : (fun (X : Type w) ↦ X) (F.obj ⟨fst, snd⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj ⟨fst, snd_2⟩.fst))
        ((Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd).snd (β := fun (c : C) ↦ F.obj c)) =
      (Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd_2).snd (β := fun (c : C) ↦ F.obj c)),
  Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd = Sigma.mk (β := fun (c : C) ↦ F.obj c) fst snd_2
Tactic: cases h₁
Cleared hypotheses: fst_1, snd_1, h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
x y : F.Elements
e : x.fst (β := fun (c : C) ↦ F.obj c) ≅ y.fst (β := fun (c : C) ↦ F.obj c)
he :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom) :
        (a : (fun (X : Type w) ↦ X) (F.obj x.fst)) → (fun (X : Type w) ↦ X) (F.obj y.fst))
      (x.snd (β := fun (c : C) ↦ F.obj c)) =
    y.snd (β := fun (c : C) ↦ F.obj c)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.inv) :
        (a : (fun (X : Type w) ↦ X) (F.obj y.fst)) → (fun (X : Type w) ↦ X) (F.obj x.fst))
      (y.snd (β := fun (c : C) ↦ F.obj c)) =
    x.snd (β := fun (c : C) ↦ F.obj c)
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.inv) :
      (a : (fun (X : Type w) ↦ X) (F.obj y.fst)) → (fun (X : Type w) ↦ X) (F.obj x.fst))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom) :
          (a : (fun (X : Type w) ↦ X) (F.obj x.fst)) → (fun (X : Type w) ↦ X) (F.obj y.fst))
        (x.snd (β := fun (c : C) ↦ F.obj c)) :
      (fun (X : Type w) ↦ X) (F.obj (y.fst (β := fun (c : C) ↦ F.obj c)))) =
  x.snd (β := fun (c : C) ↦ F.obj c)
Tactic: rw [← he, Functor.map_hom_inv'_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
x y : F.Elements
e : x.fst (β := fun (c : C) ↦ F.obj c) ≅ y.fst (β := fun (c : C) ↦ F.obj c)
he :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom) :
        (a : (fun (X : Type w) ↦ X) (F.obj x.fst)) → (fun (X : Type w) ↦ X) (F.obj y.fst))
      (x.snd (β := fun (c : C) ↦ F.obj c)) =
    y.snd (β := fun (c : C) ↦ F.obj c)
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.inv) :
        (a : (fun (X : Type w) ↦ X) (F.obj y.fst)) → (fun (X : Type w) ↦ X) (F.obj x.fst))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.hom) :
            (a : (fun (X : Type w) ↦ X) (F.obj x.fst)) → (fun (X : Type w) ↦ X) (F.obj y.fst))
          (x.snd (β := fun (c : C) ↦ F.obj c)) :
        (fun (X : Type w) ↦ X) (F.obj (y.fst (β := fun (c : C) ↦ F.obj c)))) =
    x.snd (β := fun (c : C) ↦ F.obj c)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map e.inv) :
        (a : (fun (X : Type w) ↦ X) (F.obj y.fst)) → (fun (X : Type w) ↦ X) (F.obj x.fst))
      (y.snd (β := fun (c : C) ↦ F.obj c)) =
    x.snd (β := fun (c : C) ↦ F.obj c)
have rw₁ : x.snd (β := fun (c : C) ↦ F.obj c) = x.snd (β := fun (c : C) ↦ F.obj c)
Tactic: rw [← he, Functor.map_hom_inv'_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u
inst_1 : Groupoid.{v, u} G
F : Functor.{v, w, u, w + 1} G (Type w)
p q : F.Elements
f : p ⟶ q
⊢ Eq (α := (fun (X : Type w) ↦ X) (F.obj (p.fst (β := fun (c : G) ↦ F.obj c))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Groupoid.inv (↑f : p.fst ⟶ q.fst))) :
          (a : (fun (X : Type w) ↦ X) (F.obj q.fst)) → (fun (X : Type w) ↦ X) (F.obj p.fst))
        (q.snd (β := fun (c : G) ↦ F.obj c)) :
      (fun (X : Type w) ↦ X) (F.obj (p.fst (β := fun (c : G) ↦ F.obj c))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Groupoid.inv (↑f : p.fst ⟶ q.fst))) :
          (a : (fun (X : Type w) ↦ X) (F.obj q.fst)) → (fun (X : Type w) ↦ X) (F.obj p.fst))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (↑f : p.fst ⟶ q.fst)) :
              (a : (fun (X : Type w) ↦ X) (F.obj p.fst)) → (fun (X : Type w) ↦ X) (F.obj q.fst))
            (p.snd (β := fun (c : G) ↦ F.obj c)) :
          (fun (X : Type w) ↦ X) (F.obj (q.fst (β := fun (c : G) ↦ F.obj c)))) :
      (fun (X : Type w) ↦ X) (F.obj (p.fst (β := fun (c : G) ↦ F.obj c))))
have rw : Eq (α := (fun (X : Type w) ↦ X) (F.obj (p.fst (β := fun (c : G) ↦ F.obj c))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Groupoid.inv (↑f : p.fst ⟶ q.fst))) :
        (a : (fun (X : Type w) ↦ X) (F.obj q.fst)) → (fun (X : Type w) ↦ X) (F.obj p.fst))
      (q.snd (β := fun (c : G) ↦ F.obj c)) :
    (fun (X : Type w) ↦ X) (F.obj (p.fst (β := fun (c : G) ↦ F.obj c))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Groupoid.inv (↑f : p.fst ⟶ q.fst))) :
        (a : (fun (X : Type w) ↦ X) (F.obj q.fst)) → (fun (X : Type w) ↦ X) (F.obj p.fst))
      (q.snd (β := fun (c : G) ↦ F.obj c)) :
    (fun (X : Type w) ↦ X) (F.obj (p.fst (β := fun (c : G) ↦ F.obj c))))
Tactic: rw [f.2]
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u
inst_1 : Groupoid.{v, u} G
F : Functor.{v, w, u, w + 1} G (Type w)
p q : F.Elements
f : p ⟶ q
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (↑f : p.fst ⟶ q.fst) ≫ F.map (Groupoid.inv (↑f : p.fst ⟶ q.fst))) :
        (a : (fun (X : Type w) ↦ X) (F.obj p.fst)) → (fun (X : Type w) ↦ X) (F.obj p.fst))
      (p.snd (β := fun (c : G) ↦ F.obj c)) =
    p.snd (β := fun (c : G) ↦ F.obj c)
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ((↑f : p.fst ⟶ q.fst) ≫ Groupoid.inv (↑f : p.fst ⟶ q.fst))) :
      (a : (fun (X : Type w) ↦ X) (F.obj p.fst)) → (fun (X : Type w) ↦ X) (F.obj p.fst))
    (p.snd (β := fun (c : G) ↦ F.obj c)) =
  p.snd (β := fun (c : G) ↦ F.obj c)
Tactic: rw [← F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u
inst_1 : Groupoid.{v, u} G
F : Functor.{v, w, u, w + 1} G (Type w)
X Y : F.Elements
x : X ⟶ Y
⊢ Subtype.mk (p := fun (f : Y.fst (β := fun (c : G) ↦ F.obj c) ⟶ X.fst (β := fun (c : G) ↦ F.obj c)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w) ↦ X) (F.obj Y.fst)) → (fun (X : Type w) ↦ X) (F.obj X.fst))
            (Y.snd (β := fun (c : G) ↦ F.obj c)) =
          X.snd (β := fun (c : G) ↦ F.obj c))
        (Groupoid.inv (↑x : X.fst ⟶ Y.fst)) ⋯ ≫
      x =
    𝟙 Y
have w : (↑(Subtype.mk (p := fun (f : Y.fst (β := fun (c : G) ↦ F.obj c) ⟶ X.fst (β := fun (c : G) ↦ F.obj c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w) ↦ X) (F.obj Y.fst)) → (fun (X : Type w) ↦ X) (F.obj X.fst))
              (Y.snd (β := fun (c : G) ↦ F.obj c)) =
            X.snd (β := fun (c : G) ↦ F.obj c))
          (Groupoid.inv (↑x : X.fst ⟶ Y.fst)) sorry ≫
        x) :
    Y.fst ⟶ Y.fst) =
  (↑(𝟙 Y) : Y.fst ⟶ Y.fst)
Tactic: ext