awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : B
⊢ (e : (a : A) → B) ((e.symm : (a : B) → A) x : A) = x

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

Premises used: CoalgEquiv.toLinearEquiv, LinearEquiv.apply_symm_apply
-- 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.invFun = (⇑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.toEquiv.symm = (↑e.symm : B ≃ A)

Tactic:
rfl

Premises used: Equiv.symm, EquivLike.toEquiv, 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.toEquiv = e.toEquiv.symm

Tactic:
rfl

Premises used: CoalgEquiv.toEquiv, Equiv.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 : A) → B) (⇑e.toEquiv : (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
⊢ Eq (α := (a : B) → A) (⇑e.toEquiv.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
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₁₂ : A ≃ₗc[R] B
e₂₃ : B ≃ₗc[R] C
⊢ (e₁₂.trans e₂₃).toLinearEquiv = e₁₂.toLinearEquiv ≪≫ₗ e₂₃.toLinearEquiv

Tactic:
rfl

Premises used: LinearEquiv.trans, rfl
-- 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₁₂ : A ≃ₗc[R] B
e₂₃ : B ≃ₗc[R] C
⊢ Eq (α := A →ₗc[R] C) (↑(e₁₂.trans e₂₃) : A →ₗc[R] C) (e₂₃.comp (↑e₁₂ : A →ₗc[R] B))

Tactic:
rfl

Premises used: CoalgHom.comp, CoalgHomClass.toCoalgHom, rfl
-- 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₁₂ : A ≃ₗc[R] B
e₂₃ : B ≃ₗc[R] C
⊢ (↑e₁₂ : A ≃ B).trans (↑e₂₃ : B ≃ C) = (↑(e₁₂.trans e₂₃) : A ≃ C)

Tactic:
rfl

Premises used: EquivLike.toEquiv, 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
g : B →ₗc[R] A
h₁ : f.comp g = CoalgHom.id R B
h₂ : g.comp f = CoalgHom.id R A
⊢ (↑(ofCoalgHom f g h₁ h₂) : A →ₗc[R] B) = f

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
f : A →ₗc[R] B
g : B →ₗc[R] A
h₁ : f.comp g = CoalgHom.id R B
h₂ : g.comp f = CoalgHom.id R A
⊢ (ofCoalgHom f g h₁ h₂).symm = ofCoalgHom g f h₂ h₁

Tactic:
rfl

Premises used: CoalgEquiv.symm, rfl, CoalgEquiv.ofCoalgHom
-- 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
hf : Function.Bijective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Eq (α := (a : A) → B) (⇑(ofBijective hf) : (a : A) → B) (⇑f : (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
C : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
inst_4 : AddCommMonoid B
inst_5 : Module R B
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
simp :
  ((((↑(TensorProduct.assoc R B B B) :
              TensorProduct R (TensorProduct R B B) B →ₗ[R] TensorProduct R B (TensorProduct R B B)) ∘ₗ
            LinearMap.rTensor B
              ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A))) ∘ₗ
          TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
        comul) ∘ₗ
      (↑f.toLinearEquiv.symm : B →ₗ[R] A) =
    ((LinearMap.lTensor B
            ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
          TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
        comul) ∘ₗ
      (↑f.toLinearEquiv.symm : B →ₗ[R] A)
⊢ Eq (α := B →ₗ[R] TensorProduct R B (TensorProduct R B B))
    ((↑(TensorProduct.assoc R B B B) :
        TensorProduct R (TensorProduct R B B) B →ₗ[R] TensorProduct R B (TensorProduct R B B)) ∘ₗ
      LinearMap.rTensor B comul ∘ₗ comul)
    (LinearMap.lTensor B comul ∘ₗ comul)

Tactic:
simp only [← ((f : A ≃ₗ[R] B).comp_toLinearMap_symm_eq _ _).2 f.map_comp_comul,
      ← LinearMap.comp_assoc]

Premises used: Iff.mpr, LinearEquiv.comp_toLinearMap_symm_eq, CoalgHom.map_comp_comul, LinearMap.comp_assoc, CoalgEquiv.toCoalgHom
-- 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 : Module R A
inst_3 : Coalgebra R A
inst_4 : AddCommMonoid B
inst_5 : Module R B
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
e_f :
  (((↑(TensorProduct.assoc R B B B) :
            TensorProduct R (TensorProduct R B B) B →ₗ[R] TensorProduct R B (TensorProduct R B B)) ∘ₗ
          LinearMap.rTensor B
            ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A))) ∘ₗ
        TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
      comul =
    (LinearMap.lTensor B
          ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
        TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
      comul
⊢ ((((↑(TensorProduct.assoc R B B B) :
              TensorProduct R (TensorProduct R B B) B →ₗ[R] TensorProduct R B (TensorProduct R B B)) ∘ₗ
            LinearMap.rTensor B
              ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A))) ∘ₗ
          TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
        comul) ∘ₗ
      (↑f.toLinearEquiv.symm : B →ₗ[R] A) =
    ((LinearMap.lTensor B
            ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
          TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
        comul) ∘ₗ
      (↑f.toLinearEquiv.symm : B →ₗ[R] A)

Tactic:
congr 1
-- 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 : Module R A
inst_3 : Coalgebra R A
inst_4 : AddCommMonoid B
inst_5 : Module R B
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
e_f :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := TensorProduct R B (TensorProduct R B B))
      (((((↑(TensorProduct.assoc R B B B) :
                    TensorProduct R (TensorProduct R B B) B →ₗ[R] TensorProduct R B (TensorProduct R B B)) ∘ₗ
                  LinearMap.rTensor B
                    ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ
                      (↑f.toLinearEquiv.symm : B →ₗ[R] A))) ∘ₗ
                TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
              comul :
            (a : A) → TensorProduct R B (TensorProduct R B B))
          x :
        TensorProduct R B (TensorProduct R B B))
      (((LinearMap.lTensor B
                  ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
                TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
              comul :
            (a : A) → TensorProduct R B (TensorProduct R B B))
          x :
        TensorProduct R B (TensorProduct R B B))
⊢ (((↑(TensorProduct.assoc R B B B) :
            TensorProduct R (TensorProduct R B B) B →ₗ[R] TensorProduct R B (TensorProduct R B B)) ∘ₗ
          LinearMap.rTensor B
            ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A))) ∘ₗ
        TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
      comul =
    (LinearMap.lTensor B
          ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
        TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
      comul

Tactic:
ext x
-- 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 : Module R A
inst_3 : Coalgebra R A
inst_4 : AddCommMonoid B
inst_5 : Module R B
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
x : A
⊢ Eq.{u_3 + 1} (α := TensorProduct R B (TensorProduct R B B))
    (((((↑(TensorProduct.assoc R B B B) :
                  TensorProduct R (TensorProduct R B B) B →ₗ[R] TensorProduct R B (TensorProduct R B B)) ∘ₗ
                LinearMap.rTensor B
                  ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A))) ∘ₗ
              TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
            comul :
          (a : A) → TensorProduct R B (TensorProduct R B B))
        x :
      TensorProduct R B (TensorProduct R B B))
    (((LinearMap.lTensor B
                ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
              TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
            comul :
          (a : A) → TensorProduct R B (TensorProduct R B B))
        x :
      TensorProduct R B (TensorProduct R B B))

Tactic:
simpa only [toCoalgHom_eq_coe, CoalgHom.toLinearMap_eq_coe, LinearMap.coe_comp,
      LinearEquiv.coe_coe, Function.comp_apply, ← (ℛ R _).eq, map_sum, TensorProduct.map_tmul,
      LinearMap.coe_coe, CoalgHom.coe_coe, LinearMap.rTensor_tmul, coe_symm_toLinearEquiv,
      symm_apply_apply, LinearMap.lTensor_comp_map, TensorProduct.sum_tmul,
      TensorProduct.assoc_tmul, TensorProduct.tmul_sum] using (sum_map_tmul_tmul_eq f f f x).symm

Premises used: LinearMap.rTensor_tmul, CoalgEquiv.toCoalgHom_eq_coe, Coalgebra.sum_map_tmul_tmul_eq, TensorProduct.assoc_tmul, map_sum, CoalgHom.coe_coe, TensorProduct.sum_tmul, TensorProduct.tmul_sum, LinearMap.coe_comp, CoalgEquiv.coe_symm_toLinearEquiv, TensorProduct.map_tmul, CoalgEquiv.symm_apply_apply, Function.comp_apply, CoalgHom.toLinearMap_eq_coe, LinearMap.coe_coe, Coalgebra.Repr.eq, LinearMap.lTensor_comp_map, Eq.symm, Coalgebra.Repr.arbitrary, LinearEquiv.coe_coe
-- 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 : Module R A
inst_3 : Coalgebra R A
inst_4 : AddCommMonoid B
inst_5 : Module R B
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
simp_rw :
  (LinearMap.rTensor B (counit ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
        TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
      comul =
    (TensorProduct.mk R R B : (a : R) → B →ₗ[R] TensorProduct R R B) 1 ∘ₗ f.toLinearMap
⊢ Eq (α := B →ₗ[R] TensorProduct R R B) (LinearMap.rTensor B counit ∘ₗ comul)
    ((TensorProduct.mk R R B : (a : R) → B →ₗ[R] TensorProduct R R B) 1)

Tactic:
simp_rw [(f.toLinearEquiv.eq_comp_toLinearMap_symm _ _).2 f.counit_comp,
      ← (f.toLinearEquiv.comp_toLinearMap_symm_eq _ _).2 f.map_comp_comul, ← LinearMap.comp_assoc,
      f.toLinearEquiv.comp_toLinearMap_symm_eq]

Premises used: Iff.mpr, LinearEquiv.comp_toLinearMap_symm_eq, CoalgHom.map_comp_comul, LinearMap.comp_assoc, CoalgHom.counit_comp, LinearEquiv.eq_comp_toLinearMap_symm, CoalgEquiv.toCoalgHom
-- 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 : Module R A
inst_3 : Coalgebra R A
inst_4 : AddCommMonoid B
inst_5 : Module R B
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
h :
  ∀ (x : A),
    Eq (α := TensorProduct R R B)
      (((LinearMap.rTensor B (counit ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
                TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
              comul :
            (a : A) → TensorProduct R R B)
          x :
        TensorProduct R R B)
      (((TensorProduct.mk R R B : (a : R) → B →ₗ[R] TensorProduct R R B) 1 ∘ₗ f.toLinearMap :
            (a : A) → TensorProduct R R B)
          x :
        TensorProduct R R B)
⊢ (LinearMap.rTensor B (counit ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
        TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
      comul =
    (TensorProduct.mk R R B : (a : R) → B →ₗ[R] TensorProduct R R B) 1 ∘ₗ f.toLinearMap

Tactic:
ext x
-- 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 : Module R A
inst_3 : Coalgebra R A
inst_4 : AddCommMonoid B
inst_5 : Module R B
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
x : A
⊢ Eq (α := TensorProduct R R B)
    (((LinearMap.rTensor B (counit ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
              TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
            comul :
          (a : A) → TensorProduct R R B)
        x :
      TensorProduct R R B)
    (((TensorProduct.mk R R B : (a : R) → B →ₗ[R] TensorProduct R R B) 1 ∘ₗ f.toLinearMap :
          (a : A) → TensorProduct R R B)
        x :
      TensorProduct R R B)

Tactic:
simp [← (ℛ R _).eq]

Premises used: Coalgebra.Repr.eq, Coalgebra.Repr.arbitrary
-- 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 : Module R A
inst_3 : Coalgebra R A
inst_4 : AddCommMonoid B
inst_5 : Module R B
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
simp_rw :
  (LinearMap.lTensor B (counit ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
        TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
      comul =
    (LinearMap.flip (TensorProduct.mk R B R) : (a : R) → B →ₗ[R] TensorProduct R B R) 1 ∘ₗ f.toLinearMap
⊢ Eq (α := B →ₗ[R] TensorProduct R B R) (LinearMap.lTensor B counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R B R) : (a : R) → B →ₗ[R] TensorProduct R B R) 1)

Tactic:
simp_rw [(f.toLinearEquiv.eq_comp_toLinearMap_symm _ _).2 f.counit_comp,
      ← (f.toLinearEquiv.comp_toLinearMap_symm_eq _ _).2 f.map_comp_comul, ← LinearMap.comp_assoc,
      f.toLinearEquiv.comp_toLinearMap_symm_eq]

Premises used: Iff.mpr, LinearEquiv.comp_toLinearMap_symm_eq, CoalgHom.map_comp_comul, LinearMap.comp_assoc, CoalgHom.counit_comp, LinearEquiv.eq_comp_toLinearMap_symm, CoalgEquiv.toCoalgHom
-- 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 : Module R A
inst_3 : Coalgebra R A
inst_4 : AddCommMonoid B
inst_5 : Module R B
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
h :
  ∀ (x : A),
    Eq (α := TensorProduct R B R)
      (((LinearMap.lTensor B (counit ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
                TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
              comul :
            (a : A) → TensorProduct R B R)
          x :
        TensorProduct R B R)
      (((LinearMap.flip (TensorProduct.mk R B R) : (a : R) → B →ₗ[R] TensorProduct R B R) 1 ∘ₗ f.toLinearMap :
            (a : A) → TensorProduct R B R)
          x :
        TensorProduct R B R)
⊢ (LinearMap.lTensor B (counit ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
        TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
      comul =
    (LinearMap.flip (TensorProduct.mk R B R) : (a : R) → B →ₗ[R] TensorProduct R B R) 1 ∘ₗ f.toLinearMap

Tactic:
ext x
-- 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 : Module R A
inst_3 : Coalgebra R A
inst_4 : AddCommMonoid B
inst_5 : Module R B
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
x : A
⊢ Eq (α := TensorProduct R B R)
    (((LinearMap.lTensor B (counit ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
              TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
            comul :
          (a : A) → TensorProduct R B R)
        x :
      TensorProduct R B R)
    (((LinearMap.flip (TensorProduct.mk R B R) : (a : R) → B →ₗ[R] TensorProduct R B R) 1 ∘ₗ f.toLinearMap :
          (a : A) → TensorProduct R B R)
        x :
      TensorProduct R B R)

Tactic:
simp [← (ℛ R _).eq]

Premises used: Coalgebra.Repr.eq, Coalgebra.Repr.arbitrary
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
Goal:
R : Type u_2
inst : CommSemiring R
r : R
⊢ IsGroupLikeElem R r ↔ r = 1

Tactic:
simp +contextual [isGroupLikeElem_iff]

Premises used: isGroupLikeElem_iff
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
inst_4 : Nontrivial R
ha : IsGroupLikeElem.{u_2, u_3} R (A := A) 0
⊢ False

Tactic:
simpa using ha.counit_eq_one

Premises used: IsGroupLikeElem.counit_eq_one
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : Module R B
inst_6 : Coalgebra R B
a : A
inst_7 : FunLike F A B
inst_8 : CoalgHomClass F R A B
f : F
ha : IsGroupLikeElem R a
rw : Eq.{u_2 + 1} (α := R) ((counit : (a : A) → R) a : R) (1 : R)
rw₁ rw₂ : Eq.{u_2 + 1} (α := R) 1 1
⊢ Eq.{u_2 + 1} (α := R) ((counit : (a : B) → R) ((f : (a : A) → B) a : B) : R) (1 : R)

Tactic:
rw [CoalgHomClass.counit_comp_apply, ha.counit_eq_one]

Premises used: CoalgHomClass.counit_comp_apply, IsGroupLikeElem.counit_eq_one
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : Module R B
inst_6 : Coalgebra R B
a : A
inst_7 : FunLike F A B
inst_8 : CoalgHomClass F R A B
f : F
ha : IsGroupLikeElem R a
rw :
  Eq.{u_4 + 1} (α := B ⊗[R] B)
    (((TensorProduct.map (↑f : [inst_9 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
              (↑f : [inst_9 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
            LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) (A ⊗[R] A) (B ⊗[R] B)) :
          (a : A ⊗[R] A) → B ⊗[R] B)
        (a ⊗ₜ[R] a) :
      B ⊗[R] B)
    ((f : (a : A) → B) a ⊗ₜ[R] (f : (a : A) → B) a : B ⊗[R] B)
⊢ Eq.{u_4 + 1} (α := B ⊗[R] B) ((comul : (a : B) → B ⊗[R] B) ((f : (a : A) → B) a) : B ⊗[R] B)
    ((f : (a : A) → B) a ⊗ₜ[R] (f : (a : A) → B) a : B ⊗[R] B)

Tactic:
rw [← CoalgHomClass.map_comp_comul_apply, ha.comul_eq_tmul_self]

Premises used: IsGroupLikeElem.comul_eq_tmul_self, CoalgHomClass.map_comp_comul_apply
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : Module R B
inst_6 : Coalgebra R B
a : A
inst_7 : FunLike F A B
inst_8 : CoalgHomClass F R A B
f : F
ha : IsGroupLikeElem R a
⊢ Eq.{u_4 + 1} (α := B ⊗[R] B)
    (((TensorProduct.map (↑f : [inst_9 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
              (↑f : [inst_9 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
            LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) (A ⊗[R] A) (B ⊗[R] B)) :
          (a : A ⊗[R] A) → B ⊗[R] B)
        (a ⊗ₜ[R] a) :
      B ⊗[R] B)
    ((f : (a : A) → B) a ⊗ₜ[R] (f : (a : A) → B) a : B ⊗[R] B)

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : A
ha : IsGroupLikeElem R a
⊢ ∀ ⦃a₂ : GroupLike R A⦄,
    (↑{ val := a, isGroupLikeElem_val := ha : GroupLike R A } : A) = (↑a₂ : A) →
      { val := a, isGroupLikeElem_val := ha : GroupLike R A } = a₂

Tactic:
congr!
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
a b : GroupLike R A
⊢ (↑a : A) = (↑b : A) ↔ a = b

Tactic:
val_injective.eq_iff

Premises used: GroupLike.val_injective, Function.Injective.eq_iff
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
rw : ∀ (t : Finset A), (↑t : Set A) ⊆ {a : A | IsGroupLikeElem R a} → LinearIndepOn R id (↑t : Set A)
⊢ LinearIndepOn.{u_3, u_2, u_3} (ι := A) R id {a : A | IsGroupLikeElem R a}

Tactic:
rw [linearIndepOn_iff_linearIndepOn_finset]

Premises used: linearIndepOn_iff_linearIndepOn_finset
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
hs : (↑∅ : Set A) ⊆ {a : A | IsGroupLikeElem R a}
⊢ LinearIndepOn R id (↑∅ : Set A)

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
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}
⊢ IsGroupLikeElem R a ∧ ∀ a ∈ s, IsGroupLikeElem R a

Tactic:
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

Premises used: Set.subset_def, Set.mem_setOf_eq, forall_eq_or_imp, Finset.cons_eq_insert, Set.mem_insert_iff, Finset.coe_insert, Finset.mem_coe
-- Module: Mathlib.RingTheory.Coalgebra.GroupLike
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
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 : IsGroupLikeElem R a ∧ ∀ a ∈ s, IsGroupLikeElem R a
⊢ IsGroupLikeElem R a

Tactic:
obtain ⟨ha, hs⟩ := hs