awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
⊢ (mul' R A ∘ₗ rTensor A (mul' R A)) ∘ₗ
      (((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ h.ofConv) ∘ₗ
          (↑(LinearEquiv.symm (TensorProduct.assoc R C C C)) : C ⊗[R] (C ⊗[R] C) →ₗ[R] C ⊗[R] C ⊗[R] C)) ∘ₗ
        lTensor C δ ∘ₗ δ =
    (mul' R A ∘ₗ
        rTensor A (mul' R A) ∘ₗ
          (↑(LinearEquiv.symm (TensorProduct.assoc R A A A)) : A ⊗[R] (A ⊗[R] A) →ₗ[R] A ⊗[R] A ⊗[R] A)) ∘ₗ
      (f.ofConv ⊗ₘ (g.ofConv ⊗ₘ h.ofConv)) ∘ₗ lTensor C δ ∘ₗ δ

Tactic:
simp only [map_map_comp_assoc_symm_eq, comp_assoc]

Premises used: LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_symm_eq
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
e_f :
  Eq (α := A ⊗[R] (A ⊗[R] A) →ₗ[R] A)
    (mul' R A ∘ₗ
      rTensor A (mul' R A) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.assoc R A A A)) : A ⊗[R] (A ⊗[R] A) →ₗ[R] A ⊗[R] A ⊗[R] A))
    (mul' R A ∘ₗ lTensor A (mul' R A))
⊢ (mul' R A ∘ₗ
        rTensor A (mul' R A) ∘ₗ
          (↑(LinearEquiv.symm (TensorProduct.assoc R A A A)) : A ⊗[R] (A ⊗[R] A) →ₗ[R] A ⊗[R] A ⊗[R] A)) ∘ₗ
      (f.ofConv ⊗ₘ (g.ofConv ⊗ₘ h.ofConv)) ∘ₗ lTensor C δ ∘ₗ δ =
    (mul' R A ∘ₗ lTensor A (mul' R A)) ∘ₗ (f.ofConv ⊗ₘ (g.ofConv ⊗ₘ h.ofConv)) ∘ₗ lTensor C δ ∘ₗ δ

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
e_f :
  ∀ (x x_1 x_2 : A),
    Eq (α := A)
      (((((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.curry
                              (mul' R A ∘ₗ
                                rTensor A (mul' R A) ∘ₗ
                                  (↑(LinearEquiv.symm (TensorProduct.assoc R A A A)) :
                                    A ⊗[R] (A ⊗[R] A) →ₗ[R] A ⊗[R] A ⊗[R] A)) :
                            A →ₗ[R] A ⊗[R] A →ₗ[R] A) :
                          (a : A) → A ⊗[R] A →ₗ[R] A)
                        x) :
                    A →ₗ[R] A →ₗ[R] A) :
                  (a : A) → A →ₗ[R] A)
                x_1 :
              A →ₗ[R] A) :
            (a : A) → A)
          x_2 :
        A)
      (((((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.curry (mul' R A ∘ₗ lTensor A (mul' R A)) : A →ₗ[R] A ⊗[R] A →ₗ[R] A) :
                          (a : A) → A ⊗[R] A →ₗ[R] A)
                        x) :
                    A →ₗ[R] A →ₗ[R] A) :
                  (a : A) → A →ₗ[R] A)
                x_1 :
              A →ₗ[R] A) :
            (a : A) → A)
          x_2 :
        A)
⊢ Eq (α := A ⊗[R] (A ⊗[R] A) →ₗ[R] A)
    (mul' R A ∘ₗ
      rTensor A (mul' R A) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.assoc R A A A)) : A ⊗[R] (A ⊗[R] A) →ₗ[R] A ⊗[R] A ⊗[R] A))
    (mul' R A ∘ₗ lTensor A (mul' R A))

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
x x_1 x_2 : A
⊢ Eq (α := A)
    (((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry
                            (mul' R A ∘ₗ
                              rTensor A (mul' R A) ∘ₗ
                                (↑(LinearEquiv.symm (TensorProduct.assoc R A A A)) :
                                  A ⊗[R] (A ⊗[R] A) →ₗ[R] A ⊗[R] A ⊗[R] A)) :
                          A →ₗ[R] A ⊗[R] A →ₗ[R] A) :
                        (a : A) → A ⊗[R] A →ₗ[R] A)
                      x) :
                  A →ₗ[R] A →ₗ[R] A) :
                (a : A) → A →ₗ[R] A)
              x_1 :
            A →ₗ[R] A) :
          (a : A) → A)
        x_2 :
      A)
    (((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry (mul' R A ∘ₗ lTensor A (mul' R A)) : A →ₗ[R] A ⊗[R] A →ₗ[R] A) :
                        (a : A) → A ⊗[R] A →ₗ[R] A)
                      x) :
                  A →ₗ[R] A →ₗ[R] A) :
                (a : A) → A →ₗ[R] A)
              x_1 :
            A →ₗ[R] A) :
          (a : A) → A)
        x_2 :
      A)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
h₁ :
  ∀ (x : C),
    Eq.{u_2 + 1} (α := A)
      (((mul' R A ∘ₗ lTensor A (mul' R A)) ∘ₗ (f.ofConv ⊗ₘ (g.ofConv ⊗ₘ h.ofConv)) ∘ₗ lTensor C δ ∘ₗ δ : (a : C) → A)
          x :
        A)
      ((mul' R A ∘ₗ (f.ofConv ⊗ₘ mul' R A ∘ₗ (g.ofConv ⊗ₘ h.ofConv) ∘ₗ δ) ∘ₗ δ : (a : C) → A) x : A)
⊢ (mul' R A ∘ₗ lTensor A (mul' R A)) ∘ₗ (f.ofConv ⊗ₘ (g.ofConv ⊗ₘ h.ofConv)) ∘ₗ lTensor C δ ∘ₗ δ =
    mul' R A ∘ₗ (f.ofConv ⊗ₘ mul' R A ∘ₗ (g.ofConv ⊗ₘ h.ofConv) ∘ₗ δ) ∘ₗ δ

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
x : C
⊢ Eq.{u_2 + 1} (α := A)
    (((mul' R A ∘ₗ lTensor A (mul' R A)) ∘ₗ (f.ofConv ⊗ₘ (g.ofConv ⊗ₘ h.ofConv)) ∘ₗ lTensor C δ ∘ₗ δ : (a : C) → A) x :
      A)
    ((mul' R A ∘ₗ (f.ofConv ⊗ₘ mul' R A ∘ₗ (g.ofConv ⊗ₘ h.ofConv) ∘ₗ δ) ∘ₗ δ : (a : C) → A) x : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : CoalgebraStruct R C
h : A →ₐ[R] B
f g : WithConv (C →ₗ[R] A)
⊢ h.toLinearMap ∘ₗ (f * g).ofConv = (toConv (h.toLinearMap ∘ₗ f.ofConv) * toConv (h.toLinearMap ∘ₗ g.ofConv)).ofConv

Tactic:
simp [convMul_def, map_comp, ← comp_assoc, AlgHom.comp_mul']

Premises used: LinearMap.convMul_def, LinearMap.comp_assoc, AlgHom.comp_mul', TensorProduct.map_comp
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid C
inst_4 : Module R C
inst_5 : Coalgebra R C
⊢ Eq (α := WithConv (C →ₗ[R] A)) 1 (toConv (Algebra.linearMap R A ∘ₗ ε))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid C
inst_4 : Module R C
inst_5 : Coalgebra R C
c : C
⊢ Eq.{u_2 + 1} (α := A) ((ofConv 1 : (a : C) → A) c : A) ((algebraMap R A : (a : R) → A) ((ε : (a : C) → R) c : R) : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : Coalgebra R C
f : WithConv (C →ₗ[R] A)
h : ∀ (x : C), Eq.{u_2 + 1} (α := A) (((1 * f).ofConv : (a : C) → A) x : A) ((f.ofConv : (a : C) → A) x : A)
⊢ 1 * f = f

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : Coalgebra R C
f : WithConv (C →ₗ[R] A)
x : C
⊢ Eq.{u_2 + 1} (α := A) (((1 * f).ofConv : (a : C) → A) x : A) ((f.ofConv : (a : C) → A) x : A)

Tactic:
simp [convOne_def, ← map_comp_rTensor]

Premises used: LinearMap.map_comp_rTensor, LinearMap.convOne_def
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : Coalgebra R C
f : WithConv (C →ₗ[R] A)
h : ∀ (x : C), Eq.{u_2 + 1} (α := A) (((f * 1).ofConv : (a : C) → A) x : A) ((f.ofConv : (a : C) → A) x : A)
⊢ f * 1 = f

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : AddCommMonoid C
inst_6 : Module R C
inst_7 : Coalgebra R C
f : WithConv (C →ₗ[R] A)
x : C
⊢ Eq.{u_2 + 1} (α := A) (((f * 1).ofConv : (a : C) → A) x : A) ((f.ofConv : (a : C) → A) x : A)

Tactic:
simp [convOne_def, ← map_comp_lTensor]

Premises used: LinearMap.map_comp_lTensor, LinearMap.convOne_def
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid C
inst_3 : Algebra R A
inst_4 : Module R C
inst_5 : Coalgebra R C
inst_6 : IsCocomm R C
f g : WithConv (C →ₗ[R] A)
h : ∀ (x : C), Eq.{u_2 + 1} (α := A) (((f * g).ofConv : (a : C) → A) x : A) (((g * f).ofConv : (a : C) → A) x : A)
⊢ f * g = g * f

Tactic:
ext x
-- Module: Mathlib.RingTheory.Coalgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid C
inst_3 : Algebra R A
inst_4 : Module R C
inst_5 : Coalgebra R C
inst_6 : IsCocomm R C
f g : WithConv (C →ₗ[R] A)
x : C
h :
  Eq (α := A)
    ((mul' R A : (a : A ⊗[R] A) → A)
        ((f.ofConv ⊗ₘ g.ofConv : (a : C ⊗[R] C) → A ⊗[R] A) ((δ : (a : C) → C ⊗[R] C) x) : A ⊗[R] A) :
      A)
    (((g * f).ofConv : (a : C) → A) x : A)
h₁ :
  Eq (α := A)
    ((mul' R A : (a : A ⊗[R] A) → A)
        ((f.ofConv ⊗ₘ g.ofConv : (a : C ⊗[R] C) → A ⊗[R] A)
            ((TensorProduct.comm R C C : (a : C ⊗[R] C) → C ⊗[R] C) ((δ : (a : C) → C ⊗[R] C) x)) :
          A ⊗[R] A) :
      A)
    (((g * f).ofConv : (a : C) → A) x : A)
h₂ :
  Eq (α := A)
    ((mul' R A : (a : A ⊗[R] A) → A)
        ((TensorProduct.comm R A A : (a : A ⊗[R] A) → A ⊗[R] A)
            ((g.ofConv ⊗ₘ f.ofConv : (a : C ⊗[R] C) → A ⊗[R] A) ((δ : (a : C) → C ⊗[R] C) x)) :
          A ⊗[R] A) :
      A)
    (((g * f).ofConv : (a : C) → A) x : A)
h₃ :
  Eq (α := A)
    ((mul' R A : (a : A ⊗[R] A) → A)
        ((g.ofConv ⊗ₘ f.ofConv : (a : C ⊗[R] C) → A ⊗[R] A) ((δ : (a : C) → C ⊗[R] C) x) : A ⊗[R] A) :
      A)
    (((g * f).ofConv : (a : C) → A) x : A)
h₄ h₅ :
  Eq (α := A)
    ((mul' R A : (a : A ⊗[R] A) → A)
        ((g.ofConv ⊗ₘ f.ofConv : (a : C ⊗[R] C) → A ⊗[R] A) ((δ : (a : C) → C ⊗[R] C) x) : A ⊗[R] A) :
      A)
    ((mul' R A : (a : A ⊗[R] A) → A)
        ((g.ofConv ⊗ₘ f.ofConv : (a : C ⊗[R] C) → A ⊗[R] A) ((δ : (a : C) → C ⊗[R] C) x) : A ⊗[R] A) :
      A)
⊢ Eq.{u_2 + 1} (α := A) (((f * g).ofConv : (a : C) → A) x : A) (((g * f).ofConv : (a : C) → A) x : A)

Tactic:
rw [convMul_apply, ← comm_comul R x, map_comm, mul'_comm, convMul_apply]

Premises used: Coalgebra.comm_comul, TensorProduct.map_comm, LinearMap.convMul_apply, LinearMap.mul'_comm
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
⊢ Function.Injective (α := A ≃ₗc[R] B) toEquiv

Tactic:
fun ⟨_, _, _, _⟩ ⟨_, _, _, _⟩ h =>
    (CoalgEquiv.mk.injEq _ _ _ _ _ _ _ _).mpr
      ⟨CoalgHom.ext (congr_fun (Equiv.mk.inj h).1), (Equiv.mk.inj h).2⟩

Premises used: Eq.mpr, Equiv.mk.inj, CoalgEquiv.mk, CoalgEquiv.mk.injEq, _private.0.CoalgEquiv.toEquiv_injective.match_1, And.right, And.left, CoalgHom.ext, And.intro, _private.0.CoalgEquiv.toEquiv_injective.match_2, Function.Injective, congr_fun, Eq
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e₁ e₂ : A ≃ₗc[R] B
⊢ e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂

Tactic:
toEquiv_injective.eq_iff

Premises used: Function.Injective.eq_iff, CoalgEquiv.toEquiv_injective
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
⊢ Function.Injective (α := A ≃ₗc[R] B) toCoalgHom

Tactic:
fun _ _ H => toEquiv_injective <| Equiv.ext <| CoalgHom.congr_fun H

Premises used: CoalgEquiv.toEquiv_injective, Equiv.ext, CoalgHom.congr_fun, Function.Injective
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e₁ e₂ : A ≃ₗc[R] B
⊢ Eq (α := A →ₗc[R] B) (↑e₁ : A →ₗc[R] B) (↑e₂ : A →ₗc[R] B) ↔ e₁ = e₂

Tactic:
toCoalgHom_injective.eq_iff

Premises used: Function.Injective.eq_iff, CoalgEquiv.toCoalgHom_injective, CoalgHomClass.toCoalgHom
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A → B
h : ∀ (x y : A), f (x + y) = f x + f y
h₀ :
  ∀ (m : R) (x : A),
    { toFun := f, map_add' := h : A →ₙ+ B }.toFun (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R) ({ toFun := f, map_add' := h : A →ₙ+ B }.toFun x)
h₁ : counit ∘ₗ { toFun := f, map_add' := h, map_smul' := h₀ : A →ₗ[R] B } = counit
h₂ :
  TensorProduct.map { toFun := f, map_add' := h, map_smul' := h₀ : A →ₗ[R] B }
        { toFun := f, map_add' := h, map_smul' := h₀ : A →ₗ[R] B } ∘ₗ
      comul =
    comul ∘ₗ { toFun := f, map_add' := h, map_smul' := h₀ : A →ₗ[R] B }
h₃ : B → A
h₄ :
  Function.LeftInverse h₃
    { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂ : A →ₗc[R] B }.toFun
h₅ :
  Function.RightInverse h₃
    { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂ : A →ₗc[R] B }.toFun
⊢ (⇑{ toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂, invFun := h₃, left_inv := h₄,
          right_inv := h₅ : A ≃ₗc[R] B } :
      (a : A) → B) =
    f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e : A ≃ₗc[R] B
⊢ Eq (α := (a : A) → B) (⇑(↑e : A →ₗc[R] B) : (a : A) → B) (⇑e : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ f.toLinearEquiv = f.toLinearEquiv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ f.toCoalgHom = (↑f : A →ₗc[R] B)

Tactic:
rfl

Premises used: CoalgHomClass.toCoalgHom, rfl
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e : A ≃ₗc[R] B
⊢ Eq (α := (a : A) → B) (⇑e.toLinearEquiv : (a : A) → B) (⇑e : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e : A ≃ₗc[R] B
⊢ (↑e.toLinearEquiv : A →ₗ[R] B) =
    (↑(↑e : A →ₗc[R] B) :
      [inst_7 : 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.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e e' : A ≃ₗc[R] B
h : ∀ (x : A), Eq.{u_3 + 1} (α := B) ((e : (a : A) → B) x : B) ((e' : (a : A) → B) x : B)
⊢ e = e'

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e : A ≃ₗc[R] B
x x' : A
⊢ x = x' → Eq.{u_3 + 1} (α := B) ((e : (a : A) → B) x : B) ((e : (a : A) → B) x' : B)

Tactic:
DFunLike.congr_arg e

Premises used: DFunLike.congr_arg
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e e' : A ≃ₗc[R] B
h : e = e'
x : A
⊢ Eq.{u_3 + 1} (α := B) ((e : (a : A) → B) x : B) ((e' : (a : A) → B) x : B)

Tactic:
DFunLike.congr_fun h x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
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 : AddCommMonoid B
inst_3 : AddCommMonoid C
inst_4 : Module R A
inst_5 : Module R B
inst_6 : Module R C
inst_7 : CoalgebraStruct R A
inst_8 : CoalgebraStruct R B
inst_9 : CoalgebraStruct R C
e_1 e' e : A ≃ₗc[R] B
rw :
  comul =
    (↑(TensorProduct.congr e.toLinearEquiv e.toLinearEquiv) : TensorProduct R A A →ₗ[R] TensorProduct R B B) ∘ₗ
      comul ∘ₗ (↑e.toLinearEquiv.symm : B →ₗ[R] A)
⊢ (↑(TensorProduct.congr e.toLinearEquiv e.toLinearEquiv).symm : TensorProduct R B B →ₗ[R] TensorProduct R A A) ∘ₗ
      comul =
    comul ∘ₗ (↑e.toLinearEquiv.symm : B →ₗ[R] A)

Tactic:
rw [LinearEquiv.toLinearMap_symm_comp_eq]

Premises used: LinearEquiv.toLinearMap_symm_comp_eq
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
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 : AddCommMonoid B
inst_3 : AddCommMonoid C
inst_4 : Module R A
inst_5 : Module R B
inst_6 : Module R C
inst_7 : CoalgebraStruct R A
inst_8 : CoalgebraStruct R B
inst_9 : CoalgebraStruct R C
e_1 e' e : A ≃ₗc[R] B
simp :
  comul =
    (comul ∘ₗ
        (↑(↑e : A →ₗc[R] B) :
          [inst_10 : FunLike (A →ₗc[R] B) A B] → [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B)) ∘ₗ
      (↑e.toLinearEquiv.symm : B →ₗ[R] A)
⊢ comul =
    (↑(TensorProduct.congr e.toLinearEquiv e.toLinearEquiv) : TensorProduct R A A →ₗ[R] TensorProduct R B B) ∘ₗ
      comul ∘ₗ (↑e.toLinearEquiv.symm : B →ₗ[R] A)

Tactic:
simp only [TensorProduct.congr, toCoalgHom_eq_coe, CoalgHom.toLinearMap_eq_coe,
        LinearEquiv.ofLinear_toLinearMap, ← LinearMap.comp_assoc, CoalgHomClass.map_comp_comul]

Premises used: CoalgEquiv.toCoalgHom_eq_coe, LinearMap.comp_assoc, TensorProduct.congr, CoalgHomClass.map_comp_comul, CoalgHom.toLinearMap_eq_coe, LinearEquiv.ofLinear_toLinearMap
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
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 : AddCommMonoid B
inst_3 : AddCommMonoid C
inst_4 : Module R A
inst_5 : Module R B
inst_6 : Module R C
inst_7 : CoalgebraStruct R A
inst_8 : CoalgebraStruct R B
inst_9 : CoalgebraStruct R C
e_1 e' e : A ≃ₗc[R] B
rw : comul = (comul ∘ₗ (↑e.toLinearEquiv : A →ₗ[R] B)) ∘ₗ (↑e.toLinearEquiv.symm : B →ₗ[R] A)
rw₁ rw₂ : Eq.{u_3 + 1} (α := B →ₗ[R] TensorProduct R B B) comul comul
⊢ comul =
    (comul ∘ₗ
        (↑(↑e : A →ₗc[R] B) :
          [inst_10 : FunLike (A →ₗc[R] B) A B] → [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B)) ∘ₗ
      (↑e.toLinearEquiv.symm : B →ₗ[R] A)

Tactic:
rw [← toLinearEquiv_toLinearMap, LinearEquiv.comp_symm_cancel_right]

Premises used: LinearEquiv.comp_symm_cancel_right, CoalgEquiv.toLinearEquiv_toLinearMap
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
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) (toLinearEquiv (refl R A)) (LinearEquiv.refl R A)

Tactic:
rfl

Premises used: LinearEquiv.refl, rfl
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
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 →ₗc[R] A) (↑(refl R A) : A →ₗc[R] A) (CoalgHom.id R A)

Tactic:
rfl

Premises used: CoalgHomClass.toCoalgHom, CoalgHom.id, rfl
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e : A ≃ₗc[R] B
⊢ e.symm.toLinearEquiv = e.toLinearEquiv.symm

Tactic:
rfl

Premises used: LinearEquiv.symm, rfl
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e : A ≃ₗc[R] B
⊢ Eq (α := (a : B) → A) (⇑e.toLinearEquiv.symm : (a : B) → A) (⇑e.symm : (a : B) → A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e : A ≃ₗc[R] B
⊢ (↑(↑e.symm : B →ₗc[R] A) :
      [inst_7 : FunLike (B →ₗc[R] A) B A] → [SemilinearMapClass (B →ₗc[R] A) (RingHom.id R) B A] → B →ₗ[R] A) =
    (↑e.toLinearEquiv.symm : B →ₗ[R] A)

Tactic:
rfl

Premises used: SemilinearMapClass.semilinearMap, rfl
-- Module: Mathlib.RingTheory.Coalgebra.Equiv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e : A ≃ₗc[R] B
x : A
⊢ (e.symm : (a : B) → A) ((e : (a : A) → B) x : B) = x

Tactic:
LinearEquiv.symm_apply_apply (e : A ≃ₗ[R] B) x

Premises used: CoalgEquiv.toLinearEquiv, LinearEquiv.symm_apply_apply