awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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 x_1 : ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type u_3)
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))
    ((HAdd.hAdd (α := 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.comp (↑(Homeomorph.mulLeft g⁻¹) : C(G, G))))
            (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:
simp
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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)
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))
⊢ 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))))

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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)
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:
simp
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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
f : (↑(Iobj rep).V.toModuleCat : Type (max u_2 u_3))
x : G
⊢ Eq.{u_3 + 1} (α := (↑rep.V.toModuleCat : Type u_3))
    ((((TopModuleCat.Hom.hom (((Iobj rep).ρ : (a : G) → End (Iobj rep).V) g) :
                (a : (↑(Iobj rep).V.toModuleCat : Type (max u_2 u_3))) →
                  (↑(Iobj rep).V.toModuleCat : Type (max u_2 u_3)))
              f :
            (↑(Iobj rep).V.toModuleCat : Type (max u_2 u_3))) :
          (a : G) → (↑rep.V.toModuleCat : Type u_3))
        x :
      (↑rep.V.toModuleCat : Type u_3))
    ((TopModuleCat.Hom.hom ((rep.ρ : (a : G) → End rep.V) g) :
          (a : (↑rep.V.toModuleCat : Type u_3)) → (↑rep.V.toModuleCat : Type u_3))
        ((f : (a : G) → (↑rep.V.toModuleCat : Type u_3)) (g⁻¹ * x) : (↑rep.V.toModuleCat : Type u_3)) :
      (↑rep.V.toModuleCat : Type u_3))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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
h 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))
⊢ 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))

Tactic:
rw [φ.comm]

Premises used: Action.Hom.comm
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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 : ℕ
⊢ 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)

Tactic:
exact whiskerRight (d n) (I R G)

Premises used: ContinuousCohomology.I, CategoryTheory.Functor.whiskerRight
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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)))
    (d R G 0) (const.{u_1, u_2, u_3} R G)

Tactic:
rfl

Premises used: ContinuousCohomology.MultiInd.d, rfl
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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 : ℕ
⊢ 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)

Tactic:
exact whiskerRight (d R G n) (I R G)

Premises used: ContinuousCohomology.I, ContinuousCohomology.MultiInd.d, CategoryTheory.Functor.whiskerRight
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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 : ℕ
⊢ d R G (n + 1) =
    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))

Tactic:
rfl

Premises used: ContinuousCohomology.MultiInd.d, rfl
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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
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))
⊢ 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:
rw [d_succ, Preadditive.comp_sub, sub_eq_zero]

Premises used: sub_eq_zero, CategoryTheory.Preadditive.comp_sub, ContinuousCohomology.MultiInd.d_succ
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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 ≫ 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:
rfl
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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
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
⊢ 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:
rw [d_succ R G (n + 1), Preadditive.comp_sub]

Premises used: HAdd.hAdd, OfNat.ofNat, CategoryTheory.Preadditive.comp_sub, ContinuousCohomology.MultiInd.d_succ
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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
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
⊢ 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:
nth_rw 2 [d_succ]

Premises used: ContinuousCohomology.MultiInd.d_succ
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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
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))
⊢ 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:
rw [Preadditive.sub_comp, ← whiskerRight_comp, ih,
      Functor.whiskerRight_zero, sub_zero, sub_eq_zero]

Premises used: sub_eq_zero, sub_zero, CategoryTheory.Functor.whiskerRight_zero, CategoryTheory.Functor.whiskerRight_comp, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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) ≫ 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:
rfl
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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
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
⊢ 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

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

Premises used: sub_eq_zero, sub_zero, CategoryTheory.Functor.whiskerRight_zero, HAdd.hAdd, CategoryTheory.Functor.whiskerRight_comp, OfNat.ofNat, CategoryTheory.Preadditive.comp_sub, ContinuousCohomology.MultiInd.d_succ, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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 : Action (TopModuleCat.{u_3, u_1} R) G
a b : (↑M.V.toModuleCat : Type u_3)
hx :
  Membership.mem (γ := Set (↑M.V.toModuleCat : Type u_3))
    {x : (↑M.V.toModuleCat : Type u_3) |
      ∀ (g : G),
        (TopModuleCat.Hom.hom ((M.ρ : (a : G) → End M.V) g) :
              (a : (↑M.V.toModuleCat : Type u_3)) → (↑M.V.toModuleCat : Type u_3))
            x =
          x}
    a
hy :
  Membership.mem (γ := Set (↑M.V.toModuleCat : Type u_3))
    {x : (↑M.V.toModuleCat : Type u_3) |
      ∀ (g : G),
        (TopModuleCat.Hom.hom ((M.ρ : (a : G) → End M.V) g) :
              (a : (↑M.V.toModuleCat : Type u_3)) → (↑M.V.toModuleCat : Type u_3))
            x =
          x}
    b
g : G
⊢ (TopModuleCat.Hom.hom ((M.ρ : (a : G) → End M.V) g) :
        (a : (↑M.V.toModuleCat : Type u_3)) → (↑M.V.toModuleCat : Type u_3))
      (a + b) =
    a + b

Tactic:
simp [hx g, hy g]
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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 : Action (TopModuleCat.{u_3, u_1} R) G
⊢ Membership.mem (γ := Set (↑M.V.toModuleCat : Type u_3))
    {x : (↑M.V.toModuleCat : Type u_3) |
      ∀ (g : G),
        (TopModuleCat.Hom.hom ((M.ρ : (a : G) → End M.V) g) :
              (a : (↑M.V.toModuleCat : Type u_3)) → (↑M.V.toModuleCat : Type u_3))
            x =
          x}
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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 : Action (TopModuleCat.{u_3, u_1} R) G
r : R
x : (↑M.V.toModuleCat : Type u_3)
hx :
  Membership.mem (γ := Set (↑M.V.toModuleCat : Type u_3))
    {x : (↑M.V.toModuleCat : Type u_3) |
      ∀ (g : G),
        (TopModuleCat.Hom.hom ((M.ρ : (a : G) → End M.V) g) :
              (a : (↑M.V.toModuleCat : Type u_3)) → (↑M.V.toModuleCat : Type u_3))
            x =
          x}
    x
g : G
⊢ (TopModuleCat.Hom.hom ((M.ρ : (a : G) → End M.V) g) :
        (a : (↑M.V.toModuleCat : Type u_3)) → (↑M.V.toModuleCat : Type u_3))
      (r • x) =
    r • x

Tactic:
simp [hx g]
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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
X : Action (TopModuleCat R) G
⊢ (HomologicalComplex.sc (obj (homogeneousCochains.{u_1, u_2, u_3} R G) X) 0).f = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
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
X : Action (TopModuleCat R) G
⊢ (ComplexShape.up ℕ).next 0 = 1

Tactic:
simp