awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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)
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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.{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:
assumption
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A →ₗc[R] B
h₁ :
  ∀ (x y : A),
    (f : (a : A) → B) (x + y) = HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
h₂ :
  ∀ (m : R) (x : A),
    { toFun := (⇑f : (a : A) → B), map_add' := h₁ : A →ₙ+ B }.toFun (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
        ({ toFun := (⇑f : (a : A) → B), map_add' := h₁ : A →ₙ+ B }.toFun x)
h₃ : counit ∘ₗ { toFun := (⇑f : (a : A) → B), map_add' := h₁, map_smul' := h₂ : A →ₗ[R] B } = counit
h₄ :
  map { toFun := (⇑f : (a : A) → B), map_add' := h₁, map_smul' := h₂ : A →ₗ[R] B }
        { toFun := (⇑f : (a : A) → B), map_add' := h₁, map_smul' := h₂ : A →ₗ[R] B } ∘ₗ
      comul =
    comul ∘ₗ { toFun := (⇑f : (a : A) → B), map_add' := h₁, map_smul' := h₂ : A →ₗ[R] B }
⊢ { toFun := (⇑f : (a : A) → B), map_add' := h₁, map_smul' := h₂, counit_comp := h₃, map_comp_comul := h₄ :
      A →ₗc[R] B } =
    f

Tactic:
ext fun _ => rfl

Premises used: CoalgHom.ext, rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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)
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)
⊢ 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

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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)
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:
simp_all
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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)
⊢ map
        (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)
        (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) ∘ₗ
      comul =
    comul ∘ₗ
      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

Tactic:
simp only [(f : A →ₗ[R] B).copy_eq f' h,
      CoalgHomClass.map_comp_comul]

Premises used: CoalgHomClass.map_comp_comul, SemilinearMapClass.semilinearMap, LinearMap.copy_eq
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A →ₗc[R] B
f' : A → B
h : f' = (⇑f : (a : A) → B)
⊢ (⇑(f.copy f' h) : (a : A) → B) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A →ₗc[R] B
f' : A → B
h : f' = (⇑f : (a : A) → B)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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
h : ∀ (x : A), Eq.{u_1 + 1} (α := R) ((counit ∘ₗ LinearMap.id : (a : A) → R) x : R) ((counit : (a : A) → R) x : R)
⊢ Eq (α := A →ₗ[R] R) (counit ∘ₗ LinearMap.id) counit

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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
x : A
⊢ Eq.{u_1 + 1} (α := R) ((counit ∘ₗ LinearMap.id : (a : A) → R) x : R) ((counit : (a : A) → R) x : R)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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.{u_2 + 1} (α := A →ₗ[R] A ⊗[R] A) (map LinearMap.id LinearMap.id ∘ₗ comul) (comul ∘ₗ LinearMap.id)

Tactic:
simp only [map_id, LinearMap.id_comp, LinearMap.comp_id]

Premises used: LinearMap.comp_id, LinearMap.id_comp, TensorProduct.map_id
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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
⊢ Eq (α := (a : A) → A) (⇑(CoalgHom.id R A) : (a : A) → A) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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
⊢ Eq (α := A →ₗ[R] A)
    (↑(CoalgHom.id R A) :
      [inst_4 : FunLike (A →ₗc[R] A) A A] → [SemilinearMapClass (A →ₗc[R] A) (RingHom.id R) A A] → A →ₗ[R] A)
    LinearMap.id

Tactic:
rfl

Premises used: SemilinearMapClass.semilinearMap, rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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
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)
⊢ 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

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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
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:
simp
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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
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)
⊢ 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))

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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
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:
simp [map_comp]

Premises used: TensorProduct.map_comp
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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 : CoalgebraStruct R A
inst_8 : CoalgebraStruct R B
inst_9 : CoalgebraStruct R C
φ₁ : B →ₗc[R] C
φ₂ : A →ₗc[R] B
⊢ Eq (α := (a : A) → C) (⇑(φ₁.comp φ₂) : (a : A) → C)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := B) (⇑φ₁ : (a : B) → C) (⇑φ₂ : (a : A) → B))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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 : CoalgebraStruct R A
inst_8 : CoalgebraStruct R B
inst_9 : CoalgebraStruct R C
φ₁ : B →ₗc[R] C
φ₂ : A →ₗc[R] B
⊢ Eq (α := A →ₗ[R] C)
    (↑(φ₁.comp φ₂) :
      [inst_10 : FunLike (A →ₗc[R] C) A C] → [SemilinearMapClass (A →ₗc[R] C) (RingHom.id R) A C] → A →ₗ[R] C)
    ((↑φ₁ : [inst_10 : FunLike (B →ₗc[R] C) B C] → [SemilinearMapClass (B →ₗc[R] C) (RingHom.id R) B C] → B →ₗ[R] C) ∘ₗ
      (↑φ₂ : [inst_10 : FunLike (A →ₗc[R] B) A B] → [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B))

Tactic:
rfl

Premises used: SemilinearMapClass.semilinearMap, rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
φ : A →ₗc[R] B
⊢ φ.comp (CoalgHom.id R A) = φ

Tactic:
ext fun _x => rfl

Premises used: CoalgHom.ext, rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
φ : A →ₗc[R] B
⊢ comp (CoalgHom.id R B) φ = φ

Tactic:
ext fun _x => rfl

Premises used: CoalgHom.ext, rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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
φ₁ : C →ₗc[R] D
φ₂ : B →ₗc[R] C
φ₃ : A →ₗc[R] B
⊢ (φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃)

Tactic:
ext fun _x => rfl

Premises used: CoalgHom.ext, rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
φ : A →ₗc[R] B
R' : Type u_6
inst_7 : SMul R' A
inst_8 : SMul R' B
inst_9 : LinearMap.CompatibleSMul A B R' R
r : R'
x : A
⊢ (φ : (a : A) → B) (r • x) = HSMul.hSMul (β := B) r ((φ : (a : A) → B) x : B)

Tactic:
φ.toLinearMap.map_smul_of_tower r x

Premises used: CoalgHom.toLinearMap, LinearMap.map_smul_of_tower
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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
x : A
⊢ (1 : (a : A) → A) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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
φ ψ : A →ₗc[R] A
x : A
⊢ Eq (α := A) ((φ * ψ : (a : A) → A) x : A) ((φ : (a : A) → A) ((ψ : (a : A) → A) x : A) : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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
h : ∀ (x : A), Eq.{u + 1} (α := R) ((counit ∘ₗ counit : (a : A) → R) x : R) ((counit : (a : A) → R) x : R)
⊢ Eq (α := A →ₗ[R] R) (counit ∘ₗ counit) counit

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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
x : A
⊢ Eq.{u + 1} (α := R) ((counit ∘ₗ counit : (a : A) → R) x : R) ((counit : (a : A) → R) x : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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
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)
⊢ Eq (α := A →ₗ[R] R ⊗[R] R) (map counit counit ∘ₗ comul) (comul ∘ₗ counit)

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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
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:
simp only [LinearMap.coe_comp, Function.comp_apply, CommSemiring.comul_apply,
        ← LinearMap.lTensor_comp_rTensor, rTensor_counit_comul, LinearMap.lTensor_tmul]

Premises used: LinearMap.lTensor_comp_rTensor, LinearMap.coe_comp, Coalgebra.rTensor_counit_comul, Function.comp_apply, CommSemiring.comul_apply, LinearMap.lTensor_tmul
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
x : A
⊢ Eq.{u + 1} (α := R) ((counitCoalgHom R A : (a : A) → R) x : R) ((counit : (a : A) → R) x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
⊢ Eq (α := A →ₗ[R] R)
    (↑(counitCoalgHom R A) :
      [inst_4 : FunLike (A →ₗc[R] R) A R] → [SemilinearMapClass (A →ₗc[R] R) (RingHom.id R) A R] → A →ₗ[R] R)
    counit

Tactic:
rfl

Premises used: SemilinearMapClass.semilinearMap, rfl
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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) ((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
-- Module: Mathlib.RingTheory.Coalgebra.Hom
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) ((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