Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
g : A →ₗc[R] B
toFun✝ : A → B
map_add'✝ : ∀ (x y : A), toFun✝ (x + y) = toFun✝ x + toFun✝ y
map_smul'✝ :
  ∀ (m : R) (x : A),
    { toFun := toFun✝, map_add' := map_add'✝ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := toFun✝, map_add' := map_add'✝ }.toFun x
counit_comp✝ : counit ∘ₗ { toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝ } = counit
map_comp_comul✝ :
  map { toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝ }
        { toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝ } ∘ₗ
      comul =
    comul ∘ₗ { toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝ }
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝, counit_comp := counit_comp✝,
        map_comp_comul := map_comp_comul✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝, counit_comp := counit_comp✝,
      map_comp_comul := map_comp_comul✝ } =
    g

Tactic:
rcases g with ⟨⟨⟨_, _⟩, _⟩, _, _⟩

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
toFun✝¹ : A → B
map_add'✝¹ : ∀ (x y : A), toFun✝¹ (x + y) = toFun✝¹ x + toFun✝¹ y
map_smul'✝¹ :
  ∀ (m : R) (x : A),
    { toFun := toFun✝¹, map_add' := map_add'✝¹ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := toFun✝¹, map_add' := map_add'✝¹ }.toFun x
counit_comp✝¹ : counit ∘ₗ { toFun := toFun✝¹, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ } = counit
map_comp_comul✝¹ :
  map { toFun := toFun✝¹, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }
        { toFun := toFun✝¹, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ } ∘ₗ
      comul =
    comul ∘ₗ { toFun := toFun✝¹, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }
toFun✝ : A → B
map_add'✝ : ∀ (x y : A), toFun✝ (x + y) = toFun✝ x + toFun✝ y
map_smul'✝ :
  ∀ (m : R) (x : A),
    { toFun := toFun✝, map_add' := map_add'✝ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := toFun✝, map_add' := map_add'✝ }.toFun x
counit_comp✝ : counit ∘ₗ { toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝ } = counit
map_comp_comul✝ :
  map { toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝ }
        { toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝ } ∘ₗ
      comul =
    comul ∘ₗ { toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝ }
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝¹, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, counit_comp := counit_comp✝¹,
        map_comp_comul := map_comp_comul✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝, counit_comp := counit_comp✝,
        map_comp_comul := map_comp_comul✝ }
⊢ { toFun := toFun✝¹, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, counit_comp := counit_comp✝¹,
      map_comp_comul := map_comp_comul✝¹ } =
    { toFun := toFun✝, map_add' := map_add'✝, map_smul' := map_smul'✝, counit_comp := counit_comp✝,
      map_comp_comul := map_comp_comul✝ }