awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
C : ℝ≥0
hmain : ∀ (a : A₁), 0 ≤ a → norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖
x : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖x‖
hy : x = ∑ i : Fin 4, I ^ (↑i : ℕ) • y i
⊢ ∑ i : Fin 4, ‖HSMul.hSMul (β := A₂) (I ^ (↑i : ℕ)) ((f : (a : A₁) → A₂) (y i) : A₂)‖ ≤ (↑(4 * C) : ℝ) * ‖x‖
have simp : ∑ x : Fin 4, norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (y x) : A₂) ≤ (↑(4 * C) : ℝ) * ‖x‖
Tactic: simp only [norm_smul, norm_pow, norm_I, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
C : ℝ≥0
hmain : ∀ (a : A₁), 0 ≤ a → norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖
x : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖x‖
hy : x = ∑ i : Fin 4, I ^ (↑i : ℕ) • y i
⊢ ∑ x : Fin 4, norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (y x) : A₂) ≤ (↑(4 * C) : ℝ) * ‖x‖
have apply : ∀ (i : Fin 4),
  Membership.mem (γ := Finset (Fin 4)) Finset.univ i →
    norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (y i) : A₂) ≤ (fun (x_2 : Fin 4) ↦ (↑C : ℝ) * ‖x‖) i
Tactic: apply Finset.sum_le_sum (g := fun _ ↦ C * ‖x‖) (fun i _ ↦ ?_) |>.trans <| by simp [mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
C : ℝ≥0
hmain : ∀ (a : A₁), 0 ≤ a → norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖
x : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖x‖
hy : x = ∑ i : Fin 4, I ^ (↑i : ℕ) • y i
i : Fin 4
h : Membership.mem (γ := Finset (Fin 4)) Finset.univ i
⊢ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (y i) : A₂) ≤ (fun (x_1 : Fin 4) ↦ (↑C : ℝ) * ‖x‖) i
have apply : (↑C : ℝ) * ‖y i‖ ≤ (fun (x_1 : Fin 4) ↦ (↑C : ℝ) * ‖x‖) i
Tactic: apply hmain _ (hy_nonneg i) |>.trans
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
C : ℝ≥0
hmain : ∀ (a : A₁), 0 ≤ a → norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖
x : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖x‖
hy : x = ∑ i : Fin 4, I ^ (↑i : ℕ) • y i
i : Fin 4
h : Membership.mem (γ := Finset (Fin 4)) Finset.univ i
⊢ (↑C : ℝ) * ‖y i‖ ≤ (↑C : ℝ) * ‖x‖
have hbc : ‖y i‖ ≤ ‖x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
⊢ ∃ (C : ℝ≥0), ∀ (a : A₁), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖
have suffices : ∃ (C : ℝ≥0), ∀ (a : A₁), 0 ≤ a → norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖
Tactic: suffices h_nonneg : ∃ C : ℝ≥0, ∀ a, 0 ≤ a → ‖f a‖ ≤ C * ‖a‖ by
    obtain ⟨C, hmain⟩ := h_nonneg
    refine ⟨4 * C, fun x ↦ ?_⟩
    obtain ⟨y, hy_nonneg, hy_norm, hy⟩ := CStarAlgebra.exists_sum_four_nonneg x
    conv_lhs => rw [hy]
    simp only [map_sum, map_smul]
    apply norm_sum_le _ _ |>.trans
    simp only [norm_smul, norm_pow, norm_I, one_pow, one_mul]
    apply Finset.sum_le_sum (g := fun _ ↦ C * ‖x‖) (fun i _ ↦ ?_) |>.trans <| by simp [mul_assoc]
    apply hmain _ (hy_nonneg i) |>.trans
    simp only
    gcongr
    exact hy_norm i
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
⊢ ∃ (C : ℝ≥0), ∀ (a : A₁), 0 ≤ a → norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖
have by_contra! : ∀ (hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)), False
Tactic: by_contra! hcontra
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (hypothesis)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
n : ℕ
⊢ ∃ (x : A₁), 0 ≤ x ∧ ‖x‖ = 1 ∧ HPow.hPow (α := ℝ) 2 (2 * n) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)
have hx₁ : 0 ≤
  Classical.choose (p := fun (x : A₁) ↦
    0 ≤ x ∧ (↑(HPow.hPow (α := ℝ≥0) 2 (2 * n)) : ℝ) * ‖x‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)) sorry
Tactic: obtain ⟨hx₁, hx₂⟩ := Classical.choose_spec (hcontra (2 ^ (2 * n)))
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (hypothesis)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
n : ℕ
hx₁ :
  0 ≤
    Classical.choose (p := fun (x : A₁) ↦
      0 ≤ x ∧ (↑(HPow.hPow (α := ℝ≥0) 2 (2 * n)) : ℝ) * ‖x‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)) ⋯
⊢ ∃ (x : A₁), 0 ≤ x ∧ ‖x‖ = 1 ∧ HPow.hPow (α := ℝ) 2 (2 * n) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)
have hx₂ : (↑(HPow.hPow (α := ℝ≥0) 2 (2 * n)) : ℝ) *
    ‖Classical.choose (p := fun (x : A₁) ↦
        0 ≤ x ∧ (↑(HPow.hPow (α := ℝ≥0) 2 (2 * n)) : ℝ) * ‖x‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)) sorry‖ <
  norm.{u_2} (E := A₂)
    ((f : (a : A₁) → A₂)
        (Classical.choose (p := fun (x : A₁) ↦
          0 ≤ x ∧ (↑(HPow.hPow (α := ℝ≥0) 2 (2 * n)) : ℝ) * ‖x‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂))
          sorry) :
      A₂)
Tactic: obtain ⟨hx₁, hx₂⟩ := Classical.choose_spec (hcontra (2 ^ (2 * n)))
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (hypothesis)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
n : ℕ
x : A₁ :=
  Classical.choose (p := fun (x : A₁) ↦
    0 ≤ x ∧ (↑(HPow.hPow (α := ℝ≥0) 2 (2 * n)) : ℝ) * ‖x‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)) ⋯
hx₁ : 0 ≤ x
hx₂ : (↑(HPow.hPow (α := ℝ≥0) 2 (2 * n)) : ℝ) * ‖x‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)
⊢ ∃ (x : A₁), 0 ≤ x ∧ ‖x‖ = 1 ∧ HPow.hPow (α := ℝ) 2 (2 * n) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)
have hx : 0 < ‖x‖
Tactic: have hx := (eq_zero_or_norm_pos x).resolve_left (fun hx ↦ by simp_all)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
n : ℕ
x : A₁ :=
  Classical.choose (p := fun (x : A₁) ↦
    0 ≤ x ∧ (↑(HPow.hPow (α := ℝ≥0) 2 (2 * n)) : ℝ) * ‖x‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)) ⋯
hx₁ : 0 ≤ x
hx₂ : (↑(HPow.hPow (α := ℝ≥0) 2 (2 * n)) : ℝ) * ‖x‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)
hx : 0 < ‖x‖
⊢ ∃ (x : A₁), 0 ≤ x ∧ ‖x‖ = 1 ∧ HPow.hPow (α := ℝ) 2 (2 * n) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)
have refine_1 : ‖‖x‖⁻¹ • x‖ = 1
Tactic: refine ⟨‖x‖⁻¹ • x, smul_nonneg (by positivity) hx₁, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
n : ℕ
x : A₁ :=
  Classical.choose (p := fun (x : A₁) ↦
    0 ≤ x ∧ (↑(HPow.hPow (α := ℝ≥0) 2 (2 * n)) : ℝ) * ‖x‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)) ⋯
hx₁ : 0 ≤ x
hx₂ : (↑(HPow.hPow (α := ℝ≥0) 2 (2 * n)) : ℝ) * ‖x‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)
hx : 0 < ‖x‖
refine_1 : ‖‖x‖⁻¹ • x‖ = 1
⊢ ∃ (x : A₁), 0 ≤ x ∧ ‖x‖ = 1 ∧ HPow.hPow (α := ℝ) 2 (2 * n) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)
have refine_2 : HPow.hPow (α := ℝ) 2 (2 * n) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (‖x‖⁻¹ • x) : A₂)
Tactic: refine ⟨‖x‖⁻¹ • x, smul_nonneg (by positivity) hx₁, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (hypothesis)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
⊢ False
have this : ∀ (n : ℕ),
  ∃ (x : A₁), 0 ≤ x ∧ ‖x‖ = 1 ∧ HPow.hPow (α := ℝ) 2 (2 * n) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)
Tactic: have (n : ℕ) : ∃ x, 0 ≤ x ∧ ‖x‖ = 1 ∧ 2 ^ (2 * n) < ‖f x‖ := by
    obtain ⟨hx₁, hx₂⟩ := Classical.choose_spec (hcontra (2 ^ (2 * n)))
    set x := Classical.choose (hcontra (2 ^ (2 * n)))
    have hx := (eq_zero_or_norm_pos x).resolve_left (fun hx ↦ by simp_all)
    refine ⟨‖x‖⁻¹ • x, smul_nonneg (by positivity) hx₁, ?_, ?_⟩
    · simp [norm_smul, inv_mul_cancel₀ hx.ne']
    · simpa [norm_smul] using (lt_inv_mul_iff₀' hx).mpr hx₂
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
this :
  ∀ (n : ℕ),
    ∃ (x : A₁), 0 ≤ x ∧ ‖x‖ = 1 ∧ HPow.hPow (α := ℝ) 2 (2 * n) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)
⊢ False
have choose : ∀ (x : (n : ℕ) → A₁)
  (hx :
    ∀ (n : ℕ),
      0 ≤ x n ∧ ‖x n‖ = 1 ∧ HPow.hPow (α := ℝ) 2 (2 * n) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x n) : A₂)),
  False
Tactic: choose x hx using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (hypothesis)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx :
  ∀ (n : ℕ), 0 ≤ x n ∧ ‖x n‖ = 1 ∧ HPow.hPow (α := ℝ) 2 (2 * n) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x n) : A₂)
⊢ False
have hx₁ : (∀ (x_1 : ℕ), 0 ≤ x x_1) ∧
  (∀ (x_1 : ℕ), ‖x x_1‖ = 1) ∧
    ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
Tactic: simp only [forall_and] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (hypothesis)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx :
  (∀ (x_1 : ℕ), 0 ≤ x x_1) ∧
    (∀ (x_1 : ℕ), ‖x x_1‖ = 1) ∧
      ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
⊢ False
have hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
Tactic: obtain ⟨hx_nonneg, hx_norm, hx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (hypothesis)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx :
  (∀ (x_1 : ℕ), 0 ≤ x x_1) ∧
    (∀ (x_1 : ℕ), ‖x x_1‖ = 1) ∧
      ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
⊢ False
have hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
Tactic: obtain ⟨hx_nonneg, hx_norm, hx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (hypothesis)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx :
  (∀ (x_1 : ℕ), 0 ≤ x x_1) ∧
    (∀ (x_1 : ℕ), ‖x x_1‖ = 1) ∧
      ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
⊢ False
have hx₁ : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
Tactic: obtain ⟨hx_nonneg, hx_norm, hx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
⊢ Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
have refine : Summable (α := ℝ) fun (a : ℕ) ↦ ‖HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑a : ℤ)) • x a‖
Tactic: refine Summable.of_norm ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (hypothesis)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
⊢ Summable (α := ℝ) fun (a : ℕ) ↦ ‖HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑a : ℤ)) • x a‖
have this : LT.lt (α := ℝ) 2⁻¹ 1
Tactic: have : (2 : ℝ)⁻¹ < 1 := by norm_num
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (hypothesis)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
⊢ False
have x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
Tactic: have x_summable : Summable fun n : ℕ => (2 : ℝ) ^ (-(n : ℤ)) • x n := by
    refine Summable.of_norm ?_
    have : (2 : ℝ)⁻¹ < 1 := by norm_num
    simp [norm_smul, hx_norm, ← inv_pow, this]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
⊢ False
have obtain : ∀ (n : ℕ)
  (hn :
    norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
      HPow.hPow (α := ℝ) 2 n),
  False
Tactic: obtain ⟨n, hn⟩ : ∃ n : ℕ, ‖f (∑' (n : ℕ), (2 : ℝ) ^ (-(n : ℤ)) • x n)‖ < (2 : ℝ) ^ n :=
    tendsto_pow_atTop_atTop_of_one_lt one_lt_two |>.eventually_gt_atTop _
      |>.exists
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
⊢ False
have apply : HPow.hPow (α := ℝ) 2 n ≤
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
Tactic: apply hn.not_ge
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
⊢ HPow.hPow (α := ℝ) 2 n ≤
    norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
have trans : HPow.hPow (α := ℝ) 2 n ≤
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
Tactic: trans ‖f ((2 : ℝ) ^ (-n : ℤ) • x n)‖
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
trans :
  HPow.hPow (α := ℝ) 2 n ≤
    norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
⊢ HPow.hPow (α := ℝ) 2 n ≤
    norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
have trans₁ : norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) ≤
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
Tactic: trans ‖f ((2 : ℝ) ^ (-n : ℤ) • x n)‖
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (hypothesis)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
⊢ HPow.hPow (α := ℝ) 2 n ≤
    norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
have this : HPow.hPow (α := ℝ) 2 (2 * n) ≤ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x n) : A₂)
Tactic: have := hx n |>.le
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (hypothesis)
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
this : HPow.hPow (α := ℝ) 2 (2 * n) ≤ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x n) : A₂)
⊢ HPow.hPow (α := ℝ) 2 n ≤
    norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
have this₁ : HPow.hPow (α := ℝ) 2 n * HPow.hPow (α := ℝ) 2 n ≤ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x n) : A₂)
Tactic: rw [pow_mul', sq] at this
Cleared hypotheses: this