awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra 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) (CoalgEquiv.trans (↑e₁₂ : A ≃ₗc[R] B) (↑e₂₃ : B ≃ₗc[R] C))

Tactic:
rfl

Premises used: CoalgEquivClass.toCoalgEquiv, CoalgHom.comp, CoalgHomClass.toCoalgHom, CoalgEquiv.trans, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra 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) (BialgHom.comp (↑e₂₃ : B →ₐc[R] C) (↑e₁₂ : A →ₐc[R] B))

Tactic:
rfl

Premises used: CoalgHom.comp, BialgHom.comp, BialgHomClass.toBialgHom, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra 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.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 : B), (e : (a : A) → B) ((e.symm : (a : B) → A) x : A) = x

Tactic:
e.toEquiv.apply_symm_apply

Premises used: Equiv.apply_symm_apply, BialgEquiv.toEquiv
-- 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 : A), (e.symm : (a : B) → A) ((e : (a : A) → B) x : B) = x

Tactic:
e.toEquiv.symm_apply_apply

Premises used: Equiv.symm_apply_apply, BialgEquiv.toEquiv
-- 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] B) (BialgHom.comp (↑e : A →ₐc[R] B) (↑e.symm : B →ₐc[R] A)) (BialgHom.id R B)

Tactic:
BialgHom.coe_algHom_injective e.toAlgEquiv.comp_symm

Premises used: BialgHom.coe_algHom_injective, AlgEquiv.comp_symm, BialgEquiv.toAlgEquiv
-- 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] A) (BialgHom.comp (↑e.symm : B →ₐc[R] A) (↑e : A →ₐc[R] B)) (BialgHom.id R A)

Tactic:
BialgHom.coe_algHom_injective e.toAlgEquiv.symm_comp

Premises used: BialgHom.coe_algHom_injective, AlgEquiv.symm_comp, BialgEquiv.toAlgEquiv
-- 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) (↑e.toAlgEquiv.toRingEquiv : A →+* B) (↑e : A →+* B)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, 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) (↑e.toAlgEquiv : A →+* B) (↑e : A →+* B)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, BialgEquiv.toAlgEquiv, 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
g : B →ₐc[R] A
h₁ : f.comp g = BialgHom.id R B
h₂ : g.comp f = BialgHom.id R A
⊢ (↑(ofBialgHom f g h₁ h₂) : A →ₐc[R] B) = f

Tactic:
rfl

Premises used: 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
g : B →ₐc[R] A
h₁ : f.comp g = BialgHom.id R B
h₂ : g.comp f = BialgHom.id R A
⊢ (ofBialgHom f g h₁ h₂).symm = ofBialgHom g f h₂ h₁

Tactic:
rfl

Premises used: BialgEquiv.ofBialgHom, CoalgEquiv.symm, BialgEquiv.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 : Bialgebra R A
inst_4 : Bialgebra R B
f : A ≃ₐ[R] B
counit_comp : AlgHom.comp (counitAlgHom R B) (↑f : A →ₐ[R] B) = counitAlgHom R A
map_comp_comul :
  AlgHom.comp (Algebra.TensorProduct.map (↑f : A →ₐ[R] B) (↑f : A →ₐ[R] B) : AlgHom.{u, v, w} R (A ⊗[R] A) (B ⊗[R] B))
      (comulAlgHom R A : A →ₐ[R] A ⊗[R] A) =
    AlgHom.comp (comulAlgHom R B) (↑f : A →ₐ[R] B)
⊢ (↑(↑(ofAlgEquiv f counit_comp map_comp_comul).toAlgEquiv : A ≃ₗ[R] B) : A →ₗ[R] B) = (↑(↑f : A ≃ₗ[R] B) : A →ₗ[R] B)

Tactic:
rfl

Premises used: BialgEquiv.toAlgEquiv, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Bialgebra R A
inst_4 : Bialgebra R B
f : A →ₐc[R] B
hf : Bijective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
H :
  ∀ (x : A),
    Eq.{u + 1} (α := R)
      ((AlgHom.comp (counitAlgHom R B) (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B) : (a : A) → R) x : R)
      ((counitAlgHom R A : (a : A) → R) x : R)
⊢ AlgHom.comp (counitAlgHom R B) (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B) = counitAlgHom R A

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Bialgebra R A
inst_4 : Bialgebra R B
f : A →ₐc[R] B
hf : Bijective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
x : A
⊢ Eq.{u + 1} (α := R)
    ((AlgHom.comp (counitAlgHom R B) (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B) : (a : A) → R) x : R)
    ((counitAlgHom R A : (a : A) → R) x : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Bialgebra R A
inst_4 : Bialgebra R B
f : A →ₐc[R] B
hf : Bijective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
H :
  ∀ (x : A),
    Eq.{w + 1} (α := B ⊗[R] B)
      (((AlgHom.comp
                (Algebra.TensorProduct.map (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B)
                    (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B) :
                  AlgHom.{u, v, w} R (A ⊗[R] A) (B ⊗[R] B))
                (comulAlgHom R A : A →ₐ[R] A ⊗[R] A) :
              AlgHom.{u, v, w} R A (B ⊗[R] B)) :
            (a : A) → B ⊗[R] B)
          x :
        B ⊗[R] B)
      ((AlgHom.comp (comulAlgHom R B) (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B) : (a : A) → B ⊗[R] B)
          x :
        B ⊗[R] B)
⊢ AlgHom.comp
      (Algebra.TensorProduct.map (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B)
          (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B) :
        AlgHom.{u, v, w} R (A ⊗[R] A) (B ⊗[R] B))
      (comulAlgHom R A : A →ₐ[R] A ⊗[R] A) =
    AlgHom.comp (comulAlgHom R B) (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B)

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.Equiv
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Bialgebra R A
inst_4 : Bialgebra R B
f : A →ₐc[R] B
hf : Bijective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
x : A
⊢ Eq.{w + 1} (α := B ⊗[R] B)
    (((AlgHom.comp
              (Algebra.TensorProduct.map (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B)
                  (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B) :
                AlgHom.{u, v, w} R (A ⊗[R] A) (B ⊗[R] B))
              (comulAlgHom R A : A →ₐ[R] A ⊗[R] A) :
            AlgHom.{u, v, w} R A (B ⊗[R] B)) :
          (a : A) → B ⊗[R] B)
        x :
      B ⊗[R] B)
    ((AlgHom.comp (comulAlgHom R B) (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B) : (a : A) → B ⊗[R] B) x :
      B ⊗[R] B)

Tactic:
simp
-- 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 : Bialgebra R A
inst_4 : Bialgebra R B
f : A →ₐc[R] B
hf : Bijective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Eq (α := (a : A) → B) (⇑(ofBijective f hf) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a b : A
ha : IsGroupLikeElem R a
hb : IsGroupLikeElem R b
⊢ Eq.{u_1 + 1} (α := R) ((counit : (a : A) → R) (a * b) : R) (1 : R)

Tactic:
simp [ha, hb]
-- Module: Mathlib.RingTheory.Bialgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a b : A
ha : IsGroupLikeElem R a
hb : IsGroupLikeElem R b
⊢ Eq (α := TensorProduct R A A) ((comul : (a : A) → TensorProduct R A A) (a * b) : TensorProduct R A A)
    ((a * b) ⊗ₜ[R] (a * b) : TensorProduct R A A)

Tactic:
simp [ha, hb]
-- Module: Mathlib.RingTheory.Bialgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a : A
n : ℕ
ha : IsGroupLikeElem R a
⊢ IsGroupLikeElem R (a ^ n)

Tactic:
(groupLikeSubmonoid R A).pow_mem ha _

Premises used: Submonoid.pow_mem, Set.Mem, setOf, groupLikeSubmonoid
-- Module: Mathlib.RingTheory.Bialgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a b : A
hab : a * b = 1
hba : b * a = 1
ha : IsGroupLikeElem R a
⊢ HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) b : R) ((counit : (a : A) → R) a : R) = 1

Tactic:
simp [← counit_mul, hba]

Premises used: Bialgebra.counit_mul
-- Module: Mathlib.RingTheory.Bialgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a b : A
hab : a * b = 1
hba : b * a = 1
ha : IsGroupLikeElem R a
⊢ HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) a : R) (1 : R) = 1

Tactic:
simp [ha]
-- Module: Mathlib.RingTheory.Bialgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a b : A
hab : a * b = 1
hba : b * a = 1
ha : IsGroupLikeElem R a
⊢ HMul.hMul (α := TensorProduct R A A) (β := TensorProduct R A A)
      ((comul : (a : A) → TensorProduct R A A) b : TensorProduct R A A)
      ((comul : (a : A) → TensorProduct R A A) a : TensorProduct R A A) =
    1

Tactic:
simp [← comul_mul, hba]

Premises used: Bialgebra.comul_mul
-- Module: Mathlib.RingTheory.Bialgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a b : A
hab : a * b = 1
hba : b * a = 1
ha : IsGroupLikeElem R a
⊢ HMul.hMul (α := TensorProduct R A A) (β := TensorProduct R A A)
      ((comul : (a : A) → TensorProduct R A A) a : TensorProduct R A A) (b ⊗ₜ[R] b) =
    1

Tactic:
simp [ha, hab, Algebra.TensorProduct.one_def]

Premises used: Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.Bialgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a b : A
hab : a * b = 1
hba : b * a = 1
⊢ IsGroupLikeElem R a ↔ IsGroupLikeElem R b

Tactic:
⟨.of_mul_eq_one hab hba, .of_mul_eq_one hba hab⟩

Premises used: IsGroupLikeElem.of_mul_eq_one, Iff.intro
-- Module: Mathlib.RingTheory.Bialgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
u : Aˣ
⊢ (↑u⁻¹ : A) * (↑u : A) = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Bialgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
u : Aˣ
⊢ (↑u : A) * (↑u⁻¹ : A) = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Bialgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
⊢ Eq.{u_2 + 1} (α := A) (↑1 : A) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a b : GroupLike R A
⊢ (↑(a * b) : A) = (↑a : A) * (↑b : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a : GroupLike R A
n : ℕ
⊢ (↑(a ^ n) : A) = (↑a : A) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
F : 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 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
inst_7 : FunLike F A B
inst_8 : BialgHomClass F R A B
c : F
r : R
⊢ Eq.{u_3 + 1} (α := B) ((c : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
    ((algebraMap R B : (a : R) → B) r : B)

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, map_smul, map_one]

Premises used: Algebra.algebraMap_eq_smul_one, map_one, map_smul
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
F : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
inst_3 : Semiring B
inst_4 : Bialgebra R B
inst_5 : FunLike F A B
inst_6 : BialgHomClass F R A B
f : F
⊢ Eq (α := A →ₐ[R] R) (AlgHom.comp (counitAlgHom R B) (↑f : A →ₐ[R] B)) (counitAlgHom R A)

Tactic:
AlgHom.toLinearMap_injective (CoalgHomClass.counit_comp f)

Premises used: AlgHom.toLinearMap_injective, CoalgHomClass.counit_comp
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
F : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
inst_3 : Semiring B
inst_4 : Bialgebra R B
inst_5 : FunLike F A B
inst_6 : BialgHomClass F R A B
f : F
⊢ Eq (α := AlgHom.{u_1, u_2, u_3} R A (B ⊗[R] B))
    (AlgHom.comp
        (Algebra.TensorProduct.map (↑f : A →ₐ[R] B) (↑f : A →ₐ[R] B) : AlgHom.{u_1, u_2, u_3} R (A ⊗[R] A) (B ⊗[R] B))
        (comulAlgHom R A : A →ₐ[R] A ⊗[R] A) :
      AlgHom.{u_1, u_2, u_3} R A (B ⊗[R] B))
    (AlgHom.comp (comulAlgHom R B) (↑f : A →ₐ[R] B) : AlgHom.{u_1, u_2, u_3} R A (B ⊗[R] B))

Tactic:
AlgHom.toLinearMap_injective (CoalgHomClass.map_comp_comul f)

Premises used: AlgHom.toLinearMap_injective, CoalgHomClass.map_comp_comul
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
inst_9 : CoalgebraStruct R A
inst_10 : CoalgebraStruct R B
inst_11 : CoalgebraStruct R C
inst_12 : CoalgebraStruct R D
f g : A →ₐc[R] B
h : Eq (α := (a : A) → B) ((fun (f : A →ₐc[R] B) ↦ f.toFun) f) ((fun (f : A →ₐc[R] B) ↦ f.toFun) g)
rcases :
  ∀ (toCoalgHom : A →ₗc[R] B) (map_one' : toCoalgHom.toFun 1 = 1)
    (map_mul' : ∀ (x y : A), toCoalgHom.toFun (x * y) = toCoalgHom.toFun x * toCoalgHom.toFun y)
    (h :
      Eq (α := (a : A) → B)
        ((fun (f : A →ₐc[R] B) ↦ f.toFun) { toCoalgHom := toCoalgHom, map_one' := map_one', map_mul' := map_mul' })
        ((fun (f : A →ₐc[R] B) ↦ f.toFun) g)),
    { toCoalgHom := toCoalgHom, map_one' := map_one', map_mul' := map_mul' : A →ₐc[R] B } = g
⊢ f = g

Tactic:
rcases f with ⟨_, _⟩
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
inst_9 : CoalgebraStruct R A
inst_10 : CoalgebraStruct R B
inst_11 : CoalgebraStruct R C
inst_12 : CoalgebraStruct R D
g : A →ₐc[R] B
toCoalgHom : A →ₗc[R] B
map_one' : toCoalgHom.toFun 1 = 1
map_mul' : ∀ (x y : A), toCoalgHom.toFun (x * y) = toCoalgHom.toFun x * toCoalgHom.toFun y
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →ₐc[R] B) ↦ f.toFun) { toCoalgHom := toCoalgHom, map_one' := map_one', map_mul' := map_mul' })
    ((fun (f : A →ₐc[R] B) ↦ f.toFun) g)
rcases :
  ∀ (toCoalgHom_1 : A →ₗc[R] B) (map_one'_1 : toCoalgHom_1.toFun 1 = 1)
    (map_mul'_1 : ∀ (x y : A), toCoalgHom_1.toFun (x * y) = toCoalgHom_1.toFun x * toCoalgHom_1.toFun y)
    (h :
      Eq (α := (a : A) → B)
        ((fun (f : A →ₐc[R] B) ↦ f.toFun) { toCoalgHom := toCoalgHom, map_one' := map_one', map_mul' := map_mul' })
        ((fun (f : A →ₐc[R] B) ↦ f.toFun)
          { toCoalgHom := toCoalgHom_1, map_one' := map_one'_1, map_mul' := map_mul'_1 })),
    { toCoalgHom := toCoalgHom, map_one' := map_one', map_mul' := map_mul' : A →ₐc[R] B } =
      { toCoalgHom := toCoalgHom_1, map_one' := map_one'_1, map_mul' := map_mul'_1 }
⊢ { toCoalgHom := toCoalgHom, map_one' := map_one', map_mul' := map_mul' : A →ₐc[R] B } = g

Tactic:
rcases g with ⟨_, _⟩
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
inst_9 : CoalgebraStruct R A
inst_10 : CoalgebraStruct R B
inst_11 : CoalgebraStruct R C
inst_12 : CoalgebraStruct R D
toCoalgHom : A →ₗc[R] B
map_one' : toCoalgHom.toFun 1 = 1
map_mul' : ∀ (x y : A), toCoalgHom.toFun (x * y) = toCoalgHom.toFun x * toCoalgHom.toFun y
toCoalgHom_1 : A →ₗc[R] B
map_one'_1 : toCoalgHom_1.toFun 1 = 1
map_mul'_1 : ∀ (x y : A), toCoalgHom_1.toFun (x * y) = toCoalgHom_1.toFun x * toCoalgHom_1.toFun y
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →ₐc[R] B) ↦ f.toFun) { toCoalgHom := toCoalgHom, map_one' := map_one', map_mul' := map_mul' })
    ((fun (f : A →ₐc[R] B) ↦ f.toFun) { toCoalgHom := toCoalgHom_1, map_one' := map_one'_1, map_mul' := map_mul'_1 })
⊢ { toCoalgHom := toCoalgHom, map_one' := map_one', map_mul' := map_mul' : A →ₐc[R] B } =
    { toCoalgHom := toCoalgHom_1, map_one' := map_one'_1, map_mul' := map_mul'_1 }

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
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 : Type u_6
inst_7 : FunLike F A B
inst_8 : BialgHomClass F R A B
f : F
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →ₐc[R] B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
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
h : f.toFun 1 = 1
h₁ : ∀ (x y : A), f.toFun (x * y) = f.toFun x * f.toFun y
⊢ Eq (α := (a : A) → B) (⇑{ toCoalgHom := f, map_one' := h, map_mul' := h₁ : A →ₐc[R] B } : (a : A) → B)
    (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
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 → 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₃ :
  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₄ : { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ : A →ₗc[R] B }.toFun 1 = 1
h₅ :
  ∀ (x y : A),
    { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ : A →ₗc[R] B }.toFun
        (x * y) =
      { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ : A →ₗc[R] B }.toFun x *
        { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ : A →ₗc[R] B }.toFun y
⊢ (⇑{ toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃, map_one' := h₄,
          map_mul' := h₅ : A →ₐc[R] B } :
      (a : A) → B) =
    f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
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
h : f.toFun 1 = 1
h₁ : ∀ (x y : A), f.toFun (x * y) = f.toFun x * f.toFun y
⊢ (↑{ toCoalgHom := f, map_one' := h, map_mul' := h₁ : A →ₐc[R] B } : A →ₗc[R] B) = f

Tactic:
rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
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
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →ₗc[R] B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
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
a : A
⊢ Eq.{u_3 + 1} (α := B) ((f.toCoalgHom : (a : A) → B) a : B) ((f : (a : A) → B) a : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
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
⊢ Eq (α := (a : A) → B)
    (⇑(↑f : [inst_7 : FunLike (A →ₐc[R] B) A B] → [SemilinearMapClass (A →ₐc[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
      (a : A) → B)
    (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
inst_9 : CoalgebraStruct R A
inst_10 : CoalgebraStruct R B
inst_11 : CoalgebraStruct R C
inst_12 : CoalgebraStruct R D
f : A →ₐc[R] B
⊢ ∀ (r : R), f.toFun ((algebraMap R A : (a : R) → A) r) = (algebraMap R B : (a : R) → B) r

Tactic:
simp [Algebra.algebraMap_eq_smul_one, toCoalgHom_apply]

Premises used: Algebra.algebraMap_eq_smul_one, BialgHom.toCoalgHom_apply