awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
⊢ IsClopen.{u_1} (X := ↥(unitary A)) (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod)

Tactic:
.of_thickening_subset_self zero_lt_two ?_

Premises used: IsClopen.of_thickening_subset_self, zero_lt_two
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
mp :
  Subset.{u_1} (α := Set ↥(unitary A))
    (thickening 2 (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod))
    (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod)
⊢ IsClopen.{u_1} (X := ↥(unitary A)) (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod)

Tactic:
refine .of_thickening_subset_self zero_lt_two ?_
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu :
  Membership.mem (γ := Set ↥(unitary A))
    (thickening 2 (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod)) u
⊢ ∃ (z : ↥(unitary A)),
    Membership.mem (γ := Set ↥(unitary A)) (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod)
        z ∧
      dist u z < 2

Tactic:
rw [mem_thickening_iff] at hu

Premises used: Metric.mem_thickening_iff
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u : ↥(unitary A)
hu :
  ∃ (z : ↥(unitary A)),
    Membership.mem (γ := Set ↥(unitary A)) (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod)
        z ∧
      dist u z < 2
mp :
  ∀ (v : ↥(unitary A)) (huv : dist u v < 2) (l : List ↥(selfAdjoint A)) (hlv : (List.map expUnitary l).prod = v),
    Membership.mem (γ := Set ↥(unitary A)) (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod) u
⊢ Membership.mem (γ := Set ↥(unitary A)) (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod) u

Tactic:
obtain ⟨v, ⟨⟨l, (hlv : (l.map expUnitary).prod = v)⟩, huv⟩⟩ := hu
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u v : ↥(unitary A)
huv : dist u v < 2
l : List ↥(selfAdjoint A)
hlv : (List.map expUnitary l).prod = v
⊢ Membership.mem (γ := Set ↥(unitary A)) (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod) u

Tactic:
⟨argSelfAdjoint (u * star v) :: l, ?_⟩

Premises used: HMul.hMul, Unitary.argSelfAdjoint, Set.Mem, setOf, List.cons, Exists.intro, Set.range, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u v : ↥(unitary A)
huv : dist u v < 2
l : List ↥(selfAdjoint A)
hlv : (List.map expUnitary l).prod = v
mp : (fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod) (argSelfAdjoint (u * star v) :: l) = u
⊢ Membership.mem (γ := Set ↥(unitary A)) (Set.range fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod) u

Tactic:
refine ⟨argSelfAdjoint (u * star v) :: l, ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u v : ↥(unitary A)
huv : dist u v < 2
l : List ↥(selfAdjoint A)
hlv : (List.map expUnitary l).prod = v
⊢ ‖(↑u : A) - (↑v : A)‖ < 2

Tactic:
simpa [Subtype.dist_eq, dist_eq_norm] using huv

Premises used: dist_eq_norm, Subtype.dist_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
u v : ↥(unitary A)
huv : dist u v < 2
l : List ↥(selfAdjoint A)
hlv : (List.map expUnitary l).prod = v
⊢ (fun (y : List ↥(selfAdjoint A)) ↦ (List.map expUnitary y).prod) (argSelfAdjoint (u * star v) :: l) = u

Tactic:
simp [hlv, mul_assoc,
      expUnitary_eq_mul_inv u v (by simpa [Subtype.dist_eq, dist_eq_norm] using huv)]

Premises used: mul_assoc, Unitary.expUnitary_eq_mul_inv
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
⊢ Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) (List.prod (List.map expUnitary []))

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
x : ↥(selfAdjoint A)
xs : List ↥(selfAdjoint A)
ih : Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) (List.map expUnitary xs).prod
⊢ Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) (List.map expUnitary (x :: xs)).prod

Tactic:
simpa using (joined_one_expUnitary x).mul ih

Premises used: Joined.mul, selfAdjoint.joined_one_expUnitary
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Goal:
A : Type u_1
inst : CStarAlgebra A
l : List ↥(selfAdjoint A)
mpr : Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) (List.prod (List.map expUnitary []))
mpr₁ :
  ∀ (x : ↥(selfAdjoint A)) (xs : List ↥(selfAdjoint A))
    (ih : Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) (List.map expUnitary xs).prod),
    Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) (List.map expUnitary (x :: xs)).prod
⊢ Membership.mem (γ := Set ↥(unitary A)) (pathComponent 1) (List.map expUnitary l).prod

Tactic:
induction l with
    | nil => simp
    | cons x xs ih => simpa using (joined_one_expUnitary x).mul ih
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : SMulCommClass R A A
h :
  ∀ (x : A),
    Eq (α := A)
      ((let __spread.0 : A ≃ₗ[R] A :=
              (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) 1);
            { toLinearEquiv := __spread.0, norm_map' := ⋯ } :
            (a : A) → A)
          x :
        A)
      ((1 : (a : A) → A) x : A)
⊢ Eq.{u_2 + 1} (α := A ≃ₗᵢ[R] A)
    (let __spread.0 : A ≃ₗ[R] A :=
      (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) 1);
    { toLinearEquiv := __spread.0, norm_map' := ⋯ })
    1

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : SMulCommClass R A A
x : A
⊢ Eq (α := A)
    ((let __spread.0 : A ≃ₗ[R] A :=
            (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) 1);
          { toLinearEquiv := __spread.0, norm_map' := ⋯ } :
          (a : A) → A)
        x :
      A)
    ((1 : (a : A) → A) x : A)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : SMulCommClass R A A
x x_1 : ↥(unitary A)
h :
  ∀ (x_2 : A),
    Eq (α := A)
      ((let __spread.0 : A ≃ₗ[R] A :=
              (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A)
                ((toUnits : (a : ↥(unitary A)) → Aˣ) (x * x_1) : Aˣ);
            { toLinearEquiv := __spread.0, norm_map' := ⋯ } :
            (a : A) → A)
          x_2 :
        A)
      ((HMul.hMul (α := A ≃ₗᵢ[R] A)
              (let __spread.0 : A ≃ₗ[R] A :=
                (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) x : Aˣ);
              { toLinearEquiv := __spread.0, norm_map' := ⋯ : A ≃ₗᵢ[R] A })
              (let __spread.0 : A ≃ₗ[R] A :=
                (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) x_1 : Aˣ);
              { toLinearEquiv := __spread.0, norm_map' := ⋯ : A ≃ₗᵢ[R] A }) :
            (a : A) → A)
          x_2 :
        A)
⊢ (let __spread.0 : A ≃ₗ[R] A :=
      (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) (x * x_1) : Aˣ);
    { toLinearEquiv := __spread.0, norm_map' := ⋯ }) =
    HMul.hMul (α := A ≃ₗᵢ[R] A)
      (let __spread.0 : A ≃ₗ[R] A :=
        (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) x : Aˣ);
      { toLinearEquiv := __spread.0, norm_map' := ⋯ : A ≃ₗᵢ[R] A })
      (let __spread.0 : A ≃ₗ[R] A :=
        (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) x_1 : Aˣ);
      { toLinearEquiv := __spread.0, norm_map' := ⋯ : A ≃ₗᵢ[R] A })

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : SMulCommClass R A A
x x_1 : ↥(unitary A)
x_2 : A
⊢ Eq (α := A)
    ((let __spread.0 : A ≃ₗ[R] A :=
            (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) (x * x_1) : Aˣ);
          { toLinearEquiv := __spread.0, norm_map' := ⋯ } :
          (a : A) → A)
        x_2 :
      A)
    ((HMul.hMul (α := A ≃ₗᵢ[R] A)
            (let __spread.0 : A ≃ₗ[R] A :=
              (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) x : Aˣ);
            { toLinearEquiv := __spread.0, norm_map' := ⋯ : A ≃ₗᵢ[R] A })
            (let __spread.0 : A ≃ₗ[R] A :=
              (Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) x_1 : Aˣ);
            { toLinearEquiv := __spread.0, norm_map' := ⋯ : A ≃ₗᵢ[R] A }) :
          (a : A) → A)
        x_2 :
      A)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : SMulCommClass R A A
u : ↥(unitary A)
x : A
⊢ (((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) u : A ≃ₗᵢ[R] A) : (a : A) → A) x = (↑u : A) * x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : SMulCommClass R A A
u : ↥(unitary A)
x : A
⊢ (LinearIsometryEquiv.symm ((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) u) : (a : A) → A) x = star (↑u : A) * x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : SMulCommClass R A A
u : ↥(unitary A)
h :
  ∀ (x : A),
    Eq (α := A) ((LinearIsometryEquiv.symm ((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) u) : (a : A) → A) x : A)
      ((((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) (star u) : A ≃ₗᵢ[R] A) : (a : A) → A) x : A)
⊢ Eq.{u_2 + 1} (α := A ≃ₗᵢ[R] A) (LinearIsometryEquiv.symm ((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) u))
    ((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) (star u))

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : SMulCommClass R A A
u : ↥(unitary A)
x : A
⊢ Eq (α := A) ((LinearIsometryEquiv.symm ((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) u) : (a : A) → A) x : A)
    ((((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) (star u) : A ≃ₗᵢ[R] A) : (a : A) → A) x : A)

Tactic:
rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : SMulCommClass R A A
u v : ↥(unitary A)
⊢ Eq.{u_2 + 1} (α := A ≃ₗᵢ[R] A)
    (LinearIsometryEquiv.trans (E₂ := A) ((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) u)
      ((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) v))
    ((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) (v * u))

Tactic:
map_mul _ _ _ |>.symm

Premises used: map_mul, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : SMulCommClass R A A
u v : ↥(unitary A)
x : A
⊢ Eq (α := A) ((((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) (u * v) : A ≃ₗᵢ[R] A) : (a : A) → A) x : A)
    ((((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) u : A ≃ₗᵢ[R] A) : (a : A) → A)
        ((((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) v : A ≃ₗᵢ[R] A) : (a : A) → A) x : A) :
      A)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : SMulCommClass R A A
u : ↥(unitary A)
⊢ Eq.{u_2 + 1} (α := A ≃ₗ[R] A)
    (LinearIsometryEquiv.toLinearEquiv.{u_1, u_1, u_2, u_2} (E := A) (E₂ := A)
        ((mulLeft R A : (a : ↥(unitary A)) → A ≃ₗᵢ[R] A) u) :
      A ≃ₗ[R] A)
    ((Units.mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) ((toUnits : (a : ↥(unitary A)) → Aˣ) u : Aˣ) : A ≃ₗ[R] A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : IsScalarTower R A A
u : ↥(unitary A)
x : A
⊢ (mulRight R u : (a : A) → A) x = x * (↑u : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : IsScalarTower R A A
u : ↥(unitary A)
x : A
⊢ (LinearIsometryEquiv.symm (mulRight R u) : (a : A) → A) x = x * star (↑u : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : IsScalarTower R A A
u : ↥(unitary A)
h :
  ∀ (x : A),
    Eq (α := A) ((LinearIsometryEquiv.symm (mulRight R u) : (a : A) → A) x : A)
      ((mulRight R (star u) : (a : A) → A) x : A)
⊢ Eq (α := A ≃ₗᵢ[R] A) (LinearIsometryEquiv.symm (mulRight R u)) (mulRight R (star u))

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : IsScalarTower R A A
u : ↥(unitary A)
x : A
⊢ Eq (α := A) ((LinearIsometryEquiv.symm (mulRight R u) : (a : A) → A) x : A)
    ((mulRight R (star u) : (a : A) → A) x : A)

Tactic:
rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : IsScalarTower R A A
u v : ↥(unitary A)
h :
  ∀ (x : A),
    Eq (α := A) ((LinearIsometryEquiv.trans (mulRight R u) (mulRight R v) : (a : A) → A) x : A)
      ((mulRight R (u * v) : (a : A) → A) x : A)
⊢ Eq (α := A ≃ₗᵢ[R] A) (LinearIsometryEquiv.trans (mulRight R u) (mulRight R v)) (mulRight R (u * v))

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : IsScalarTower R A A
u v : ↥(unitary A)
x : A
⊢ Eq (α := A) ((LinearIsometryEquiv.trans (mulRight R u) (mulRight R v) : (a : A) → A) x : A)
    ((mulRight R (u * v) : (a : A) → A) x : A)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : IsScalarTower R A A
u v : ↥(unitary A)
x : A
⊢ Eq (α := A) ((mulRight R (u * v) : (a : A) → A) x : A)
    ((mulRight R v : (a : A) → A) ((mulRight R u : (a : A) → A) x : A) : A)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : IsScalarTower R A A
u : ↥(unitary A)
⊢ Eq (α := A →ₗ[R] A) (↑(LinearIsometryEquiv.toLinearEquiv (mulRight R u)) : A →ₗ[R] A) (LinearMap.mulRight R (↑u : A))

Tactic:
rfl

Premises used: LinearMap.mulRight, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : IsScalarTower R A A
h : ∀ (x : A), Eq (α := A) ((mulRight R 1 : (a : A) → A) x : A) ((LinearIsometryEquiv.refl R A : (a : A) → A) x : A)
⊢ Eq (α := A ≃ₗᵢ[R] A) (mulRight R 1) (LinearIsometryEquiv.refl R A)

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : IsScalarTower R A A
x : A
⊢ Eq (α := A) ((mulRight R 1 : (a : A) → A) x : A) ((LinearIsometryEquiv.refl R A : (a : A) → A) x : A)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Goal:
R : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : CStarRing A
inst_3 : Ring R
inst_4 : Module R A
inst_5 : IsScalarTower R A A
u : ↥(unitary A)
⊢ Eq (α := A ≃ₗ[R] A) (LinearIsometryEquiv.toLinearEquiv (mulRight R u))
    (Units.mulRightLinearEquiv R ((toUnits : (a : ↥(unitary A)) → Aˣ) u))

Tactic:
rfl

Premises used: Units.mulRightLinearEquiv, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
inl : Subsingleton A → Membership.mem (γ := Submonoid A) (unitary A) (a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2))
inr : Nontrivial A → Membership.mem (γ := Submonoid A) (unitary A) (a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2))
⊢ Membership.mem (γ := Submonoid A) (unitary A) (a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2))

Tactic:
obtain (_ | _) := subsingleton_or_nontrivial A

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h : Subsingleton A
⊢ Membership.mem (γ := Submonoid A) (unitary A) (a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2))

Tactic:
simp [Subsingleton.elim (a + I • CFC.sqrt (1 - a ^ 2)) 1, one_mem (unitary A)]

Premises used: CFC.sqrt, unitary, HSub.hSub, HPow.hPow, HAdd.hAdd, HSMul.hSMul, OneMemClass.one_mem, Subsingleton.elim, OfNat.ofNat, Complex.I
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h : Nontrivial A
rw :
  a + I • cfcₙ (p := IsSelfAdjoint) Real.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
rw₁ : 0 ≤ 1 - HPow.hPow (β := ℕ) a 2
⊢ a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a

Tactic:
rw [CFC.sqrt_eq_real_sqrt (1 - a ^ 2) ?nonneg]

Premises used: HSub.hSub, HPow.hPow, OfNat.ofNat, CFC.sqrt_eq_real_sqrt
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h : Nontrivial A
⊢ 0 ≤ ‖a‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h : Nontrivial A
rwa : HPow.hPow (β := ℕ) a 2 ≤ 1
rwa₁ : ‖HPow.hPow (β := ℕ) a 2‖ ≤ 1
rwa₂ : ‖a * a‖ ≤ 1
rwa₃ : HPow.hPow (β := ℕ) ‖a‖ 2 ≤ 1
rwa₄ rwa₅ rwa₆ rwa₇ : ‖a‖ ≤ 1
⊢ 0 ≤ 1 - HPow.hPow (β := ℕ) a 2

Tactic:
rwa [sub_nonneg, ← CStarAlgebra.norm_le_one_iff_of_nonneg (a ^ 2), sq, ha.norm_mul_self,
        sq_le_one_iff₀ (by positivity)]

Premises used: IsSelfAdjoint.norm_mul_self, sq_le_one_iff₀, sq, HPow.hPow, CStarAlgebra.norm_le_one_iff_of_nonneg, OfNat.ofNat, sub_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h : Nontrivial A
⊢ 0 ≤ 1 - HPow.hPow (β := ℕ) a 2

Tactic:
case nonneg =>
      rwa [sub_nonneg, ← CStarAlgebra.norm_le_one_iff_of_nonneg (a ^ 2), sq, ha.norm_mul_self,
        sq_le_one_iff₀ (by positivity)]

Premises used: IsSelfAdjoint.norm_mul_self, sq_le_one_iff₀, sq, HPow.hPow, CStarAlgebra.norm_le_one_iff_of_nonneg, OfNat.ofNat, sub_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h : Nontrivial A
⊢ a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a

Tactic:
have key : a + I • CFC.sqrt (1 - a ^ 2) = cfc (fun x : ℂ ↦ x.re + I * √(1 - x.re ^ 2)) a := by
    rw [CFC.sqrt_eq_real_sqrt (1 - a ^ 2) ?nonneg]
    case nonneg =>
      rwa [sub_nonneg, ← CStarAlgebra.norm_le_one_iff_of_nonneg (a ^ 2), sq, ha.norm_mul_self,
        sq_le_one_iff₀ (by positivity)]
    rw [cfc_add .., cfc_const_mul .., ← cfc_real_eq_complex (fun x ↦ x) ha, cfc_id' ℝ a,
      ← cfc_real_eq_complex (fun x ↦ √(1 - x ^ 2)) ha, cfcₙ_eq_cfc, cfc_comp' (√·) (1 - · ^ 2) a,
      cfc_sub .., cfc_pow .., cfc_const_one .., cfc_id' ..]
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h : Nontrivial A
key :
  a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
inr :
  ∀ x ∈ spectrum ℂ a,
    star ((↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) *
        ((↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) =
      1
⊢ Membership.mem (γ := Submonoid A) (unitary A) (a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2))

Tactic:
rw [key, cfc_unitary_iff ..]

Premises used: cfc_unitary_iff
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h : Nontrivial A
key :
  a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
x : ℂ
hx : x ∈ spectrum ℂ a
inr : ‖x.re‖ ≤ 1
⊢ star ((↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) *
      ((↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) =
    1

Tactic:
rw [← starRingEnd_apply, ← Complex.normSq_eq_conj_mul_self,
    Complex.normSq_ofReal_add_I_mul_sqrt_one_sub, Complex.ofReal_one]

Premises used: Complex.ofReal_one, Complex.normSq_ofReal_add_I_mul_sqrt_one_sub, starRingEnd_apply, Complex.normSq_eq_conj_mul_self
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h : Nontrivial A
key :
  a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
x : ℂ
hx : x ∈ spectrum ℂ a
⊢ ‖x.re‖ ≤ 1

Tactic:
spectrum.norm_le_norm_of_mem (ha.spectrumRestricts.apply_mem hx) |>.trans ha_norm

Premises used: spectrum.norm_le_norm_of_mem, IsSelfAdjoint.spectrumRestricts, SpectrumRestricts.apply_mem, LE.le.trans
-- Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h : Nontrivial A
key :
  a + I • CFC.sqrt (1 - HPow.hPow (β := ℕ) a 2) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x.re 2) : ℂ)) a
x : ℂ
hx : x ∈ spectrum ℂ a
⊢ ‖x.re‖ ≤ 1

Tactic:
exact spectrum.norm_le_norm_of_mem (ha.spectrumRestricts.apply_mem hx) |>.trans ha_norm

Premises used: spectrum.norm_le_norm_of_mem, IsSelfAdjoint.spectrumRestricts, SpectrumRestricts.apply_mem, LE.le.trans