awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
z : ℂ
⊢ (↑(((ℜ : ℂ →ₗ[ℝ] ↥(selfAdjoint ℂ)) : (a : ℂ) → ↥(selfAdjoint ℂ)) ((↑z.re : ℂ) + (↑z.im : ℂ) * I)) : ℂ) = (↑z.re : ℂ)
have rw : HAdd.hAdd (α := ℂ) (↑(((ℜ : ℂ →ₗ[ℝ] ↥(selfAdjoint ℂ)) : (a : ℂ) → ↥(selfAdjoint ℂ)) (↑z.re : ℂ)) : ℂ)
    (↑(-((ℑ : ℂ →ₗ[ℝ] ↥(selfAdjoint ℂ)) : (a : ℂ) → ↥(selfAdjoint ℂ)) (↑z.im : ℂ)) : ℂ) =
  (↑z.re : ℂ)
Tactic: rw [map_add, AddSubmonoid.coe_add, mul_comm, ← smul_eq_mul, realPart_I_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : IsScalarTower ℂ A A
inst_4 : SMulCommClass ℂ A A
inst_5 : StarModule ℂ A
x : A
⊢ IsStarNormal x ↔
    Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
      (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
have rw : Commute (star x) x ↔
  Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
    (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
Tactic: rw [isStarNormal_iff, commute_iff_eq, ← sub_eq_zero, star_mul_self_sub_self_mul_star,
    two_smul ℕ, ← two_smul ℂ, smul_eq_zero_iff_right two_ne_zero, smul_eq_zero_iff_right I_ne_zero,
    sub_eq_zero, commute_iff_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : IsScalarTower ℂ A A
inst_4 : SMulCommClass ℂ A A
inst_5 : StarModule ℂ A
x : A
rw :
  Commute (star x) x ↔
    Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
      (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
⊢ IsStarNormal x ↔
    Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
      (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
have rw₁ : star x * x = x * star x ↔
  Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
    (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
Tactic: rw [isStarNormal_iff, commute_iff_eq, ← sub_eq_zero, star_mul_self_sub_self_mul_star,
    two_smul ℕ, ← two_smul ℂ, smul_eq_zero_iff_right two_ne_zero, smul_eq_zero_iff_right I_ne_zero,
    sub_eq_zero, commute_iff_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : IsScalarTower ℂ A A
inst_4 : SMulCommClass ℂ A A
inst_5 : StarModule ℂ A
x : A
rw :
  Commute (star x) x ↔
    Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
      (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
rw₁ :
  star x * x = x * star x ↔
    Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
      (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
⊢ IsStarNormal x ↔
    Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
      (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
have rw₂ : star x * x - x * star x = 0 ↔
  Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
    (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
Tactic: rw [isStarNormal_iff, commute_iff_eq, ← sub_eq_zero, star_mul_self_sub_self_mul_star,
    two_smul ℕ, ← two_smul ℂ, smul_eq_zero_iff_right two_ne_zero, smul_eq_zero_iff_right I_ne_zero,
    sub_eq_zero, commute_iff_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : IsScalarTower ℂ A A
inst_4 : SMulCommClass ℂ A A
inst_5 : StarModule ℂ A
x : A
rw :
  Commute (star x) x ↔
    Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
      (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
rw₁ :
  star x * x = x * star x ↔
    Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
      (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
rw₂ :
  star x * x - x * star x = 0 ↔
    Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
      (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
⊢ IsStarNormal x ↔
    Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
      (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
have rw₃ : HSMul.hSMul (α := ℕ) 2
      (I •
        (HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) -
          HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A))) =
    0 ↔
  Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
    (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
Tactic: rw [isStarNormal_iff, commute_iff_eq, ← sub_eq_zero, star_mul_self_sub_self_mul_star,
    two_smul ℕ, ← two_smul ℂ, smul_eq_zero_iff_right two_ne_zero, smul_eq_zero_iff_right I_ne_zero,
    sub_eq_zero, commute_iff_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : IsScalarTower ℂ A A
inst_4 : SMulCommClass ℂ A A
inst_5 : StarModule ℂ A
x : A
rw :
  Commute (star x) x ↔
    Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
      (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
rw₁ :
  star x * x = x * star x ↔
    Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
      (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
rw₂ :
  star x * x - x * star x = 0 ↔
    Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
      (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
rw₃ :
  HSMul.hSMul (α := ℕ) 2
        (I •
          (HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
              (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) -
            HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
              (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A))) =
      0 ↔
    Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
      (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
⊢ IsStarNormal x ↔
    Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
      (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
have rw₄ : I •
        (HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) -
          HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) +
      I •
        (HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) -
          HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) =
    0 ↔
  Commute.{u_1} (S := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
    (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
Tactic: rw [isStarNormal_iff, commute_iff_eq, ← sub_eq_zero, star_mul_self_sub_self_mul_star,
    two_smul ℕ, ← two_smul ℂ, smul_eq_zero_iff_right two_ne_zero, smul_eq_zero_iff_right I_ne_zero,
    sub_eq_zero, commute_iff_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : IsScalarTower ℂ A A
inst_4 : SMulCommClass ℂ A A
inst_5 : StarModule ℂ A
x : A
hx : IsStarNormal x
| star x * x
have rw : star
    ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) *
  ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
    HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A))
Tactic: rw [← realPart_add_I_smul_imaginaryPart x]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : IsScalarTower ℂ A A
inst_4 : SMulCommClass ℂ A A
inst_5 : StarModule ℂ A
x : A
hx : IsStarNormal x
⊢ star x * x =
    HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
        HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      I •
        (HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) -
          HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A))
have conv_lhs : star
      ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
        HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) *
    ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) =
  HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
        (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
        (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
    I •
      (HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) -
        HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A))
Tactic: conv_lhs => rw [← realPart_add_I_smul_imaginaryPart x]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : IsScalarTower ℂ A A
inst_4 : SMulCommClass ℂ A A
inst_5 : StarModule ℂ A
x : A
hx : IsStarNormal x
⊢ star
        ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
          HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) *
      ((↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
        HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) =
    HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
        HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      I •
        (HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) -
          HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A))
have simp : HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
        (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      -(I •
          HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
            (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) +
    (I •
        HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
        (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)) =
  HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
        (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
      HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
        (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) +
    (I •
        HMul.hMul (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) -
      I •
        HMul.hMul (α := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)
          (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A))
Tactic: simp [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, smul_smul, smul_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : StarModule ℂ A
⊢ Eq.{u_1 + 1} (α := ↥(selfAdjoint A)) (((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) 1) 1
have a : Eq.{u_1 + 1} (α := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) 1) : A) (↑1 : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : SMulCommClass ℂ A A
inst_4 : IsScalarTower ℂ A A
inst_5 : StarModule ℂ A
x : A
⊢ star x * x = 1 ∧ x * star x = 1 ↔
    IsStarNormal x ∧
      HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 +
          HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 =
        1
have refine_1 : star x * x = 1 ∧ x * star x = 1 →
  ∀ (h : star x * x = 1) (h' : x * star x = 1),
    IsStarNormal x ∧
      HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 +
          HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 =
        1
Tactic: refine ⟨fun ⟨h, h'⟩ ↦ ?_, fun ⟨hx, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : SMulCommClass ℂ A A
inst_4 : IsScalarTower ℂ A A
inst_5 : StarModule ℂ A
x : A
refine_1 :
  star x * x = 1 ∧ x * star x = 1 →
    ∀ (h : star x * x = 1) (h' : x * star x = 1),
      IsStarNormal x ∧
        HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 +
            HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 =
          1
⊢ star x * x = 1 ∧ x * star x = 1 ↔
    IsStarNormal x ∧
      HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 +
          HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 =
        1
have refine_2 : IsStarNormal x ∧
    HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 +
        HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 =
      1 →
  ∀ (hx : IsStarNormal x)
    (h :
      HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 +
          HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 =
        1),
    star x * x = 1 ∧ x * star x = 1
Tactic: refine ⟨fun ⟨h, h'⟩ ↦ ?_, fun ⟨hx, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (hypothesis)
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Module ℂ A
inst_3 : SMulCommClass ℂ A A
inst_4 : IsScalarTower ℂ A A
inst_5 : StarModule ℂ A
x : A
h_1 : star x * x = 1 ∧ x * star x = 1
h : star x * x = 1
h' : x * star x = 1
⊢ IsStarNormal x ∧
    HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 +
        HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A) 2 =
      1
have this : IsStarNormal x
Tactic: have : IsStarNormal x := ⟨h.trans h'.symm⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : Dual R M
m : M
⊢ Eq (α := Dual R M →ₗ[R] Dual R M)
    ((Dual.transpose : (a : M →ₗ[R] M) → Dual R M →ₗ[R] Dual R M)
        ((dualTensorHom R M M : (a : Dual R M ⊗[R] M) → M →ₗ[R] M) (f ⊗ₜ[R] m)) :
      Dual R M →ₗ[R] Dual R M)
    ((dualTensorHom R (Dual R M) (Dual R M) : (a : Dual R (Dual R M) ⊗[R] Dual R M) → Dual R M →ₗ[R] Dual R M)
        ((Dual.eval R M : (a : M) → Dual R (Dual R M)) m ⊗ₜ[R] f) :
      Dual R M →ₗ[R] Dual R M)
have h : ∀ (f' : Dual R M) (m' : M),
  Eq.{u_2 + 1} (α := R)
    ((((((Dual.transpose : (a : M →ₗ[R] M) → Dual R M →ₗ[R] Dual R M)
                    ((dualTensorHom R M M : (a : Dual R M ⊗[R] M) → M →ₗ[R] M) (f ⊗ₜ[R] m)) :
                  Dual R M →ₗ[R] Dual R M) :
                (a : Dual R M) → Dual R M)
              f' :
            Dual R M) :
          (a : M) → R)
        m' :
      R)
    ((((((dualTensorHom R (Dual R M) (Dual R M) : (a : Dual R (Dual R M) ⊗[R] Dual R M) → Dual R M →ₗ[R] Dual R M)
                    ((Dual.eval R M : (a : M) → Dual R (Dual R M)) m ⊗ₜ[R] f) :
                  Dual R M →ₗ[R] Dual R M) :
                (a : Dual R M) → Dual R M)
              f' :
            Dual R M) :
          (a : M) → R)
        m' :
      R)
Tactic: ext f' m'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : Dual R M
m : M
f' : Dual R M
m' : M
⊢ Eq.{u_2 + 1} (α := R)
    ((((((Dual.transpose : (a : M →ₗ[R] M) → Dual R M →ₗ[R] Dual R M)
                    ((dualTensorHom R M M : (a : Dual R M ⊗[R] M) → M →ₗ[R] M) (f ⊗ₜ[R] m)) :
                  Dual R M →ₗ[R] Dual R M) :
                (a : Dual R M) → Dual R M)
              f' :
            Dual R M) :
          (a : M) → R)
        m' :
      R)
    ((((((dualTensorHom R (Dual R M) (Dual R M) : (a : Dual R (Dual R M) ⊗[R] Dual R M) → Dual R M →ₗ[R] Dual R M)
                    ((Dual.eval R M : (a : M) → Dual R (Dual R M)) m ⊗ₜ[R] f) :
                  Dual R M →ₗ[R] Dual R M) :
                (a : Dual R M) → Dual R M)
              f' :
            Dual R M) :
          (a : M) → R)
        m' :
      R)
have h : HMul.hMul (α := R) (β := R) ((f : (a : M) → R) m' : R) ((f' : (a : M) → R) m : R) =
  HMul.hMul (α := R) (β := R) ((f' : (a : M) → R) m : R) ((f : (a : M) → R) m' : R)
Tactic: simp only [Dual.transpose_apply, coe_comp, Function.comp_apply, dualTensorHom_apply,
    map_smulₛₗ, RingHom.id_apply, smul_eq_mul, Dual.eval_apply,
    LinearMap.smul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : Dual R M
p : P
⊢ Eq (α := M × N →ₗ[R] P × Q) (prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0)
    ((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
      ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p))
have hl : ∀ (x : M),
  Eq.{u_5 + 1} (α := P)
    ((prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0 ∘ₗ inl R M N : (a : M) → P × Q)
        x).1
    (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
              ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p) ∘ₗ
            inl R M N :
          (a : M) → P × Q)
        x).1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Contraction (goal)
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : Dual R M
p : P
hl :
  ∀ (x : M),
    Eq.{u_5 + 1} (α := P)
      ((prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0 ∘ₗ inl R M N :
            (a : M) → P × Q)
          x).1
      (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
                ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p) ∘ₗ
              inl R M N :
            (a : M) → P × Q)
          x).1
⊢ Eq (α := M × N →ₗ[R] P × Q) (prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0)
    ((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
      ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p))
have hl₁ : ∀ (x : M),
  Eq.{u_6 + 1} (α := Q)
    ((prodMap ((dualTensorHom R M P : (a : Dual R M ⊗[R] P) → M →ₗ[R] P) (f ⊗ₜ[R] p)) 0 ∘ₗ inl R M N : (a : M) → P × Q)
        x).2
    (((dualTensorHom R (M × N) (P × Q) : (a : Dual R (M × N) ⊗[R] (P × Q)) → M × N →ₗ[R] P × Q)
              ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q : (a : P) → P × Q) p) ∘ₗ
            inl R M N :
          (a : M) → P × Q)
        x).2
Tactic: ext