awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.LinearMap
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)
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))
⊢ 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:
rw [star_map_apply_eq_map_intrinsicStar, this, map_comm]

Premises used: TensorProduct.map_comm, TensorProduct.star_map_apply_eq_map_intrinsicStar
-- Module: Mathlib.Algebra.Star.LinearMap
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))
    ((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:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
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
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)
⊢ Eq (α := WithConv (R →ₗ[R] R ⊗[R] R)) (star (toConv comul))
    (toConv ((↑(TensorProduct.comm R R R) : R ⊗[R] R →ₗ[R] R ⊗[R] R) ∘ₗ comul))

Tactic:
ext
-- Module: Mathlib.Algebra.Star.LinearMap
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 (α := 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:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R_1 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R_1
inst_1 : InvolutiveStar R_1
inst_2 : AddCommMonoid E
inst_3 : Module R_1 E
inst_4 : StarAddMonoid E
inst_5 : StarModule R_1 E
inst_6 : AddCommMonoid F
inst_7 : Module R_1 F
inst_8 : StarAddMonoid F
inst_9 : StarModule R_1 F
G : Type u_4
inst_10 : AddCommMonoid G
inst_11 : Module R_1 G
inst_12 : StarAddMonoid G
inst_13 : StarModule R_1 G
R : Type u_5
A : Type u_6
C : Type u_7
inst_14 : CommSemiring R
inst_15 : StarRing R
inst_16 : NonUnitalNonAssocSemiring A
inst_17 : Module R A
inst_18 : SMulCommClass R A A
inst_19 : IsScalarTower R A A
inst_20 : StarRing A
inst_21 : StarModule R A
inst_22 : AddCommMonoid C
inst_23 : Module R C
inst_24 : StarAddMonoid C
inst_25 : StarModule R C
n : Type u_8
inst_26 : DecidableEq n
B : n → Type u_9
inst_27 : (i : n) → AddCommMonoid (B i)
inst_28 : (i : n) → Module.{u_5, u_9} R (B i)
inst_29 : (i : n) → StarAddMonoid (B i)
inst_30 : ∀ (i : n), StarModule.{u_5, u_9} R (B i)
inst_31 : Fintype n
m : Type u_10
⊢ Eq (α := WithConv ((n → R) →ₗ[R] (n → R) ⊗[R] (n → R))) (star (toConv comul))
    (toConv ((↑(TensorProduct.comm R (n → R) (n → R)) : (n → R) ⊗[R] (n → R) →ₗ[R] (n → R) ⊗[R] (n → R)) ∘ₗ comul))

Tactic:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
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)
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Algebra.Star.LinearMap
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)
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:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
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)
⊢ IsSelfAdjoint f ↔
    ∀ (i : n) (j : m),
      IsSelfAdjoint.{u_4} (R := R) ((toMatrix' : (a : (m → R) →ₗ[R] n → R) → Matrix n m R) f.ofConv i j : R)

Tactic:
simp [IsSelfAdjoint, ← toMatrix'.injective.eq_iff, toMatrix'_intrinsicStar, ← Matrix.ext_iff,
    WithConv.ext_iff]

Premises used: IsSelfAdjoint, Function.Injective.eq_iff, LinearMap.toMatrix', LinearMap.toMatrix'_intrinsicStar, Matrix.ext_iff, LinearEquiv.injective, WithConv.ext_iff
-- Module: Mathlib.Algebra.Star.LinearMap
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
A : Matrix n m R
⊢ Eq (α := WithConv ((m → R) →ₗ[R] n → R))
    (star (toConv ((toLin' : (a : Matrix n m R) → (m → R) →ₗ[R] n → R) A)) : WithConv ((m → R) →ₗ[R] n → R))
    (toConv ((toLin' : (a : Matrix n m R) → (m → R) →ₗ[R] n → R) (A.map star)) : WithConv ((m → R) →ₗ[R] n → R))

Tactic:
simp [← LinearMap.toMatrix'.injective.eq_iff, LinearMap.toMatrix'_intrinsicStar, WithConv.ext_iff]

Premises used: Function.Injective.eq_iff, LinearMap.toMatrix', LinearMap.toMatrix'_intrinsicStar, LinearEquiv.injective, WithConv.ext_iff
-- Module: Mathlib.Algebra.Star.LinearMap
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
A : Matrix n m R
⊢ IsSelfAdjoint (R := WithConv ((m → R) →ₗ[R] n → R))
      (toConv ((toLin' : (a : Matrix n m R) → (m → R) →ₗ[R] n → R) A) : WithConv ((m → R) →ₗ[R] n → R)) ↔
    ∀ (i : n) (j : m), IsSelfAdjoint (A i j)

Tactic:
simp [IsSelfAdjoint, intrinsicStar_toLin', ← ext_iff]

Premises used: IsSelfAdjoint, Matrix.intrinsicStar_toLin', Matrix.ext_iff
-- Module: Mathlib.Algebra.Star.LinearMap
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)ˣ
refine_1 : (star (toConv (↑f.ofConv : End R E))).ofConv * (star (toConv (↑f.ofConv⁻¹ : End R E))).ofConv = 1
refine_2 : (star (toConv (↑f.ofConv⁻¹ : End R E))).ofConv * (star (toConv (↑f.ofConv : End R E))).ofConv = 1
⊢ (End R E)ˣ

Tactic:
refine ⟨(star (toConv ↑f.ofConv : WithConv (End R E))).ofConv,
      (star (toConv ↑(f.ofConv⁻¹ : (End R E)ˣ))).ofConv, ?_, ?_⟩
-- Module: Mathlib.Algebra.Star.LinearMap
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)ˣ
refine_1 : star (toConv ((↑f.ofConv : End R E) ∘ₗ (↑f.ofConv⁻¹ : End R E))) = toConv 1
⊢ (star (toConv (↑f.ofConv : End R E))).ofConv * (star (toConv (↑f.ofConv⁻¹ : End R E))).ofConv = 1

Tactic:
rw [mul_eq_comp, ← toConv_injective.eq_iff, ← LinearMap.intrinsicStar_comp']

Premises used: Module.End.mul_eq_comp, Function.Injective.eq_iff, LinearMap.intrinsicStar_comp', WithConv.toConv_injective
-- Module: Mathlib.Algebra.Star.LinearMap
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)ˣ
⊢ star (toConv ((↑f.ofConv : End R E) ∘ₗ (↑f.ofConv⁻¹ : End R E))) = toConv 1

Tactic:
simp [← mul_eq_comp, one_eq_id]

Premises used: Module.End.mul_eq_comp, Module.End.one_eq_id
-- Module: Mathlib.Algebra.Star.LinearMap
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)ˣ
refine_2 : star (toConv ((↑f.ofConv⁻¹ : End R E) ∘ₗ (↑f.ofConv : End R E))) = toConv 1
⊢ (star (toConv (↑f.ofConv⁻¹ : End R E))).ofConv * (star (toConv (↑f.ofConv : End R E))).ofConv = 1

Tactic:
rw [mul_eq_comp, ← toConv_injective.eq_iff, ← LinearMap.intrinsicStar_comp']

Premises used: Module.End.mul_eq_comp, Function.Injective.eq_iff, LinearMap.intrinsicStar_comp', WithConv.toConv_injective
-- Module: Mathlib.Algebra.Star.LinearMap
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)ˣ
⊢ star (toConv ((↑f.ofConv⁻¹ : End R E) ∘ₗ (↑f.ofConv : End R E))) = toConv 1

Tactic:
simp [← mul_eq_comp, one_eq_id]

Premises used: Module.End.mul_eq_comp, Module.End.one_eq_id
-- Module: Mathlib.Algebra.Star.LinearMap
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
f : WithConv (End R E)
hf : IsUnit f.ofConv
have : ∀ (u : (End R E)ˣ) (hu : (↑u : End R E) = f.ofConv), IsUnit (star f).ofConv
⊢ IsUnit (star f).ofConv

Tactic:
have ⟨u, hu⟩ := hf
-- Module: Mathlib.Algebra.Star.LinearMap
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
f : WithConv (End R E)
hf : IsUnit f.ofConv
u : (End R E)ˣ
hu : (↑u : End R E) = f.ofConv
⊢ IsUnit (star (toConv (↑u : End R E))).ofConv

Tactic:
have : IsUnit (star (toConv (u : End R E))).ofConv := (star (toConv u)).ofConv.isUnit
-- Module: Mathlib.Algebra.Star.LinearMap
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
f : WithConv (End R E)
hf : IsUnit f.ofConv
u : (End R E)ˣ
hu : (↑u : End R E) = f.ofConv
this : IsUnit (star (toConv (↑u : End R E))).ofConv
⊢ IsUnit (star f).ofConv

Tactic:
simpa [hu] using this
-- Module: Mathlib.Algebra.Star.LinearMap
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
f : WithConv (End R E)
⊢ IsUnit (star f).ofConv ↔ IsUnit f.ofConv

Tactic:
⟨fun h ↦ star_star f ▸ h.intrinsicStar, fun h ↦ h.intrinsicStar⟩

Premises used: star_star, Eq.rec, Iff.intro, Module.End.IsUnit.intrinsicStar
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_4
V : Type u_5
inst : CommRing R
inst_1 : InvolutiveStar R
inst_2 : AddCommGroup V
inst_3 : StarAddMonoid V
inst_4 : Module R V
inst_5 : StarModule R V
f : WithConv (End R V)
α : R
x : V
simp_rw : ((star f).ofConv : (a : V) → V) x = α • x ↔ (f.ofConv : (a : V) → V) (star x) = star α • star x
simp_rw₁ : star ((f.ofConv : (a : V) → V) (star x)) = α • x ↔ (f.ofConv : (a : V) → V) (star x) = star α • star x
simp_rw₂ : star (α • x) = (f.ofConv : (a : V) → V) (star x) ↔ (f.ofConv : (a : V) → V) (star x) = star α • star x
simp_rw₃ : star α • star x = (f.ofConv : (a : V) → V) (star x) ↔ (f.ofConv : (a : V) → V) (star x) = star α • star x
⊢ x ∈ (star f).ofConv.eigenspace α ↔ star x ∈ f.ofConv.eigenspace (star α)

Tactic:
simp_rw [mem_eigenspace_iff, intrinsicStar_apply, star_eq_iff_star_eq, star_smul, eq_comm]

Premises used: StarModule.star_smul, eq_comm, star_eq_iff_star_eq, Module.End.mem_eigenspace_iff, LinearMap.intrinsicStar_apply
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_4
V : Type u_5
inst : CommRing R
inst_1 : InvolutiveStar R
inst_2 : AddCommGroup V
inst_3 : StarAddMonoid V
inst_4 : Module R V
inst_5 : StarModule R V
f : WithConv (End R V)
h : ∀ (x : R), x ∈ spectrum R (star f).ofConv ↔ x ∈ star (spectrum R f.ofConv)
⊢ spectrum R (star f).ofConv = star (spectrum R f.ofConv)

Tactic:
ext x
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_4
V : Type u_5
inst : CommRing R
inst_1 : InvolutiveStar R
inst_2 : AddCommGroup V
inst_3 : StarAddMonoid V
inst_4 : Module R V
inst_5 : StarModule R V
f : WithConv (End R V)
x : R
h :
  IsUnit (HSMul.hSMul (β := End R V) x 1 - (star f).ofConv) ↔ IsUnit (HSMul.hSMul (β := End R V) (star x) 1 - f.ofConv)
⊢ x ∈ spectrum R (star f).ofConv ↔ x ∈ star (spectrum R f.ofConv)

Tactic:
simp_rw [Set.mem_star, spectrum.mem_iff, not_iff_not, Algebra.algebraMap_eq_smul_one]

Premises used: not_iff_not, Algebra.algebraMap_eq_smul_one, spectrum.mem_iff, Set.mem_star
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_4
V : Type u_5
inst : CommRing R
inst_1 : InvolutiveStar R
inst_2 : AddCommGroup V
inst_3 : StarAddMonoid V
inst_4 : Module R V
inst_5 : StarModule R V
f : WithConv (End R V)
x : R
h :
  IsUnit (star (toConv (HSMul.hSMul (β := End R V) x 1 - (star f).ofConv))).ofConv ↔
    IsUnit (HSMul.hSMul (β := End R V) (star x) 1 - f.ofConv)
⊢ IsUnit (HSMul.hSMul (β := End R V) x 1 - (star f).ofConv) ↔ IsUnit (HSMul.hSMul (β := End R V) (star x) 1 - f.ofConv)

Tactic:
rw [← isUnit_intrinsicStar_iff]

Premises used: Module.End.isUnit_intrinsicStar_iff
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_4
V : Type u_5
inst : CommRing R
inst_1 : InvolutiveStar R
inst_2 : AddCommGroup V
inst_3 : StarAddMonoid V
inst_4 : Module R V
inst_5 : StarModule R V
f : WithConv (End R V)
x : R
⊢ IsUnit (star (toConv (HSMul.hSMul (β := End R V) x 1 - (star f).ofConv))).ofConv ↔
    IsUnit (HSMul.hSMul (β := End R V) (star x) 1 - f.ofConv)

Tactic:
simp [one_eq_id]

Premises used: Module.End.one_eq_id
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StarAddMonoid M
n : ℕ
x : M
⊢ star (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑n : R) x) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑n : R) (star x)

Tactic:
map_natCast_smul (starAddEquiv : M ≃+ M) R R n x

Premises used: map_natCast_smul, starAddEquiv
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : StarAddMonoid M
n : ℤ
x : M
⊢ star (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑n : R) x) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑n : R) (star x)

Tactic:
map_intCast_smul (starAddEquiv : M ≃+ M) R R n x

Premises used: map_intCast_smul, starAddEquiv
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
M : Type u_2
inst : DivisionSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StarAddMonoid M
n : ℕ
x : M
⊢ star (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑n : R)⁻¹ x) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑n : R)⁻¹ (star x)

Tactic:
map_inv_natCast_smul (starAddEquiv : M ≃+ M) R R n x

Premises used: map_inv_natCast_smul, starAddEquiv
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
M : Type u_2
inst : DivisionRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : StarAddMonoid M
n : ℤ
x : M
⊢ star (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑n : R)⁻¹ x) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑n : R)⁻¹ (star x)

Tactic:
map_inv_intCast_smul (starAddEquiv : M ≃+ M) R R n x

Premises used: starAddEquiv, map_inv_intCast_smul
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
M : Type u_2
inst : DivisionRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : StarAddMonoid M
n : ℚ
x : M
⊢ star (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑n : R) x) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑n : R) (star x)

Tactic:
map_ratCast_smul (starAddEquiv : M ≃+ M) _ _ _ x

Premises used: map_ratCast_smul, starAddEquiv
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : StarAddMonoid R
inst_2 : Module ℚ≥0 R
q : ℚ≥0
x : R
⊢ star (q • x) = q • star x

Tactic:
map_nnrat_smul (starAddEquiv : R ≃+ R) _ _

Premises used: map_nnrat_smul, starAddEquiv
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : StarAddMonoid R
inst_2 : Module ℚ R
q : ℚ
x : R
⊢ star (q • x) = q • star x

Tactic:
map_rat_smul (starAddEquiv : R ≃+ R) _ _

Premises used: starAddEquiv, map_rat_smul
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x : A
rw :
  star
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (x + star x)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + star x)
rw₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (star (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _))
      (star (x + star x)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + star x)
rw₂ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (star (x + star x)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + star x)
rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (star x + star (star x)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + star x)
rw₄ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (star x + x) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + star x)
rw₅ rw₆ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + star x) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + star x)
⊢ Membership.mem (γ := AddSubgroup A) (selfAdjoint A)
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + star x))

Tactic:
rw [selfAdjoint.mem_iff, star_smul, star_trivial, star_add, star_star, add_comm]

Premises used: star_star, StarAddMonoid.star_add, StarModule.star_smul, TrivialStar.star_trivial, add_comm, selfAdjoint.mem_iff
-- Module: Mathlib.Algebra.Star.Module
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : TrivialStar R
inst_3 : AddCommGroup A
inst_4 : Module R A
inst_5 : StarAddMonoid A
inst_6 : StarModule R A
inst_7 : Invertible (α := R) 2
x y : A
a :
  (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (x + y + star (x + y)))
          ⋯) :
      A) =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
              (x + star x))
            ⋯ +
          Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
              (y + star y))
            ⋯) :
      A)
⊢ Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (x + y + star (x + y)))
      ⋯ =
    Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (x + star x))
        ⋯ +
      Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (selfAdjoint A) x)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (y + star y))
        ⋯

Tactic:
ext