awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Homology (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
s : CokernelCofork φ
rw :
  Eq.{v + 1} (α := (↑M.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v))
    (↑(Hom.hom 0) : (↑M.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v)) 0
⊢ (↑(Hom.hom (φ ≫ Cofork.π s)) : (↑M.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v)) = 0
have rw₁ : Eq.{v + 1} (α := (↑M.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v))
  (↑0 : (↑M.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v)) 0
Tactic: rw [s.condition, hom_zero, ContinuousLinearMap.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Homology (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
s : CokernelCofork φ
rw :
  Eq.{v + 1} (α := (↑M.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v))
    (↑(Hom.hom 0) : (↑M.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v)) 0
rw₁ :
  Eq.{v + 1} (α := (↑M.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v))
    (↑0 : (↑M.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v)) 0
⊢ (↑(Hom.hom (φ ≫ Cofork.π s)) : (↑M.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v)) = 0
have rw₂ : Eq.{v + 1} (α := (↑M.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v)) 0 0
Tactic: rw [s.condition, hom_zero, ContinuousLinearMap.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Homology (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
s : CokernelCofork φ
m : (CokernelCofork.ofπ (cokerπ φ) ⋯).pt ⟶ s.pt
h : cokerπ φ ≫ m = Cofork.π s
⊢ m =
    ofHom
      {
        toLinearMap :=
          (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range.liftQ
            (↑(Hom.hom (Cofork.π s)) : (↑N.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v)) ⋯,
        cont := ⋯ }
have rw : Cofork.π s =
  cokerπ φ ≫
    ofHom
      {
        toLinearMap :=
          (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range.liftQ
            (↑(Hom.hom (Cofork.π s)) : (↑N.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v)) sorry,
        cont := sorry }
Tactic: rw [← cancel_epi (cokerπ φ), h]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Ulift (goal)
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
h : S.Exact
⊢ ShortComplex.Exact (S.map (uliftFunctor.{u_1, v, u} R))
have rw : Function.Exact (M := (↑(ShortComplex.X₁ (S.map (uliftFunctor.{u_1, v, u} R))) : Type (max u_1 v))) (N :=
  (↑(ShortComplex.X₂ (S.map (uliftFunctor.{u_1, v, u} R))) : Type (max u_1 v))) (P :=
  (↑(ShortComplex.X₃ (S.map (uliftFunctor.{u_1, v, u} R))) : Type (max u_1 v)))
  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u_1 v)) →ₗ[R] (↑x2 : Type (max u_1 v)))
        (CC := carrier) (X := ShortComplex.X₁ (S.map (uliftFunctor.{u_1, v, u} R)))
        (ShortComplex.f (S.map (uliftFunctor.{u_1, v, u} R)))) :
    (a : (↑(S.map (uliftFunctor.{u_1, v, u} R)).X₁ : Type (max u_1 v))) →
      (↑(S.map (uliftFunctor.{u_1, v, u} R)).X₂ : Type (max u_1 v)))
  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u_1 v)) →ₗ[R] (↑x2 : Type (max u_1 v)))
        (CC := carrier) (X := ShortComplex.X₂ (S.map (uliftFunctor.{u_1, v, u} R)))
        (ShortComplex.g (S.map (uliftFunctor.{u_1, v, u} R)))) :
    (a : (↑(S.map (uliftFunctor.{u_1, v, u} R)).X₂ : Type (max u_1 v))) →
      (↑(S.map (uliftFunctor.{u_1, v, u} R)).X₃ : Type (max u_1 v)))
Tactic: rw [CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Ulift (goal)
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
h : S.Exact
⊢ Function.Exact (M := (↑(ShortComplex.X₁ (S.map (uliftFunctor.{u_1, v, u} R))) : Type (max u_1 v))) (N :=
    (↑(ShortComplex.X₂ (S.map (uliftFunctor.{u_1, v, u} R))) : Type (max u_1 v))) (P :=
    (↑(ShortComplex.X₃ (S.map (uliftFunctor.{u_1, v, u} R))) : Type (max u_1 v)))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u_1 v)) →ₗ[R] (↑x2 : Type (max u_1 v)))
          (CC := carrier) (X := ShortComplex.X₁ (S.map (uliftFunctor.{u_1, v, u} R)))
          (ShortComplex.f (S.map (uliftFunctor.{u_1, v, u} R)))) :
      (a : (↑(S.map (uliftFunctor.{u_1, v, u} R)).X₁ : Type (max u_1 v))) →
        (↑(S.map (uliftFunctor.{u_1, v, u} R)).X₂ : Type (max u_1 v)))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u_1 v)) →ₗ[R] (↑x2 : Type (max u_1 v)))
          (CC := carrier) (X := ShortComplex.X₂ (S.map (uliftFunctor.{u_1, v, u} R)))
          (ShortComplex.g (S.map (uliftFunctor.{u_1, v, u} R)))) :
      (a : (↑(S.map (uliftFunctor.{u_1, v, u} R)).X₂ : Type (max u_1 v))) →
        (↑(S.map (uliftFunctor.{u_1, v, u} R)).X₃ : Type (max u_1 v)))
have dsimp : Function.Exact (M := ULift.{u_1, v} (↑S.X₁ : Type v)) (N := ULift.{u_1, v} (↑S.X₂ : Type v)) (P :=
  ULift.{u_1, v} (↑S.X₃ : Type v))
  (Function.comp (β := (↑S.X₂ : Type v))
    (⇑(LinearEquiv.symm ULift.moduleEquiv) : (a : (↑S.X₂ : Type v)) → ULift.{u_1, v} (↑S.X₂ : Type v))
    (Function.comp (β := (↑S.X₁ : Type v)) (⇑(Hom.hom S.f) : (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v))
      (⇑ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₁ : Type v)) → (↑S.X₁ : Type v))))
  (Function.comp (β := (↑S.X₃ : Type v))
    (⇑(LinearEquiv.symm ULift.moduleEquiv) : (a : (↑S.X₃ : Type v)) → ULift.{u_1, v} (↑S.X₃ : Type v))
    (Function.comp (β := (↑S.X₂ : Type v)) (⇑(Hom.hom S.g) : (a : (↑S.X₂ : Type v)) → (↑S.X₃ : Type v))
      (⇑ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₂ : Type v)) → (↑S.X₂ : Type v))))
Tactic: dsimp [uliftFunctor]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Ulift (goal)
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
h : S.Exact
x : ULift.{u_1, v} (↑S.X₂ : Type v)
⊢ Eq (α := ULift.{u_1, v} (↑S.X₃ : Type v))
      (Function.comp (β := (↑S.X₃ : Type v))
        (⇑(LinearEquiv.symm ULift.moduleEquiv) : (a : (↑S.X₃ : Type v)) → ULift.{u_1, v} (↑S.X₃ : Type v))
        (Function.comp (β := (↑S.X₂ : Type v)) (⇑(Hom.hom S.g) : (a : (↑S.X₂ : Type v)) → (↑S.X₃ : Type v))
          (⇑ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₂ : Type v)) → (↑S.X₂ : Type v)))
        x)
      0 ↔
    Membership.mem (γ := Set (ULift.{u_1, v} (↑S.X₂ : Type v)))
      (Set.range (ι := ULift.{u_1, v} (↑S.X₁ : Type v))
        (Function.comp (β := (↑S.X₂ : Type v))
          (⇑(LinearEquiv.symm ULift.moduleEquiv) : (a : (↑S.X₂ : Type v)) → ULift.{u_1, v} (↑S.X₂ : Type v))
          (Function.comp (β := (↑S.X₁ : Type v)) (⇑(Hom.hom S.f) : (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v))
            (⇑ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₁ : Type v)) → (↑S.X₁ : Type v)))))
      x
have simp : Eq (α := (↑S.X₃ : Type v))
    ((Hom.hom S.g : (a : (↑S.X₂ : Type v)) → (↑S.X₃ : Type v))
        ((ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₂ : Type v)) → (↑S.X₂ : Type v)) x : (↑S.X₂ : Type v)) :
      (↑S.X₃ : Type v))
    (0 : (↑S.X₃ : Type v)) ↔
  ∃ (y : ULift.{u_1, v} (↑S.X₁ : Type v)),
    Eq (α := (↑S.X₂ : Type v))
      ((Hom.hom S.f : (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v))
          ((ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₁ : Type v)) → (↑S.X₁ : Type v)) y : (↑S.X₁ : Type v)) :
        (↑S.X₂ : Type v))
      ((ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₂ : Type v)) → (↑S.X₂ : Type v)) x : (↑S.X₂ : Type v))
Tactic: simp only [Function.comp_apply, Set.mem_range, LinearEquiv.symm_apply_eq, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Ulift (goal)
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
h : S.Exact
x : ULift.{u_1, v} (↑S.X₂ : Type v)
⊢ Eq (α := (↑S.X₃ : Type v))
      ((Hom.hom S.g : (a : (↑S.X₂ : Type v)) → (↑S.X₃ : Type v))
          ((ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₂ : Type v)) → (↑S.X₂ : Type v)) x : (↑S.X₂ : Type v)) :
        (↑S.X₃ : Type v))
      (0 : (↑S.X₃ : Type v)) ↔
    ∃ (y : ULift.{u_1, v} (↑S.X₁ : Type v)),
      Eq (α := (↑S.X₂ : Type v))
        ((Hom.hom S.f : (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v))
            ((ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₁ : Type v)) → (↑S.X₁ : Type v)) y : (↑S.X₁ : Type v)) :
          (↑S.X₂ : Type v))
        ((ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₂ : Type v)) → (↑S.X₂ : Type v)) x : (↑S.X₂ : Type v))
have rw : Membership.mem (α := (↑S.X₂ : Type v)) (γ := Set (↑S.X₂ : Type v))
    (Set.range (ι := (↑S.X₁ : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) S.f) :
        (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v)))
    ((ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₂ : Type v)) → (↑S.X₂ : Type v)) x : (↑S.X₂ : Type v)) ↔
  ∃ (y : ULift.{u_1, v} (↑S.X₁ : Type v)),
    Eq (α := (↑S.X₂ : Type v))
      ((Hom.hom S.f : (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v))
          ((ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₁ : Type v)) → (↑S.X₁ : Type v)) y : (↑S.X₁ : Type v)) :
        (↑S.X₂ : Type v))
      ((ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₂ : Type v)) → (↑S.X₂ : Type v)) x : (↑S.X₂ : Type v))
Tactic: rw [(CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact S).mp h]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Ulift (hypothesis)
Goal:
R : Type u
inst : Ring R
⊢ Limits.PreservesFiniteColimits (C := ModuleCat.{v, u} R) (uliftFunctor.{v', v, u} R)
have this : Limits.PreservesFiniteLimits (C := ModuleCat.{v, u} R) (uliftFunctor.{v', v, u} R) ∧
  Limits.PreservesFiniteColimits (C := ModuleCat.{v, u} R) (uliftFunctor.{v', v, u} R)
Tactic: have := ((CategoryTheory.Functor.exact_tfae (uliftFunctor.{v', v} R)).out 1 3).mp
    (uliftFunctor_map_exact R)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Ulift (hypothesis)
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
M : ModuleCat.{v, u} R
proj : Projective M
⊢ Projective (Functor.obj (uliftFunctor.{v', v, u} R) M)
have this : Small.{max v v', u} R
Tactic: have := small_lift.{u, v'} R
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Basic (goal)
Goal:
X_1 Y_1 : Type u
X Y : MonCat
i : X ≅ Y
⊢ (MonCat.Hom.hom i.inv).comp (MonCat.Hom.hom i.hom) = MonoidHom.id (↑X : Type u_1)
have h : ∀ (x : (↑X : Type u_1)),
  Eq (α := (↑X : Type u_1))
    (((MonCat.Hom.hom i.inv).comp (MonCat.Hom.hom i.hom) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((MonoidHom.id (↑X : Type u_1) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Basic (goal)
Goal:
X_1 Y_1 : Type u
X Y : MonCat
i : X ≅ Y
⊢ (MonCat.Hom.hom i.hom).comp (MonCat.Hom.hom i.inv) = MonoidHom.id (↑Y : Type u_1)
have h : ∀ (x : (↑Y : Type u_1)),
  Eq (α := (↑Y : Type u_1))
    (((MonCat.Hom.hom i.hom).comp (MonCat.Hom.hom i.inv) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x : (↑Y : Type u_1))
    ((MonoidHom.id (↑Y : Type u_1) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x : (↑Y : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Basic (goal)
Goal:
X_1 Y_1 : Type u
X Y : CommMonCat
i : X ≅ Y
⊢ (CommMonCat.Hom.hom i.inv).comp (CommMonCat.Hom.hom i.hom) = MonoidHom.id (↑X : Type u_1)
have h : ∀ (x : (↑X : Type u_1)),
  Eq (α := (↑X : Type u_1))
    (((CommMonCat.Hom.hom i.inv).comp (CommMonCat.Hom.hom i.hom) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x :
      (↑X : Type u_1))
    ((MonoidHom.id (↑X : Type u_1) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Basic (goal)
Goal:
X_1 Y_1 : Type u
X Y : CommMonCat
i : X ≅ Y
⊢ (CommMonCat.Hom.hom i.hom).comp (CommMonCat.Hom.hom i.inv) = MonoidHom.id (↑Y : Type u_1)
have h : ∀ (x : (↑Y : Type u_1)),
  Eq (α := (↑Y : Type u_1))
    (((CommMonCat.Hom.hom i.hom).comp (CommMonCat.Hom.hom i.inv) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x :
      (↑Y : Type u_1))
    ((MonoidHom.id (↑Y : Type u_1) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x : (↑Y : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Colimits (goal)
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j
have hf : ∀ (x : (↑(F.obj j) : Type v)),
  Eq (α := (↑(colimit F) : Type v))
    ((Hom.hom (F.map f ≫ coconeMorphism F j') : (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v)) x :
      (↑(colimit F) : Type v))
    ((Hom.hom (coconeMorphism F j) : (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v)) x : (↑(colimit F) : Type v))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Colimits (goal)
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type v)
⊢ Eq (α := (↑(colimit F) : Type v))
    ((Hom.hom (F.map f ≫ coconeMorphism F j') : (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v)) x :
      (↑(colimit F) : Type v))
    ((Hom.hom (coconeMorphism F j) : (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v)) x : (↑(colimit F) : Type v))
have hf : (colimitSetoid F : Prequotient F → Prequotient F → Prop)
  (Prequotient.of j' (((F.map f).hom' : (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v)) x)) (Prequotient.of j x)
Tactic: apply Quot.sound
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Colimits (goal)
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type v)
⊢ Eq (α := (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
            (coconeMorphism F j') :
          (a : (↑(F.obj j') : Type v)) → (↑(colimit F) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
          x) :
      (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
            (coconeMorphism F j) :
          (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v))
        x :
      (↑(colimit F) : Type v))
have rw : Eq (α := (↑(colimit F) : Type v))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
          (coconeMorphism F j') :
        (a : (↑(F.obj j') : Type v)) → (↑(colimit F) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
            (F.map f) :
          (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
        x) :
    (↑(colimit F) : Type v))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
          (F.map f ≫ coconeMorphism F j') :
        (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v))
      x :
    (↑(colimit F) : Type v))
Tactic: rw [← cocone_naturality F f]
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Colimits (goal)
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
s : Cocone F
⊢ ColimitType F → (↑s.pt : Type v)
have f : (a : Prequotient F) → (↑s.pt : Type v)
Tactic: fapply Quot.lift
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Colimits (goal)
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
s : Cocone F
f : (a : Prequotient F) → (↑s.pt : Type v)
⊢ ColimitType F → (↑s.pt : Type v)
have a : ∀ (a b : Prequotient F) (a_1 : (colimitSetoid F : Prequotient F → Prequotient F → Prop) a b),
  descFunLift F s a = descFunLift F s b
Tactic: fapply Quot.lift
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Colimits (goal)
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
s : Cocone F
x y : Prequotient F
r : (colimitSetoid F : Prequotient F → Prequotient F → Prop) x y
⊢ descFunLift F s x = descFunLift F s y
have a : ∀ (x : Prequotient F), descFunLift F s x = descFunLift F s x
Tactic: induction r with
    | refl x => rfl
    | symm x y _ h => exact h.symm
    | trans x y z _ _ h₁ h₂ => exact h₁.trans h₂
    | map j j' f x => exact s.w_apply f x
    | mul j x y => exact map_mul (s.ι.app j).hom x y
    | one j => exact map_one (s.ι.app j).hom
    | mul_1 x x' y _ h => exact congr_arg (· * _) h
    | mul_2 x y y' _ h => exact congr_arg (_ * ·) h
    | mul_assoc x y z => exact mul_assoc _ _ _
    | one_mul x => exact one_mul _
    | mul_one x => exact mul_one _
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Colimits (goal)
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
s : Cocone F
x y : Prequotient F
r : (colimitSetoid F : Prequotient F → Prequotient F → Prop) x y
a : ∀ (x : Prequotient F), descFunLift F s x = descFunLift F s x
⊢ descFunLift F s x = descFunLift F s y
have a₁ : ∀ (x y : Prequotient F),
  Relation F x y → ∀ (h : descFunLift F s x = descFunLift F s y), descFunLift F s y = descFunLift F s x
Tactic: induction r with
    | refl x => rfl
    | symm x y _ h => exact h.symm
    | trans x y z _ _ h₁ h₂ => exact h₁.trans h₂
    | map j j' f x => exact s.w_apply f x
    | mul j x y => exact map_mul (s.ι.app j).hom x y
    | one j => exact map_one (s.ι.app j).hom
    | mul_1 x x' y _ h => exact congr_arg (· * _) h
    | mul_2 x y y' _ h => exact congr_arg (_ * ·) h
    | mul_assoc x y z => exact mul_assoc _ _ _
    | one_mul x => exact one_mul _
    | mul_one x => exact mul_one _
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Colimits (goal)
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
s : Cocone F
x y : Prequotient F
r : (colimitSetoid F : Prequotient F → Prequotient F → Prop) x y
a : ∀ (x : Prequotient F), descFunLift F s x = descFunLift F s x
a₁ :
  ∀ (x y : Prequotient F),
    Relation F x y → ∀ (h : descFunLift F s x = descFunLift F s y), descFunLift F s y = descFunLift F s x
⊢ descFunLift F s x = descFunLift F s y
have a₂ : ∀ (x y z : Prequotient F),
  Relation F x y →
    Relation F y z →
      ∀ (h₁ : descFunLift F s x = descFunLift F s y) (h₂ : descFunLift F s y = descFunLift F s z),
        descFunLift F s x = descFunLift F s z
Tactic: induction r with
    | refl x => rfl
    | symm x y _ h => exact h.symm
    | trans x y z _ _ h₁ h₂ => exact h₁.trans h₂
    | map j j' f x => exact s.w_apply f x
    | mul j x y => exact map_mul (s.ι.app j).hom x y
    | one j => exact map_one (s.ι.app j).hom
    | mul_1 x x' y _ h => exact congr_arg (· * _) h
    | mul_2 x y y' _ h => exact congr_arg (_ * ·) h
    | mul_assoc x y z => exact mul_assoc _ _ _
    | one_mul x => exact one_mul _
    | mul_one x => exact mul_one _
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Colimits (goal)
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
s : Cocone F
x y : Prequotient F
r : (colimitSetoid F : Prequotient F → Prequotient F → Prop) x y
a : ∀ (x : Prequotient F), descFunLift F s x = descFunLift F s x
a₁ :
  ∀ (x y : Prequotient F),
    Relation F x y → ∀ (h : descFunLift F s x = descFunLift F s y), descFunLift F s y = descFunLift F s x
a₂ :
  ∀ (x y z : Prequotient F),
    Relation F x y →
      Relation F y z →
        ∀ (h₁ : descFunLift F s x = descFunLift F s y) (h₂ : descFunLift F s y = descFunLift F s z),
          descFunLift F s x = descFunLift F s z
⊢ descFunLift F s x = descFunLift F s y
have a₃ : ∀ (j j' : J) (f : j ⟶ j') (x : (↑(F.obj j) : Type v)),
  descFunLift F s
      (Prequotient.of j'
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
          x)) =
    descFunLift F s (Prequotient.of j x)
Tactic: induction r with
    | refl x => rfl
    | symm x y _ h => exact h.symm
    | trans x y z _ _ h₁ h₂ => exact h₁.trans h₂
    | map j j' f x => exact s.w_apply f x
    | mul j x y => exact map_mul (s.ι.app j).hom x y
    | one j => exact map_one (s.ι.app j).hom
    | mul_1 x x' y _ h => exact congr_arg (· * _) h
    | mul_2 x y y' _ h => exact congr_arg (_ * ·) h
    | mul_assoc x y z => exact mul_assoc _ _ _
    | one_mul x => exact one_mul _
    | mul_one x => exact mul_one _
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Colimits (goal)
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
s : Cocone F
x y : Prequotient F
r : (colimitSetoid F : Prequotient F → Prequotient F → Prop) x y
a : ∀ (x : Prequotient F), descFunLift F s x = descFunLift F s x
a₁ :
  ∀ (x y : Prequotient F),
    Relation F x y → ∀ (h : descFunLift F s x = descFunLift F s y), descFunLift F s y = descFunLift F s x
a₂ :
  ∀ (x y z : Prequotient F),
    Relation F x y →
      Relation F y z →
        ∀ (h₁ : descFunLift F s x = descFunLift F s y) (h₂ : descFunLift F s y = descFunLift F s z),
          descFunLift F s x = descFunLift F s z
a₃ :
  ∀ (j j' : J) (f : j ⟶ j') (x : (↑(F.obj j) : Type v)),
    descFunLift F s
        (Prequotient.of j'
          ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
                (F.map f) :
              (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
            x)) =
      descFunLift F s (Prequotient.of j x)
⊢ descFunLift F s x = descFunLift F s y
have a₄ : ∀ (j : J) (x y : (↑(F.obj j) : Type v)),
  descFunLift F s (Prequotient.of j (x * y)) = descFunLift F s ((Prequotient.of j x).mul (Prequotient.of j y))
Tactic: induction r with
    | refl x => rfl
    | symm x y _ h => exact h.symm
    | trans x y z _ _ h₁ h₂ => exact h₁.trans h₂
    | map j j' f x => exact s.w_apply f x
    | mul j x y => exact map_mul (s.ι.app j).hom x y
    | one j => exact map_one (s.ι.app j).hom
    | mul_1 x x' y _ h => exact congr_arg (· * _) h
    | mul_2 x y y' _ h => exact congr_arg (_ * ·) h
    | mul_assoc x y z => exact mul_assoc _ _ _
    | one_mul x => exact one_mul _
    | mul_one x => exact mul_one _
Cleared hypotheses: r