awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
s : Finset A
hs : (↑s : Set A) ⊆ {a : A | IsGroupLikeElem R a}
⊢ LinearIndepOn R id (↑s : Set A)
have empty : ∀ (hs : (↑∅ : Set A) ⊆ {a : A | IsGroupLikeElem R a}), LinearIndepOn R id (↑∅ : Set A)
Tactic: induction s using Finset.cons_induction with
  -- The case `s = ∅` is trivial.
  | empty => simp
  -- Let's deal with the `s ∪ {a}` case.
  | cons a s has ih =>
  simp only [Finset.cons_eq_insert, Finset.coe_insert, Set.subset_def, Set.mem_insert_iff,
    Finset.mem_coe, Set.mem_setOf_eq, forall_eq_or_imp] at hs
  obtain ⟨ha, hs⟩ := hs
  specialize ih hs
  -- Assume that there is some `c : A → R` and `d : R` such that `∑ x ∈ s, c x • x = d • a`.
  -- We want to prove `d = 0` and `∀ x ∈ s, c x = 0`.
  rw [Finset.coe_cons]
  refine ih.id_insert' ?_
  simp only [mem_span_finset, forall_exists_index, and_imp]
  rintro d c - hc
  -- `x ⊗ y` over `x, y ∈ s` are linearly independent since `s` is linearly independent and
  -- `R` is a domain.
  replace ih := ih.tmul_of_isDomain ih
  simp_rw [← Finset.coe_product, linearIndepOn_finset_iffₛ, id] at ih
  -- Tensoring the equality `∑ x ∈ s, c x • x = d • a` with itself, we get by linear independence
  -- that `c x ^ 2 = d * c x` and `c x * c y = 0` for `x ≠ y`.
  have key := calc
        ∑ x ∈ s, ∑ y ∈ s, (if x = y then d * c x else 0) • x ⊗ₜ[R] y
    _ = d • ∑ x ∈ s, c x • x ⊗ₜ[R] x := by simp [Finset.smul_sum, mul_smul]
    _ = d • comul (d • a) := by rw [← hc]; simp +contextual [(hs _ _).comul_eq_tmul_self]
    _ = (d • a) ⊗ₜ (d • a) := by simp [ha.comul_eq_tmul_self, smul_tmul, tmul_smul, -neg_smul]
    _ = ∑ x ∈ s, ∑ y ∈ s, (c x * c y) • x ⊗ₜ[R] y := by
      simp_rw [← hc, sum_tmul, smul_tmul, Finset.smul_sum, tmul_sum, tmul_smul, mul_smul]
  simp_rw [← Finset.sum_product'] at key
  apply ih at key
  -- Therefore, `c x = 0` for all `x ∈ s`.
  replace key x (hx : x ∈ s) : c x = 0 := by
    -- Otherwise, we deduce from `key` that `c y = 0` for any `y ≠ x` with `y ∈ s`.
    by_contra! hcx
    have hcy (y) (hys : y ∈ s) (hyx : y ≠ x) : c y = 0 := by
      simpa [*] using (key (y, x) (by simp [*])).symm
    -- Then substitute this into `hc` to get `c x • x = d • a`.
    rw [Finset.sum_eq_single x (by simp +contextual [hcy]) (by simp [hx])] at hc
    -- But `key` also says that `c x = d`.
    have hcxa : d = c x := mul_left_injective₀ hcx (by simpa using (key (x, x) (by simp [*])))
    -- So `x = a`...
    obtain rfl : x = a := by rwa [hcxa, smul_right_inj hcx] at hc
    -- ... which contradicts `x ∈ s` and `a ∉ s`.
    contradiction
  -- We are now done, since `d • a = ∑ x ∈ s, c x • x = 0`
  simp_all [ha.ne_zero, eq_comm]
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
s : Finset A
hs : (↑s : Set A) ⊆ {a : A | IsGroupLikeElem R a}
empty : ∀ (hs : (↑∅ : Set A) ⊆ {a : A | IsGroupLikeElem R a}), LinearIndepOn R id (↑∅ : Set A)
⊢ LinearIndepOn R id (↑s : Set A)
have cons : ∀ (a : A) (s : Finset A) (has : a ∉ s)
  (ih : ∀ (hs : (↑s : Set A) ⊆ {a : A | IsGroupLikeElem R a}), LinearIndepOn R id (↑s : Set A))
  (hs : (↑(Finset.cons a s has) : Set A) ⊆ {a : A | IsGroupLikeElem R a}),
  LinearIndepOn R id (↑(Finset.cons a s has) : Set A)
Tactic: induction s using Finset.cons_induction with
  -- The case `s = ∅` is trivial.
  | empty => simp
  -- Let's deal with the `s ∪ {a}` case.
  | cons a s has ih =>
  simp only [Finset.cons_eq_insert, Finset.coe_insert, Set.subset_def, Set.mem_insert_iff,
    Finset.mem_coe, Set.mem_setOf_eq, forall_eq_or_imp] at hs
  obtain ⟨ha, hs⟩ := hs
  specialize ih hs
  -- Assume that there is some `c : A → R` and `d : R` such that `∑ x ∈ s, c x • x = d • a`.
  -- We want to prove `d = 0` and `∀ x ∈ s, c x = 0`.
  rw [Finset.coe_cons]
  refine ih.id_insert' ?_
  simp only [mem_span_finset, forall_exists_index, and_imp]
  rintro d c - hc
  -- `x ⊗ y` over `x, y ∈ s` are linearly independent since `s` is linearly independent and
  -- `R` is a domain.
  replace ih := ih.tmul_of_isDomain ih
  simp_rw [← Finset.coe_product, linearIndepOn_finset_iffₛ, id] at ih
  -- Tensoring the equality `∑ x ∈ s, c x • x = d • a` with itself, we get by linear independence
  -- that `c x ^ 2 = d * c x` and `c x * c y = 0` for `x ≠ y`.
  have key := calc
        ∑ x ∈ s, ∑ y ∈ s, (if x = y then d * c x else 0) • x ⊗ₜ[R] y
    _ = d • ∑ x ∈ s, c x • x ⊗ₜ[R] x := by simp [Finset.smul_sum, mul_smul]
    _ = d • comul (d • a) := by rw [← hc]; simp +contextual [(hs _ _).comul_eq_tmul_self]
    _ = (d • a) ⊗ₜ (d • a) := by simp [ha.comul_eq_tmul_self, smul_tmul, tmul_smul, -neg_smul]
    _ = ∑ x ∈ s, ∑ y ∈ s, (c x * c y) • x ⊗ₜ[R] y := by
      simp_rw [← hc, sum_tmul, smul_tmul, Finset.smul_sum, tmul_sum, tmul_smul, mul_smul]
  simp_rw [← Finset.sum_product'] at key
  apply ih at key
  -- Therefore, `c x = 0` for all `x ∈ s`.
  replace key x (hx : x ∈ s) : c x = 0 := by
    -- Otherwise, we deduce from `key` that `c y = 0` for any `y ≠ x` with `y ∈ s`.
    by_contra! hcx
    have hcy (y) (hys : y ∈ s) (hyx : y ≠ x) : c y = 0 := by
      simpa [*] using (key (y, x) (by simp [*])).symm
    -- Then substitute this into `hc` to get `c x • x = d • a`.
    rw [Finset.sum_eq_single x (by simp +contextual [hcy]) (by simp [hx])] at hc
    -- But `key` also says that `c x = d`.
    have hcxa : d = c x := mul_left_injective₀ hcx (by simpa using (key (x, x) (by simp [*])))
    -- So `x = a`...
    obtain rfl : x = a := by rwa [hcxa, smul_right_inj hcx] at hc
    -- ... which contradicts `x ∈ s` and `a ∉ s`.
    contradiction
  -- We are now done, since `d • a = ∑ x ∈ s, c x • x = 0`
  simp_all [ha.ne_zero, eq_comm]
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
⊢ LinearIndepOn.{u_3, u_2, u_3} (ι := A) R id {a : A | IsGroupLikeElem R a}
have We : ∀ (t : Finset A), (↑t : Set A) ⊆ {a : A | IsGroupLikeElem R a} → LinearIndepOn R id (↑t : Set A)
Tactic: classical
  -- We show that any finset `s` of group-like elements is linearly independent.
  rw [linearIndepOn_iff_linearIndepOn_finset]
  rintro s hs
  -- For this, we do induction on `s`.
  induction s using Finset.cons_induction with
  -- The case `s = ∅` is trivial.
  | empty => simp
  -- Let's deal with the `s ∪ {a}` case.
  | cons a s has ih =>
  simp only [Finset.cons_eq_insert, Finset.coe_insert, Set.subset_def, Set.mem_insert_iff,
    Finset.mem_coe, Set.mem_setOf_eq, forall_eq_or_imp] at hs
  obtain ⟨ha, hs⟩ := hs
  specialize ih hs
  -- Assume that there is some `c : A → R` and `d : R` such that `∑ x ∈ s, c x • x = d • a`.
  -- We want to prove `d = 0` and `∀ x ∈ s, c x = 0`.
  rw [Finset.coe_cons]
  refine ih.id_insert' ?_
  simp only [mem_span_finset, forall_exists_index, and_imp]
  rintro d c - hc
  -- `x ⊗ y` over `x, y ∈ s` are linearly independent since `s` is linearly independent and
  -- `R` is a domain.
  replace ih := ih.tmul_of_isDomain ih
  simp_rw [← Finset.coe_product, linearIndepOn_finset_iffₛ, id] at ih
  -- Tensoring the equality `∑ x ∈ s, c x • x = d • a` with itself, we get by linear independence
  -- that `c x ^ 2 = d * c x` and `c x * c y = 0` for `x ≠ y`.
  have key := calc
        ∑ x ∈ s, ∑ y ∈ s, (if x = y then d * c x else 0) • x ⊗ₜ[R] y
    _ = d • ∑ x ∈ s, c x • x ⊗ₜ[R] x := by simp [Finset.smul_sum, mul_smul]
    _ = d • comul (d • a) := by rw [← hc]; simp +contextual [(hs _ _).comul_eq_tmul_self]
    _ = (d • a) ⊗ₜ (d • a) := by simp [ha.comul_eq_tmul_self, smul_tmul, tmul_smul, -neg_smul]
    _ = ∑ x ∈ s, ∑ y ∈ s, (c x * c y) • x ⊗ₜ[R] y := by
      simp_rw [← hc, sum_tmul, smul_tmul, Finset.smul_sum, tmul_sum, tmul_smul, mul_smul]
  simp_rw [← Finset.sum_product'] at key
  apply ih at key
  -- Therefore, `c x = 0` for all `x ∈ s`.
  replace key x (hx : x ∈ s) : c x = 0 := by
    -- Otherwise, we deduce from `key` that `c y = 0` for any `y ≠ x` with `y ∈ s`.
    by_contra! hcx
    have hcy (y) (hys : y ∈ s) (hyx : y ≠ x) : c y = 0 := by
      simpa [*] using (key (y, x) (by simp [*])).symm
    -- Then substitute this into `hc` to get `c x • x = d • a`.
    rw [Finset.sum_eq_single x (by simp +contextual [hcy]) (by simp [hx])] at hc
    -- But `key` also says that `c x = d`.
    have hcxa : d = c x := mul_left_injective₀ hcx (by simpa using (key (x, x) (by simp [*])))
    -- So `x = a`...
    obtain rfl : x = a := by rwa [hcxa, smul_right_inj hcx] at hc
    -- ... which contradicts `x ∈ s` and `a ∉ s`.
    contradiction
  -- We are now done, since `d • a = ∑ x ∈ s, c x • x = 0`
  simp_all [ha.ne_zero, eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Hom (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : AddCommMonoid D
inst_8 : Module R D
inst_9 : CoalgebraStruct R A
inst_10 : CoalgebraStruct R B
inst_11 : CoalgebraStruct R C
inst_12 : CoalgebraStruct R D
f g : A →ₗc[R] B
h : Eq (α := (a : A) → B) ((fun (f : A →ₗc[R] B) ↦ f.toFun) f) ((fun (f : A →ₗc[R] B) ↦ f.toFun) g)
⊢ f = g
have rcases : ∀ (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' : A →ₙ+ B }.toFun (m • x) =
        HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
          ({ toFun := toFun, map_add' := map_add' : A →ₙ+ B }.toFun x))
  (counit_comp : counit ∘ₗ { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B } = counit)
  (map_comp_comul :
    map { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B }
          { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B } ∘ₗ
        comul =
      comul ∘ₗ { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B })
  (h :
    Eq (α := (a : A) → B)
      ((fun (f : A →ₗc[R] B) ↦ f.toFun)
        { toFun := toFun, map_add' := map_add', map_smul' := map_smul', counit_comp := counit_comp,
          map_comp_comul := map_comp_comul })
      ((fun (f : A →ₗc[R] B) ↦ f.toFun) g)),
  { toFun := toFun, map_add' := map_add', map_smul' := map_smul', counit_comp := counit_comp,
      map_comp_comul := map_comp_comul : A →ₗc[R] B } =
    g
Tactic: rcases f with ⟨⟨⟨_, _⟩, _⟩, _, _⟩
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Hom (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : AddCommMonoid D
inst_8 : Module R D
inst_9 : CoalgebraStruct R A
inst_10 : CoalgebraStruct R B
inst_11 : CoalgebraStruct R C
inst_12 : 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' : A →ₙ+ B }.toFun (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
        ({ toFun := toFun, map_add' := map_add' : A →ₙ+ B }.toFun x)
counit_comp : counit ∘ₗ { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B } = counit
map_comp_comul :
  map { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B }
        { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B } ∘ₗ
      comul =
    comul ∘ₗ { toFun := toFun, map_add' := map_add', map_smul' := map_smul' : A →ₗ[R] B }
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →ₗc[R] B) ↦ f.toFun)
      { toFun := toFun, map_add' := map_add', map_smul' := map_smul', counit_comp := counit_comp,
        map_comp_comul := map_comp_comul })
    ((fun (f : A →ₗc[R] B) ↦ f.toFun) g)
⊢ { toFun := toFun, map_add' := map_add', map_smul' := map_smul', counit_comp := counit_comp,
      map_comp_comul := map_comp_comul : A →ₗc[R] B } =
    g
have rcases : ∀ (toFun_1 : A → B) (map_add'_1 : ∀ (x y : A), toFun_1 (x + y) = toFun_1 x + toFun_1 y)
  (map_smul'_1 :
    ∀ (m : R) (x : A),
      { toFun := toFun_1, map_add' := map_add'_1 : A →ₙ+ B }.toFun (m • x) =
        HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
          ({ toFun := toFun_1, map_add' := map_add'_1 : A →ₙ+ B }.toFun x))
  (counit_comp_1 :
    counit ∘ₗ { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1 : A →ₗ[R] B } = counit)
  (map_comp_comul_1 :
    map { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1 : A →ₗ[R] B }
          { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1 : A →ₗ[R] B } ∘ₗ
        comul =
      comul ∘ₗ { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1 : A →ₗ[R] B })
  (h :
    Eq (α := (a : A) → B)
      ((fun (f : A →ₗc[R] B) ↦ f.toFun)
        { toFun := toFun, map_add' := map_add', map_smul' := map_smul', counit_comp := counit_comp,
          map_comp_comul := map_comp_comul })
      ((fun (f : A →ₗc[R] B) ↦ f.toFun)
        { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1, counit_comp := counit_comp_1,
          map_comp_comul := map_comp_comul_1 })),
  { toFun := toFun, map_add' := map_add', map_smul' := map_smul', counit_comp := counit_comp,
      map_comp_comul := map_comp_comul : A →ₗc[R] B } =
    { toFun := toFun_1, map_add' := map_add'_1, map_smul' := map_smul'_1, counit_comp := counit_comp_1,
      map_comp_comul := map_comp_comul_1 }
Tactic: rcases g with ⟨⟨⟨_, _⟩, _⟩, _, _⟩
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Hom (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : CoalgebraStruct R A
f g : R →ₗc[R] A
h : Eq.{u_2 + 1} (α := A) ((f : (a : R) → A) 1 : A) ((g : (a : R) → A) 1 : A)
⊢ Eq (α := R →ₗ[R] A)
    ((fun (x : R →ₗc[R] A) ↦
        ((↑x : [inst_4 : FunLike (R →ₗc[R] A) R A] → [SemilinearMapClass (R →ₗc[R] A) (RingHom.id R) R A] → R →ₗ[R] A) :
          R →ₗ[R] A))
      f)
    ((fun (x : R →ₗc[R] A) ↦
        ((↑x : [inst_4 : FunLike (R →ₗc[R] A) R A] → [SemilinearMapClass (R →ₗc[R] A) (RingHom.id R) R A] → R →ₗ[R] A) :
          R →ₗ[R] A))
      g)
have h₁ : Eq.{u_2 + 1} (α := A)
  (((fun (x : R →ₗc[R] A) ↦
            ((↑x :
                [inst_4 : FunLike (R →ₗc[R] A) R A] →
                  [SemilinearMapClass (R →ₗc[R] A) (RingHom.id R) R A] → R →ₗ[R] A) :
              R →ₗ[R] A))
          f :
        (a : R) → A)
      1 :
    A)
  (((fun (x : R →ₗc[R] A) ↦
            ((↑x :
                [inst_4 : FunLike (R →ₗc[R] A) R A] →
                  [SemilinearMapClass (R →ₗc[R] A) (RingHom.id R) R A] → R →ₗ[R] A) :
              R →ₗ[R] A))
          g :
        (a : R) → A)
      1 :
    A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Hom (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : AddCommMonoid D
inst_8 : Module R D
inst_9 : CoalgebraStruct R A
inst_10 : CoalgebraStruct R B
inst_11 : CoalgebraStruct R C
inst_12 : CoalgebraStruct R D
f : A →ₗc[R] B
f' : A → B
h : f' = (⇑f : (a : A) → B)
⊢ counit ∘ₗ
      LinearMap.copy
        (↑f : [inst_13 : FunLike (A →ₗc[R] B) A B] → [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B)
        f' h =
    counit
have h₁ : ∀ (x : A),
  Eq.{u_1 + 1} (α := R)
    ((counit ∘ₗ
            LinearMap.copy
              (↑f :
                [inst_13 : FunLike (A →ₗc[R] B) A B] → [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B)
              f' h :
          (a : A) → R)
        x :
      R)
    ((counit : (a : A) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Hom (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : AddCommMonoid D
inst_8 : Module R D
inst_9 : CoalgebraStruct R A
inst_10 : CoalgebraStruct R B
inst_11 : CoalgebraStruct R C
inst_12 : CoalgebraStruct R D
⊢ Eq (α := A →ₗ[R] R) (counit ∘ₗ LinearMap.id) counit
have h : ∀ (x : A), Eq.{u_1 + 1} (α := R) ((counit ∘ₗ LinearMap.id : (a : A) → R) x : R) ((counit : (a : A) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Hom (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : AddCommMonoid D
inst_8 : Module R D
inst_9 : CoalgebraStruct R A
inst_10 : CoalgebraStruct R B
inst_11 : CoalgebraStruct R C
inst_12 : CoalgebraStruct R D
φ₁ : B →ₗc[R] C
φ₂ : A →ₗc[R] B
⊢ Eq (α := A →ₗ[R] R)
    (counit ∘ₗ
      (↑φ₁ : [inst_13 : FunLike (B →ₗc[R] C) B C] → [SemilinearMapClass (B →ₗc[R] C) (RingHom.id R) B C] → B →ₗ[R] C) ∘ₗ
        (↑φ₂ : [inst_13 : FunLike (A →ₗc[R] B) A B] → [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
    counit
have h : ∀ (x : A),
  Eq.{u_1 + 1} (α := R)
    ((counit ∘ₗ
            (↑φ₁ :
                [inst_13 : FunLike (B →ₗc[R] C) B C] →
                  [SemilinearMapClass (B →ₗc[R] C) (RingHom.id R) B C] → B →ₗ[R] C) ∘ₗ
              (↑φ₂ :
                [inst_13 : FunLike (A →ₗc[R] B) A B] →
                  [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
          (a : A) → R)
        x :
      R)
    ((counit : (a : A) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Hom (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : AddCommMonoid D
inst_8 : Module R D
inst_9 : CoalgebraStruct R A
inst_10 : CoalgebraStruct R B
inst_11 : CoalgebraStruct R C
inst_12 : CoalgebraStruct R D
φ₁ : B →ₗc[R] C
φ₂ : A →ₗc[R] B
⊢ Eq (α := LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) A (C ⊗[R] C))
    (map
        ((↑φ₁ :
            [inst_13 : FunLike (B →ₗc[R] C) B C] → [SemilinearMapClass (B →ₗc[R] C) (RingHom.id R) B C] → B →ₗ[R] C) ∘ₗ
          (↑φ₂ :
            [inst_13 : FunLike (A →ₗc[R] B) A B] → [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
        ((↑φ₁ :
            [inst_13 : FunLike (B →ₗc[R] C) B C] → [SemilinearMapClass (B →ₗc[R] C) (RingHom.id R) B C] → B →ₗ[R] C) ∘ₗ
          (↑φ₂ :
            [inst_13 : FunLike (A →ₗc[R] B) A B] → [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B)) ∘ₗ
      comul)
    (comul ∘ₗ
      (↑φ₁ : [inst_13 : FunLike (B →ₗc[R] C) B C] → [SemilinearMapClass (B →ₗc[R] C) (RingHom.id R) B C] → B →ₗ[R] C) ∘ₗ
        (↑φ₂ : [inst_13 : FunLike (A →ₗc[R] B) A B] → [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
have h : ∀ (x : A),
  Eq.{u_4 + 1} (α := C ⊗[R] C)
    (((map
                ((↑φ₁ :
                    [inst_13 : FunLike (B →ₗc[R] C) B C] →
                      [SemilinearMapClass (B →ₗc[R] C) (RingHom.id R) B C] → B →ₗ[R] C) ∘ₗ
                  (↑φ₂ :
                    [inst_13 : FunLike (A →ₗc[R] B) A B] →
                      [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
                ((↑φ₁ :
                    [inst_13 : FunLike (B →ₗc[R] C) B C] →
                      [SemilinearMapClass (B →ₗc[R] C) (RingHom.id R) B C] → B →ₗ[R] C) ∘ₗ
                  (↑φ₂ :
                    [inst_13 : FunLike (A →ₗc[R] B) A B] →
                      [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B)) ∘ₗ
              comul :
            LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) A (C ⊗[R] C)) :
          (a : A) → C ⊗[R] C)
        x :
      C ⊗[R] C)
    (((comul ∘ₗ
              (↑φ₁ :
                  [inst_13 : FunLike (B →ₗc[R] C) B C] →
                    [SemilinearMapClass (B →ₗc[R] C) (RingHom.id R) B C] → B →ₗ[R] C) ∘ₗ
                (↑φ₂ :
                  [inst_13 : FunLike (A →ₗc[R] B) A B] →
                    [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
            LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) A (C ⊗[R] C)) :
          (a : A) → C ⊗[R] C)
        x :
      C ⊗[R] C)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Hom (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : Coalgebra R A
inst_6 : Coalgebra R B
⊢ Eq (α := A →ₗ[R] R) (counit ∘ₗ counit) counit
have h : ∀ (x : A), Eq.{u + 1} (α := R) ((counit ∘ₗ counit : (a : A) → R) x : R) ((counit : (a : A) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Hom (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : Coalgebra R A
inst_6 : Coalgebra R B
⊢ Eq (α := A →ₗ[R] R ⊗[R] R) (map counit counit ∘ₗ comul) (comul ∘ₗ counit)
have h : ∀ (x : A),
  Eq.{u + 1} (α := R ⊗[R] R) ((map counit counit ∘ₗ comul : (a : A) → R ⊗[R] R) x : R ⊗[R] R)
    ((comul ∘ₗ counit : (a : A) → R ⊗[R] R) x : R ⊗[R] R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Hom (hypothesis)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : Coalgebra R A
inst_6 : Coalgebra R B
f g : A →ₗc[R] R
x : A
⊢ Eq.{u + 1} (α := R) ((f : (a : A) → R) x : R) ((g : (a : A) → R) x : R)
have hf : Eq.{u + 1} (α := R) ((counit : (a : R) → R) ((f : (a : A) → R) x : R) : R) ((counit : (a : A) → R) x : R)
Tactic: have hf := CoalgHomClass.counit_comp_apply f x
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Hom (hypothesis)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : Coalgebra R A
inst_6 : Coalgebra R B
f g : A →ₗc[R] R
x : A
hf : Eq.{u + 1} (α := R) ((counit : (a : R) → R) ((f : (a : A) → R) x : R) : R) ((counit : (a : A) → R) x : R)
⊢ Eq.{u + 1} (α := R) ((f : (a : A) → R) x : R) ((g : (a : A) → R) x : R)
have hg : Eq.{u + 1} (α := R) ((counit : (a : R) → R) ((g : (a : A) → R) x : R) : R) ((counit : (a : A) → R) x : R)
Tactic: have hg := CoalgHomClass.counit_comp_apply g x