awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ :
  Eq (α := A → Unitization ℂ A) (inr ∘ cfcₙ (p := IsSelfAdjoint) f) fun (x : A) ↦
    (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A)
h₂ :
  Eq.{u_1 + 1} (α := (x : A) → Unitization ℂ A) (fun (x : A) ↦ (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A))
    fun (x : A) ↦ cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)
⊢ ConvexOn ℝ (β := Unitization ℂ A) s (inr ∘ cfcₙ (p := IsSelfAdjoint) f)
have pos : ConvexOn ℝ (β := Unitization ℂ A) s fun (x : A) ↦ cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)
Tactic: rw [h₁, h₂]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ :
  Eq (α := A → Unitization ℂ A) (inr ∘ cfcₙ (p := IsSelfAdjoint) f) fun (x : A) ↦
    (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A)
h₂ :
  Eq.{u_1 + 1} (α := (x : A) → Unitization ℂ A) (fun (x : A) ↦ (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A))
    fun (x : A) ↦ cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)
⊢ ConvexOn ℝ (β := Unitization ℂ A) s fun (x : A) ↦ cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)
have h₃ : ConvexOn ℝ (E := A)
  (Set.preimage (β := Unitization ℂ A) (⇑inrl : (a : A) → Unitization ℂ A) ((⇑inrl : (a : A) → Unitization ℂ A) '' s))
  (cfc (p := IsSelfAdjoint) f ∘ (⇑inrl : (a : A) → Unitization ℂ A))
Tactic: have h₃ : ConvexOn ℝ (inrl ⁻¹' inrl '' s) ((cfc f) ∘ inrl) :=
    ConvexOn.comp_linearMap (g := inrl) hf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ :
  Eq (α := A → Unitization ℂ A) (inr ∘ cfcₙ (p := IsSelfAdjoint) f) fun (x : A) ↦
    (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A)
h₂ :
  Eq.{u_1 + 1} (α := (x : A) → Unitization ℂ A) (fun (x : A) ↦ (↑(cfcₙ (p := IsSelfAdjoint) f x) : Unitization ℂ A))
    fun (x : A) ↦ cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)
h₃ :
  ConvexOn ℝ (E := A)
    (Set.preimage (β := Unitization ℂ A) (⇑inrl : (a : A) → Unitization ℂ A) ((⇑inrl : (a : A) → Unitization ℂ A) '' s))
    (cfc (p := IsSelfAdjoint) f ∘ (⇑inrl : (a : A) → Unitization ℂ A))
⊢ ConvexOn ℝ (β := Unitization ℂ A) s fun (x : A) ↦ cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)
have pos : ∀ (h₃ : ConvexOn ℝ s (cfc (p := IsSelfAdjoint) f ∘ (⇑inrl : (a : A) → Unitization ℂ A))),
  ConvexOn ℝ (β := Unitization ℂ A) s fun (x : A) ↦ cfc (p := IsSelfAdjoint) f (↑x : Unitization ℂ A)
Tactic: rwa [Set.preimage_image_eq _ inrHom_injective] at h₃
Cleared hypotheses: h₃
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConcaveOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
⊢ ConcaveOn ℝ s (- -cfcₙ (p := IsSelfAdjoint) f)
have rw : ConcaveOn ℝ s (-cfcₙ (p := IsSelfAdjoint) (-f))
Tactic: rw [← cfcₙ_neg' f]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConcaveOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
⊢ ConcaveOn ℝ s (-cfcₙ (p := IsSelfAdjoint) (-f))
have refine : ConvexOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) (-f))
Tactic: refine (convexOn_cfcₙ_of_convexOn_cfc ?_).neg
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConcaveOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
⊢ ConvexOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) (-f))
have rw : ConvexOn ℝ (inr '' s) (-cfc (p := IsSelfAdjoint) f)
Tactic: rw [cfc_neg']
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConcaveOn ℝ (inr '' s) (cfc (p := IsSelfAdjoint) f)
⊢ ConcaveOn ℝ s (cfcₙ (p := IsSelfAdjoint) f)
have this : ConcaveOn ℝ s (- -cfcₙ (p := IsSelfAdjoint) f)
Tactic: have : ConcaveOn ℝ s (- -cfcₙ f) := by
    rw [← cfcₙ_neg' f]
    refine (convexOn_cfcₙ_of_convexOn_cfc ?_).neg
    rw [cfc_neg']
    exact hf.neg
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
⊢ Membership.mem (γ := Set (Unitization ℂ A)) (Icc 0 1) (↑x : Unitization ℂ A) ↔ 0 ≤ x ∧ ‖x‖ ≤ 1
have simp : 0 ≤ x → (LE.le (α := Unitization ℂ A) (↑x : Unitization ℂ A) 1 ↔ ‖x‖ ≤ 1)
Tactic: simp only [mem_Icc, inr_nonneg_iff, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
⊢ 0 ≤ x → (LE.le (α := Unitization ℂ A) (↑x : Unitization ℂ A) 1 ↔ ‖x‖ ≤ 1)
have rw : LE.le (α := Unitization ℂ A) 0 (↑x : Unitization ℂ A) →
  (norm (E := Unitization ℂ A) (↑x : Unitization ℂ A) ≤ 1 ↔ LE.le (α := Unitization ℂ A) (↑x : Unitization ℂ A) 1)
Tactic: rw [← norm_inr (𝕜 := ℂ), ← inr_nonneg_iff, iff_comm]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ Eq.{u_1 + 1} (α := Set A) (preimage (β := Unitization ℂ A) inr (Icc 0 1)) ({x : A | 0 ≤ x} ∩ closedBall 0 1)
have h : ∀ (x : A),
  Membership.mem (γ := Set A) (preimage (β := Unitization ℂ A) inr (Icc 0 1)) x ↔
    Membership.mem (γ := Set A) ({x : A | 0 ≤ x} ∩ closedBall 0 1) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a e : A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ a * e = a ∧ e * a = a
have suffices : a * e = a
Tactic: suffices a * e = a from
    ⟨this, by simpa [ha.star_eq, he.isSelfAdjoint.star_eq] using congr(star $this)⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a e : A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ a * e = a
have suffices : ∀ (a e : Unitization ℂ A), IsStarProjection e → 0 ≤ a → a ≤ e → a * e = a
Tactic: suffices ∀ a e : A⁺¹, IsStarProjection e → 0 ≤ a → a ≤ e → a * e = a from
    mod_cast this a e he.inr ha.inr (inr_le_iff a e |>.mpr hae)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a_1 e_1 : A
he_1 : IsStarProjection e_1
ha_1 : 0 ≤ a_1
hae_1 : a_1 ≤ e_1
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ a * e = a
have suffices : sqrt a * (1 - e) = 0
Tactic: suffices sqrt a * (1 - e : A⁺¹) = 0 by
    simpa [← mul_assoc, sqrt_mul_sqrt_self a, mul_sub, sub_eq_zero, eq_comm (a := a)]
      using congr(sqrt a * $this)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a_1 e_1 : A
he_1 : IsStarProjection e_1
ha_1 : 0 ≤ a_1
hae_1 : a_1 ≤ e_1
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ sqrt a * (1 - e) = 0
have rw : star (1 - e) * a * (1 - e) = 0
Tactic: rw [← norm_eq_zero, ← sq_eq_zero_iff, ← norm_star_mul_mul_self_of_nonneg, norm_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a_1 e_1 : A
he_1 : IsStarProjection e_1
ha_1 : 0 ≤ a_1
hae_1 : a_1 ≤ e_1
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ star (1 - e) * a * (1 - e) = 0
have refine : star (1 - e) * a * (1 - e) ≤ 0
Tactic: refine le_antisymm ?_ <| star_left_conjugate_nonneg ha _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a_1 e_1 : A
he_1 : IsStarProjection e_1
ha_1 : 0 ≤ a_1
hae_1 : a_1 ≤ e_1
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ star (1 - e) * a * (1 - e) ≤ 0
have grw : star (1 - e) * e * (1 - e) ≤ 0
Tactic: grw [star_left_conjugate_le_conjugate hae (1 - e), mul_assoc, he.mul_one_sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a_1 e_1 : A
he_1 : IsStarProjection e_1
ha_1 : 0 ≤ a_1
hae_1 : a_1 ≤ e_1
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
grw : star (1 - e) * e * (1 - e) ≤ 0
⊢ star (1 - e) * a * (1 - e) ≤ 0
have grw₁ : star (1 - e) * (e * (1 - e)) ≤ 0
Tactic: grw [star_left_conjugate_le_conjugate hae (1 - e), mul_assoc, he.mul_one_sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a_1 e_1 : A
he_1 : IsStarProjection e_1
ha_1 : 0 ≤ a_1
hae_1 : a_1 ≤ e_1
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
grw : star (1 - e) * e * (1 - e) ≤ 0
grw₁ : star (1 - e) * (e * (1 - e)) ≤ 0
⊢ star (1 - e) * a * (1 - e) ≤ 0
have grw₂ : star (1 - e) * 0 ≤ 0
Tactic: grw [star_left_conjugate_le_conjugate hae (1 - e), mul_assoc, he.mul_one_sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a_1 e_1 : A
he_1 : IsStarProjection e_1
ha_1 : 0 ≤ a_1
hae_1 : a_1 ≤ e_1
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
grw : star (1 - e) * e * (1 - e) ≤ 0
grw₁ : star (1 - e) * (e * (1 - e)) ≤ 0
grw₂ : star (1 - e) * 0 ≤ 0
⊢ star (1 - e) * a * (1 - e) ≤ 0
have grw₃ : LE.le.{u_1} (α := Unitization ℂ A) 0 0
Tactic: grw [star_left_conjugate_le_conjugate hae (1 - e), mul_assoc, he.mul_one_sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ n
have rw : 0 ≤ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ n) a
Tactic: rw [← cfc_pow_id (R := ℝ≥0) a]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 1 ≤ a
⊢ Monotone.{0, u_1} (β := A) fun (x : ℕ) ↦ a ^ x
have ha' : 0 ≤ a
Tactic: have ha' : 0 ≤ a := zero_le_one.trans ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 1 ≤ a
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
⊢ a ^ n ≤ a ^ m
have rw : ∀ x ∈ spectrum ℝ a, x ^ n ≤ x ^ m
Tactic: rw [← cfc_pow_id (R := ℝ) a, ← cfc_pow_id (R := ℝ) a, cfc_le_iff ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 1 ≤ a
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ n ≤ x ^ m
have rw : ∀ (ha : ∀ x ∈ spectrum ℝ a, 1 ≤ x) (ha' : 0 ≤ a) ⦃n m : ℕ⦄ (hnm : n ≤ m), ∀ x ∈ spectrum ℝ a, x ^ n ≤ x ^ m
Tactic: rw [CFC.one_le_iff (R := ℝ) a] at ha
Cleared hypotheses: ha, ha', n, m, hnm
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : ∀ x ∈ spectrum ℝ a, 1 ≤ x
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ n ≤ x ^ m
have h : ∀ (x : ℝ) (hx : x ∈ spectrum ℝ a) (this : 1 ≤ x), x ^ n ≤ x ^ m
Tactic: peel ha with x hx _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n m : ℕ
hnm : n ≤ m
⊢ a ^ m ≤ a ^ n
have rw : ∀ x ∈ spectrum ℝ a, x ^ m ≤ x ^ n
Tactic: rw [← cfc_pow_id (R := ℝ) a, ← cfc_pow_id (R := ℝ) a, cfc_le_iff ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n m : ℕ
hnm : n ≤ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ m ≤ x ^ n
have rw : ∀ (ha₁ : ∀ x ∈ spectrum ℝ a, x ≤ 1) ⦃n m : ℕ⦄ (hnm : n ≤ m), ∀ x ∈ spectrum ℝ a, x ^ m ≤ x ^ n
Tactic: rw [CFC.le_one_iff (R := ℝ) a] at ha₁
Cleared hypotheses: ha₁, n, m, hnm
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha₀ : 0 ≤ a
ha₁ : ∀ x ∈ spectrum ℝ a, x ≤ 1
n m : ℕ
hnm : n ≤ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ m ≤ x ^ n
have h : ∀ (x : ℝ) (hx : x ∈ spectrum ℝ a) (this : x ≤ 1), x ^ m ≤ x ^ n
Tactic: peel ha₁ with x hx _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi (goal)
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : (i : ι) → NonUnitalRing (A i)
inst_9 : (i : ι) → Module.{u_3, u_4} S (A i)
inst_10 : (i : ι) → Module.{u_2, u_4} R (A i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R S (A i)
inst_12 : ∀ (i : ι), SMulCommClass.{u_2, u_4, u_4} R (A i) (A i)
inst_13 : ∀ (i : ι), IsScalarTower.{u_2, u_4, u_4} R (A i) (A i)
inst_14 : (i : ι) → StarRing (A i)
inst_15 : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst_16 : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst_17 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst_18 : ∀ (i : ι), ContinuousMapZero.UniqueHom.{u_2, u_4} R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ (i : ι), quasispectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
⊢ cfcₙ (p := p) f a = fun (i : ι) ↦ cfcₙ (p := q i) f (a i)
have pos : ∀ (hf₀ : f 0 = 0), cfcₙ (p := p) f a = fun (i : ι) ↦ cfcₙ (p := q i) f (a i)
Tactic: by_cases hf₀ : f 0 = 0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi (goal)
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : (i : ι) → NonUnitalRing (A i)
inst_9 : (i : ι) → Module.{u_3, u_4} S (A i)
inst_10 : (i : ι) → Module.{u_2, u_4} R (A i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R S (A i)
inst_12 : ∀ (i : ι), SMulCommClass.{u_2, u_4, u_4} R (A i) (A i)
inst_13 : ∀ (i : ι), IsScalarTower.{u_2, u_4, u_4} R (A i) (A i)
inst_14 : (i : ι) → StarRing (A i)
inst_15 : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst_16 : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst_17 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst_18 : ∀ (i : ι), ContinuousMapZero.UniqueHom.{u_2, u_4} R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ (i : ι), quasispectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
pos : ∀ (hf₀ : f 0 = 0), cfcₙ (p := p) f a = fun (i : ι) ↦ cfcₙ (p := q i) f (a i)
⊢ cfcₙ (p := p) f a = fun (i : ι) ↦ cfcₙ (p := q i) f (a i)
have neg : ∀ (hf₀ : ¬f 0 = 0), cfcₙ (p := p) f a = fun (i : ι) ↦ cfcₙ (p := q i) f (a i)
Tactic: by_cases hf₀ : f 0 = 0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi (goal)
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : (i : ι) → NonUnitalRing (A i)
inst_9 : (i : ι) → Module.{u_3, u_4} S (A i)
inst_10 : (i : ι) → Module.{u_2, u_4} R (A i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R S (A i)
inst_12 : ∀ (i : ι), SMulCommClass.{u_2, u_4, u_4} R (A i) (A i)
inst_13 : ∀ (i : ι), IsScalarTower.{u_2, u_4, u_4} R (A i) (A i)
inst_14 : (i : ι) → StarRing (A i)
inst_15 : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst_16 : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst_17 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst_18 : ∀ (i : ι), ContinuousMapZero.UniqueHom.{u_2, u_4} R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ (i : ι), quasispectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
hf₀ : f 0 = 0
⊢ cfcₙ (p := p) f a = fun (i : ι) ↦ cfcₙ (p := q i) f (a i)
have pos : ∀ (i : ι), cfcₙ (p := p) f a i = cfcₙ (p := q i) f (a i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : (i : ι) → NonUnitalRing (A i)
inst_9 : (i : ι) → Module.{u_3, u_4} S (A i)
inst_10 : (i : ι) → Module.{u_2, u_4} R (A i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R S (A i)
inst_12 : ∀ (i : ι), SMulCommClass.{u_2, u_4, u_4} R (A i) (A i)
inst_13 : ∀ (i : ι), IsScalarTower.{u_2, u_4, u_4} R (A i) (A i)
inst_14 : (i : ι) → StarRing (A i)
inst_15 : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst_16 : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst_17 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst_18 : ∀ (i : ι), ContinuousMapZero.UniqueHom.{u_2, u_4} R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ (i : ι), quasispectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
hf₀ : f 0 = 0
i : ι
⊢ cfcₙ (p := p) f a i = cfcₙ (p := q i) f (a i)
have this : Nonempty ι
Tactic: have : Nonempty ι := ⟨i⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi (goal)
Goal:
A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommRing S
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : Algebra R S
inst_8 : NonUnitalRing A
inst_9 : NonUnitalRing B
inst_10 : Module S A
inst_11 : Module R A
inst_12 : Module R B
inst_13 : Module S B
inst_14 : SMulCommClass R A A
inst_15 : SMulCommClass R B B
inst_16 : IsScalarTower R A A
inst_17 : IsScalarTower R B B
inst_18 : StarRing A
inst_19 : StarRing B
inst_20 : TopologicalSpace A
inst_21 : TopologicalSpace B
inst_22 : IsScalarTower R S A
inst_23 : IsScalarTower R S B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst_24 : NonUnitalContinuousFunctionalCalculus R (A × B) pab
inst_25 : NonUnitalContinuousFunctionalCalculus R A pa
inst_26 : NonUnitalContinuousFunctionalCalculus R B pb
inst_27 : ContinuousMapZero.UniqueHom R A
inst_28 : ContinuousMapZero.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (quasispectrum R a ∪ quasispectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
⊢ cfcₙ (p := pab) f (a, b) = (cfcₙ (p := pa) f a, cfcₙ (p := pb) f b)
have by_cases : ∀ (hf₀ : f 0 = 0), cfcₙ (p := pab) f (a, b) = (cfcₙ (p := pa) f a, cfcₙ (p := pb) f b)
Tactic: by_cases hf₀ : f 0 = 0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi (goal)
Goal:
A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommRing S
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : Algebra R S
inst_8 : NonUnitalRing A
inst_9 : NonUnitalRing B
inst_10 : Module S A
inst_11 : Module R A
inst_12 : Module R B
inst_13 : Module S B
inst_14 : SMulCommClass R A A
inst_15 : SMulCommClass R B B
inst_16 : IsScalarTower R A A
inst_17 : IsScalarTower R B B
inst_18 : StarRing A
inst_19 : StarRing B
inst_20 : TopologicalSpace A
inst_21 : TopologicalSpace B
inst_22 : IsScalarTower R S A
inst_23 : IsScalarTower R S B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst_24 : NonUnitalContinuousFunctionalCalculus R (A × B) pab
inst_25 : NonUnitalContinuousFunctionalCalculus R A pa
inst_26 : NonUnitalContinuousFunctionalCalculus R B pb
inst_27 : ContinuousMapZero.UniqueHom R A
inst_28 : ContinuousMapZero.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (quasispectrum R a ∪ quasispectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
by_cases : ∀ (hf₀ : f 0 = 0), cfcₙ (p := pab) f (a, b) = (cfcₙ (p := pa) f a, cfcₙ (p := pb) f b)
⊢ cfcₙ (p := pab) f (a, b) = (cfcₙ (p := pa) f a, cfcₙ (p := pb) f b)
have by_cases₁ : ∀ (hf₀ : ¬f 0 = 0), cfcₙ (p := pab) f (a, b) = (cfcₙ (p := pa) f a, cfcₙ (p := pb) f b)
Tactic: by_cases hf₀ : f 0 = 0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi (goal)
Goal:
A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommRing S
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : Algebra R S
inst_8 : NonUnitalRing A
inst_9 : NonUnitalRing B
inst_10 : Module S A
inst_11 : Module R A
inst_12 : Module R B
inst_13 : Module S B
inst_14 : SMulCommClass R A A
inst_15 : SMulCommClass R B B
inst_16 : IsScalarTower R A A
inst_17 : IsScalarTower R B B
inst_18 : StarRing A
inst_19 : StarRing B
inst_20 : TopologicalSpace A
inst_21 : TopologicalSpace B
inst_22 : IsScalarTower R S A
inst_23 : IsScalarTower R S B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst_24 : NonUnitalContinuousFunctionalCalculus R (A × B) pab
inst_25 : NonUnitalContinuousFunctionalCalculus R A pa
inst_26 : NonUnitalContinuousFunctionalCalculus R B pb
inst_27 : ContinuousMapZero.UniqueHom R A
inst_28 : ContinuousMapZero.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (quasispectrum R a ∪ quasispectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
hf₀ : f 0 = 0
⊢ cfcₙ (p := pab) f (a, b) = (cfcₙ (p := pa) f a, cfcₙ (p := pb) f b)
have ext : (cfcₙ (p := pab) f (a, b)).1 = (cfcₙ (p := pa) f a, cfcₙ (p := pb) f b).1
Tactic: ext