awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.CommAlgCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
A B C D T : CommAlgCat R
f : A ⟶ T
g : B ⟶ T
⊢ (A.binaryCofan B).inr ≫
      (fun {T : CommAlgCat R} (f : A ⟶ T) (g : B ⟶ T) ↦
          (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯) :
            Quiver.Hom (V := CommAlgCat R) (of R ((↑A : Type u) ⊗[R] (↑B : Type u))) (of R (↑T : Type u))))
        f g =
    g
have hf : Hom.hom
    ((A.binaryCofan B).inr ≫
      (fun {T : CommAlgCat R} (f : A ⟶ T) (g : B ⟶ T) ↦
          (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) sorry) :
            Quiver.Hom (V := CommAlgCat R) (of R ((↑A : Type u) ⊗[R] (↑B : Type u))) (of R (↑T : Type u))))
        f g) =
  Hom.hom g
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.CommAlgCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
A B C D T : CommAlgCat R
f : A ⟶ T
g : B ⟶ T
m : (A.binaryCofan B).pt ⟶ T
hm₁ : (A.binaryCofan B).inl ≫ m = f
hm₂ : (A.binaryCofan B).inr ≫ m = g
⊢ m =
    (fun {T : CommAlgCat R} (f : A ⟶ T) (g : B ⟶ T) ↦
        (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯) :
          Quiver.Hom (V := CommAlgCat R) (of R ((↑A : Type u) ⊗[R] (↑B : Type u))) (of R (↑T : Type u))))
      f g
have hf : Hom.hom m =
  Hom.hom
    ((fun {T : CommAlgCat R} (f : A ⟶ T) (g : B ⟶ T) ↦
        (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) sorry) :
          Quiver.Hom (V := CommAlgCat R) (of R ((↑A : Type u) ⊗[R] (↑B : Type u))) (of R (↑T : Type u))))
      f g)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.CommAlgCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
A B C D T : CommAlgCat R
f : A ⟶ T
g : B ⟶ T
m : (A.binaryCofan B).pt ⟶ T
hm₁ : (A.binaryCofan B).inl ≫ m = f
hm₂ : (A.binaryCofan B).inr ≫ m = g
⊢ Hom.hom m =
    Hom.hom
      ((fun {T : CommAlgCat R} (f : A ⟶ T) (g : B ⟶ T) ↦
          (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯) :
            Quiver.Hom (V := CommAlgCat R) (of R ((↑A : Type u) ⊗[R] (↑B : Type u))) (of R (↑T : Type u))))
        f g)
have hf : Eq (α :=
  { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
    ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
      Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
        ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)) })
  (((Equiv.symm Algebra.TensorProduct.liftEquiv :
          ((↑A : Type u) ⊗[R] (↑B : Type u) →ₐ[R] (↑T : Type u)) ≃
            { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
              ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
                Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
                  ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)) }) :
        (a : (↑A : Type u) ⊗[R] (↑B : Type u) →ₐ[R] (↑T : Type u)) →
          { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
            ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
              Commute ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x)
                ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y) })
      (Hom.hom m) :
    { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
      ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
        Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
          ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)) })
  (Subtype.mk (p := fun (fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u))) ↦
      ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
        Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
          ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)))
      (ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier) f,
        ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier) g)
      sorry :
    { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
      ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
        Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
          ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)) })
Tactic: refine liftEquiv.symm_apply_eq (y := ⟨⟨_, _⟩, fun _ _ ↦ .all _ _⟩).mp ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.CommAlgCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
A B C D : CommAlgCat R
S T : (CommAlgCat R)ᵒᵖ
⊢ Quiver.Hom.op (BinaryCofan.inl ((unop S).binaryCofan (unop T))) =
    S ◁ IsTerminal.from (terminalOpOfInitial isInitialSelf) T ≫ Iso.hom (ρ_ S)
have a : ∀
  (x :
    (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.left : Discrete WalkingPair }))) : Type u)),
  Eq (α :=
    (↑(unop
          (op
            (Functor.obj
              (Functor.obj (Functor.const (Discrete WalkingPair))
                (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
              { as := WalkingPair.left : Discrete WalkingPair }))) :
      Type u))
    ((Hom.hom (Quiver.Hom.unop (Quiver.Hom.op (BinaryCofan.inl ((unop S).binaryCofan (unop T))))) :
          (a : (↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.left }))) : Type u)) →
            (↑(unop
                  (op
                    (((Functor.const (Discrete WalkingPair)).obj ((unop S).binaryCofan (unop T)).pt).obj
                      { as := WalkingPair.left }))) :
              Type u))
        x :
      (↑(unop
            (op
              (Functor.obj
                (Functor.obj (Functor.const (Discrete WalkingPair))
                  (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
                { as := WalkingPair.left : Discrete WalkingPair }))) :
        Type u))
    ((Hom.hom (S ◁ IsTerminal.from (terminalOpOfInitial isInitialSelf) T ≫ Iso.hom (ρ_ S)).unop :
          (a : (↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.left }))) : Type u)) →
            (↑(unop
                  (op
                    (((Functor.const (Discrete WalkingPair)).obj ((unop S).binaryCofan (unop T)).pt).obj
                      { as := WalkingPair.left }))) :
              Type u))
        x :
      (↑(unop
            (op
              (Functor.obj
                (Functor.obj (Functor.const (Discrete WalkingPair))
                  (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
                { as := WalkingPair.left : Discrete WalkingPair }))) :
        Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.CommAlgCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
A B C D : CommAlgCat R
S T : (CommAlgCat R)ᵒᵖ
x : (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.left : Discrete WalkingPair }))) : Type u)
⊢ Eq (α :=
    (↑(unop
          (op
            (Functor.obj
              (Functor.obj (Functor.const (Discrete WalkingPair))
                (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
              { as := WalkingPair.left : Discrete WalkingPair }))) :
      Type u))
    ((Hom.hom (Quiver.Hom.unop (Quiver.Hom.op (BinaryCofan.inl ((unop S).binaryCofan (unop T))))) :
          (a : (↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.left }))) : Type u)) →
            (↑(unop
                  (op
                    (((Functor.const (Discrete WalkingPair)).obj ((unop S).binaryCofan (unop T)).pt).obj
                      { as := WalkingPair.left }))) :
              Type u))
        x :
      (↑(unop
            (op
              (Functor.obj
                (Functor.obj (Functor.const (Discrete WalkingPair))
                  (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
                { as := WalkingPair.left : Discrete WalkingPair }))) :
        Type u))
    ((Hom.hom (S ◁ IsTerminal.from (terminalOpOfInitial isInitialSelf) T ≫ Iso.hom (ρ_ S)).unop :
          (a : (↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.left }))) : Type u)) →
            (↑(unop
                  (op
                    (((Functor.const (Discrete WalkingPair)).obj ((unop S).binaryCofan (unop T)).pt).obj
                      { as := WalkingPair.left }))) :
              Type u))
        x :
      (↑(unop
            (op
              (Functor.obj
                (Functor.obj (Functor.const (Discrete WalkingPair))
                  (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
                { as := WalkingPair.left : Discrete WalkingPair }))) :
        Type u))
have a : Eq (α :=
  (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.left : Discrete WalkingPair }))) : Type u) ⊗[R]
    (↑(unop T) : Type u))
  (x ⊗ₜ[R] 1 :
    (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.left : Discrete WalkingPair }))) :
        Type u) ⊗[R]
      (↑(unop T) : Type u))
  (x ⊗ₜ[R] (algebraMap R (↑(unop T) : Type u) : (a : R) → (↑(unop T) : Type u)) 1 :
    (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.left : Discrete WalkingPair }))) :
        Type u) ⊗[R]
      (↑(unop T) : Type u))
Tactic: change x ⊗ₜ 1 = x ⊗ₜ algebraMap R T.unop 1
-- Lean 4 proof step from Mathlib.Algebra.Category.CommAlgCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
A B C D : CommAlgCat R
S T : (CommAlgCat R)ᵒᵖ
⊢ Quiver.Hom.op (BinaryCofan.inr ((unop S).binaryCofan (unop T))) =
    IsTerminal.from (terminalOpOfInitial isInitialSelf) S ▷ T ≫ Iso.hom (λ_ T)
have a : ∀
  (x :
    (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.right : Discrete WalkingPair }))) : Type u)),
  Eq (α :=
    (↑(unop
          (op
            (Functor.obj
              (Functor.obj (Functor.const (Discrete WalkingPair))
                (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
              { as := WalkingPair.right : Discrete WalkingPair }))) :
      Type u))
    ((Hom.hom (Quiver.Hom.unop (Quiver.Hom.op (BinaryCofan.inr ((unop S).binaryCofan (unop T))))) :
          (a : (↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.right }))) : Type u)) →
            (↑(unop
                  (op
                    (((Functor.const (Discrete WalkingPair)).obj ((unop S).binaryCofan (unop T)).pt).obj
                      { as := WalkingPair.right }))) :
              Type u))
        x :
      (↑(unop
            (op
              (Functor.obj
                (Functor.obj (Functor.const (Discrete WalkingPair))
                  (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
                { as := WalkingPair.right : Discrete WalkingPair }))) :
        Type u))
    ((Hom.hom (IsTerminal.from (terminalOpOfInitial isInitialSelf) S ▷ T ≫ Iso.hom (λ_ T)).unop :
          (a : (↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.right }))) : Type u)) →
            (↑(unop
                  (op
                    (((Functor.const (Discrete WalkingPair)).obj ((unop S).binaryCofan (unop T)).pt).obj
                      { as := WalkingPair.right }))) :
              Type u))
        x :
      (↑(unop
            (op
              (Functor.obj
                (Functor.obj (Functor.const (Discrete WalkingPair))
                  (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
                { as := WalkingPair.right : Discrete WalkingPair }))) :
        Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.CommAlgCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
A B C D : CommAlgCat R
S T : (CommAlgCat R)ᵒᵖ
x : (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.right : Discrete WalkingPair }))) : Type u)
⊢ Eq (α :=
    (↑(unop
          (op
            (Functor.obj
              (Functor.obj (Functor.const (Discrete WalkingPair))
                (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
              { as := WalkingPair.right : Discrete WalkingPair }))) :
      Type u))
    ((Hom.hom (Quiver.Hom.unop (Quiver.Hom.op (BinaryCofan.inr ((unop S).binaryCofan (unop T))))) :
          (a : (↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.right }))) : Type u)) →
            (↑(unop
                  (op
                    (((Functor.const (Discrete WalkingPair)).obj ((unop S).binaryCofan (unop T)).pt).obj
                      { as := WalkingPair.right }))) :
              Type u))
        x :
      (↑(unop
            (op
              (Functor.obj
                (Functor.obj (Functor.const (Discrete WalkingPair))
                  (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
                { as := WalkingPair.right : Discrete WalkingPair }))) :
        Type u))
    ((Hom.hom (IsTerminal.from (terminalOpOfInitial isInitialSelf) S ▷ T ≫ Iso.hom (λ_ T)).unop :
          (a : (↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.right }))) : Type u)) →
            (↑(unop
                  (op
                    (((Functor.const (Discrete WalkingPair)).obj ((unop S).binaryCofan (unop T)).pt).obj
                      { as := WalkingPair.right }))) :
              Type u))
        x :
      (↑(unop
            (op
              (Functor.obj
                (Functor.obj (Functor.const (Discrete WalkingPair))
                  (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
                { as := WalkingPair.right : Discrete WalkingPair }))) :
        Type u))
have a : Eq (α :=
  (↑(unop S) : Type u) ⊗[R]
    (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.right : Discrete WalkingPair }))) : Type u))
  (1 ⊗ₜ[R] x :
    (↑(unop S) : Type u) ⊗[R]
      (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.right : Discrete WalkingPair }))) : Type u))
  ((algebraMap R (↑(unop S) : Type u) : (a : R) → (↑(unop S) : Type u)) 1 ⊗ₜ[R] x :
    (↑(unop S) : Type u) ⊗[R]
      (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.right : Discrete WalkingPair }))) : Type u))
Tactic: change 1 ⊗ₜ x = algebraMap R S.unop 1 ⊗ₜ x
-- Lean 4 proof step from Mathlib.Algebra.Category.CommBialgCat (goal)
Goal:
R : Type u
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Bialgebra R A
⊢ Eq (α :=
    Quiver.Hom (V := (CommAlgCat R)ᵒᵖ)
      (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite))
        (op (of R A)))
      (op (of R A)))
    (Quiver.Hom.op (ofHom (counitAlgHom R A)) ▷ op (of R A) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))
    (Iso.hom (λ_ (op (of R A))))
have a : ∀ (x : (↑(unop (op (of R A))) : Type u)),
  Eq (α :=
    (↑(unop
          (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite))
            (op (of R A)))) :
      Type u))
    ((Hom.hom
            (Quiver.Hom.unop
              (Quiver.Hom.op (ofHom (counitAlgHom R A)) ▷ op (of R A) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))) :
          (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop (𝟙_ (CommAlgCat R)ᵒᵖ ⊗ op (of R A))) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite))
              (op (of R A)))) :
        Type u))
    ((Hom.hom (Quiver.Hom.unop (Iso.hom (λ_ (op (of R A))))) :
          (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop (𝟙_ (CommAlgCat R)ᵒᵖ ⊗ op (of R A))) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite))
              (op (of R A)))) :
        Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.CommBialgCat (goal)
Goal:
R : Type u
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Bialgebra R A
⊢ Eq (α :=
    Quiver.Hom (V := (CommAlgCat R)ᵒᵖ)
      (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A))
        ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite)))
      (op (of R A)))
    (op (of R A) ◁ Quiver.Hom.op (ofHom (counitAlgHom R A)) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))
    (Iso.hom (ρ_ (op (of R A))))
have a : ∀ (x : (↑(unop (op (of R A))) : Type u)),
  Eq (α :=
    (↑(unop
          (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A))
            ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite)))) :
      Type u))
    ((Hom.hom
            (Quiver.Hom.unop
              (op (of R A) ◁ Quiver.Hom.op (ofHom (counitAlgHom R A)) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))) :
          (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop (op (of R A) ⊗ 𝟙_ (CommAlgCat R)ᵒᵖ)) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A))
              ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite)))) :
        Type u))
    ((Hom.hom (Quiver.Hom.unop (Iso.hom (ρ_ (op (of R A))))) :
          (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop (op (of R A) ⊗ 𝟙_ (CommAlgCat R)ᵒᵖ)) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A))
              ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite)))) :
        Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.CommBialgCat (goal)
Goal:
R : Type u
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Bialgebra R A
⊢ Eq (α :=
    Quiver.Hom (V := (CommAlgCat R)ᵒᵖ)
      (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite)
        (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A)) (op (of R A))) (op (of R A)))
      (op (of R A)))
    (Quiver.Hom.op (ofHom (comulAlgHom R A)) ▷ op (of R A) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))
    (Iso.hom (α_ (op (of R A)) (op (of R A)) (op (of R A))) ≫
      op (of R A) ◁ Quiver.Hom.op (ofHom (comulAlgHom R A)) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))
have a : ∀ (x : (↑(unop (op (of R A))) : Type u)),
  Eq (α :=
    (↑(unop
          (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite)
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A)) (op (of R A))) (op (of R A)))) :
      Type u))
    ((Hom.hom
            (Quiver.Hom.unop
              (Quiver.Hom.op (ofHom (comulAlgHom R A)) ▷ op (of R A) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))) :
          (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop ((op (of R A) ⊗ op (of R A)) ⊗ op (of R A))) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite)
              (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A)) (op (of R A))) (op (of R A)))) :
        Type u))
    ((Hom.hom
            (Quiver.Hom.unop
              (Iso.hom (α_ (op (of R A)) (op (of R A)) (op (of R A))) ≫
                op (of R A) ◁ Quiver.Hom.op (ofHom (comulAlgHom R A)) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))) :
          (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop ((op (of R A) ⊗ op (of R A)) ⊗ op (of R A))) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite)
              (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A)) (op (of R A))) (op (of R A)))) :
        Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.CommBialgCat (goal)
Goal:
R : Type u
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Bialgebra R A
inst_3 : IsCocomm R A
⊢ Eq (α :=
    Quiver.Hom (V := (CommAlgCat R)ᵒᵖ)
      (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (CommAlgCat.of R A)) (op (CommAlgCat.of R A)))
      (op (CommAlgCat.of R A)))
    (Iso.hom (β_ (op (CommAlgCat.of R A)) (op (CommAlgCat.of R A))) ≫ μ) μ
have a : ∀ (x : (↑(unop (op (CommAlgCat.of R A))) : Type u)),
  Eq (α :=
    (↑(unop
          (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (CommAlgCat.of R A))
            (op (CommAlgCat.of R A)))) :
      Type u))
    ((CommAlgCat.Hom.hom (Quiver.Hom.unop (Iso.hom (β_ (op (CommAlgCat.of R A)) (op (CommAlgCat.of R A))) ≫ μ)) :
          (a : (↑(unop (op (CommAlgCat.of R A))) : Type u)) →
            (↑(unop (op (CommAlgCat.of R A) ⊗ op (CommAlgCat.of R A))) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (CommAlgCat.of R A))
              (op (CommAlgCat.of R A)))) :
        Type u))
    ((CommAlgCat.Hom.hom (Quiver.Hom.unop μ) :
          (a : (↑(unop (op (CommAlgCat.of R A))) : Type u)) →
            (↑(unop (op (CommAlgCat.of R A) ⊗ op (CommAlgCat.of R A))) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (CommAlgCat.of R A))
              (op (CommAlgCat.of R A)))) :
        Type u))
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
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)
⊢ 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))) =
    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))))
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))
    ((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: ext