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 (End R E)ˣ
refine_1 : (star (toConv (↑f.ofConv : End R E))).ofConv * (star (toConv (↑f.ofConv⁻¹ : End R E))).ofConv = 1
⊢ (End R E)ˣ
have refine_2 : (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, ?_, ?_⟩
-- 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)ˣ
⊢ (star (toConv (↑f.ofConv : End R E))).ofConv * (star (toConv (↑f.ofConv⁻¹ : End R E))).ofConv = 1
have refine_1 : star (toConv ((↑f.ofConv : End R E) ∘ₗ (↑f.ofConv⁻¹ : End R E))) = toConv 1
Tactic: rw [mul_eq_comp, ← toConv_injective.eq_iff, ← LinearMap.intrinsicStar_comp']
-- 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)ˣ
⊢ (star (toConv (↑f.ofConv⁻¹ : End R E))).ofConv * (star (toConv (↑f.ofConv : End R E))).ofConv = 1
have refine_2 : star (toConv ((↑f.ofConv⁻¹ : End R E) ∘ₗ (↑f.ofConv : End R E))) = toConv 1
Tactic: rw [mul_eq_comp, ← toConv_injective.eq_iff, ← LinearMap.intrinsicStar_comp']
-- 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
f : WithConv (End R E)
hf : IsUnit f.ofConv
⊢ IsUnit (star f).ofConv
have have : ∀ (u : (End R E)ˣ) (hu : (↑u : End R E) = f.ofConv), IsUnit (star f).ofConv
Tactic: have ⟨u, hu⟩ := hf
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (hypothesis)
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 f).ofConv
have this : IsUnit (star (toConv (↑u : End R E))).ofConv
Tactic: have : IsUnit (star (toConv (u : End R E))).ofConv := (star (toConv u)).ofConv.isUnit
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
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
⊢ x ∈ (star f).ofConv.eigenspace α ↔ star x ∈ f.ofConv.eigenspace (star α)
have simp_rw : ((star f).ofConv : (a : V) → V) x = α • x ↔ (f.ofConv : (a : V) → V) (star x) = star α • star x
Tactic: simp_rw [mem_eigenspace_iff, intrinsicStar_apply, star_eq_iff_star_eq, star_smul, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
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
⊢ x ∈ (star f).ofConv.eigenspace α ↔ star x ∈ f.ofConv.eigenspace (star α)
have simp_rw₁ : star ((f.ofConv : (a : V) → V) (star x)) = α • x ↔ (f.ofConv : (a : V) → V) (star x) = star α • star x
Tactic: simp_rw [mem_eigenspace_iff, intrinsicStar_apply, star_eq_iff_star_eq, star_smul, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
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
⊢ x ∈ (star f).ofConv.eigenspace α ↔ star x ∈ f.ofConv.eigenspace (star α)
have simp_rw₂ : star (α • x) = (f.ofConv : (a : V) → V) (star x) ↔ (f.ofConv : (a : V) → V) (star x) = star α • star x
Tactic: simp_rw [mem_eigenspace_iff, intrinsicStar_apply, star_eq_iff_star_eq, star_smul, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
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
⊢ x ∈ (star f).ofConv.eigenspace α ↔ star x ∈ f.ofConv.eigenspace (star α)
have simp_rw₃ : star α • star x = (f.ofConv : (a : V) → V) (star x) ↔ (f.ofConv : (a : V) → V) (star x) = star α • star x
Tactic: simp_rw [mem_eigenspace_iff, intrinsicStar_apply, star_eq_iff_star_eq, star_smul, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
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)
⊢ spectrum R (star f).ofConv = star (spectrum R f.ofConv)
have h : ∀ (x : R), x ∈ spectrum R (star f).ofConv ↔ x ∈ star (spectrum R f.ofConv)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
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
⊢ x ∈ spectrum R (star f).ofConv ↔ x ∈ star (spectrum R f.ofConv)
have h : IsUnit (HSMul.hSMul (β := End R V) x 1 - (star f).ofConv) ↔ IsUnit (HSMul.hSMul (β := End R V) (star x) 1 - f.ofConv)
Tactic: simp_rw [Set.mem_star, spectrum.mem_iff, not_iff_not, Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
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 (HSMul.hSMul (β := End R V) x 1 - (star f).ofConv) ↔ IsUnit (HSMul.hSMul (β := End R V) (star x) 1 - f.ofConv)
have 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)
Tactic: rw [← isUnit_intrinsicStar_iff]
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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
⊢ 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))
have 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)
Tactic: rw [selfAdjoint.mem_iff, star_smul, star_trivial, star_add, star_star, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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)
⊢ 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))
have 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)
Tactic: rw [selfAdjoint.mem_iff, star_smul, star_trivial, star_add, star_star, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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)
⊢ 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))
have 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)
Tactic: rw [selfAdjoint.mem_iff, star_smul, star_trivial, star_add, star_star, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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)
⊢ 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))
have 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)
Tactic: rw [selfAdjoint.mem_iff, star_smul, star_trivial, star_add, star_star, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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)
⊢ 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))
have 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)
Tactic: rw [selfAdjoint.mem_iff, star_smul, star_trivial, star_add, star_star, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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)
⊢ 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))
have 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)
Tactic: rw [selfAdjoint.mem_iff, star_smul, star_trivial, star_add, star_star, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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
⊢ 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))
        ⋯
have 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)))
        sorry) :
    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))
          sorry +
        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))
          sorry) :
    A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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
r : R
x : 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 _)
        (r • x + star (r • x)))
      ⋯ =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
      (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))
        ⋯)
have 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 _)
          (r • x + star (r • x)))
        sorry) :
    A) =
  (↑(HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
        (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))
          sorry)) :
    A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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
⊢ Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint 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) (skewAdjoint 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) (skewAdjoint A) x)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (y - star y))
        ⋯
have a : (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (x + y - star (x + y)))
        sorry) :
    A) =
  (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (x - star x))
          sorry +
        Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (y - star y))
          sorry) :
    A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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
r : R
x : A
⊢ Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (r • x - star (r • x)))
      ⋯ =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (x - star x))
        ⋯)
have a : (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (r • x - star (r • x)))
        sorry) :
    A) =
  (↑(HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (x - star x))
          sorry)) :
    A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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
hx : IsSelfAdjoint x
⊢ (↑((selfAdjointPart R : (a : A) → ↥(selfAdjoint A)) x) : A) = x
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + star x) = x
Tactic: rw [selfAdjointPart_apply_coe, hx.star_eq, smul_add, invOf_two_smul_add_invOf_two_smul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Module (goal)
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
hx : IsSelfAdjoint x
rw :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + star x) = x
⊢ (↑((selfAdjointPart R : (a : A) → ↥(selfAdjoint A)) x) : A) = x
have rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x + x) = x
Tactic: rw [selfAdjointPart_apply_coe, hx.star_eq, smul_add, invOf_two_smul_add_invOf_two_smul]