awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ContinuousCohomology.Basic (goal)
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : Group G
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
rep : Action (TopModuleCat.{u_3, u_1} R) G
g : G
x : R
x_1 : ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type u_3)
⊢ ContinuousMap.comp
      (↑(TopModuleCat.Hom.hom ((rep.ρ : (a : G) → End rep.V) g)) :
        C((↑rep.V.toModuleCat : Type u_3), (↑rep.V.toModuleCat : Type u_3)))
      ((x • x_1).comp (↑(Homeomorph.mulLeft g⁻¹) : C(G, G))) =
    HSMul.hSMul (α := R) (β := ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type u_3))
      ((RingHom.id R : (a : R) → R) x : R)
      (ContinuousMap.comp
        (↑(TopModuleCat.Hom.hom ((rep.ρ : (a : G) → End rep.V) g)) :
          C((↑rep.V.toModuleCat : Type u_3), (↑rep.V.toModuleCat : Type u_3)))
        (x_1.comp (↑(Homeomorph.mulLeft g⁻¹) : C(G, G))))
have h : ∀ (a : G),
  Eq.{u_3 + 1} (α := (↑rep.V.toModuleCat : Type u_3))
    (((ContinuousMap.comp
              (↑(TopModuleCat.Hom.hom ((rep.ρ : (a : G) → End rep.V) g)) :
                C((↑rep.V.toModuleCat : Type u_3), (↑rep.V.toModuleCat : Type u_3)))
              ((x • x_1).comp (↑(Homeomorph.mulLeft g⁻¹) : C(G, G))) :
            ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type u_3)) :
          (a : G) → (↑rep.V.toModuleCat : Type u_3))
        a :
      (↑rep.V.toModuleCat : Type u_3))
    ((HSMul.hSMul (α := R) (β := ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type u_3))
            ((RingHom.id R : (a : R) → R) x : R)
            (ContinuousMap.comp
              (↑(TopModuleCat.Hom.hom ((rep.ρ : (a : G) → End rep.V) g)) :
                C((↑rep.V.toModuleCat : Type u_3), (↑rep.V.toModuleCat : Type u_3)))
              (x_1.comp (↑(Homeomorph.mulLeft g⁻¹) : C(G, G)))) :
          (a : G) → (↑rep.V.toModuleCat : Type u_3))
        a :
      (↑rep.V.toModuleCat : Type u_3))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ContinuousCohomology.Basic (goal)
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : Group G
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
M N : Action (TopModuleCat.{u_3, u_1} R) G
φ : M ⟶ N
g : G
f : (↑(Iobj M).V.toModuleCat : Type (max u_2 u_3))
g' : G
⊢ Eq (α := (↑N.V.toModuleCat : Type u_3))
    ((TopModuleCat.Hom.hom ((M.ρ : (a : G) → End M.V) g ≫ φ.hom) :
          (a : (↑M.V.toModuleCat : Type u_3)) → (↑N.V.toModuleCat : Type u_3))
        ((f : (a : G) → (↑M.V.toModuleCat : Type u_3)) (g⁻¹ * g') : (↑M.V.toModuleCat : Type u_3)) :
      (↑N.V.toModuleCat : Type u_3))
    ((TopModuleCat.Hom.hom (φ.hom ≫ (N.ρ : (a : G) → End N.V) g) :
          (a : (↑M.V.toModuleCat : Type u_3)) → (↑N.V.toModuleCat : Type u_3))
        ((f : (a : G) → (↑M.V.toModuleCat : Type u_3)) (g⁻¹ * g') : (↑M.V.toModuleCat : Type u_3)) :
      (↑N.V.toModuleCat : Type u_3))
have h : Eq (α := (↑N.V.toModuleCat : Type u_3))
  ((TopModuleCat.Hom.hom (φ.hom ≫ (N.ρ : (a : G) → End N.V) g) :
        (a : (↑M.V.toModuleCat : Type u_3)) → (↑N.V.toModuleCat : Type u_3))
      ((f : (a : G) → (↑M.V.toModuleCat : Type u_3)) (g⁻¹ * g') : (↑M.V.toModuleCat : Type u_3)) :
    (↑N.V.toModuleCat : Type u_3))
  ((TopModuleCat.Hom.hom (φ.hom ≫ (N.ρ : (a : G) → End N.V) g) :
        (a : (↑M.V.toModuleCat : Type u_3)) → (↑N.V.toModuleCat : Type u_3))
      ((f : (a : G) → (↑M.V.toModuleCat : Type u_3)) (g⁻¹ * g') : (↑M.V.toModuleCat : Type u_3)) :
    (↑N.V.toModuleCat : Type u_3))
Tactic: rw [φ.comm]
-- Lean 4 proof step from Mathlib.Algebra.Category.ContinuousCohomology.Basic (goal)
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : Group G
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
⊢ Eq (α :=
    Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G) (functor.{u_1, u_2, u_3} R G 0)
      (functor.{u_1, u_2, u_3} R G (HAdd.hAdd (α := ℕ) 0 1 + 1)))
    (d R G 0 ≫ d R G (HAdd.hAdd (α := ℕ) 0 1)) 0
have zero : Eq (α :=
  Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G) (functor.{u_1, u_2, u_3} R G 0)
    (functor.{u_1, u_2, u_3} R G (HAdd.hAdd (α := ℕ) 0 1 + 1)))
  (d R G 0 ≫ whiskerLeft (functor.{u_1, u_2, u_3} R G (HAdd.hAdd (α := ℕ) 0 1)) (const.{u_1, u_2, u_3} R G))
  (d R G 0 ≫ whiskerRight (d R G 0) (I R G))
Tactic: rw [d_succ, Preadditive.comp_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Category.ContinuousCohomology.Basic (goal)
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : Group G
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
n : ℕ
ih :
  Eq (α :=
    Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G) (functor.{u_1, u_2, u_3} R G n)
      (functor.{u_1, u_2, u_3} R G (n + 1 + 1)))
    (d R G n ≫ d R G (n + 1)) 0
⊢ Eq (α :=
    Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G) (functor.{u_1, u_2, u_3} R G (n + 1))
      (functor.{u_1, u_2, u_3} R G (n + 1 + 1 + 1)))
    (d R G (n + 1) ≫ d R G (n + 1 + 1)) 0
have succ : HSub.hSub (α :=
    Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G) (functor.{u_1, u_2, u_3} R G (n + 1))
      (functor.{u_1, u_2, u_3} R G (n + 1 + 1 + 1)))
    (d R G (n + 1) ≫ whiskerLeft (functor.{u_1, u_2, u_3} R G (n + 1 + 1)) (const.{u_1, u_2, u_3} R G))
    (d R G (n + 1) ≫ whiskerRight (d R G (n + 1)) (I R G)) =
  0
Tactic: rw [d_succ R G (n + 1), Preadditive.comp_sub]
-- Lean 4 proof step from Mathlib.Algebra.Category.ContinuousCohomology.Basic (goal)
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : Group G
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
n : ℕ
ih :
  Eq (α :=
    Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G) (functor.{u_1, u_2, u_3} R G n)
      (functor.{u_1, u_2, u_3} R G (n + 1 + 1)))
    (d R G n ≫ d R G (n + 1)) 0
⊢ HSub.hSub (α :=
      Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G) (functor.{u_1, u_2, u_3} R G (n + 1))
        (functor.{u_1, u_2, u_3} R G (n + 1 + 1 + 1)))
      (d R G (n + 1) ≫ whiskerLeft (functor.{u_1, u_2, u_3} R G (n + 1 + 1)) (const.{u_1, u_2, u_3} R G))
      (d R G (n + 1) ≫ whiskerRight (d R G (n + 1)) (I R G)) =
    0
have succ : d R G (n + 1) ≫ whiskerLeft (functor.{u_1, u_2, u_3} R G (n + 1 + 1)) (const.{u_1, u_2, u_3} R G) -
    HSub.hSub (α :=
        Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G)
          (functor.{u_1, u_2, u_3} R G (n + 1) ⋙ 𝟭 (Action (TopModuleCat R) G))
          (functor.{u_1, u_2, u_3} R G (n + 1) ⋙ I R G))
        (β :=
        Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G)
          (functor.{u_1, u_2, u_3} R G (n + 1) ⋙ 𝟭 (Action (TopModuleCat R) G))
          (functor.{u_1, u_2, u_3} R G (n + 1) ⋙ I R G))
        (whiskerLeft (functor.{u_1, u_2, u_3} R G (n + 1)) (const.{u_1, u_2, u_3} R G) :
          Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G)
            (functor.{u_1, u_2, u_3} R G (n + 1) ⋙ 𝟭 (Action (TopModuleCat R) G))
            (functor.{u_1, u_2, u_3} R G (n + 1) ⋙ I R G))
        (whiskerRight (d R G n) (I R G) :
          Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G)
            (functor.{u_1, u_2, u_3} R G n ⋙ I R G) (functor.{u_1, u_2, u_3} R G (n + 1) ⋙ I R G)) ≫
      whiskerRight (d R G (n + 1)) (I R G) =
  0
Tactic: nth_rw 2 [d_succ]
-- Lean 4 proof step from Mathlib.Algebra.Category.ContinuousCohomology.Basic (goal)
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : Group G
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
n : ℕ
ih :
  Eq (α :=
    Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G) (functor.{u_1, u_2, u_3} R G n)
      (functor.{u_1, u_2, u_3} R G (n + 1 + 1)))
    (d R G n ≫ d R G (n + 1)) 0
⊢ d R G (n + 1) ≫ whiskerLeft (functor.{u_1, u_2, u_3} R G (n + 1 + 1)) (const.{u_1, u_2, u_3} R G) -
      HSub.hSub (α :=
          Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G)
            (functor.{u_1, u_2, u_3} R G (n + 1) ⋙ 𝟭 (Action (TopModuleCat R) G))
            (functor.{u_1, u_2, u_3} R G (n + 1) ⋙ I R G))
          (β :=
          Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G)
            (functor.{u_1, u_2, u_3} R G (n + 1) ⋙ 𝟭 (Action (TopModuleCat R) G))
            (functor.{u_1, u_2, u_3} R G (n + 1) ⋙ I R G))
          (whiskerLeft (functor.{u_1, u_2, u_3} R G (n + 1)) (const.{u_1, u_2, u_3} R G) :
            Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G)
              (functor.{u_1, u_2, u_3} R G (n + 1) ⋙ 𝟭 (Action (TopModuleCat R) G))
              (functor.{u_1, u_2, u_3} R G (n + 1) ⋙ I R G))
          (whiskerRight (d R G n) (I R G) :
            Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G)
              (functor.{u_1, u_2, u_3} R G n ⋙ I R G) (functor.{u_1, u_2, u_3} R G (n + 1) ⋙ I R G)) ≫
        whiskerRight (d R G (n + 1)) (I R G) =
    0
have succ : Eq (α :=
  Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G) (functor.{u_1, u_2, u_3} R G (n + 1))
    (functor.{u_1, u_2, u_3} R G (n + 1 + 1 + 1)))
  (d R G (n + 1) ≫ whiskerLeft (functor.{u_1, u_2, u_3} R G (n + 1 + 1)) (const.{u_1, u_2, u_3} R G))
  (whiskerLeft (functor.{u_1, u_2, u_3} R G (n + 1)) (const.{u_1, u_2, u_3} R G) ≫ whiskerRight (d R G (n + 1)) (I R G))
Tactic: rw [Preadditive.sub_comp, ← whiskerRight_comp, ih,
      Functor.whiskerRight_zero, sub_zero, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Category.ContinuousCohomology.Basic (goal)
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : Group G
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
n : ℕ
⊢ Eq (α :=
    Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G) (functor.{u_1, u_2, u_3} R G n)
      (functor.{u_1, u_2, u_3} R G (n + 1 + 1)))
    (d R G n ≫ d R G (n + 1)) 0
have zero : Eq (α :=
  Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G) (functor.{u_1, u_2, u_3} R G 0)
    (functor.{u_1, u_2, u_3} R G (HAdd.hAdd (α := ℕ) 0 1 + 1)))
  (d R G 0 ≫ d R G (HAdd.hAdd (α := ℕ) 0 1)) 0
Tactic: induction n with
  | zero =>
    rw [d_succ, Preadditive.comp_sub, sub_eq_zero]
    rfl
  | succ n ih =>
    rw [d_succ R G (n + 1), Preadditive.comp_sub]
    nth_rw 2 [d_succ]
    rw [Preadditive.sub_comp, ← whiskerRight_comp, ih,
      Functor.whiskerRight_zero, sub_zero, sub_eq_zero]
    rfl
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Category.ContinuousCohomology.Basic (goal)
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : Group G
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
n : ℕ
zero :
  Eq (α :=
    Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G) (functor.{u_1, u_2, u_3} R G 0)
      (functor.{u_1, u_2, u_3} R G (HAdd.hAdd (α := ℕ) 0 1 + 1)))
    (d R G 0 ≫ d R G (HAdd.hAdd (α := ℕ) 0 1)) 0
⊢ Eq (α :=
    Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G) (functor.{u_1, u_2, u_3} R G n)
      (functor.{u_1, u_2, u_3} R G (n + 1 + 1)))
    (d R G n ≫ d R G (n + 1)) 0
have succ : ∀ (n : ℕ)
  (ih :
    Eq (α :=
      Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G) (functor.{u_1, u_2, u_3} R G n)
        (functor.{u_1, u_2, u_3} R G (n + 1 + 1)))
      (d R G n ≫ d R G (n + 1)) 0),
  Eq (α :=
    Quiver.Hom (V := Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G) (functor.{u_1, u_2, u_3} R G (n + 1))
      (functor.{u_1, u_2, u_3} R G (n + 1 + 1 + 1)))
    (d R G (n + 1) ≫ d R G (n + 1 + 1)) 0
Tactic: induction n with
  | zero =>
    rw [d_succ, Preadditive.comp_sub, sub_eq_zero]
    rfl
  | succ n ih =>
    rw [d_succ R G (n + 1), Preadditive.comp_sub]
    nth_rw 2 [d_succ]
    rw [Preadditive.sub_comp, ← whiskerRight_comp, ih,
      Functor.whiskerRight_zero, sub_zero, sub_eq_zero]
    rfl
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Category.FGModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
V W : Type v
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
inst_4 : AddCommGroup W
inst_5 : Module R W
inst_6 : Module.Finite R W
e : V ≃ₗ[R] W
⊢ Eq (α := Quiver.Hom (V := FGModuleCat.{v, u} R) (of R V) (of R V))
    (CategoryStruct.comp (Y := of R W)
      (ConcreteCategory.ofHom (FC :=
        fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
        fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e : V →ₗ[R] W))
      (ConcreteCategory.ofHom (FC :=
        fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
        fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e.symm : W →ₗ[R] V)))
    (𝟙 (of R V))
have h : ∀ (x : (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R V)) : Type v)),
  Eq (α := (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R V)) : Type v))
    ((ModuleCat.Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := of R W)
                (ConcreteCategory.ofHom (FC :=
                  fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e : V →ₗ[R] W))
                (ConcreteCategory.ofHom (FC :=
                  fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e.symm : W →ₗ[R] V)))) :
          (a : (↑(of R V).obj : Type v)) → (↑(of R V).obj : Type v))
        x :
      (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R V)) : Type v))
    ((ModuleCat.Hom.hom (InducedCategory.Hom.hom (𝟙 (of R V))) :
          (a : (↑(of R V).obj : Type v)) → (↑(of R V).obj : Type v))
        x :
      (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R V)) : Type v))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.FGModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
V W : Type v
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
inst_4 : AddCommGroup W
inst_5 : Module R W
inst_6 : Module.Finite R W
e : V ≃ₗ[R] W
⊢ Eq (α := Quiver.Hom (V := FGModuleCat.{v, u} R) (of R W) (of R W))
    (CategoryStruct.comp (Y := of R V)
      (ConcreteCategory.ofHom (FC :=
        fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
        fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e.symm : W →ₗ[R] V))
      (ConcreteCategory.ofHom (FC :=
        fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
        fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
        (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e : V →ₗ[R] W)))
    (𝟙 (of R W))
have h : ∀ (x : (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R W)) : Type v)),
  Eq (α := (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R W)) : Type v))
    ((ModuleCat.Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := of R V)
                (ConcreteCategory.ofHom (FC :=
                  fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e.symm : W →ₗ[R] V))
                (ConcreteCategory.ofHom (FC :=
                  fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type v)) (CC :=
                  fun (X : ObjectProperty.FullSubcategory (C := ModuleCat.{v, u} R) (ModuleCat.isFG R)) ↦
                  (↑(X.obj (P := ModuleCat.isFG R)) : Type v)) (↑e : V →ₗ[R] W)))) :
          (a : (↑(of R W).obj : Type v)) → (↑(of R W).obj : Type v))
        x :
      (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R W)) : Type v))
    ((ModuleCat.Hom.hom (InducedCategory.Hom.hom (𝟙 (of R W))) :
          (a : (↑(of R W).obj : Type v)) → (↑(of R W).obj : Type v))
        x :
      (↑(ObjectProperty.FullSubcategory.obj (P := ModuleCat.isFG R) (of R W)) : Type v))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.FGModuleCat.Basic (goal)
Goal:
K : Type u
inst : Field K
V : FGModuleCat K
⊢ FGModuleCatDual K V ◁ FGModuleCatCoevaluation K V ≫
      Iso.inv (α_ (FGModuleCatDual K V) V (FGModuleCatDual K V)) ≫ FGModuleCatEvaluation K V ▷ FGModuleCatDual K V =
    Iso.hom (ρ_ (FGModuleCatDual K V)) ≫ Iso.inv (λ_ (FGModuleCatDual K V))
have h : ModuleCat.Hom.hom
    (FGModuleCatDual K V ◁ FGModuleCatCoevaluation K V ≫
        Iso.inv (α_ (FGModuleCatDual K V) V (FGModuleCatDual K V)) ≫
          FGModuleCatEvaluation K V ▷ FGModuleCatDual K V).hom =
  ModuleCat.Hom.hom (InducedCategory.Hom.hom (Iso.hom (ρ_ (FGModuleCatDual K V)) ≫ Iso.inv (λ_ (FGModuleCatDual K V))))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.FGModuleCat.Basic (goal)
Goal:
K : Type u
inst : Field K
V : FGModuleCat K
⊢ FGModuleCatCoevaluation K V ▷ V ≫ Iso.hom (α_ V (FGModuleCatDual K V) V) ≫ V ◁ FGModuleCatEvaluation K V =
    Iso.hom (λ_ V) ≫ Iso.inv (ρ_ V)
have h : ModuleCat.Hom.hom
    (FGModuleCatCoevaluation K V ▷ V ≫ Iso.hom (α_ V (FGModuleCatDual K V) V) ≫ V ◁ FGModuleCatEvaluation K V).hom =
  ModuleCat.Hom.hom (InducedCategory.Hom.hom (Iso.hom (λ_ V) ≫ Iso.inv (ρ_ V)))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.AB (hypothesis)
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS : S.Exact
⊢ ShortComplex.Exact (S.map colim)
have hS₁ : ∀ (j : J), ShortComplex.Exact (S.map (Functor.obj (evaluation J AddCommGrpCat) j))
Tactic: replace hS := fun j => hS.map ((evaluation _ _).obj j)
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.AB (goal)
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS : ∀ (j : J), ShortComplex.Exact (S.map (Functor.obj (evaluation J AddCommGrpCat) j))
⊢ ShortComplex.Exact (S.map colim)
have simp : ∀
  (hS :
    ∀ (j : J),
      LE.le (α := AddSubgroup (↑(ShortComplex.X₂ (S.map (Functor.obj (evaluation J AddCommGrpCat) j))) : Type u))
        (AddMonoidHom.ker (AddCommGrpCat.Hom.hom (ShortComplex.g (S.map (Functor.obj (evaluation J AddCommGrpCat) j)))))
        (AddMonoidHom.range
          (AddCommGrpCat.Hom.hom (ShortComplex.f (S.map (Functor.obj (evaluation J AddCommGrpCat) j)))))),
  LE.le (α := AddSubgroup (↑(ShortComplex.X₂ (S.map colim)) : Type u))
    (AddMonoidHom.ker (AddCommGrpCat.Hom.hom (ShortComplex.g (S.map colim))))
    (AddMonoidHom.range (AddCommGrpCat.Hom.hom (ShortComplex.f (S.map colim))))
Tactic: simp only [ShortComplex.ab_exact_iff_ker_le_range] at hS ⊢
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.AB (goal)
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    LE.le (α := AddSubgroup (↑(ShortComplex.X₂ (S.map (Functor.obj (evaluation J AddCommGrpCat) j))) : Type u))
      (AddMonoidHom.ker (AddCommGrpCat.Hom.hom (ShortComplex.g (S.map (Functor.obj (evaluation J AddCommGrpCat) j)))))
      (AddMonoidHom.range (AddCommGrpCat.Hom.hom (ShortComplex.f (S.map (Functor.obj (evaluation J AddCommGrpCat) j)))))
x : (↑(ShortComplex.X₂ (S.map colim)) : Type u)
⊢ Membership.mem (γ := AddSubgroup (↑(ShortComplex.X₂ (S.map colim)) : Type u))
      (AddMonoidHom.ker (AddCommGrpCat.Hom.hom (ShortComplex.g (S.map colim)))) x →
    Membership.mem (γ := AddSubgroup (↑(ShortComplex.X₂ (S.map colim)) : Type u))
      (AddMonoidHom.range (AddCommGrpCat.Hom.hom (ShortComplex.f (S.map colim)))) x
have _ : ∀
  (hx :
    Eq (α := (↑(ShortComplex.X₃ (S.map colim)) : Type u))
      ((AddCommGrpCat.Hom.hom (ShortComplex.g (S.map colim)) :
            (a : (↑(S.map colim).X₂ : Type u)) → (↑(S.map colim).X₃ : Type u))
          x :
        (↑(ShortComplex.X₃ (S.map colim)) : Type u))
      (0 : (↑(ShortComplex.X₃ (S.map colim)) : Type u))),
  Membership.mem (γ := AddSubgroup (↑(ShortComplex.X₂ (S.map colim)) : Type u))
    (AddMonoidHom.range (AddCommGrpCat.Hom.hom (ShortComplex.f (S.map colim)))) x
Tactic: (hx : _ = _)
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.AB (goal)
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    LE.le (α := AddSubgroup (↑(ShortComplex.X₂ (S.map (Functor.obj (evaluation J AddCommGrpCat) j))) : Type u))
      (AddMonoidHom.ker (AddCommGrpCat.Hom.hom (ShortComplex.g (S.map (Functor.obj (evaluation J AddCommGrpCat) j)))))
      (AddMonoidHom.range (AddCommGrpCat.Hom.hom (ShortComplex.f (S.map (Functor.obj (evaluation J AddCommGrpCat) j)))))
x : (↑(ShortComplex.X₂ (S.map colim)) : Type u)
hx :
  Eq (α := (↑(colimit S.X₃) : Type u))
    ((AddCommGrpCat.Hom.hom (colimMap S.g) : (a : (↑(colimit S.X₂) : Type u)) → (↑(colimit S.X₃) : Type u)) x :
      (↑(colimit S.X₃) : Type u))
    (0 : (↑(ShortComplex.X₃ (S.map colim)) : Type u))
⊢ Membership.mem (γ := AddSubgroup (↑(ShortComplex.X₂ (S.map colim)) : Type u))
    (AddMonoidHom.range (AddCommGrpCat.Hom.hom (ShortComplex.f (S.map colim)))) x
have rcases : ∀ (j : J)
  (y :
    ToType (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)
      (S.X₂.obj j))
  (hx :
    Eq (α := (↑(colimit S.X₃) : Type u))
      ((AddCommGrpCat.Hom.hom (colimMap S.g) : (a : (↑(colimit S.X₂) : Type u)) → (↑(colimit S.X₃) : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier) (Y := colimit S.X₂) (colimit.ι S.X₂ j) :
                (a : (↑(S.X₂.obj j) : Type u)) → (↑(colimit S.X₂) : Type u))
              y :
            (↑(colimit S.X₂) : Type u)) :
        (↑(colimit S.X₃) : Type u))
      (0 : (↑(ShortComplex.X₃ (S.map colim)) : Type u))),
  Membership.mem (α := (↑(ShortComplex.X₂ (S.map colim)) : Type u)) (γ :=
    AddSubgroup (↑(ShortComplex.X₂ (S.map colim)) : Type u))
    (AddMonoidHom.range (AddCommGrpCat.Hom.hom (ShortComplex.f (S.map colim))))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (Y := colimit S.X₂) (colimit.ι S.X₂ j) :
          (a : (↑(S.X₂.obj j) : Type u)) → (↑(colimit S.X₂) : Type u))
        y :
      (↑(colimit S.X₂) : Type u))
Tactic: rcases Concrete.colimit_exists_rep S.X₂ x with ⟨j, y, rfl⟩
Cleared hypotheses: x, hx