awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
S : Type u_3
L : Type u_4
inst_5 : CommRing S
inst_6 : IsDomain S
inst_7 : Field L
inst_8 : Algebra S L
inst_9 : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ
h : ∃ (x : Lˣ), spanSingleton S⁰ (↑x : L) = (↑I : FractionalIdeal S⁰ L)
u : Lˣ
hu : spanSingleton S⁰ (↑u : L) = (↑I : FractionalIdeal S⁰ L)
⊢ Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (((RingEquiv.symm (ringEquivOfRingEquiv K L f) :
            RingEquiv.{u_4, u_2} (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
              (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)) :
          (a : FractionalIdeal S⁰ L) → FractionalIdeal R⁰ K)
        (↑I : FractionalIdeal S⁰ L) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (((MulEquiv.symm (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L) :
            MulEquiv.{u_4, u_2} (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L) (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)) :
          (a : FractionalIdeal S⁰ L) → FractionalIdeal R⁰ K)
        (↑I : FractionalIdeal S⁰ L) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : A
⊢ Eq (α := A ⊗[R] (A ⊗[R] A))
    ((TensorProduct.assoc R A A A : (a : A ⊗[R] A ⊗[R] A) → A ⊗[R] (A ⊗[R] A))
        ((LinearMap.rTensor A comul : (a : A ⊗[R] A) → A ⊗[R] A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) a)) :
      A ⊗[R] (A ⊗[R] A))
    ((LinearMap.lTensor A comul : (a : A ⊗[R] A) → A ⊗[R] (A ⊗[R] A)) ((comul : (a : A) → A ⊗[R] A) a) :
      A ⊗[R] (A ⊗[R] A))

Tactic:
LinearMap.congr_fun coassoc a

Premises used: Quotient.liftOn', AddCon.liftOn, Coalgebra.coassoc, LinearMap.congr_fun
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : A
rw :
  Eq (α := A ⊗[R] (A ⊗[R] A))
    ((LinearMap.lTensor A comul : (a : A ⊗[R] A) → A ⊗[R] (A ⊗[R] A)) ((comul : (a : A) → A ⊗[R] A) a) :
      A ⊗[R] (A ⊗[R] A))
    ((TensorProduct.assoc R A A A : (a : A ⊗[R] A ⊗[R] A) → A ⊗[R] (A ⊗[R] A))
        ((LinearMap.rTensor A comul : (a : A ⊗[R] A) → A ⊗[R] A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) a)) :
      A ⊗[R] (A ⊗[R] A))
rw₁ rw₂ :
  Eq (α := A ⊗[R] (A ⊗[R] A))
    ((LinearMap.lTensor A comul : (a : A ⊗[R] A) → A ⊗[R] (A ⊗[R] A)) ((comul : (a : A) → A ⊗[R] A) a) :
      A ⊗[R] (A ⊗[R] A))
    ((LinearMap.lTensor A comul : (a : A ⊗[R] A) → A ⊗[R] (A ⊗[R] A)) ((comul : (a : A) → A ⊗[R] A) a) :
      A ⊗[R] (A ⊗[R] A))
⊢ Eq (α := A ⊗[R] A ⊗[R] A)
    ((LinearEquiv.symm (TensorProduct.assoc R A A A) : (a : A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A ⊗[R] A)
        ((LinearMap.lTensor A comul : (a : A ⊗[R] A) → A ⊗[R] (A ⊗[R] A)) ((comul : (a : A) → A ⊗[R] A) a)) :
      A ⊗[R] A ⊗[R] A)
    ((LinearMap.rTensor A comul : (a : A ⊗[R] A) → A ⊗[R] A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) a) : A ⊗[R] A ⊗[R] A)

Tactic:
rw [(TensorProduct.assoc R A A A).symm_apply_eq, coassoc_apply a]

Premises used: LinearEquiv.symm_apply_eq, TensorProduct.assoc, Coalgebra.coassoc_apply
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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] A ⊗[R] A ⊗[R] A)
    ((↑(LinearEquiv.symm (TensorProduct.assoc R A A A)) : A ⊗[R] (A ⊗[R] A) →ₗ[R] A ⊗[R] A ⊗[R] A) ∘ₗ
      LinearMap.lTensor A comul ∘ₗ comul)
    (LinearMap.rTensor A comul ∘ₗ comul)

Tactic:
LinearMap.ext coassoc_symm_apply

Premises used: Coalgebra.coassoc_symm_apply, LinearMap.ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : A
⊢ Eq (α := R ⊗[R] A)
    ((LinearMap.rTensor A counit : (a : A ⊗[R] A) → R ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) a) : R ⊗[R] A)
    (1 ⊗ₜ[R] a : R ⊗[R] A)

Tactic:
LinearMap.congr_fun rTensor_counit_comp_comul a

Premises used: Quotient.liftOn', AddCon.liftOn, Coalgebra.rTensor_counit_comp_comul, LinearMap.congr_fun, TensorProduct.tmul, AddCon.toQuotient
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : A
⊢ Eq (α := A ⊗[R] R)
    ((LinearMap.lTensor A counit : (a : A ⊗[R] A) → A ⊗[R] R) ((comul : (a : A) → A ⊗[R] A) a) : A ⊗[R] R)
    (a ⊗ₜ[R] 1 : A ⊗[R] R)

Tactic:
LinearMap.congr_fun lTensor_counit_comp_comul a

Premises used: Quotient.liftOn', AddCon.liftOn, LinearMap.congr_fun, Coalgebra.lTensor_counit_comp_comul, TensorProduct.tmul, AddCon.toQuotient
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : A
repr : Repr.{u, v, u_1} R a
⊢ Eq (α := R ⊗[R] A) (∑ i ∈ repr.index, (counit : (a : A) → R) (repr.left i) ⊗ₜ[R] repr.right i) (1 ⊗ₜ[R] a)

Tactic:
simpa [← repr.eq, map_sum] using congr($(rTensor_counit_comp_comul (R := R) (A := A)) a)

Premises used: map_sum, Coalgebra.Repr.eq
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : A
repr : Repr.{u, v, u_1} R a
⊢ Eq (α := A ⊗[R] R) (∑ i ∈ repr.index, repr.left i ⊗ₜ[R] (counit : (a : A) → R) (repr.right i)) (a ⊗ₜ[R] 1)

Tactic:
simpa [← repr.eq, map_sum] using congr($(lTensor_counit_comp_comul (R := R) (A := A)) a)

Premises used: map_sum, Coalgebra.Repr.eq
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : A
repr : Repr.{u, v, u_1} R a
a₁ : (i : repr.ι) → Repr.{u, v, u_2} R (repr.left i)
a₂ : (i : repr.ι) → Repr.{u, v, u_3} R (repr.right i)
⊢ Eq.{v + 1} (α := A ⊗[R] (A ⊗[R] A))
    (∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] ((a₁ i).right j ⊗ₜ[R] repr.right i))
    (∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] ((a₂ i).left j ⊗ₜ[R] (a₂ i).right j))

Tactic:
simpa [(a₂ _).eq, ← (a₁ _).eq, ← TensorProduct.tmul_sum,
    TensorProduct.sum_tmul, ← repr.eq] using congr($(coassoc (R := R)) a)

Premises used: TensorProduct.sum_tmul, TensorProduct.tmul_sum, Coalgebra.Repr.eq
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
B : Type u_1
inst_4 : AddCommMonoid B
inst_5 : Module R B
F : Type u_2
inst_6 : FunLike F A B
inst_7 : LinearMapClass F R A B
f : F
a : A
repr : Repr.{u, v, u_3} R a
⊢ Eq (α := R ⊗[R] A) (∑ i ∈ repr.index, (counit : (a : A) → R) (repr.left i) ⊗ₜ[R] repr.right i) (1 ⊗ₜ[R] a)

Tactic:
have := sum_counit_tmul_eq repr
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
B : Type u_1
inst_4 : AddCommMonoid B
inst_5 : Module R B
F : Type u_2
inst_6 : FunLike F A B
inst_7 : LinearMapClass F R A B
f : F
a : A
repr : Repr.{u, v, u_3} R a
this : Eq (α := R ⊗[R] A) (∑ i ∈ repr.index, (counit : (a : A) → R) (repr.left i) ⊗ₜ[R] repr.right i) (1 ⊗ₜ[R] a)
⊢ Eq (α := R ⊗[R] B)
    ((LinearMap.lTensor R (↑f : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
          (a : R ⊗[R] A) → R ⊗[R] B)
        (∑ i ∈ repr.index, (counit : (a : A) → R) (repr.left i) ⊗ₜ[R] repr.right i) :
      R ⊗[R] B)
    ((LinearMap.lTensor R (↑f : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
          (a : R ⊗[R] A) → R ⊗[R] B)
        (1 ⊗ₜ[R] a) :
      R ⊗[R] B)

Tactic:
apply_fun LinearMap.lTensor R (f : A →ₗ[R] B) at this

Premises used: LinearMap.lTensor, SemilinearMapClass.semilinearMap
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
B : Type u_1
inst_4 : AddCommMonoid B
inst_5 : Module R B
F : Type u_2
inst_6 : FunLike F A B
inst_7 : LinearMapClass F R A B
f : F
a : A
repr : Repr.{u, v, u_3} R a
this :
  Eq (α := R ⊗[R] B)
    ((LinearMap.lTensor R (↑f : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
          (a : R ⊗[R] A) → R ⊗[R] B)
        (∑ i ∈ repr.index, (counit : (a : A) → R) (repr.left i) ⊗ₜ[R] repr.right i) :
      R ⊗[R] B)
    ((LinearMap.lTensor R (↑f : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
          (a : R ⊗[R] A) → R ⊗[R] B)
        (1 ⊗ₜ[R] a) :
      R ⊗[R] B)
⊢ Eq (α := R ⊗[R] B)
    (∑ i ∈ repr.index, (counit : (a : A) → R) (repr.left i) ⊗ₜ[R] (f : (a : A) → B) (repr.right i) : R ⊗[R] B)
    (1 ⊗ₜ[R] (f : (a : A) → B) a : R ⊗[R] B)

Tactic:
simp_all only [map_sum, LinearMap.lTensor_tmul, LinearMap.coe_coe]

Premises used: map_sum, LinearMap.coe_coe, LinearMap.lTensor_tmul
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
B : Type u_1
inst_4 : AddCommMonoid B
inst_5 : Module R B
F : Type u_2
inst_6 : FunLike F A B
inst_7 : LinearMapClass F R A B
f : F
a : A
repr : Repr.{u, v, u_3} R a
⊢ Eq (α := A ⊗[R] R) (∑ i ∈ repr.index, repr.left i ⊗ₜ[R] (counit : (a : A) → R) (repr.right i)) (a ⊗ₜ[R] 1)

Tactic:
have := sum_tmul_counit_eq repr
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
B : Type u_1
inst_4 : AddCommMonoid B
inst_5 : Module R B
F : Type u_2
inst_6 : FunLike F A B
inst_7 : LinearMapClass F R A B
f : F
a : A
repr : Repr.{u, v, u_3} R a
this : Eq (α := A ⊗[R] R) (∑ i ∈ repr.index, repr.left i ⊗ₜ[R] (counit : (a : A) → R) (repr.right i)) (a ⊗ₜ[R] 1)
⊢ Eq (α := B ⊗[R] R)
    ((LinearMap.rTensor R (↑f : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
          (a : A ⊗[R] R) → B ⊗[R] R)
        (∑ i ∈ repr.index, repr.left i ⊗ₜ[R] (counit : (a : A) → R) (repr.right i)) :
      B ⊗[R] R)
    ((LinearMap.rTensor R (↑f : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
          (a : A ⊗[R] R) → B ⊗[R] R)
        (a ⊗ₜ[R] 1) :
      B ⊗[R] R)

Tactic:
apply_fun LinearMap.rTensor R (f : A →ₗ[R] B) at this

Premises used: SemilinearMapClass.semilinearMap, LinearMap.rTensor
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
B : Type u_1
inst_4 : AddCommMonoid B
inst_5 : Module R B
F : Type u_2
inst_6 : FunLike F A B
inst_7 : LinearMapClass F R A B
f : F
a : A
repr : Repr.{u, v, u_3} R a
this :
  Eq (α := B ⊗[R] R)
    ((LinearMap.rTensor R (↑f : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
          (a : A ⊗[R] R) → B ⊗[R] R)
        (∑ i ∈ repr.index, repr.left i ⊗ₜ[R] (counit : (a : A) → R) (repr.right i)) :
      B ⊗[R] R)
    ((LinearMap.rTensor R (↑f : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
          (a : A ⊗[R] R) → B ⊗[R] R)
        (a ⊗ₜ[R] 1) :
      B ⊗[R] R)
⊢ Eq (α := B ⊗[R] R)
    (∑ i ∈ repr.index, (f : (a : A) → B) (repr.left i) ⊗ₜ[R] (counit : (a : A) → R) (repr.right i) : B ⊗[R] R)
    ((f : (a : A) → B) a ⊗ₜ[R] 1 : B ⊗[R] R)

Tactic:
simp_all only [map_sum, LinearMap.rTensor_tmul, LinearMap.coe_coe]

Premises used: LinearMap.rTensor_tmul, map_sum, LinearMap.coe_coe
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
B : Type u_1
inst_4 : AddCommMonoid B
inst_5 : Module R B
F : Type u_2
inst_6 : FunLike F A B
inst_7 : LinearMapClass F R A B
f g h : F
a : A
repr : Repr.{u, v, u_3} R a
a₁ : (i : repr.ι) → Repr.{u, v, u_4} R (repr.left i)
a₂ : (i : repr.ι) → Repr.{u, v, u_5} R (repr.right i)
⊢ Eq.{v + 1} (α := A ⊗[R] (A ⊗[R] A))
    (∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] ((a₁ i).right j ⊗ₜ[R] repr.right i))
    (∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] ((a₂ i).left j ⊗ₜ[R] (a₂ i).right j))

Tactic:
have := sum_tmul_tmul_eq repr a₁ a₂
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
B : Type u_1
inst_4 : AddCommMonoid B
inst_5 : Module R B
F : Type u_2
inst_6 : FunLike F A B
inst_7 : LinearMapClass F R A B
f g h : F
a : A
repr : Repr.{u, v, u_3} R a
a₁ : (i : repr.ι) → Repr.{u, v, u_4} R (repr.left i)
a₂ : (i : repr.ι) → Repr.{u, v, u_5} R (repr.right i)
this :
  Eq.{v + 1} (α := A ⊗[R] (A ⊗[R] A))
    (∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] ((a₁ i).right j ⊗ₜ[R] repr.right i))
    (∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] ((a₂ i).left j ⊗ₜ[R] (a₂ i).right j))
⊢ Eq.{u_1 + 1} (α := B ⊗[R] (B ⊗[R] B))
    ((TensorProduct.map (↑f : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
          (TensorProduct.map (↑g : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
            (↑h : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)) :
        (a : A ⊗[R] (A ⊗[R] A)) → B ⊗[R] (B ⊗[R] B))
      (∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] ((a₁ i).right j ⊗ₜ[R] repr.right i)))
    ((TensorProduct.map (↑f : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
          (TensorProduct.map (↑g : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
            (↑h : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)) :
        (a : A ⊗[R] (A ⊗[R] A)) → B ⊗[R] (B ⊗[R] B))
      (∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] ((a₂ i).left j ⊗ₜ[R] (a₂ i).right j)))

Tactic:
apply_fun TensorProduct.map (f : A →ₗ[R] B)
    (TensorProduct.map (g : A →ₗ[R] B) (h : A →ₗ[R] B)) at this

Premises used: TensorProduct.map, SemilinearMapClass.semilinearMap
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
B : Type u_1
inst_4 : AddCommMonoid B
inst_5 : Module R B
F : Type u_2
inst_6 : FunLike F A B
inst_7 : LinearMapClass F R A B
f g h : F
a : A
repr : Repr.{u, v, u_3} R a
a₁ : (i : repr.ι) → Repr.{u, v, u_4} R (repr.left i)
a₂ : (i : repr.ι) → Repr.{u, v, u_5} R (repr.right i)
this :
  Eq.{u_1 + 1} (α := B ⊗[R] (B ⊗[R] B))
    ((TensorProduct.map (↑f : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
          (TensorProduct.map (↑g : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
            (↑h : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)) :
        (a : A ⊗[R] (A ⊗[R] A)) → B ⊗[R] (B ⊗[R] B))
      (∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] ((a₁ i).right j ⊗ₜ[R] repr.right i)))
    ((TensorProduct.map (↑f : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
          (TensorProduct.map (↑g : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
            (↑h : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)) :
        (a : A ⊗[R] (A ⊗[R] A)) → B ⊗[R] (B ⊗[R] B))
      (∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] ((a₂ i).left j ⊗ₜ[R] (a₂ i).right j)))
⊢ Eq.{u_1 + 1} (α := B ⊗[R] (B ⊗[R] B))
    (∑ i ∈ repr.index,
      ∑ j ∈ (a₂ i).index,
        (f : (a : A) → B) (repr.left i) ⊗ₜ[R]
          ((g : (a : A) → B) ((a₂ i).left j) ⊗ₜ[R] (h : (a : A) → B) ((a₂ i).right j)))
    (∑ i ∈ repr.index,
      ∑ j ∈ (a₁ i).index,
        (f : (a : A) → B) ((a₁ i).left j) ⊗ₜ[R]
          ((g : (a : A) → B) ((a₁ i).right j) ⊗ₜ[R] (h : (a : A) → B) (repr.right i)))

Tactic:
simp_all only [map_sum, TensorProduct.map_tmul, LinearMap.coe_coe]

Premises used: map_sum, TensorProduct.map_tmul, LinearMap.coe_coe
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : A
𝓡 : Repr.{u, v, u_1} R a
⊢ ∑ x ∈ 𝓡.index, HSMul.hSMul.{u, v, v} (α := R) ((counit : (a : A) → R) (𝓡.left x) : R) (𝓡.right x) = a

Tactic:
simpa only [map_sum, TensorProduct.lift.tmul, LinearMap.lsmul_apply, one_smul]
    using congr(TensorProduct.lift (LinearMap.lsmul R A) $(sum_counit_tmul_eq (R := R) 𝓡))

Premises used: TensorProduct.lift.tmul, map_sum, one_smul, LinearMap.lsmul_apply
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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 ⊗[R] A) (LinearMap.rTensor A counit ∘ₗ comul)
    ((TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)

Tactic:
have := rTensor_counit_comp_comul (R := R) (A := A)
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
this :
  Eq (α := A →ₗ[R] R ⊗[R] A) (LinearMap.rTensor A counit ∘ₗ comul)
    ((TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)
⊢ Eq (α := A →ₗ[R] A) (TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ LinearMap.rTensor A counit ∘ₗ comul)
    (TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ (TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)

Tactic:
apply_fun (TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ ·) at this

Premises used: LinearMap.lsmul, LinearMap.comp, TensorProduct.lift
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
this :
  Eq (α := A →ₗ[R] A) (TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ LinearMap.rTensor A counit ∘ₗ comul)
    (TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ (TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)
⊢ Eq (α := A →ₗ[R] A) (TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul)
    (TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ (TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)

Tactic:
rw [LinearMap.rTensor, ← LinearMap.comp_assoc, TensorProduct.lift_comp_map, LinearMap.compl₂_id]
    at this

Premises used: LinearMap.comp_assoc, TensorProduct.lift_comp_map, LinearMap.compl₂_id, LinearMap.rTensor
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
this :
  Eq (α := A →ₗ[R] A) (TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul)
    (TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ (TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)
h :
  ∀ (x : A),
    Eq (α := A) ((TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul : (a : A) → A) x : A)
      ((LinearMap.id : (a : A) → A) x : A)
⊢ Eq (α := A →ₗ[R] A) (TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul) LinearMap.id

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
this :
  Eq (α := A →ₗ[R] A) (TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul)
    (TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ (TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)
x : A
⊢ Eq (α := A) ((TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul : (a : A) → A) x : A)
    ((LinearMap.id : (a : A) → A) x : A)

Tactic:
simp [this]
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
inst_4 : IsCocomm R A
⊢ Eq (α := A →ₗ[R] A ⊗[R] A) ((↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A) ∘ₗ comul) comul

Tactic:
IsCocomm.comm_comp_comul

Premises used: Coalgebra.IsCocomm.comm_comp_comul
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
inst_4 : IsCocomm R A
a : A
⊢ Eq (α := A ⊗[R] A)
    ((TensorProduct.comm R A A : (a : A ⊗[R] A) → A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) a) : A ⊗[R] A)
    ((comul : (a : A) → A ⊗[R] A) a : A ⊗[R] A)

Tactic:
congr($(comm_comp_comul R A) a)

Premises used: congrArg, id, DFunLike.coe, Coalgebra.comm_comp_comul
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
inst : CommSemiring R
h :
  Eq (α := R ⊗[R] R)
    ((LinearMap.rTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R : (a : R) → R →ₗ[R] R ⊗[R] R) 1 : (a : R) → R ⊗[R] R)
      1)
    (((TensorProduct.mk R R R : (a : R) → R →ₗ[R] R ⊗[R] R) 1 : (a : R) → R ⊗[R] R) 1)
⊢ Eq (α := R →ₗ[R] R ⊗[R] R)
    (LinearMap.rTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R : (a : R) → R →ₗ[R] R ⊗[R] R) 1)
    ((TensorProduct.mk R R R : (a : R) → R →ₗ[R] R ⊗[R] R) 1)

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := R ⊗[R] R)
    ((LinearMap.rTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R : (a : R) → R →ₗ[R] R ⊗[R] R) 1 : (a : R) → R ⊗[R] R)
      1)
    (((TensorProduct.mk R R R : (a : R) → R →ₗ[R] R ⊗[R] R) 1 : (a : R) → R ⊗[R] R) 1)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
inst : CommSemiring R
h :
  Eq (α := R ⊗[R] R)
    ((LinearMap.lTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R : (a : R) → R →ₗ[R] R ⊗[R] R) 1 : (a : R) → R ⊗[R] R)
      1)
    (((LinearMap.flip (TensorProduct.mk R R R) : (a : R) → R →ₗ[R] R ⊗[R] R) 1 : (a : R) → R ⊗[R] R) 1)
⊢ Eq (α := R →ₗ[R] R ⊗[R] R)
    (LinearMap.lTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R : (a : R) → R →ₗ[R] R ⊗[R] R) 1)
    ((LinearMap.flip (TensorProduct.mk R R R) : (a : R) → R →ₗ[R] R ⊗[R] R) 1)

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := R ⊗[R] R)
    ((LinearMap.lTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R : (a : R) → R →ₗ[R] R ⊗[R] R) 1 : (a : R) → R ⊗[R] R)
      1)
    (((LinearMap.flip (TensorProduct.mk R R R) : (a : R) → R →ₗ[R] R ⊗[R] R) 1 : (a : R) → R ⊗[R] R) 1)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
inst : CommSemiring R
r : R
⊢ Eq (α := R ⊗[R] R) ((comul : (a : R) → R ⊗[R] R) r : R ⊗[R] R) (1 ⊗ₜ[R] r : R ⊗[R] R)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
inst : CommSemiring R
r : R
⊢ (counit : (a : R) → R) r = r

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
inst : CommSemiring R
h :
  Eq (α := R ⊗[R] R) (((↑(TensorProduct.comm R R R) : R ⊗[R] R →ₗ[R] R ⊗[R] R) ∘ₗ comul : (a : R) → R ⊗[R] R) 1)
    ((comul : (a : R) → R ⊗[R] R) 1)
⊢ Eq (α := R →ₗ[R] R ⊗[R] R) ((↑(TensorProduct.comm R R R) : R ⊗[R] R →ₗ[R] R ⊗[R] R) ∘ₗ comul) comul

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := R ⊗[R] R) (((↑(TensorProduct.comm R R R) : R ⊗[R] R →ₗ[R] R ⊗[R] R) ∘ₗ comul : (a : R) → R ⊗[R] R) 1)
    ((comul : (a : R) → R ⊗[R] R) 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
r : A × B
⊢ (comul : (a : A × B) → (A × B) ⊗[R] (A × B)) r =
    HAdd.hAdd (α := (A × B) ⊗[R] (A × B)) (β := (A × B) ⊗[R] (A × B))
      ((TensorProduct.map (inl R A B) (inl R A B) : (a : A ⊗[R] A) → (A × B) ⊗[R] (A × B))
          ((comul : (a : A) → A ⊗[R] A) r.1) :
        (A × B) ⊗[R] (A × B))
      ((TensorProduct.map (inr R A B) (inr R A B) : (a : B ⊗[R] B) → (A × B) ⊗[R] (A × B))
          ((comul : (a : B) → B ⊗[R] B) r.2) :
        (A × B) ⊗[R] (A × B))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl