awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
f : WithConv (E →ₗ[R] F)
simp_rw :
  star f = f ↔
    ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
simp_rw₁ :
  (star f).ofConv = f.ofConv ↔
    ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
simp_rw₂ :
  (∀ (x : E), Eq.{u_3 + 1} (α := F) (((star f).ofConv : (a : E) → F) x : F) ((f.ofConv : (a : E) → F) x : F)) ↔
    ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
⊢ IsSelfAdjoint f ↔
    ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
have simp_rw₃ : (∀ (x : E), Eq.{u_3 + 1} (α := F) (star ((f.ofConv : (a : E) → F) (star x)) : F) ((f.ofConv : (a : E) → F) x : F)) ↔
  ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
Tactic: simp_rw [IsSelfAdjoint, WithConv.ext_iff, LinearMap.ext_iff, intrinsicStar_apply,
   star_eq_iff_star_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
f : WithConv (E →ₗ[R] F)
simp_rw :
  star f = f ↔
    ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
simp_rw₁ :
  (star f).ofConv = f.ofConv ↔
    ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
simp_rw₂ :
  (∀ (x : E), Eq.{u_3 + 1} (α := F) (((star f).ofConv : (a : E) → F) x : F) ((f.ofConv : (a : E) → F) x : F)) ↔
    ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
simp_rw₃ :
  (∀ (x : E), Eq.{u_3 + 1} (α := F) (star ((f.ofConv : (a : E) → F) (star x)) : F) ((f.ofConv : (a : E) → F) x : F)) ↔
    ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
⊢ IsSelfAdjoint f ↔
    ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
have simp_rw₄ : (∀ (x : E), Eq.{u_3 + 1} (α := F) (star ((f.ofConv : (a : E) → F) x) : F) ((f.ofConv : (a : E) → F) (star x) : F)) ↔
  ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
Tactic: simp_rw [IsSelfAdjoint, WithConv.ext_iff, LinearMap.ext_iff, intrinsicStar_apply,
   star_eq_iff_star_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
G : Type u_4
inst_10 : AddCommMonoid G
inst_11 : Module R G
inst_12 : StarAddMonoid G
inst_13 : StarModule R G
f : WithConv (E →ₗ[R] F)
g : WithConv (G →ₗ[R] E)
⊢ star (toConv (f.ofConv ∘ₗ g.ofConv)) = toConv ((star f).ofConv ∘ₗ (star g).ofConv)
have h : ∀ (x : G),
  Eq.{u_3 + 1} (α := F) (((star (toConv (f.ofConv ∘ₗ g.ofConv))).ofConv : (a : G) → F) x : F)
    (((toConv ((star f).ofConv ∘ₗ (star g).ofConv)).ofConv : (a : G) → F) x : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
⊢ Eq.{u_2 + 1} (α := WithConv (E →ₗ[R] E)) (star (toConv id)) (toConv id)
have h : ∀ (x : E), Eq (α := E) ((ofConv (star (toConv id)) : (a : E) → E) x : E) ((ofConv (toConv id) : (a : E) → E) x : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : InvolutiveStar R
E : Type u_6
inst_2 : NonUnitalNonAssocSemiring E
inst_3 : StarRing E
inst_4 : Module R E
inst_5 : StarModule R E
inst_6 : SMulCommClass R E E
inst_7 : IsScalarTower R E E
x : E
⊢ Eq (α := WithConv (E →ₗ[R] E)) (star (toConv (mulLeft R x))) (toConv (mulRight R (star x)))
have h : ∀ (x_1 : E),
  Eq (α := E) ((ofConv (star (toConv (mulLeft R x))) : (a : E) → E) x_1 : E)
    ((ofConv (toConv (mulRight R (star x))) : (a : E) → E) x_1 : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : InvolutiveStar R
E : Type u_6
inst_2 : NonUnitalNonAssocSemiring E
inst_3 : StarRing E
inst_4 : Module R E
inst_5 : StarModule R E
inst_6 : SMulCommClass R E E
inst_7 : IsScalarTower R E E
x : E
⊢ Eq (α := WithConv (E →ₗ[R] E)) (star (toConv (mulRight R x))) (toConv (mulLeft R (star x)))
have rw : Eq (α := WithConv (E →ₗ[R] E)) (star (toConv (mulLeft R (star x)))) (toConv (mulRight R x))
Tactic: rw [star_eq_iff_star_eq, intrinsicStar_mulLeft, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : InvolutiveStar R
E : Type u_6
inst_2 : NonUnitalNonAssocSemiring E
inst_3 : StarRing E
inst_4 : Module R E
inst_5 : StarModule R E
inst_6 : SMulCommClass R E E
inst_7 : IsScalarTower R E E
x : E
rw : Eq (α := WithConv (E →ₗ[R] E)) (star (toConv (mulLeft R (star x)))) (toConv (mulRight R x))
⊢ Eq (α := WithConv (E →ₗ[R] E)) (star (toConv (mulRight R x))) (toConv (mulLeft R (star x)))
have rw₁ : Eq (α := WithConv (E →ₗ[R] E)) (toConv (mulRight R (star (star x)))) (toConv (mulRight R x))
Tactic: rw [star_eq_iff_star_eq, intrinsicStar_mulLeft, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : InvolutiveStar R
E : Type u_6
inst_2 : NonUnitalNonAssocSemiring E
inst_3 : StarRing E
inst_4 : Module R E
inst_5 : StarModule R E
inst_6 : SMulCommClass R E E
inst_7 : IsScalarTower R E E
x : E
rw : Eq (α := WithConv (E →ₗ[R] E)) (star (toConv (mulLeft R (star x)))) (toConv (mulRight R x))
rw₁ : Eq (α := WithConv (E →ₗ[R] E)) (toConv (mulRight R (star (star x)))) (toConv (mulRight R x))
⊢ Eq (α := WithConv (E →ₗ[R] E)) (star (toConv (mulRight R x))) (toConv (mulLeft R (star x)))
have rw₂ : Eq (α := WithConv (E →ₗ[R] E)) (toConv (mulRight R x)) (toConv (mulRight R x))
Tactic: rw [star_eq_iff_star_eq, intrinsicStar_mulLeft, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
G : Type u_4
inst_10 : AddCommMonoid G
inst_11 : Module R G
inst_12 : StarAddMonoid G
inst_13 : StarModule R G
inst_14 : SMulCommClass R R F
x : R
x_1 : WithConv (E →ₗ[R] F)
⊢ star (x • x_1) = star x • star x_1
have h : ∀ (x_2 : E),
  Eq.{u_3 + 1} (α := F) (((star (x • x_1)).ofConv : (a : E) → F) x_2 : F)
    (((star x • star x_1).ofConv : (a : E) → F) x_2 : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid E
inst_3 : StarAddMonoid E
inst_4 : Module R E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : StarAddMonoid F
inst_8 : Module R F
inst_9 : StarModule R F
inst_10 : AddCommMonoid G
inst_11 : StarAddMonoid G
inst_12 : Module R G
inst_13 : StarModule R G
f : WithConv (F →ₗ[R] G)
⊢ Eq (α := WithConv (TensorProduct R E F →ₗ[R] TensorProduct R E G)) (star (toConv (lTensor E f.ofConv)))
    (toConv (lTensor E (star f).ofConv))
have h : ∀ (x : E) (x_1 : F),
  Eq (α := TensorProduct R E G)
    (((((TensorProduct.AlgebraTensorModule.curry (ofConv (star (toConv (lTensor E f.ofConv)))) :
                  E →ₗ[R] F →ₗ[R] TensorProduct R E G) :
                (a : E) → F →ₗ[R] TensorProduct R E G)
              x :
            F →ₗ[R] TensorProduct R E G) :
          (a : F) → TensorProduct R E G)
        x_1 :
      TensorProduct R E G)
    (((((TensorProduct.AlgebraTensorModule.curry (ofConv (toConv (lTensor E (star f).ofConv))) :
                  E →ₗ[R] F →ₗ[R] TensorProduct R E G) :
                (a : E) → F →ₗ[R] TensorProduct R E G)
              x :
            F →ₗ[R] TensorProduct R E G) :
          (a : F) → TensorProduct R E G)
        x_1 :
      TensorProduct R E G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid E
inst_3 : StarAddMonoid E
inst_4 : Module R E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : StarAddMonoid F
inst_8 : Module R F
inst_9 : StarModule R F
inst_10 : AddCommMonoid G
inst_11 : StarAddMonoid G
inst_12 : Module R G
inst_13 : StarModule R G
f : WithConv (E →ₗ[R] F)
⊢ Eq (α := WithConv (TensorProduct R E G →ₗ[R] TensorProduct R F G)) (star (toConv (rTensor G f.ofConv)))
    (toConv (rTensor G (star f).ofConv))
have h : ∀ (x : E) (x_1 : G),
  Eq (α := TensorProduct R F G)
    (((((TensorProduct.AlgebraTensorModule.curry (ofConv (star (toConv (rTensor G f.ofConv)))) :
                  E →ₗ[R] G →ₗ[R] TensorProduct R F G) :
                (a : E) → G →ₗ[R] TensorProduct R F G)
              x :
            G →ₗ[R] TensorProduct R F G) :
          (a : G) → TensorProduct R F G)
        x_1 :
      TensorProduct R F G)
    (((((TensorProduct.AlgebraTensorModule.curry (ofConv (toConv (rTensor G (star f).ofConv))) :
                  E →ₗ[R] G →ₗ[R] TensorProduct R F G) :
                (a : E) → G →ₗ[R] TensorProduct R F G)
              x :
            G →ₗ[R] TensorProduct R F G) :
          (a : G) → TensorProduct R F G)
        x_1 :
      TensorProduct R F G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
E : Type u_2
inst : AddCommMonoid E
inst_1 : StarAddMonoid E
S : Type u_5
inst_2 : Semiring S
inst_3 : StarAddMonoid S
inst_4 : StarModule S S
inst_5 : Module S E
inst_6 : StarModule S E
a : E
⊢ Eq (α := WithConv (S →ₗ[S] E)) (star (toConv (toSpanSingleton S E a))) (toConv (toSpanSingleton S E (star a)))
have h : Eq.{u_2 + 1} (α := E) ((ofConv (star (toConv (toSpanSingleton S E a))) : (a : S) → E) 1 : E)
  ((ofConv (toConv (toSpanSingleton S E (star a))) : (a : S) → E) 1 : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
E : Type u_2
F : Type u_3
inst : AddCommMonoid E
inst_1 : StarAddMonoid E
inst_2 : AddCommMonoid F
inst_3 : StarAddMonoid F
S : Type u_5
inst_4 : Semiring S
inst_5 : StarAddMonoid S
inst_6 : StarModule S S
inst_7 : Module S E
inst_8 : StarModule S E
inst_9 : Module S F
inst_10 : StarModule S F
f : WithConv (E →ₗ[S] S)
x : F
⊢ Eq (α := WithConv (E →ₗ[S] F)) (star (toConv (f.ofConv.smulRight x))) (toConv ((star f).ofConv.smulRight (star x)))
have h : ∀ (x_1 : E),
  Eq.{u_3 + 1} (α := F) ((ofConv (star (toConv (f.ofConv.smulRight x))) : (a : E) → F) x_1 : F)
    ((ofConv (toConv ((star f).ofConv.smulRight (star x))) : (a : E) → F) x_1 : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_5
A : Type u_6
C : Type u_7
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
inst_6 : StarRing A
inst_7 : StarModule R A
inst_8 : AddCommMonoid C
inst_9 : Module R C
inst_10 : StarAddMonoid C
inst_11 : StarModule R C
inst_12 : CoalgebraStruct R C
h :
  Eq (α := WithConv (C →ₗ[R] C ⊗[R] C)) (star (toConv comul))
    (toConv ((↑(TensorProduct.comm R C C) : C ⊗[R] C →ₗ[R] C ⊗[R] C) ∘ₗ comul))
f g : WithConv (C →ₗ[R] A)
⊢ star (f * g) = star g * star f
have simp_rw : toConv
    ((mul' R A ∘ₗ (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A)) ∘ₗ
      ((↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A) ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv) ∘ₗ
        comul) =
  toConv (mul' R A ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv ∘ₗ comul)
Tactic: simp_rw [convMul_def, intrinsicStar_comp', intrinsicStar_mul', intrinsicStar_map,
    h, comp_assoc, ← comp_assoc _ _ (map _ _), map_comp_comm_eq,
    ← comp_assoc _ (TensorProduct.comm R A A).toLinearMap]
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_5
A : Type u_6
C : Type u_7
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
inst_6 : StarRing A
inst_7 : StarModule R A
inst_8 : AddCommMonoid C
inst_9 : Module R C
inst_10 : StarAddMonoid C
inst_11 : StarModule R C
inst_12 : CoalgebraStruct R C
h :
  Eq (α := WithConv (C →ₗ[R] C ⊗[R] C)) (star (toConv comul))
    (toConv ((↑(TensorProduct.comm R C C) : C ⊗[R] C →ₗ[R] C ⊗[R] C) ∘ₗ comul))
f g : WithConv (C →ₗ[R] A)
⊢ toConv
      ((mul' R A ∘ₗ (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A)) ∘ₗ
        ((↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A) ∘ₗ
            TensorProduct.map (star g).ofConv (star f).ofConv) ∘ₗ
          comul) =
    toConv (mul' R A ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv ∘ₗ comul)
have h₁ : ∀ (x : C),
  Eq.{u_6 + 1} (α := A)
    (((toConv
              ((mul' R A ∘ₗ (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A)) ∘ₗ
                ((↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A) ∘ₗ
                    TensorProduct.map (star g).ofConv (star f).ofConv) ∘ₗ
                  comul)).ofConv :
          (a : C) → A)
        x :
      A)
    (((toConv (mul' R A ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv ∘ₗ comul)).ofConv : (a : C) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
n : Type u_8
inst_2 : DecidableEq n
B : n → Type u_9
inst_3 : (i : n) → AddCommMonoid (B i)
inst_4 : (i : n) → Module.{u_5, u_9} R (B i)
inst_5 : (i : n) → StarAddMonoid (B i)
inst_6 : ∀ (i : n), StarModule.{u_5, u_9} R (B i)
inst_7 : Fintype n
inst_8 : (i : n) → CoalgebraStruct.{u_5, u_9} R (B i)
h :
  ∀ (i : n),
    Eq.{u_9 + 1} (α := WithConv (B i →ₗ[R] B i ⊗[R] B i)) (star (toConv comul))
      (toConv ((↑(TensorProduct.comm R (B i) (B i)) : B i ⊗[R] B i →ₗ[R] B i ⊗[R] B i) ∘ₗ comul))
⊢ Eq (α := WithConv (((i : n) → B i) →ₗ[R] ((i : n) → B i) ⊗[R] ((i : n) → B i))) (star (toConv comul))
    (toConv
      ((↑(TensorProduct.comm R ((i : n) → B i) ((i : n) → B i)) :
          ((i : n) → B i) ⊗[R] ((i : n) → B i) →ₗ[R] ((i : n) → B i) ⊗[R] ((i : n) → B i)) ∘ₗ
        comul))
have h₁ : ∀ (i : n) (x : B i),
  Eq (α := ((i : n) → B i) ⊗[R] ((i : n) → B i))
    ((ofConv (star (toConv comul)) ∘ₗ single R B i : (a : B i) → ((i : n) → B i) ⊗[R] ((i : n) → B i)) x :
      ((i : n) → B i) ⊗[R] ((i : n) → B i))
    ((ofConv
              (toConv
                ((↑(TensorProduct.comm R ((i : n) → B i) ((i : n) → B i)) :
                    ((i : n) → B i) ⊗[R] ((i : n) → B i) →ₗ[R] ((i : n) → B i) ⊗[R] ((i : n) → B i)) ∘ₗ
                  comul)) ∘ₗ
            single R B i :
          (a : B i) → ((i : n) → B i) ⊗[R] ((i : n) → B i))
        x :
      ((i : n) → B i) ⊗[R] ((i : n) → B i))
Tactic: ext i x
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (hypothesis)
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
n : Type u_8
inst_2 : DecidableEq n
B : n → Type u_9
inst_3 : (i : n) → AddCommMonoid (B i)
inst_4 : (i : n) → Module.{u_5, u_9} R (B i)
inst_5 : (i : n) → StarAddMonoid (B i)
inst_6 : ∀ (i : n), StarModule.{u_5, u_9} R (B i)
inst_7 : Fintype n
inst_8 : (i : n) → CoalgebraStruct.{u_5, u_9} R (B i)
h :
  ∀ (i : n),
    Eq.{u_9 + 1} (α := WithConv (B i →ₗ[R] B i ⊗[R] B i)) (star (toConv comul))
      (toConv ((↑(TensorProduct.comm R (B i) (B i)) : B i ⊗[R] B i →ₗ[R] B i ⊗[R] B i) ∘ₗ comul))
i : n
x : B i
⊢ Eq (α := ((i : n) → B i) ⊗[R] ((i : n) → B i))
    ((ofConv (star (toConv comul)) ∘ₗ single R B i : (a : B i) → ((i : n) → B i) ⊗[R] ((i : n) → B i)) x :
      ((i : n) → B i) ⊗[R] ((i : n) → B i))
    ((ofConv
              (toConv
                ((↑(TensorProduct.comm R ((i : n) → B i) ((i : n) → B i)) :
                    ((i : n) → B i) ⊗[R] ((i : n) → B i) →ₗ[R] ((i : n) → B i) ⊗[R] ((i : n) → B i)) ∘ₗ
                  comul)) ∘ₗ
            single R B i :
          (a : B i) → ((i : n) → B i) ⊗[R] ((i : n) → B i))
        x :
      ((i : n) → B i) ⊗[R] ((i : n) → B i))
have this : Eq (α := B i ⊗[R] B i) (star ((comul : (a : B i) → B i ⊗[R] B i) (star x)) : B i ⊗[R] B i)
  ((TensorProduct.comm R (B i) (B i) : (a : B i ⊗[R] B i) → B i ⊗[R] B i) ((comul : (a : B i) → B i ⊗[R] B i) x) :
    B i ⊗[R] B i)
Tactic: have := by simpa using congr($(h i) x)
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
n : Type u_8
inst_2 : DecidableEq n
B : n → Type u_9
inst_3 : (i : n) → AddCommMonoid (B i)
inst_4 : (i : n) → Module.{u_5, u_9} R (B i)
inst_5 : (i : n) → StarAddMonoid (B i)
inst_6 : ∀ (i : n), StarModule.{u_5, u_9} R (B i)
inst_7 : Fintype n
inst_8 : (i : n) → CoalgebraStruct.{u_5, u_9} R (B i)
h :
  ∀ (i : n),
    Eq.{u_9 + 1} (α := WithConv (B i →ₗ[R] B i ⊗[R] B i)) (star (toConv comul))
      (toConv ((↑(TensorProduct.comm R (B i) (B i)) : B i ⊗[R] B i →ₗ[R] B i ⊗[R] B i) ∘ₗ comul))
i : n
x : B i
this :
  Eq (α := B i ⊗[R] B i) (star ((comul : (a : B i) → B i ⊗[R] B i) (star x)) : B i ⊗[R] B i)
    ((TensorProduct.comm R (B i) (B i) : (a : B i ⊗[R] B i) → B i ⊗[R] B i) ((comul : (a : B i) → B i ⊗[R] B i) x) :
      B i ⊗[R] B i)
⊢ Eq (α := ((i : n) → B i) ⊗[R] ((i : n) → B i))
    ((ofConv (star (toConv comul)) ∘ₗ single R B i : (a : B i) → ((i : n) → B i) ⊗[R] ((i : n) → B i)) x :
      ((i : n) → B i) ⊗[R] ((i : n) → B i))
    ((ofConv
              (toConv
                ((↑(TensorProduct.comm R ((i : n) → B i) ((i : n) → B i)) :
                    ((i : n) → B i) ⊗[R] ((i : n) → B i) →ₗ[R] ((i : n) → B i) ⊗[R] ((i : n) → B i)) ∘ₗ
                  comul)) ∘ₗ
            single R B i :
          (a : B i) → ((i : n) → B i) ⊗[R] ((i : n) → B i))
        x :
      ((i : n) → B i) ⊗[R] ((i : n) → B i))
have h₁ : Eq (α := ((i : n) → B i) ⊗[R] ((i : n) → B i))
  (star
      ((TensorProduct.map (single R B i) (single R B i) : (a : B i ⊗[R] B i) → ((i : n) → B i) ⊗[R] ((i : n) → B i))
        ((comul : (a : B i) → B i ⊗[R] B i) (star x))) :
    ((i : n) → B i) ⊗[R] ((i : n) → B i))
  ((TensorProduct.comm R ((i : n) → B i) ((i : n) → B i) :
        (a : ((i : n) → B i) ⊗[R] ((i : n) → B i)) → ((i : n) → B i) ⊗[R] ((i : n) → B i))
      ((TensorProduct.map (single R B i) (single R B i) : (a : B i ⊗[R] B i) → ((i : n) → B i) ⊗[R] ((i : n) → B i))
        ((comul : (a : B i) → B i ⊗[R] B i) x)) :
    ((i : n) → B i) ⊗[R] ((i : n) → B i))
Tactic: simp only [coe_comp, coe_single, Function.comp_apply, intrinsicStar_apply, Pi.star_single,
    Pi.comul_single, LinearEquiv.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
n : Type u_8
inst_2 : DecidableEq n
B : n → Type u_9
inst_3 : (i : n) → AddCommMonoid (B i)
inst_4 : (i : n) → Module.{u_5, u_9} R (B i)
inst_5 : (i : n) → StarAddMonoid (B i)
inst_6 : ∀ (i : n), StarModule.{u_5, u_9} R (B i)
inst_7 : Fintype n
inst_8 : (i : n) → CoalgebraStruct.{u_5, u_9} R (B i)
h :
  ∀ (i : n),
    Eq.{u_9 + 1} (α := WithConv (B i →ₗ[R] B i ⊗[R] B i)) (star (toConv comul))
      (toConv ((↑(TensorProduct.comm R (B i) (B i)) : B i ⊗[R] B i →ₗ[R] B i ⊗[R] B i) ∘ₗ comul))
i : n
x : B i
this :
  Eq (α := B i ⊗[R] B i) (star ((comul : (a : B i) → B i ⊗[R] B i) (star x)) : B i ⊗[R] B i)
    ((TensorProduct.comm R (B i) (B i) : (a : B i ⊗[R] B i) → B i ⊗[R] B i) ((comul : (a : B i) → B i ⊗[R] B i) x) :
      B i ⊗[R] B i)
⊢ Eq (α := ((i : n) → B i) ⊗[R] ((i : n) → B i))
    (star
        ((TensorProduct.map (single R B i) (single R B i) : (a : B i ⊗[R] B i) → ((i : n) → B i) ⊗[R] ((i : n) → B i))
          ((comul : (a : B i) → B i ⊗[R] B i) (star x))) :
      ((i : n) → B i) ⊗[R] ((i : n) → B i))
    ((TensorProduct.comm R ((i : n) → B i) ((i : n) → B i) :
          (a : ((i : n) → B i) ⊗[R] ((i : n) → B i)) → ((i : n) → B i) ⊗[R] ((i : n) → B i))
        ((TensorProduct.map (single R B i) (single R B i) : (a : B i ⊗[R] B i) → ((i : n) → B i) ⊗[R] ((i : n) → B i))
          ((comul : (a : B i) → B i ⊗[R] B i) x)) :
      ((i : n) → B i) ⊗[R] ((i : n) → B i))
have h₁ : Eq (α := ((i : n) → B i) ⊗[R] ((i : n) → B i))
  ((TensorProduct.comm R ((i : n) → B i) ((i : n) → B i) :
        (a : ((i : n) → B i) ⊗[R] ((i : n) → B i)) → ((i : n) → B i) ⊗[R] ((i : n) → B i))
      ((TensorProduct.map (ofConv (star (toConv (single R B i)))) (ofConv (star (toConv (single R B i)))) :
          (a : B i ⊗[R] B i) → ((i : n) → B i) ⊗[R] ((i : n) → B i))
        ((comul : (a : B i) → B i ⊗[R] B i) x)) :
    ((i : n) → B i) ⊗[R] ((i : n) → B i))
  ((TensorProduct.comm R ((i : n) → B i) ((i : n) → B i) :
        (a : ((i : n) → B i) ⊗[R] ((i : n) → B i)) → ((i : n) → B i) ⊗[R] ((i : n) → B i))
      ((TensorProduct.map (single R B i) (single R B i) : (a : B i ⊗[R] B i) → ((i : n) → B i) ⊗[R] ((i : n) → B i))
        ((comul : (a : B i) → B i ⊗[R] B i) x)) :
    ((i : n) → B i) ⊗[R] ((i : n) → B i))
Tactic: rw [star_map_apply_eq_map_intrinsicStar, this, map_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
n : Type u_8
inst_2 : DecidableEq n
inst_3 : Fintype n
x : n
⊢ Eq (α := WithConv (R →ₗ[R] R ⊗[R] R)) (star (toConv comul))
    (toConv ((↑(TensorProduct.comm R R R) : R ⊗[R] R →ₗ[R] R ⊗[R] R) ∘ₗ comul))
have h : Eq (α := R ⊗[R] R) ((ofConv (star (toConv comul)) : (a : R) → R ⊗[R] R) 1)
  ((ofConv (toConv ((↑(TensorProduct.comm R R R) : R ⊗[R] R →ₗ[R] R ⊗[R] R) ∘ₗ comul)) : (a : R) → R ⊗[R] R) 1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_4
m : Type u_5
n : Type u_6
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Fintype m
inst_3 : DecidableEq m
f : WithConv ((m → R) →ₗ[R] n → R)
⊢ Eq (α := Matrix n m R) ((toMatrix' : (a : (m → R) →ₗ[R] n → R) → Matrix n m R) (star f).ofConv : Matrix n m R)
    (Matrix.map ((toMatrix' : (a : (m → R) →ₗ[R] n → R) → Matrix n m R) f.ofConv) star : Matrix n m R)
have a : ∀ (i : n) (j : m),
  Eq.{u_4 + 1} (α := R) ((toMatrix' : (a : (m → R) →ₗ[R] n → R) → Matrix n m R) (star f).ofConv i j : R)
    (Matrix.map ((toMatrix' : (a : (m → R) →ₗ[R] n → R) → Matrix n m R) f.ofConv) star i j : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
f : WithConv (End R E)ˣ
⊢ (End R E)ˣ
have refine_1 : (star (toConv (↑f.ofConv : End R E))).ofConv * (star (toConv (↑f.ofConv⁻¹ : End R E))).ofConv = 1
Tactic: refine ⟨(star (toConv ↑f.ofConv : WithConv (End R E))).ofConv,
      (star (toConv ↑(f.ofConv⁻¹ : (End R E)ˣ))).ofConv, ?_, ?_⟩