awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R
h : WellFounded.{u + 1} (α := R) DvdNotUnit
this : ∀ (I : { J : Ideal R // J.FG }), ∃ (x : R), (↑I : Ideal R) = Ideal.span {x}
choose :
  (f : (I : { J : Ideal R // J.FG }) → R) →
    (hf : ∀ (I : { J : Ideal R // J.FG }), (↑I : Ideal R) = Ideal.span {f I}) →
      RelEmbedding (β := R) (fun (x1 x2 : { N : Submodule R R // N.FG }) ↦ x2 < x1) DvdNotUnit
⊢ RelEmbedding (β := R) (fun (x1 x2 : { N : Submodule R R // N.FG }) ↦ x2 < x1) DvdNotUnit

Tactic:
choose f hf using this
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R
h : WellFounded.{u + 1} (α := R) DvdNotUnit
f : (I : { J : Ideal R // J.FG }) → R
hf : ∀ (I : { J : Ideal R // J.FG }), (↑I : Ideal R) = Ideal.span {f I}
x y : { N : Submodule R R // N.FG }
e : f x = f y
a : (↑x : Submodule R R) = (↑y : Submodule R R)
⊢ x = y

Tactic:
ext1
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R
h : WellFounded.{u + 1} (α := R) DvdNotUnit
f : (I : { J : Ideal R // J.FG }) → R
hf : ∀ (I : { J : Ideal R // J.FG }), (↑I : Ideal R) = Ideal.span {f I}
x y : { N : Submodule R R // N.FG }
e : f x = f y
a : Ideal.span {f x} = (↑y : Submodule R R)
a₁ : Eq (α := Submodule R R) (Ideal.span {f x}) (Ideal.span {f y})
a₂ a₃ : Eq (α := Submodule R R) (Ideal.span {f y}) (Ideal.span {f y})
⊢ (↑x : Submodule R R) = (↑y : Submodule R R)

Tactic:
rw [hf, hf, e]
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R
h : WellFounded.{u + 1} (α := R) DvdNotUnit
f : (I : { J : Ideal R // J.FG }) → R
hf : ∀ (I : { J : Ideal R // J.FG }), (↑I : Ideal R) = Ideal.span {f I}
dsimp : ∀ {a b : { N : Submodule R R // N.FG }}, DvdNotUnit (f a) (f b) ↔ b < a
⊢ ∀ {a b : { N : Submodule R R // N.FG }},
    DvdNotUnit (α := R)
        (({ toFun := f, inj' := ⋯ : { N : Submodule R R // N.FG } ↪ R } : (a : { N : Submodule R R // N.FG }) → R) a :
          R)
        (({ toFun := f, inj' := ⋯ : { N : Submodule R R // N.FG } ↪ R } : (a : { N : Submodule R R // N.FG }) → R) b :
          R) ↔
      b < a

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R
h : WellFounded.{u + 1} (α := R) DvdNotUnit
f : (I : { J : Ideal R // J.FG }) → R
hf : ∀ (I : { J : Ideal R // J.FG }), (↑I : Ideal R) = Ideal.span {f I}
a b : { N : Submodule R R // N.FG }
rw : (↑b : Ideal R) < (↑a : Ideal R) ↔ b < a
⊢ DvdNotUnit (f a) (f b) ↔ b < a

Tactic:
rw [← Ideal.span_singleton_lt_span_singleton, ← hf, ← hf]

Premises used: Ideal.span_singleton_lt_span_singleton
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R
h : WellFounded.{u + 1} (α := R) DvdNotUnit
f : (I : { J : Ideal R // J.FG }) → R
hf : ∀ (I : { J : Ideal R // J.FG }), (↑I : Ideal R) = Ideal.span {f I}
a b : { N : Submodule R R // N.FG }
⊢ (↑b : Ideal R) < (↑a : Ideal R) ↔ b < a

Tactic:
rfl
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R
h : WellFounded.{u + 1} (α := R) DvdNotUnit
f : (I : { J : Ideal R // J.FG }) → R
hf : ∀ (I : { J : Ideal R // J.FG }), (↑I : Ideal R) = Ideal.span {f I}
⊢ RelEmbedding (β := R) (fun (x1 x2 : { N : Submodule R R // N.FG }) ↦ x2 < x1) DvdNotUnit

Tactic:
exact
        { toFun := f
          inj' := fun x y e => by ext1; rw [hf, hf, e]
          map_rel_iff' := by
            dsimp
            intro a b
            rw [← Ideal.span_singleton_lt_span_singleton, ← hf, ← hf]
            rfl }
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R
⊢ ∀ (a : WfDvdMonoid R), IsNoetherianRing R

Tactic:
tfae_have 4 → 1
    | ⟨h⟩ => by
      rw [isNoetherianRing_iff, isNoetherian_iff_fg_wellFounded]
      refine ⟨RelEmbedding.wellFounded ?_ h⟩
      have : ∀ I : { J : Ideal R // J.FG }, ∃ x : R, (I : Ideal R) = Ideal.span {x} :=
        fun ⟨I, hI⟩ => (IsBezout.isPrincipal_of_FG I hI).1
      choose f hf using this
      exact
        { toFun := f
          inj' := fun x y e => by ext1; rw [hf, hf, e]
          map_rel_iff' := by
            dsimp
            intro a b
            rw [← Ideal.span_singleton_lt_span_singleton, ← hf, ← hf]
            rfl }
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R
tfae_4_to_1 : ∀ (a : WfDvdMonoid R), IsNoetherianRing R
⊢ [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_have tfae_have₁ tfae_have₂ :
  ∀ (tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R),
    [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE
tfae_have₃ :
  ∀ (tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R)
    (tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R),
    [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE
tfae_have₄ :
  ∀ (tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R)
    (tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R)
    (tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R),
    [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE
tfae_have₅ :
  ∀ (tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R)
    (tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R)
    (tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R)
    (tfae_4_to_1 : ∀ (a : WfDvdMonoid R), IsNoetherianRing R),
    [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE
⊢ [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE

Tactic:
classical
    tfae_have 1 → 2
    | _ => inferInstance
    tfae_have 2 → 3
    | _ => inferInstance
    tfae_have 3 → 4
    | _ => inferInstance
    tfae_have 4 → 1
    | ⟨h⟩ => by
      rw [isNoetherianRing_iff, isNoetherian_iff_fg_wellFounded]
      refine ⟨RelEmbedding.wellFounded ?_ h⟩
      have : ∀ I : { J : Ideal R // J.FG }, ∃ x : R, (I : Ideal R) = Ideal.span {x} :=
        fun ⟨I, hI⟩ => (IsBezout.isPrincipal_of_FG I hI).1
      choose f hf using this
      exact
        { toFun := f
          inj' := fun x y e => by ext1; rw [hf, hf, e]
          map_rel_iff' := by
            dsimp
            intro a b
            rw [← Ideal.span_singleton_lt_span_singleton, ← hf, ← hf]
            rfl }
    tfae_finish
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a b : A
⊢ (counit : (a : A) → R) (a * b) =
    HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) a : R) ((counit : (a : A) → R) b : R)

Tactic:
DFunLike.congr_fun (DFunLike.congr_fun mul_compr₂_counit a) b

Premises used: DFunLike.congr_fun, Bialgebra.mul_compr₂_counit
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a b : A
⊢ (comul : (a : A) → A ⊗[R] A) (a * b) =
    HMul.hMul (α := A ⊗[R] A) (β := A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) a : A ⊗[R] A)
      ((comul : (a : A) → A ⊗[R] A) b : A ⊗[R] A)

Tactic:
DFunLike.congr_fun (DFunLike.congr_fun mul_compr₂_comul a) b

Premises used: DFunLike.congr_fun, Bialgebra.mul_compr₂_comul
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R_1 : Type u
A_1 : Type v
inst : CommSemiring R_1
inst_1 : Semiring A_1
inst_2 : Bialgebra R_1 A_1
R : Type u
A : Type v
inst_3 : CommSemiring R
inst_4 : Semiring A
inst_5 : Algebra R A
C : Coalgebra R A
counit_one : Eq.{u + 1} (α := R) ((counit : (a : A) → R) 1 : R) (1 : R)
counit_mul :
  ∀ {a b : A},
    (counit : (a : A) → R) (a * b) =
      HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) a : R) ((counit : (a : A) → R) b : R)
comul_one : Eq.{v + 1} (α := A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) 1) 1
comul_mul :
  ∀ {a b : A},
    (comul : (a : A) → A ⊗[R] A) (a * b) =
      HMul.hMul (α := A ⊗[R] A) (β := A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) a : A ⊗[R] A)
        ((comul : (a : A) → A ⊗[R] A) b : A ⊗[R] A)
h :
  ∀ (x x_1 : A),
    Eq.{u + 1} (α := R)
      ((((LinearMap.compr₂ (LinearMap.mul R A) counit : (a : A) → A →ₗ[R] R) x : A →ₗ[R] R) : (a : A) → R) x_1 : R)
      ((((LinearMap.compl₁₂ (LinearMap.mul R R) counit counit : (a : A) → A →ₗ[R] R) x : A →ₗ[R] R) : (a : A) → R) x_1 :
        R)
⊢ Eq (α := A →ₗ[R] A →ₗ[R] R) (LinearMap.compr₂ (LinearMap.mul R A) counit)
    (LinearMap.compl₁₂ (LinearMap.mul R R) counit counit)

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R_1 : Type u
A_1 : Type v
inst : CommSemiring R_1
inst_1 : Semiring A_1
inst_2 : Bialgebra R_1 A_1
R : Type u
A : Type v
inst_3 : CommSemiring R
inst_4 : Semiring A
inst_5 : Algebra R A
C : Coalgebra R A
counit_one : Eq.{u + 1} (α := R) ((counit : (a : A) → R) 1 : R) (1 : R)
counit_mul :
  ∀ {a b : A},
    (counit : (a : A) → R) (a * b) =
      HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) a : R) ((counit : (a : A) → R) b : R)
comul_one : Eq.{v + 1} (α := A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) 1) 1
comul_mul :
  ∀ {a b : A},
    (comul : (a : A) → A ⊗[R] A) (a * b) =
      HMul.hMul (α := A ⊗[R] A) (β := A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) a : A ⊗[R] A)
        ((comul : (a : A) → A ⊗[R] A) b : A ⊗[R] A)
x x_1 : A
⊢ Eq.{u + 1} (α := R)
    ((((LinearMap.compr₂ (LinearMap.mul R A) counit : (a : A) → A →ₗ[R] R) x : A →ₗ[R] R) : (a : A) → R) x_1 : R)
    ((((LinearMap.compl₁₂ (LinearMap.mul R R) counit counit : (a : A) → A →ₗ[R] R) x : A →ₗ[R] R) : (a : A) → R) x_1 :
      R)

Tactic:
counit_mul
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R_1 : Type u
A_1 : Type v
inst : CommSemiring R_1
inst_1 : Semiring A_1
inst_2 : Bialgebra R_1 A_1
R : Type u
A : Type v
inst_3 : CommSemiring R
inst_4 : Semiring A
inst_5 : Algebra R A
C : Coalgebra R A
counit_one : Eq.{u + 1} (α := R) ((counit : (a : A) → R) 1 : R) (1 : R)
counit_mul :
  ∀ {a b : A},
    (counit : (a : A) → R) (a * b) =
      HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) a : R) ((counit : (a : A) → R) b : R)
comul_one : Eq.{v + 1} (α := A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) 1) 1
comul_mul :
  ∀ {a b : A},
    (comul : (a : A) → A ⊗[R] A) (a * b) =
      HMul.hMul (α := A ⊗[R] A) (β := A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) a : A ⊗[R] A)
        ((comul : (a : A) → A ⊗[R] A) b : A ⊗[R] A)
x x_1 : A
⊢ Eq.{u + 1} (α := R)
    ((((LinearMap.compr₂ (LinearMap.mul R A) counit : (a : A) → A →ₗ[R] R) x : A →ₗ[R] R) : (a : A) → R) x_1 : R)
    ((((LinearMap.compl₁₂ (LinearMap.mul R R) counit counit : (a : A) → A →ₗ[R] R) x : A →ₗ[R] R) : (a : A) → R) x_1 :
      R)

Tactic:
exact counit_mul
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R_1 : Type u
A_1 : Type v
inst : CommSemiring R_1
inst_1 : Semiring A_1
inst_2 : Bialgebra R_1 A_1
R : Type u
A : Type v
inst_3 : CommSemiring R
inst_4 : Semiring A
inst_5 : Algebra R A
C : Coalgebra R A
counit_one : Eq.{u + 1} (α := R) ((counit : (a : A) → R) 1 : R) (1 : R)
counit_mul :
  ∀ {a b : A},
    (counit : (a : A) → R) (a * b) =
      HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) a : R) ((counit : (a : A) → R) b : R)
comul_one : Eq.{v + 1} (α := A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) 1) 1
comul_mul :
  ∀ {a b : A},
    (comul : (a : A) → A ⊗[R] A) (a * b) =
      HMul.hMul (α := A ⊗[R] A) (β := A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) a : A ⊗[R] A)
        ((comul : (a : A) → A ⊗[R] A) b : A ⊗[R] A)
h :
  ∀ (x x_1 : A),
    Eq (α := A ⊗[R] A)
      ((((LinearMap.compr₂ (LinearMap.mul R A) comul : (a : A) → A →ₗ[R] A ⊗[R] A) x : A →ₗ[R] A ⊗[R] A) :
            (a : A) → A ⊗[R] A)
          x_1 :
        A ⊗[R] A)
      ((((LinearMap.compl₁₂ (LinearMap.mul R (A ⊗[R] A)) comul comul : (a : A) → A →ₗ[R] A ⊗[R] A) x :
              A →ₗ[R] A ⊗[R] A) :
            (a : A) → A ⊗[R] A)
          x_1 :
        A ⊗[R] A)
⊢ Eq (α := A →ₗ[R] A →ₗ[R] A ⊗[R] A) (LinearMap.compr₂ (LinearMap.mul R A) comul)
    (LinearMap.compl₁₂ (LinearMap.mul R (A ⊗[R] A)) comul comul)

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R_1 : Type u
A_1 : Type v
inst : CommSemiring R_1
inst_1 : Semiring A_1
inst_2 : Bialgebra R_1 A_1
R : Type u
A : Type v
inst_3 : CommSemiring R
inst_4 : Semiring A
inst_5 : Algebra R A
C : Coalgebra R A
counit_one : Eq.{u + 1} (α := R) ((counit : (a : A) → R) 1 : R) (1 : R)
counit_mul :
  ∀ {a b : A},
    (counit : (a : A) → R) (a * b) =
      HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) a : R) ((counit : (a : A) → R) b : R)
comul_one : Eq.{v + 1} (α := A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) 1) 1
comul_mul :
  ∀ {a b : A},
    (comul : (a : A) → A ⊗[R] A) (a * b) =
      HMul.hMul (α := A ⊗[R] A) (β := A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) a : A ⊗[R] A)
        ((comul : (a : A) → A ⊗[R] A) b : A ⊗[R] A)
x x_1 : A
⊢ Eq (α := A ⊗[R] A)
    ((((LinearMap.compr₂ (LinearMap.mul R A) comul : (a : A) → A →ₗ[R] A ⊗[R] A) x : A →ₗ[R] A ⊗[R] A) :
          (a : A) → A ⊗[R] A)
        x_1 :
      A ⊗[R] A)
    ((((LinearMap.compl₁₂ (LinearMap.mul R (A ⊗[R] A)) comul comul : (a : A) → A →ₗ[R] A ⊗[R] A) x : A →ₗ[R] A ⊗[R] A) :
          (a : A) → A ⊗[R] A)
        x_1 :
      A ⊗[R] A)

Tactic:
comul_mul
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R_1 : Type u
A_1 : Type v
inst : CommSemiring R_1
inst_1 : Semiring A_1
inst_2 : Bialgebra R_1 A_1
R : Type u
A : Type v
inst_3 : CommSemiring R
inst_4 : Semiring A
inst_5 : Algebra R A
C : Coalgebra R A
counit_one : Eq.{u + 1} (α := R) ((counit : (a : A) → R) 1 : R) (1 : R)
counit_mul :
  ∀ {a b : A},
    (counit : (a : A) → R) (a * b) =
      HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) a : R) ((counit : (a : A) → R) b : R)
comul_one : Eq.{v + 1} (α := A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) 1) 1
comul_mul :
  ∀ {a b : A},
    (comul : (a : A) → A ⊗[R] A) (a * b) =
      HMul.hMul (α := A ⊗[R] A) (β := A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) a : A ⊗[R] A)
        ((comul : (a : A) → A ⊗[R] A) b : A ⊗[R] A)
x x_1 : A
⊢ Eq (α := A ⊗[R] A)
    ((((LinearMap.compr₂ (LinearMap.mul R A) comul : (a : A) → A →ₗ[R] A ⊗[R] A) x : A →ₗ[R] A ⊗[R] A) :
          (a : A) → A ⊗[R] A)
        x_1 :
      A ⊗[R] A)
    ((((LinearMap.compl₁₂ (LinearMap.mul R (A ⊗[R] A)) comul comul : (a : A) → A →ₗ[R] A ⊗[R] A) x : A →ₗ[R] A ⊗[R] A) :
          (a : A) → A ⊗[R] A)
        x_1 :
      A ⊗[R] A)

Tactic:
exact comul_mul
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
⊢ Eq (α := A →ₗ[R] R) (AlgHom.toLinearMap (counitAlgHom R A)) counit

Tactic:
rfl

Premises used: AlgHom.toLinearMap, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
⊢ Eq (α := A →ₗ[R] A ⊗[R] A) (AlgHom.toLinearMap (comulAlgHom R A)) comul

Tactic:
rfl

Premises used: AlgHom.toLinearMap, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
r : R
⊢ (counit : (a : A) → R) ((algebraMap R A : (a : R) → A) r : A) = r

Tactic:
(counitAlgHom R A).commutes r

Premises used: Bialgebra.counitAlgHom, AlgHom.commutes
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
r : R
⊢ Eq.{v + 1} (α := A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) ((algebraMap R A : (a : R) → A) r) : A ⊗[R] A)
    ((algebraMap R (A ⊗[R] A) : (a : R) → A ⊗[R] A) r : A ⊗[R] A)

Tactic:
(comulAlgHom R A).commutes r

Premises used: Bialgebra.comulAlgHom, AlgHom.commutes
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
n : ℕ
⊢ Eq.{u + 1} (α := R) ((counit : (a : A) → R) (↑n : A) : R) ((↑n : R) : R)

Tactic:
map_natCast (counitAlgHom R A) _

Premises used: Bialgebra.counitAlgHom, map_natCast
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
n : ℕ
⊢ Eq.{v + 1} (α := A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) (↑n : A)) (↑n : A ⊗[R] A)

Tactic:
map_natCast (comulAlgHom R A) _

Premises used: Bialgebra.comulAlgHom, map_natCast
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a : A
n : ℕ
⊢ (counit : (a : A) → R) (a ^ n) = HPow.hPow (α := R) ((counit : (a : A) → R) a : R) n

Tactic:
map_pow (counitAlgHom R A) a n

Premises used: map_pow, Bialgebra.counitAlgHom
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a : A
n : ℕ
⊢ (comul : (a : A) → A ⊗[R] A) (a ^ n) = HPow.hPow (α := A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) a : A ⊗[R] A) n

Tactic:
map_pow (comulAlgHom R A) a n

Premises used: Bialgebra.comulAlgHom, map_pow
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R : Type u
inst : CommSemiring R
h :
  Eq (α := R)
    (((LinearMap.compr₂ (LinearMap.mul R R) CoalgebraStruct.counit : (a : R) → R →ₗ[R] R) 1 : (a : R) → R) 1 : R)
    (((LinearMap.compl₁₂ (LinearMap.mul R R) CoalgebraStruct.counit CoalgebraStruct.counit : (a : R) → R →ₗ[R] R) 1 :
          (a : R) → R)
        1 :
      R)
⊢ Eq (α := R →ₗ[R] R →ₗ[R] R) (LinearMap.compr₂ (LinearMap.mul R R) CoalgebraStruct.counit)
    (LinearMap.compl₁₂ (LinearMap.mul R R) CoalgebraStruct.counit CoalgebraStruct.counit)

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := R)
    (((LinearMap.compr₂ (LinearMap.mul R R) CoalgebraStruct.counit : (a : R) → R →ₗ[R] R) 1 : (a : R) → R) 1 : R)
    (((LinearMap.compl₁₂ (LinearMap.mul R R) CoalgebraStruct.counit CoalgebraStruct.counit : (a : R) → R →ₗ[R] R) 1 :
          (a : R) → R)
        1 :
      R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R : Type u
inst : CommSemiring R
h :
  Eq (α := R ⊗[R] R)
    (((LinearMap.compr₂ (LinearMap.mul R R) CoalgebraStruct.comul : (a : R) → R →ₗ[R] R ⊗[R] R) 1 : (a : R) → R ⊗[R] R)
      1)
    (((LinearMap.compl₁₂ (LinearMap.mul R (R ⊗[R] R)) CoalgebraStruct.comul CoalgebraStruct.comul :
            (a : R) → R →ₗ[R] R ⊗[R] R)
          1 :
        (a : R) → R ⊗[R] R)
      1)
⊢ Eq (α := R →ₗ[R] R →ₗ[R] R ⊗[R] R) (LinearMap.compr₂ (LinearMap.mul R R) CoalgebraStruct.comul)
    (LinearMap.compl₁₂ (LinearMap.mul R (R ⊗[R] R)) CoalgebraStruct.comul CoalgebraStruct.comul)

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := R ⊗[R] R)
    (((LinearMap.compr₂ (LinearMap.mul R R) CoalgebraStruct.comul : (a : R) → R →ₗ[R] R ⊗[R] R) 1 : (a : R) → R ⊗[R] R)
      1)
    (((LinearMap.compl₁₂ (LinearMap.mul R (R ⊗[R] R)) CoalgebraStruct.comul CoalgebraStruct.comul :
            (a : R) → R →ₗ[R] R ⊗[R] R)
          1 :
        (a : R) → R ⊗[R] R)
      1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := R →ₐ[R] R) (counitAlgHom R R) (AlgHom.id R R)

Tactic:
rfl

Premises used: AlgHom.ofLinearMap, AlgHom.id, Bialgebra.counitAlgHom, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
⊢ Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)

Tactic:
RightInverse.injective counit_algebraMap

Premises used: Bialgebra.counit_algebraMap, Function.RightInverse.injective
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
⊢ Surjective.{u_2 + 1, u_1 + 1} (α := A) (β := R) (⇑CoalgebraStruct.counit : (a : A) → R)

Tactic:
RightInverse.surjective counit_algebraMap

Premises used: Bialgebra.counit_algebraMap, Function.RightInverse.surjective
-- Module: Mathlib.RingTheory.Bialgebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
inst_3 : Nontrivial R
⊢ Nontrivial A

Tactic:
(algebraMap_injective (R := R) _).nontrivial

Premises used: Function.Injective.nontrivial, Bialgebra.algebraMap_injective
-- 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)) 1 (toConv (comp (ofId R A) (counitAlgHom 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 C
inst_4 : Algebra R A
f g : WithConv (C →ₐ[R] A)
⊢ f * g =
    toConv
      (comp (lmul' R)
        (comp (Algebra.TensorProduct.map f.ofConv g.ofConv : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) (A ⊗[R] A))
          (comulAlgHom R C : C →ₐ[R] C ⊗[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 C
inst_4 : Algebra R A
f : WithConv (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 C
inst_4 : Algebra R A
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