awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
⊢ ∃ (C : ℝ), ∀ (a : A₁), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ C * ‖a‖

Tactic:
have hbound : ∃ C : ℝ, ∀ a, ‖f a‖ ≤ C * ‖a‖ := by
      obtain ⟨C, h⟩ := exists_norm_apply_le (f : A₁ →ₚ[ℂ] A₂)
      exact ⟨C, h⟩
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
hbound : ∃ (C : ℝ), ∀ (a : A₁), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ C * ‖a‖
⊢ Continuous.{u_1, u_2} (X := A₁) (Y := A₂) (⇑f : (a : A₁) → A₂)

Tactic:
(LinearMap.mkContinuousOfExistsBound (f : A₁ →ₗ[ℂ] A₂) hbound).continuous

Premises used: LinearMap.mkContinuousOfExistsBound, SemilinearMapClass.semilinearMap, ContinuousLinearMap.continuous
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
hbound : ∃ (C : ℝ), ∀ (a : A₁), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ C * ‖a‖
⊢ Continuous.{u_1, u_2} (X := A₁) (Y := A₂) (⇑f : (a : A₁) → A₂)

Tactic:
exact (LinearMap.mkContinuousOfExistsBound (f : A₁ →ₗ[ℂ] A₂) hbound).continuous

Premises used: LinearMap.mkContinuousOfExistsBound, SemilinearMapClass.semilinearMap, ContinuousLinearMap.continuous
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
a : A₁
obtain :
  ∀ (y : Fin 4 → A₁) (hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i) (hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖a‖)
    (hy : a = ∑ i : Fin 4, Complex.I ^ (↑i : ℕ) • y i),
    Eq.{u_2 + 1} (α := A₂) ((f : (a : A₁) → A₂) (star a) : A₂) (star ((f : (a : A₁) → A₂) a) : A₂)
⊢ Eq.{u_2 + 1} (α := A₂) ((f : (a : A₁) → A₂) (star a) : A₂) (star ((f : (a : A₁) → A₂) a) : A₂)

Tactic:
obtain ⟨y, hy_nonneg, hy_norm, hy⟩ := CStarAlgebra.exists_sum_four_nonneg a

Premises used: CStarAlgebra.exists_sum_four_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
a : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖a‖
hy : a = ∑ i : Fin 4, Complex.I ^ (↑i : ℕ) • y i
x : Fin 4
rw rw₁ : y x = y x
⊢ star (y x) = y x

Tactic:
rw [IsSelfAdjoint.star_eq (hy_nonneg x).isSelfAdjoint]

Premises used: LE.le.isSelfAdjoint, IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
a : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖a‖
hy : a = ∑ i : Fin 4, Complex.I ^ (↑i : ℕ) • y i
⊢ ∀ (x : Fin 4), star (y x) = y x

Tactic:
have hy' : ∀ x : Fin 4, star (y x) = y x := fun x => by
      rw [IsSelfAdjoint.star_eq (hy_nonneg x).isSelfAdjoint]
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
a : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖a‖
hy : a = ∑ i : Fin 4, Complex.I ^ (↑i : ℕ) • y i
hy' : ∀ (x : Fin 4), star (y x) = y x
x : Fin 4
rw rw₁ : Eq.{u_2 + 1} (α := A₂) ((f : (a : A₁) → A₂) (y x) : A₂) ((f : (a : A₁) → A₂) (y x) : A₂)
⊢ Eq.{u_2 + 1} (α := A₂) (star ((f : (a : A₁) → A₂) (y x)) : A₂) ((f : (a : A₁) → A₂) (y x) : A₂)

Tactic:
rw [IsSelfAdjoint.star_eq (map_nonneg f (hy_nonneg x)).isSelfAdjoint]

Premises used: LE.le.isSelfAdjoint, map_nonneg, IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
a : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖a‖
hy : a = ∑ i : Fin 4, Complex.I ^ (↑i : ℕ) • y i
hy' : ∀ (x : Fin 4), star (y x) = y x
⊢ ∀ (x : Fin 4), Eq.{u_2 + 1} (α := A₂) (star ((f : (a : A₁) → A₂) (y x)) : A₂) ((f : (a : A₁) → A₂) (y x) : A₂)

Tactic:
have hy'' : ∀ x : Fin 4, star (f (y x)) = f (y x) := fun x => by
      rw [IsSelfAdjoint.star_eq (map_nonneg f (hy_nonneg x)).isSelfAdjoint]
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
a : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖a‖
hy : a = ∑ i : Fin 4, Complex.I ^ (↑i : ℕ) • y i
hy' : ∀ (x : Fin 4), star (y x) = y x
hy'' : ∀ (x : Fin 4), Eq.{u_2 + 1} (α := A₂) (star ((f : (a : A₁) → A₂) (y x)) : A₂) ((f : (a : A₁) → A₂) (y x) : A₂)
⊢ Eq.{u_2 + 1} (α := A₂) ((f : (a : A₁) → A₂) (star a) : A₂) (star ((f : (a : A₁) → A₂) a) : A₂)

Tactic:
simp [hy, hy', hy'']
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℝ A
inst_4 : IsScalarTower ℝ A A
inst_5 : SMulCommClass ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
p : A
⊢ IsStarProjection p ↔ quasispectrum ℝ p ⊆ {0, 1} ∧ IsSelfAdjoint p

Tactic:
(isStarProjection_iff p).eq ▸
    and_congr_left_iff.mpr fun h ↦ isIdempotentElem_iff_quasispectrum_subset ℝ p h

Premises used: Iff.mpr, Real, Eq.rec, isStarProjection_iff, isIdempotentElem_iff_quasispectrum_subset, and_congr_left_iff, Eq.symm, Iff.eq
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
p : A
hp : IsIdempotentElem p
simp : IsStarNormal p → ∀ x ∈ quasispectrum ℂ p, x = (↑x.re : ℂ)
⊢ IsSelfAdjoint p ↔ IsStarNormal p

Tactic:
simp only [isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts,
    QuasispectrumRestricts.real_iff, and_iff_left_iff_imp]

Premises used: QuasispectrumRestricts.real_iff, isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, and_iff_left_iff_imp
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
p : A
hp : IsIdempotentElem p
h : IsStarNormal p
x : ℂ
hx : x ∈ quasispectrum ℂ p
inl : ∀ (hx : x = 0), x = (↑x.re : ℂ)
inr : ∀ (hx : Membership.mem (γ := Set ℂ) {1} x), x = (↑x.re : ℂ)
⊢ x = (↑x.re : ℂ)

Tactic:
rcases hp.quasispectrum_subset _ hx with (hx | hx)

Premises used: IsIdempotentElem.quasispectrum_subset
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
p : A
hp : IsIdempotentElem p
h : IsStarNormal p
x : ℂ
hx_1 : x ∈ quasispectrum ℂ p
hx : x = 0
⊢ x = (↑x.re : ℂ)

Tactic:
simp [Set.mem_singleton_iff.mp hx]

Premises used: Set.mem_singleton_iff, Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
p : A
hp : IsIdempotentElem p
h : IsStarNormal p
x : ℂ
hx_1 : x ∈ quasispectrum ℂ p
hx : Membership.mem (γ := Set ℂ) {1} x
⊢ x = (↑x.re : ℂ)

Tactic:
simp [Set.mem_singleton_iff.mp hx]

Premises used: Set.mem_singleton_iff, Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
p : A
⊢ IsStarProjection p ↔ IsIdempotentElem p ∧ IsStarNormal p

Tactic:
(isStarProjection_iff p).eq ▸ and_congr_right_iff.eq ▸ fun h => h.isSelfAdjoint_iff_isStarNormal

Premises used: Eq.rec, IsIdempotentElem.isSelfAdjoint_iff_isStarNormal, and_congr_right_iff, isStarProjection_iff, Eq.symm, Iff.eq
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
p : A
⊢ IsStarProjection p ↔ quasispectrum ℂ p ⊆ {0, 1} ∧ IsStarNormal p

Tactic:
isStarProjection_iff_isIdempotentElem_and_isStarNormal (p := p).eq ▸
    and_congr_left_iff.mpr fun h ↦ isIdempotentElem_iff_quasispectrum_subset ℂ p h

Premises used: Iff.mpr, Eq.rec, isIdempotentElem_iff_quasispectrum_subset, and_congr_left_iff, isStarProjection_iff_isIdempotentElem_and_isStarNormal, Complex, Eq.symm, Iff.eq
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℝ A
inst_4 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
p : A
⊢ IsStarProjection p ↔ spectrum ℝ p ⊆ {0, 1} ∧ IsSelfAdjoint p

Tactic:
(isStarProjection_iff p).eq ▸
    and_congr_left_iff.mpr fun h ↦ isIdempotentElem_iff_spectrum_subset ℝ p h

Premises used: Iff.mpr, Real, Eq.rec, isStarProjection_iff, isIdempotentElem_iff_spectrum_subset, and_congr_left_iff, Eq.symm, Iff.eq
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
p : A
⊢ IsStarProjection p ↔ spectrum ℂ p ⊆ {0, 1} ∧ IsStarNormal p

Tactic:
isStarProjection_iff_isIdempotentElem_and_isStarNormal (p := p).eq ▸
    and_congr_left_iff.mpr fun h ↦ isIdempotentElem_iff_spectrum_subset ℂ p h

Premises used: Iff.mpr, Eq.rec, isIdempotentElem_iff_spectrum_subset, and_congr_left_iff, isStarProjection_iff_isIdempotentElem_and_isStarNormal, Complex, Eq.symm, Iff.eq
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p ≤ q

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
⊢ q * p = p

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
⊢ ∀ (a : p ≤ q), q * p = p

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
⊢ ∀ (a : p ≤ q), q * p = p

Tactic:
tfae_have 1 → 2 := fun h ↦ (hq.mul_right_and_mul_left_of_nonneg_of_le hp.nonneg h).2

Premises used: IsStarProjection.mul_right_and_mul_left_of_nonneg_of_le, And.right, IsStarProjection.nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
⊢ q * p = p

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
⊢ p * q = p

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
⊢ ∀ (a : q * p = p), p * q = p

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
h : q * p = p
⊢ p * q = p

Tactic:
simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $h)

Premises used: IsStarProjection.isSelfAdjoint, IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
⊢ ∀ (a : q * p = p), p * q = p

Tactic:
tfae_have 2 → 3 := fun h ↦ by
    simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $h)
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
tfae_2_to_3 : ∀ (a : q * p = p), p * q = p
⊢ p * q = p

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
tfae_2_to_3 : ∀ (a : q * p = p), p * q = p
⊢ IsStarProjection (q - p)

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
tfae_2_to_3 : ∀ (a : q * p = p), p * q = p
⊢ ∀ (a : p * q = p), IsStarProjection (q - p)

Tactic:
3 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
tfae_2_to_3 : ∀ (a : q * p = p), p * q = p
⊢ ∀ (a : p * q = p), IsStarProjection (q - p)

Tactic:
tfae_have 3 → 4 := hp.sub_of_mul_eq_left hq

Premises used: IsStarProjection.sub_of_mul_eq_left
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
tfae_2_to_3 : ∀ (a : q * p = p), p * q = p
tfae_3_to_4 : ∀ (a : p * q = p), IsStarProjection (q - p)
⊢ IsStarProjection (q - p)

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
tfae_2_to_3 : ∀ (a : q * p = p), p * q = p
tfae_3_to_4 : ∀ (a : p * q = p), IsStarProjection (q - p)
⊢ p ≤ q

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
tfae_2_to_3 : ∀ (a : q * p = p), p * q = p
tfae_3_to_4 : ∀ (a : p * q = p), IsStarProjection (q - p)
⊢ ∀ (a : IsStarProjection (q - p)), p ≤ q

Tactic:
4 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
tfae_2_to_3 : ∀ (a : q * p = p), p * q = p
tfae_3_to_4 : ∀ (a : p * q = p), IsStarProjection (q - p)
h : IsStarProjection (q - p)
⊢ p ≤ q

Tactic:
simpa using h.nonneg

Premises used: IsStarProjection.nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
tfae_2_to_3 : ∀ (a : q * p = p), p * q = p
tfae_3_to_4 : ∀ (a : p * q = p), IsStarProjection (q - p)
⊢ ∀ (a : IsStarProjection (q - p)), p ≤ q

Tactic:
tfae_have 4 → 1 := fun h ↦ by simpa using h.nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
tfae_2_to_3 : ∀ (a : q * p = p), p * q = p
tfae_3_to_4 : ∀ (a : p * q = p), IsStarProjection (q - p)
tfae_4_to_1 : ∀ (a : IsStarProjection (q - p)), p ≤ q
⊢ IsStarProjection (q - p)

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
tfae_2_to_3 : ∀ (a : q * p = p), p * q = p
tfae_3_to_4 : ∀ (a : p * q = p), IsStarProjection (q - p)
tfae_4_to_1 : ∀ (a : IsStarProjection (q - p)), p ≤ q
⊢ IsIdempotentElem (q - p)

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
tfae_2_to_3 : ∀ (a : q * p = p), p * q = p
tfae_3_to_4 : ∀ (a : p * q = p), IsStarProjection (q - p)
tfae_4_to_1 : ∀ (a : IsStarProjection (q - p)), p ≤ q
⊢ IsStarProjection (q - p) ↔ IsIdempotentElem (q - p)

Tactic:
4 ↔ 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
tfae_2_to_3 : ∀ (a : q * p = p), p * q = p
tfae_3_to_4 : ∀ (a : p * q = p), IsStarProjection (q - p)
tfae_4_to_1 : ∀ (a : IsStarProjection (q - p)), p ≤ q
⊢ IsStarProjection (q - p) ↔ IsIdempotentElem (q - p)

Tactic:
simp [isStarProjection_iff, hq.isSelfAdjoint.sub hp.isSelfAdjoint]

Premises used: IsSelfAdjoint.sub, isStarProjection_iff, IsStarProjection.isSelfAdjoint
-- Module: Mathlib.Analysis.CStarAlgebra.Projection
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : ∀ (a : p ≤ q), q * p = p
tfae_2_to_3 : ∀ (a : q * p = p), p * q = p
tfae_3_to_4 : ∀ (a : p * q = p), IsStarProjection (q - p)
tfae_4_to_1 : ∀ (a : IsStarProjection (q - p)), p ≤ q
⊢ IsStarProjection (q - p) ↔ IsIdempotentElem (q - p)

Tactic:
tfae_have 4 ↔ 5 := by simp [isStarProjection_iff, hq.isSelfAdjoint.sub hp.isSelfAdjoint]