awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.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 : AddCommMonoid C
inst_3 : Algebra R A
inst_4 : Module R C
inst_5 : Coalgebra R C
inst_6 : IsCocomm R C
f g : WithConv (C →ₗ[R] A)
x : C
h :
  Eq (α := A)
    ((mul' R A : (a : A ⊗[R] A) → A)
        ((f.ofConv ⊗ₘ g.ofConv : (a : C ⊗[R] C) → A ⊗[R] A) ((δ : (a : C) → C ⊗[R] C) x) : A ⊗[R] A) :
      A)
    (((g * f).ofConv : (a : C) → A) x : A)
h₁ :
  Eq (α := A)
    ((mul' R A : (a : A ⊗[R] A) → A)
        ((f.ofConv ⊗ₘ g.ofConv : (a : C ⊗[R] C) → A ⊗[R] A)
            ((TensorProduct.comm R C C : (a : C ⊗[R] C) → C ⊗[R] C) ((δ : (a : C) → C ⊗[R] C) x)) :
          A ⊗[R] A) :
      A)
    (((g * f).ofConv : (a : C) → A) x : A)
h₂ :
  Eq (α := A)
    ((mul' R A : (a : A ⊗[R] A) → A)
        ((TensorProduct.comm R A A : (a : A ⊗[R] A) → A ⊗[R] A)
            ((g.ofConv ⊗ₘ f.ofConv : (a : C ⊗[R] C) → A ⊗[R] A) ((δ : (a : C) → C ⊗[R] C) x)) :
          A ⊗[R] A) :
      A)
    (((g * f).ofConv : (a : C) → A) x : A)
⊢ Eq.{u_2 + 1} (α := A) (((f * g).ofConv : (a : C) → A) x : A) (((g * f).ofConv : (a : C) → A) x : A)
have h₃ : Eq (α := A)
  ((mul' R A : (a : A ⊗[R] A) → A)
      ((g.ofConv ⊗ₘ f.ofConv : (a : C ⊗[R] C) → A ⊗[R] A) ((δ : (a : C) → C ⊗[R] C) x) : A ⊗[R] A) :
    A)
  (((g * f).ofConv : (a : C) → A) x : A)
Tactic: rw [convMul_apply, ← comm_comul R x, map_comm, mul'_comm, convMul_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.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 : AddCommMonoid C
inst_3 : Algebra R A
inst_4 : Module R C
inst_5 : Coalgebra R C
inst_6 : IsCocomm R C
f g : WithConv (C →ₗ[R] A)
x : C
h :
  Eq (α := A)
    ((mul' R A : (a : A ⊗[R] A) → A)
        ((f.ofConv ⊗ₘ g.ofConv : (a : C ⊗[R] C) → A ⊗[R] A) ((δ : (a : C) → C ⊗[R] C) x) : A ⊗[R] A) :
      A)
    (((g * f).ofConv : (a : C) → A) x : A)
h₁ :
  Eq (α := A)
    ((mul' R A : (a : A ⊗[R] A) → A)
        ((f.ofConv ⊗ₘ g.ofConv : (a : C ⊗[R] C) → A ⊗[R] A)
            ((TensorProduct.comm R C C : (a : C ⊗[R] C) → C ⊗[R] C) ((δ : (a : C) → C ⊗[R] C) x)) :
          A ⊗[R] A) :
      A)
    (((g * f).ofConv : (a : C) → A) x : A)
h₂ :
  Eq (α := A)
    ((mul' R A : (a : A ⊗[R] A) → A)
        ((TensorProduct.comm R A A : (a : A ⊗[R] A) → A ⊗[R] A)
            ((g.ofConv ⊗ₘ f.ofConv : (a : C ⊗[R] C) → A ⊗[R] A) ((δ : (a : C) → C ⊗[R] C) x)) :
          A ⊗[R] A) :
      A)
    (((g * f).ofConv : (a : C) → A) x : A)
h₃ :
  Eq (α := A)
    ((mul' R A : (a : A ⊗[R] A) → A)
        ((g.ofConv ⊗ₘ f.ofConv : (a : C ⊗[R] C) → A ⊗[R] A) ((δ : (a : C) → C ⊗[R] C) x) : A ⊗[R] A) :
      A)
    (((g * f).ofConv : (a : C) → A) x : A)
⊢ Eq.{u_2 + 1} (α := A) (((f * g).ofConv : (a : C) → A) x : A) (((g * f).ofConv : (a : C) → A) x : A)
have h₄ : Eq (α := A)
  ((mul' R A : (a : A ⊗[R] A) → A)
      ((g.ofConv ⊗ₘ f.ofConv : (a : C ⊗[R] C) → A ⊗[R] A) ((δ : (a : C) → C ⊗[R] C) x) : A ⊗[R] A) :
    A)
  ((mul' R A : (a : A ⊗[R] A) → A)
      ((g.ofConv ⊗ₘ f.ofConv : (a : C ⊗[R] C) → A ⊗[R] A) ((δ : (a : C) → C ⊗[R] C) x) : A ⊗[R] A) :
    A)
Tactic: rw [convMul_apply, ← comm_comul R x, map_comm, mul'_comm, convMul_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : AddCommMonoid C
inst_4 : Module R A
inst_5 : Module R B
inst_6 : Module R C
inst_7 : CoalgebraStruct R A
inst_8 : CoalgebraStruct R B
inst_9 : CoalgebraStruct R C
e_1 e' e : A ≃ₗc[R] B
⊢ (↑(TensorProduct.congr e.toLinearEquiv e.toLinearEquiv).symm : TensorProduct R B B →ₗ[R] TensorProduct R A A) ∘ₗ
      comul =
    comul ∘ₗ (↑e.toLinearEquiv.symm : B →ₗ[R] A)
have rw : comul =
  (↑(TensorProduct.congr e.toLinearEquiv e.toLinearEquiv) : TensorProduct R A A →ₗ[R] TensorProduct R B B) ∘ₗ
    comul ∘ₗ (↑e.toLinearEquiv.symm : B →ₗ[R] A)
Tactic: rw [LinearEquiv.toLinearMap_symm_comp_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : AddCommMonoid C
inst_4 : Module R A
inst_5 : Module R B
inst_6 : Module R C
inst_7 : CoalgebraStruct R A
inst_8 : CoalgebraStruct R B
inst_9 : CoalgebraStruct R C
e_1 e' e : A ≃ₗc[R] B
⊢ comul =
    (↑(TensorProduct.congr e.toLinearEquiv e.toLinearEquiv) : TensorProduct R A A →ₗ[R] TensorProduct R B B) ∘ₗ
      comul ∘ₗ (↑e.toLinearEquiv.symm : B →ₗ[R] A)
have simp : comul =
  (comul ∘ₗ
      (↑(↑e : A →ₗc[R] B) :
        [inst_10 : FunLike (A →ₗc[R] B) A B] → [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B)) ∘ₗ
    (↑e.toLinearEquiv.symm : B →ₗ[R] A)
Tactic: simp only [TensorProduct.congr, toCoalgHom_eq_coe, CoalgHom.toLinearMap_eq_coe,
        LinearEquiv.ofLinear_toLinearMap, ← LinearMap.comp_assoc, CoalgHomClass.map_comp_comul]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : AddCommMonoid C
inst_4 : Module R A
inst_5 : Module R B
inst_6 : Module R C
inst_7 : CoalgebraStruct R A
inst_8 : CoalgebraStruct R B
inst_9 : CoalgebraStruct R C
e_1 e' e : A ≃ₗc[R] B
⊢ comul =
    (comul ∘ₗ
        (↑(↑e : A →ₗc[R] B) :
          [inst_10 : FunLike (A →ₗc[R] B) A B] → [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B)) ∘ₗ
      (↑e.toLinearEquiv.symm : B →ₗ[R] A)
have rw : comul = (comul ∘ₗ (↑e.toLinearEquiv : A →ₗ[R] B)) ∘ₗ (↑e.toLinearEquiv.symm : B →ₗ[R] A)
Tactic: rw [← toLinearEquiv_toLinearMap, LinearEquiv.comp_symm_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : AddCommMonoid C
inst_4 : Module R A
inst_5 : Module R B
inst_6 : Module R C
inst_7 : CoalgebraStruct R A
inst_8 : CoalgebraStruct R B
inst_9 : CoalgebraStruct R C
e_1 e' e : A ≃ₗc[R] B
rw : comul = (comul ∘ₗ (↑e.toLinearEquiv : A →ₗ[R] B)) ∘ₗ (↑e.toLinearEquiv.symm : B →ₗ[R] A)
⊢ comul =
    (comul ∘ₗ
        (↑(↑e : A →ₗc[R] B) :
          [inst_10 : FunLike (A →ₗc[R] B) A B] → [SemilinearMapClass (A →ₗc[R] B) (RingHom.id R) A B] → A →ₗ[R] B)) ∘ₗ
      (↑e.toLinearEquiv.symm : B →ₗ[R] A)
have rw₁ : Eq.{u_3 + 1} (α := B →ₗ[R] TensorProduct R B B) comul comul
Tactic: rw [← toLinearEquiv_toLinearMap, LinearEquiv.comp_symm_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
inst_4 : AddCommMonoid B
inst_5 : Module R B
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ Eq (α := B →ₗ[R] TensorProduct R B (TensorProduct R B B))
    ((↑(TensorProduct.assoc R B B B) :
        TensorProduct R (TensorProduct R B B) B →ₗ[R] TensorProduct R B (TensorProduct R B B)) ∘ₗ
      LinearMap.rTensor B comul ∘ₗ comul)
    (LinearMap.lTensor B comul ∘ₗ comul)
have simp : ((((↑(TensorProduct.assoc R B B B) :
            TensorProduct R (TensorProduct R B B) B →ₗ[R] TensorProduct R B (TensorProduct R B B)) ∘ₗ
          LinearMap.rTensor B
            ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A))) ∘ₗ
        TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
      comul) ∘ₗ
    (↑f.toLinearEquiv.symm : B →ₗ[R] A) =
  ((LinearMap.lTensor B
          ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
        TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
      comul) ∘ₗ
    (↑f.toLinearEquiv.symm : B →ₗ[R] A)
Tactic: simp only [← ((f : A ≃ₗ[R] B).comp_toLinearMap_symm_eq _ _).2 f.map_comp_comul,
      ← LinearMap.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
inst_4 : AddCommMonoid B
inst_5 : Module R B
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ ((((↑(TensorProduct.assoc R B B B) :
              TensorProduct R (TensorProduct R B B) B →ₗ[R] TensorProduct R B (TensorProduct R B B)) ∘ₗ
            LinearMap.rTensor B
              ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A))) ∘ₗ
          TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
        comul) ∘ₗ
      (↑f.toLinearEquiv.symm : B →ₗ[R] A) =
    ((LinearMap.lTensor B
            ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
          TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
        comul) ∘ₗ
      (↑f.toLinearEquiv.symm : B →ₗ[R] A)
have e_f : (((↑(TensorProduct.assoc R B B B) :
          TensorProduct R (TensorProduct R B B) B →ₗ[R] TensorProduct R B (TensorProduct R B B)) ∘ₗ
        LinearMap.rTensor B
          ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A))) ∘ₗ
      TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
    comul =
  (LinearMap.lTensor B
        ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
      TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
    comul
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
inst_4 : AddCommMonoid B
inst_5 : Module R B
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ (((↑(TensorProduct.assoc R B B B) :
            TensorProduct R (TensorProduct R B B) B →ₗ[R] TensorProduct R B (TensorProduct R B B)) ∘ₗ
          LinearMap.rTensor B
            ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A))) ∘ₗ
        TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
      comul =
    (LinearMap.lTensor B
          ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
        TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
      comul
have e_f : ∀ (x : A),
  Eq.{u_3 + 1} (α := TensorProduct R B (TensorProduct R B B))
    (((((↑(TensorProduct.assoc R B B B) :
                  TensorProduct R (TensorProduct R B B) B →ₗ[R] TensorProduct R B (TensorProduct R B B)) ∘ₗ
                LinearMap.rTensor B
                  ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A))) ∘ₗ
              TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
            comul :
          (a : A) → TensorProduct R B (TensorProduct R B B))
        x :
      TensorProduct R B (TensorProduct R B B))
    (((LinearMap.lTensor B
                ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
              TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
            comul :
          (a : A) → TensorProduct R B (TensorProduct R B B))
        x :
      TensorProduct R B (TensorProduct R B B))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
inst_4 : AddCommMonoid B
inst_5 : Module R B
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ Eq (α := B →ₗ[R] TensorProduct R R B) (LinearMap.rTensor B counit ∘ₗ comul)
    ((TensorProduct.mk R R B : (a : R) → B →ₗ[R] TensorProduct R R B) 1)
have simp_rw : (LinearMap.rTensor B (counit ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
      TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
    comul =
  (TensorProduct.mk R R B : (a : R) → B →ₗ[R] TensorProduct R R B) 1 ∘ₗ f.toLinearMap
Tactic: simp_rw [(f.toLinearEquiv.eq_comp_toLinearMap_symm _ _).2 f.counit_comp,
      ← (f.toLinearEquiv.comp_toLinearMap_symm_eq _ _).2 f.map_comp_comul, ← LinearMap.comp_assoc,
      f.toLinearEquiv.comp_toLinearMap_symm_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
inst_4 : AddCommMonoid B
inst_5 : Module R B
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ (LinearMap.rTensor B (counit ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
        TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
      comul =
    (TensorProduct.mk R R B : (a : R) → B →ₗ[R] TensorProduct R R B) 1 ∘ₗ f.toLinearMap
have h : ∀ (x : A),
  Eq (α := TensorProduct R R B)
    (((LinearMap.rTensor B (counit ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
              TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
            comul :
          (a : A) → TensorProduct R R B)
        x :
      TensorProduct R R B)
    (((TensorProduct.mk R R B : (a : R) → B →ₗ[R] TensorProduct R R B) 1 ∘ₗ f.toLinearMap :
          (a : A) → TensorProduct R R B)
        x :
      TensorProduct R R B)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
inst_4 : AddCommMonoid B
inst_5 : Module R B
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ Eq (α := B →ₗ[R] TensorProduct R B R) (LinearMap.lTensor B counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R B R) : (a : R) → B →ₗ[R] TensorProduct R B R) 1)
have simp_rw : (LinearMap.lTensor B (counit ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
      TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
    comul =
  (LinearMap.flip (TensorProduct.mk R B R) : (a : R) → B →ₗ[R] TensorProduct R B R) 1 ∘ₗ f.toLinearMap
Tactic: simp_rw [(f.toLinearEquiv.eq_comp_toLinearMap_symm _ _).2 f.counit_comp,
      ← (f.toLinearEquiv.comp_toLinearMap_symm_eq _ _).2 f.map_comp_comul, ← LinearMap.comp_assoc,
      f.toLinearEquiv.comp_toLinearMap_symm_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
inst_4 : AddCommMonoid B
inst_5 : Module R B
inst_6 : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ (LinearMap.lTensor B (counit ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
        TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
      comul =
    (LinearMap.flip (TensorProduct.mk R B R) : (a : R) → B →ₗ[R] TensorProduct R B R) 1 ∘ₗ f.toLinearMap
have h : ∀ (x : A),
  Eq (α := TensorProduct R B R)
    (((LinearMap.lTensor B (counit ∘ₗ (↑f.toLinearEquiv.symm : B →ₗ[R] A)) ∘ₗ
              TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
            comul :
          (a : A) → TensorProduct R B R)
        x :
      TensorProduct R B R)
    (((LinearMap.flip (TensorProduct.mk R B R) : (a : R) → B →ₗ[R] TensorProduct R B R) 1 ∘ₗ f.toLinearMap :
          (a : A) → TensorProduct R B R)
        x :
      TensorProduct R B R)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : Module R B
inst_6 : Coalgebra R B
a : A
inst_7 : FunLike F A B
inst_8 : CoalgHomClass F R A B
f : F
ha : IsGroupLikeElem R a
⊢ Eq.{u_2 + 1} (α := R) ((counit : (a : B) → R) ((f : (a : A) → B) a : B) : R) (1 : R)
have rw : Eq.{u_2 + 1} (α := R) ((counit : (a : A) → R) a : R) (1 : R)
Tactic: rw [CoalgHomClass.counit_comp_apply, ha.counit_eq_one]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : Module R B
inst_6 : Coalgebra R B
a : A
inst_7 : FunLike F A B
inst_8 : CoalgHomClass F R A B
f : F
ha : IsGroupLikeElem R a
rw : Eq.{u_2 + 1} (α := R) ((counit : (a : A) → R) a : R) (1 : R)
⊢ Eq.{u_2 + 1} (α := R) ((counit : (a : B) → R) ((f : (a : A) → B) a : B) : R) (1 : R)
have rw₁ : Eq.{u_2 + 1} (α := R) 1 1
Tactic: rw [CoalgHomClass.counit_comp_apply, ha.counit_eq_one]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : Module R B
inst_6 : Coalgebra R B
a : A
inst_7 : FunLike F A B
inst_8 : CoalgHomClass F R A B
f : F
ha : IsGroupLikeElem R a
⊢ Eq.{u_4 + 1} (α := B ⊗[R] B) ((comul : (a : B) → B ⊗[R] B) ((f : (a : A) → B) a) : B ⊗[R] B)
    ((f : (a : A) → B) a ⊗ₜ[R] (f : (a : A) → B) a : B ⊗[R] B)
have rw : Eq.{u_4 + 1} (α := B ⊗[R] B)
  (((TensorProduct.map (↑f : [inst_9 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
            (↑f : [inst_9 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
          LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) (A ⊗[R] A) (B ⊗[R] B)) :
        (a : A ⊗[R] A) → B ⊗[R] B)
      (a ⊗ₜ[R] a) :
    B ⊗[R] B)
  ((f : (a : A) → B) a ⊗ₜ[R] (f : (a : A) → B) a : B ⊗[R] B)
Tactic: rw [← CoalgHomClass.map_comp_comul_apply, ha.comul_eq_tmul_self]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
⊢ LinearIndepOn.{u_3, u_2, u_3} (ι := A) R id {a : A | IsGroupLikeElem R a}
have rw : ∀ (t : Finset A), (↑t : Set A) ⊆ {a : A | IsGroupLikeElem R a} → LinearIndepOn R id (↑t : Set A)
Tactic: rw [linearIndepOn_iff_linearIndepOn_finset]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (hypothesis)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ih : ∀ (hs : (↑s : Set A) ⊆ {a : A | IsGroupLikeElem R a}), LinearIndepOn R id (↑s : Set A)
hs : (↑(Finset.cons a s has) : Set A) ⊆ {a : A | IsGroupLikeElem R a}
⊢ LinearIndepOn R id (↑(Finset.cons a s has) : Set A)
have hs₁ : IsGroupLikeElem R a ∧ ∀ a ∈ s, IsGroupLikeElem R a
Tactic: simp only [Finset.cons_eq_insert, Finset.coe_insert, Set.subset_def, Set.mem_insert_iff,
    Finset.mem_coe, Set.mem_setOf_eq, forall_eq_or_imp] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (hypothesis)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ih : ∀ (hs : (↑s : Set A) ⊆ {a : A | IsGroupLikeElem R a}), LinearIndepOn R id (↑s : Set A)
hs : IsGroupLikeElem R a ∧ ∀ a ∈ s, IsGroupLikeElem R a
⊢ LinearIndepOn R id (↑(Finset.cons a s has) : Set A)
have ha : IsGroupLikeElem R a
Tactic: obtain ⟨ha, hs⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (hypothesis)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ih : ∀ (hs : (↑s : Set A) ⊆ {a : A | IsGroupLikeElem R a}), LinearIndepOn R id (↑s : Set A)
hs : IsGroupLikeElem R a ∧ ∀ a ∈ s, IsGroupLikeElem R a
ha : IsGroupLikeElem R a
⊢ LinearIndepOn R id (↑(Finset.cons a s has) : Set A)
have hs₁ : ∀ a ∈ s, IsGroupLikeElem R a
Tactic: obtain ⟨ha, hs⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (hypothesis)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ih : ∀ (hs : (↑s : Set A) ⊆ {a : A | IsGroupLikeElem R a}), LinearIndepOn R id (↑s : Set A)
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
⊢ LinearIndepOn R id (↑(Finset.cons a s has) : Set A)
have ih₁ : LinearIndepOn R id (↑s : Set A)
Tactic: specialize ih hs
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
ih : LinearIndepOn R id (↑s : Set A)
⊢ LinearIndepOn R id (↑(Finset.cons a s has) : Set A)
have cons : LinearIndepOn R id (insert a (↑s : Set A))
Tactic: rw [Finset.coe_cons]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
ih : LinearIndepOn R id (↑s : Set A)
⊢ LinearIndepOn R id (insert a (↑s : Set A))
have cons : ∀ (r : R), Membership.mem (γ := Submodule R A) (span R (↑s : Set A)) (r • a) → r = 0
Tactic: refine ih.id_insert' ?_
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
ih : LinearIndepOn R id (↑s : Set A)
⊢ ∀ (r : R), Membership.mem (γ := Submodule R A) (span R (↑s : Set A)) (r • a) → r = 0
have cons : ∀ (r : R) (x : A → R), support x ⊆ (↑s : Set A) → ∑ a ∈ s, x a • a = r • a → r = 0
Tactic: simp only [mem_span_finset, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (hypothesis)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
ih : LinearIndepOn R id (↑s : Set A)
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
⊢ d = 0
have ih₁ : LinearIndepOn R (M := A ⊗[R] A) (fun (i : A × A) ↦ id i.1 ⊗ₜ[R] id i.2) ((↑s : Set A) ×ˢ (↑s : Set A))
Tactic: replace ih := ih.tmul_of_isDomain ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.GroupLike (hypothesis)
Goal:
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : Coalgebra R A
inst_5 : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih : LinearIndepOn R (M := A ⊗[R] A) (fun (i : A × A) ↦ id i.1 ⊗ₜ[R] id i.2) ((↑s : Set A) ×ˢ (↑s : Set A))
⊢ d = 0
have ih₁ : ∀ (f g : A × A → R),
  Eq (α := A ⊗[R] A) (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (f x) (x.1 ⊗ₜ[R] x.2))
      (∑ x ∈ s ×ˢ s, HSMul.hSMul (β := A ⊗[R] A) (g x) (x.1 ⊗ₜ[R] x.2)) →
    ∀ i ∈ s ×ˢ s, f i = g i
Tactic: simp_rw [← Finset.coe_product, linearIndepOn_finset_iffₛ, id] at ih
Cleared hypotheses: ih