awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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
⊢ (↑x : Submodule R R) = (↑y : Submodule R R)
have a : Ideal.span {f x} = (↑y : Submodule R R)
Tactic: rw [hf, hf, e]
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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)
⊢ (↑x : Submodule R R) = (↑y : Submodule R R)
have a₁ : Eq (α := Submodule R R) (Ideal.span {f x}) (Ideal.span {f y})
Tactic: rw [hf, hf, e]
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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})
⊢ (↑x : Submodule R R) = (↑y : Submodule R R)
have a₂ : Eq (α := Submodule R R) (Ideal.span {f y}) (Ideal.span {f y})
Tactic: rw [hf, hf, e]
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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 }},
    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
have dsimp : ∀ {a b : { N : Submodule R R // N.FG }}, DvdNotUnit (f a) (f b) ↔ b < a
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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 }
⊢ DvdNotUnit (f a) (f b) ↔ b < a
have rw : (↑b : Ideal R) < (↑a : Ideal R) ↔ b < a
Tactic: rw [← Ideal.span_singleton_lt_span_singleton, ← hf, ← hf]
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (hypothesis)
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
⊢ [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE
have tfae_4_to_1 : ∀ (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 }
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
⊢ [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE
have tfae_have : ∀ (tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R),
  [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
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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
⊢ [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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
⊢ [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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
⊢ [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.Basic (goal)
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)
⊢ Eq (α := A →ₗ[R] A →ₗ[R] R) (LinearMap.compr₂ (LinearMap.mul R A) counit)
    (LinearMap.compl₁₂ (LinearMap.mul R R) counit counit)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.Basic (goal)
Goal:
R : Type u
inst : CommSemiring 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.Convolution (goal)
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
⊢ 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)
have 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 sorry : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.Convolution (goal)
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
⊢ 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)
have 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 sorry : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.Convolution (goal)
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
⊢ 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)
have 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 sorry : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.Convolution (goal)
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
⊢ 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)
have 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 sorry : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A)
            (includeLeft : C →ₐ[R] C ⊗[R] C) :
          (a : C) → A)
        x :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.Convolution (goal)
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)
⊢ 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)
have 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 sorry : AlgHom.{u_1, u_4, u_2} R (C ⊗[R] C) A))
            includeRight :
          (a : C) → A)
        x :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.Convolution (goal)
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)
⊢ h.comp (f * g).ofConv = (toConv (h.comp f.ofConv) * toConv (h.comp g.ofConv)).ofConv
have a : (h.comp (f * g).ofConv).toLinearMap = (toConv (h.comp f.ofConv) * toConv (h.comp g.ofConv)).ofConv.toLinearMap
Tactic: apply toLinearMap_injective
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.Convolution (goal)
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)
⊢ (h.comp (f * g).ofConv).toLinearMap = (toConv (h.comp f.ofConv) * toConv (h.comp g.ofConv)).ofConv.toLinearMap
have a : toConv (h.comp (f * g).ofConv).toLinearMap =
  toConv (toConv (h.comp f.ofConv) * toConv (h.comp g.ofConv)).ofConv.toLinearMap
Tactic: apply WithConv.toConv_injective
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.Convolution (goal)
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.comp (f * g).ofConv).toLinearMap =
    toConv (toConv (h.comp f.ofConv) * toConv (h.comp g.ofConv)).ofConv.toLinearMap
have 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: rw [AlgHom.comp_toLinearMap, ← ofConv_toConv (f * g).ofConv.toLinearMap, toLinearMap_convMul]
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.Equiv (goal)
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)
⊢ AlgHom.comp (counitAlgHom R B) (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B) = counitAlgHom R A
have 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)
Tactic: ext