awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Bialgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring C
inst_3 : Bialgebra R C
inst_4 : Algebra R A
f g : WithConv (C →ₐ[R] A)
c : C
simp :
  Eq.{u_2 + 1} (α := A)
    ((lmul' R : (a : A ⊗[R] A) → A)
        (((Algebra.TensorProduct.map f.ofConv g.ofConv : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) (A ⊗[R] A)) :
              (a : C ⊗[R] C) → A ⊗[R] A)
            ((comul : (a : C) → C ⊗[R] C) c) :
          A ⊗[R] A) :
      A)
    (((Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯ : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A) : (a : C ⊗[R] C) → A)
        ((comul : (a : C) → C ⊗[R] C) c : C ⊗[R] C) :
      A)
⊢ Eq.{u_2 + 1} (α := A) (((f * g).ofConv : (a : C) → A) c : A)
    (((Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯ : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A) : (a : C ⊗[R] C) → A)
        ((comul : (a : C) → C ⊗[R] C) c : C ⊗[R] C) :
      A)

Tactic:
simp only [convMul_def, coe_comp, Function.comp_apply, Bialgebra.comulAlgHom_apply]

Premises used: Bialgebra.comulAlgHom_apply, AlgHom.convMul_def, AlgHom.coe_comp, Function.comp_apply
-- Module: Mathlib.RingTheory.Bialgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring C
inst_3 : Bialgebra R C
inst_4 : Algebra R A
f g : WithConv (C →ₐ[R] A)
c : C
rw :
  Eq.{u_2 + 1} (α := A)
    (((comp (lmul' R) (Algebra.TensorProduct.map f.ofConv g.ofConv) : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A) :
          (a : C ⊗[R] C) → A)
        ((comul : (a : C) → C ⊗[R] C) c : C ⊗[R] C) :
      A)
    (((Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯ : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A) : (a : C ⊗[R] C) → A)
        ((comul : (a : C) → C ⊗[R] C) c : C ⊗[R] C) :
      A)
⊢ Eq.{u_2 + 1} (α := A)
    ((lmul' R : (a : A ⊗[R] A) → A)
        (((Algebra.TensorProduct.map f.ofConv g.ofConv : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) (A ⊗[R] A)) :
              (a : C ⊗[R] C) → A ⊗[R] A)
            ((comul : (a : C) → C ⊗[R] C) c) :
          A ⊗[R] A) :
      A)
    (((Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯ : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A) : (a : C ⊗[R] C) → A)
        ((comul : (a : C) → C ⊗[R] C) c : C ⊗[R] C) :
      A)

Tactic:
rw [← comp_apply]

Premises used: AlgHom.comp_apply
-- Module: Mathlib.RingTheory.Bialgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring C
inst_3 : Bialgebra R C
inst_4 : Algebra R A
f g : WithConv (C →ₐ[R] A)
c : C
e_a :
  Eq (α := AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A)
    (comp (lmul' R) (Algebra.TensorProduct.map f.ofConv g.ofConv) : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A)
    (Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯ : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A)
⊢ Eq.{u_2 + 1} (α := A)
    (((comp (lmul' R) (Algebra.TensorProduct.map f.ofConv g.ofConv) : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A) :
          (a : C ⊗[R] C) → A)
        ((comul : (a : C) → C ⊗[R] C) c : C ⊗[R] C) :
      A)
    (((Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯ : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A) : (a : C ⊗[R] C) → A)
        ((comul : (a : C) → C ⊗[R] C) c : C ⊗[R] C) :
      A)

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Bialgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring C
inst_3 : Bialgebra R C
inst_4 : Algebra R A
f g : WithConv (C →ₐ[R] A)
c : C
e_a :
  ∀ (x : C),
    Eq.{u_2 + 1} (α := A)
      ((comp (B := C ⊗[R] C)
              (comp (lmul' R) (Algebra.TensorProduct.map f.ofConv g.ofConv) : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A)
              (includeLeft : C →ₐ[R] C ⊗[R] C) :
            (a : C) → A)
          x :
        A)
      ((comp (B := C ⊗[R] C) (Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯ : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A)
              (includeLeft : C →ₐ[R] C ⊗[R] C) :
            (a : C) → A)
          x :
        A)
e_a₁ :
  ∀ (x : C),
    Eq.{u_2 + 1} (α := A)
      ((comp (B := C ⊗[R] C)
              (restrictScalars R
                (comp (lmul' R) (Algebra.TensorProduct.map f.ofConv g.ofConv) : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A))
              includeRight :
            (a : C) → A)
          x :
        A)
      ((comp (B := C ⊗[R] C)
              (restrictScalars R
                (Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯ : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A))
              includeRight :
            (a : C) → A)
          x :
        A)
⊢ Eq (α := AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A)
    (comp (lmul' R) (Algebra.TensorProduct.map f.ofConv g.ofConv) : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A)
    (Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯ : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A)

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring C
inst_3 : Bialgebra R C
inst_4 : Algebra R A
f g : WithConv (C →ₐ[R] A)
c x : C
⊢ Eq.{u_2 + 1} (α := A)
    ((comp (B := C ⊗[R] C)
            (comp (lmul' R) (Algebra.TensorProduct.map f.ofConv g.ofConv) : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A)
            (includeLeft : C →ₐ[R] C ⊗[R] C) :
          (a : C) → A)
        x :
      A)
    ((comp (B := C ⊗[R] C) (Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯ : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A)
            (includeLeft : C →ₐ[R] C ⊗[R] C) :
          (a : C) → A)
        x :
      A)

Tactic:
simp
-- Module: Mathlib.RingTheory.Bialgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring C
inst_3 : Bialgebra R C
inst_4 : Algebra R A
f g : WithConv (C →ₐ[R] A)
c x : C
⊢ Eq.{u_2 + 1} (α := A)
    ((comp (B := C ⊗[R] C)
            (restrictScalars R
              (comp (lmul' R) (Algebra.TensorProduct.map f.ofConv g.ofConv) : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A))
            includeRight :
          (a : C) → A)
        x :
      A)
    ((comp (B := C ⊗[R] C)
            (restrictScalars R (Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯ : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A))
            includeRight :
          (a : C) → A)
        x :
      A)

Tactic:
simp
-- Module: Mathlib.RingTheory.Bialgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring C
inst_3 : Bialgebra R C
inst_4 : Algebra R A
⊢ Eq (α := WithConv (C →ₗ[R] A)) (toConv (toLinearMap (ofConv 1))) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring C
inst_3 : Bialgebra R C
inst_4 : Algebra R A
f g : WithConv (C →ₐ[R] A)
⊢ toConv (f * g).ofConv.toLinearMap = toConv f.ofConv.toLinearMap * toConv g.ofConv.toLinearMap

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring C
inst_3 : Bialgebra R C
inst_4 : Algebra R A
f : WithConv (C →ₐ[R] A)
n : ℕ
⊢ toConv (f ^ (n + 1)).ofConv.toLinearMap = toConv f.ofConv.toLinearMap ^ (n + 1)

Tactic:
simp only [convPow_succ, toLinearMap_convMul, toLinearMap_convPow, pow_succ]

Premises used: _private.0.AlgHom.convPow_succ, pow_succ, AlgHom.toLinearMap_convMul
-- Module: Mathlib.RingTheory.Bialgebra.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 : CommSemiring B
inst_3 : Semiring C
inst_4 : Bialgebra R C
inst_5 : Algebra R A
inst_6 : Bialgebra R B
f g : WithConv (C →ₐ[R] A)
h : B →ₐc[R] C
⊢ (f * g).ofConv.comp (↑h : B →ₐ[R] C) =
    (toConv (f.ofConv.comp (↑h : B →ₐ[R] C)) * toConv (g.ofConv.comp (↑h : B →ₐ[R] C))).ofConv

Tactic:
simp [convMul_def, comp_assoc, Algebra.TensorProduct.map_comp]

Premises used: Algebra.TensorProduct.map_comp, AlgHom.comp_assoc, AlgHom.convMul_def
-- Module: Mathlib.RingTheory.Bialgebra.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 : CommSemiring B
inst_3 : Semiring C
inst_4 : Bialgebra R C
inst_5 : Algebra R A
inst_6 : Algebra R B
h : A →ₐ[R] B
f g : WithConv (C →ₐ[R] A)
a : (h.comp (f * g).ofConv).toLinearMap = (toConv (h.comp f.ofConv) * toConv (h.comp g.ofConv)).ofConv.toLinearMap
⊢ h.comp (f * g).ofConv = (toConv (h.comp f.ofConv) * toConv (h.comp g.ofConv)).ofConv

Tactic:
apply toLinearMap_injective

Premises used: AlgHom.toLinearMap_injective
-- Module: Mathlib.RingTheory.Bialgebra.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 : CommSemiring B
inst_3 : Semiring C
inst_4 : Bialgebra R C
inst_5 : Algebra R A
inst_6 : Algebra R B
h : A →ₐ[R] B
f g : WithConv (C →ₐ[R] A)
a :
  toConv (h.comp (f * g).ofConv).toLinearMap =
    toConv (toConv (h.comp f.ofConv) * toConv (h.comp g.ofConv)).ofConv.toLinearMap
⊢ (h.comp (f * g).ofConv).toLinearMap = (toConv (h.comp f.ofConv) * toConv (h.comp g.ofConv)).ofConv.toLinearMap

Tactic:
apply WithConv.toConv_injective

Premises used: WithConv.toConv_injective
-- Module: Mathlib.RingTheory.Bialgebra.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 : CommSemiring B
inst_3 : Semiring C
inst_4 : Bialgebra R C
inst_5 : Algebra R A
inst_6 : Algebra R B
h : A →ₐ[R] B
f g : WithConv (C →ₐ[R] A)
a :
  toConv (h.toLinearMap ∘ₗ (toConv f.ofConv.toLinearMap * toConv g.ofConv.toLinearMap).ofConv) =
    toConv (toConv (h.comp f.ofConv) * toConv (h.comp g.ofConv)).ofConv.toLinearMap
⊢ toConv (h.comp (f * g).ofConv).toLinearMap =
    toConv (toConv (h.comp f.ofConv) * toConv (h.comp g.ofConv)).ofConv.toLinearMap

Tactic:
rw [AlgHom.comp_toLinearMap, ← ofConv_toConv (f * g).ofConv.toLinearMap, toLinearMap_convMul]

Premises used: AlgHom.toLinearMap, AlgHom.comp_toLinearMap, HMul.hMul, WithConv.ofConv, WithConv.ofConv_toConv, AlgHom.toLinearMap_convMul
-- Module: Mathlib.RingTheory.Bialgebra.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 : CommSemiring B
inst_3 : Semiring C
inst_4 : Bialgebra R C
inst_5 : Algebra R A
inst_6 : Algebra R B
h : A →ₐ[R] B
f g : WithConv (C →ₐ[R] A)
⊢ toConv (h.toLinearMap ∘ₗ (toConv f.ofConv.toLinearMap * toConv g.ofConv.toLinearMap).ofConv) =
    toConv (toConv (h.comp f.ofConv) * toConv (h.comp g.ofConv)).ofConv.toLinearMap

Tactic:
simp [LinearMap.algHom_comp_convMul_distrib, toLinearMap_convMul]

Premises used: AlgHom.toLinearMap_convMul, LinearMap.algHom_comp_convMul_distrib
-- Module: Mathlib.RingTheory.Bialgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring C
inst_3 : Bialgebra R A
inst_4 : Bialgebra R C
⊢ Eq (α := WithConv (C →ₐc[R] A)) 1 (toConv (comp (unitBialgHom R A) (counitBialgHom R C)))

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring C
inst_3 : Bialgebra R A
inst_4 : Bialgebra R C
⊢ Eq (α := WithConv (C →ₗ[R] A))
    (toConv
      (↑(ofConv 1) :
        [inst_5 : FunLike (C →ₐc[R] A) C A] → [SemilinearMapClass (C →ₐc[R] A) (RingHom.id R) C A] → C →ₗ[R] A))
    1

Tactic:
rfl

Premises used: SemilinearMapClass.semilinearMap, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring C
inst_3 : Bialgebra R A
inst_4 : Bialgebra R C
⊢ Eq (α := WithConv (C →ₐ[R] A)) (toConv (↑(ofConv 1) : C →ₐ[R] A)) 1

Tactic:
rfl

Premises used: BialgHom.toAlgHom, AlgHom.comp, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring C
inst_3 : Bialgebra R A
inst_4 : Bialgebra R C
inst_5 : IsCocomm R C
f g : WithConv (C →ₐc[R] A)
⊢ f * g = toConv (comp (mulBialgHom R A) (comp (Bialgebra.TensorProduct.map f.ofConv g.ofConv) (comulBialgHom R C)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring C
inst_3 : Bialgebra R A
inst_4 : Bialgebra R C
inst_5 : IsCocomm R C
f : WithConv (C →ₐc[R] A)
n : ℕ
⊢ f ^ (n + 1) = f ^ n * f

Tactic:
rfl

Premises used: npowRec, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring C
inst_3 : Bialgebra R A
inst_4 : Bialgebra R C
inst_5 : IsCocomm R C
f g : WithConv (C →ₐc[R] A)
⊢ toConv (f * g).ofConv.toLinearMap = toConv f.ofConv.toLinearMap * toConv g.ofConv.toLinearMap

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring C
inst_3 : Bialgebra R A
inst_4 : Bialgebra R C
inst_5 : IsCocomm R C
f g : WithConv (C →ₐc[R] A)
⊢ toConv (↑(f * g).ofConv : C →ₐ[R] A) = toConv (↑f.ofConv : C →ₐ[R] A) * toConv (↑g.ofConv : C →ₐ[R] A)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, BialgHom.toAlgHom, AlgHom.comp, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring C
inst_3 : Bialgebra R A
inst_4 : Bialgebra R C
inst_5 : IsCocomm R C
f : WithConv (C →ₐc[R] A)
n : ℕ
⊢ toConv (f ^ (n + 1)).ofConv.toLinearMap = toConv f.ofConv.toLinearMap ^ (n + 1)

Tactic:
simp only [convPow_succ, pow_succ, toLinearMap_convMul, toLinearMap_convPow]

Premises used: pow_succ, _private.0.BialgHom.convPow_succ, BialgHom.toLinearMap_convMul
-- Module: Mathlib.RingTheory.Bialgebra.Convolution
Goal:
R : Type u_1
A : Type u_2
C : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring C
inst_3 : Bialgebra R A
inst_4 : Bialgebra R C
inst_5 : IsCocomm R C
f : WithConv (C →ₐc[R] A)
n : ℕ
⊢ toConv (↑(f ^ (n + 1)).ofConv : C →ₐ[R] A) = toConv (↑f.ofConv : C →ₐ[R] A) ^ (n + 1)

Tactic:
simp only [convPow_succ, pow_succ, toAlgHom_convMul, toAlgHom_convPow]

Premises used: pow_succ, _private.0.BialgHom.convPow_succ, BialgHom.toAlgHom_convMul
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
⊢ Injective (α := A ≃ₐc[R] B) toEquiv

Tactic:
fun ⟨_, _⟩ ⟨_, _⟩ h =>
    (BialgEquiv.mk.injEq _ _ _ _).mpr (CoalgEquiv.toEquiv_injective h)

Premises used: Eq.mpr, BialgEquiv.mk.injEq, CoalgEquiv.toEquiv_injective, _private.0.BialgEquiv.toEquiv_injective.match_2, Function.Injective, BialgEquiv.mk, _private.0.BialgEquiv.toEquiv_injective.match_1, Eq
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra 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, BialgEquiv.toEquiv_injective
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
⊢ Injective (α := A ≃ₐc[R] B) toBialgHom

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

Premises used: Equiv.ext, BialgEquiv.toEquiv_injective, BialgHom.congr_fun, Function.Injective
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra 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:
toBialgHom_injective.eq_iff

Premises used: Function.Injective.eq_iff, BialgEquiv.toBialgHom, BialgEquiv.toBialgHom_injective, BialgHomClass.toBialgHom
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e : A ≃ₗc[R] B
h : ∀ (x y : A), e.toFun (x * y) = e.toFun x * e.toFun y
⊢ (↑{ toCoalgEquiv := e, map_mul' := h : A ≃ₐc[R] B } : A ≃ₗc[R] B) = e

Tactic:
rfl

Premises used: CoalgEquivClass.toCoalgEquiv, CoalgHomClass.toCoalgHom, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra 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.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A ≃ₐc[R] B
⊢ f.toCoalgEquiv = (↑f : A ≃ₗc[R] B)

Tactic:
rfl

Premises used: CoalgEquivClass.toCoalgEquiv, CoalgHomClass.toCoalgHom, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A ≃ₐc[R] B
⊢ f.toBialgHom = (↑f : A →ₐc[R] B)

Tactic:
rfl

Premises used: BialgEquiv.toBialgHom, BialgHomClass.toBialgHom, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A ≃ₐc[R] B
⊢ f.toAlgEquiv = f.toAlgEquiv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e : A ≃ₐc[R] B
⊢ Eq (α := (a : A) → B) (⇑e.toAlgEquiv : (a : A) → B) (⇑e : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e : A ≃ₐc[R] B
⊢ Eq (α := A →ₗc[R] B) (↑e : A →ₗc[R] B) (↑(↑e : A →ₐc[R] B) : A →ₗc[R] B)

Tactic:
rfl

Premises used: CoalgHomClass.toCoalgHom, BialgHomClass.toBialgHom, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e : A ≃ₐc[R] B
⊢ (↑(↑e : A →ₐc[R] B) : A →ₐ[R] B) = (↑e.toAlgEquiv : A →ₐ[R] B)

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, BialgHom.toAlgHom, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e e' : A ≃ₐc[R] B
h : ∀ (x : A), Eq.{w + 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.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e : A ≃ₐc[R] B
x x' : A
⊢ x = x' → Eq.{w + 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.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e e' : A ≃ₐc[R] B
h : e = e'
x : A
⊢ Eq.{w + 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.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CoalgebraStruct R A
⊢ Eq (α := A ≃ₗc[R] A) (↑(refl R A) : A ≃ₗc[R] A) (CoalgEquiv.refl R A)

Tactic:
rfl

Premises used: CoalgEquivClass.toCoalgEquiv, CoalgEquiv.refl, CoalgHomClass.toCoalgHom, CoalgHom.id, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CoalgebraStruct R A
⊢ Eq (α := A →ₐc[R] A) (↑(refl R A) : A →ₐc[R] A) (BialgHom.id R A)

Tactic:
rfl

Premises used: BialgHom.id, BialgHomClass.toBialgHom, CoalgHom.id, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
e : A ≃ₐc[R] B
⊢ Eq (α := B ≃ₗc[R] A) (↑e.symm : B ≃ₗc[R] A) (CoalgEquiv.symm (↑e : A ≃ₗc[R] B))

Tactic:
rfl

Premises used: CoalgHomClass.toCoalgHom, CoalgEquiv.symm, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra 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: CoalgHomClass.toCoalgHom, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra 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: CoalgHomClass.toCoalgHom, Equiv.symm, EquivLike.toEquiv, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra 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: BialgEquiv.toEquiv, CoalgHomClass.toCoalgHom, CoalgEquiv.toEquiv, Equiv.symm, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra 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.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra 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: CoalgHomClass.toCoalgHom, rfl