awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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
conv_lhs : norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑ i : Fin 4, I ^ (↑i : ℕ) • y i) : A₂) ≤ (↑(4 * C) : ℝ) * ‖x‖
⊢ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂) ≤ (↑(4 * C) : ℝ) * ‖x‖

Tactic:
conv_lhs => rw [hy]
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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
simp :
  norm.{u_2} (E := A₂) (∑ x : Fin 4, HSMul.hSMul (β := A₂) (I ^ (↑x : ℕ)) ((f : (a : A₁) → A₂) (y x) : A₂)) ≤
    (↑(4 * C) : ℝ) * ‖x‖
⊢ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑ i : Fin 4, I ^ (↑i : ℕ) • y i) : A₂) ≤ (↑(4 * C) : ℝ) * ‖x‖

Tactic:
simp only [map_sum, map_smul]

Premises used: map_sum, map_smul
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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
apply : ∑ i : Fin 4, ‖HSMul.hSMul (β := A₂) (I ^ (↑i : ℕ)) ((f : (a : A₁) → A₂) (y i) : A₂)‖ ≤ (↑(4 * C) : ℝ) * ‖x‖
⊢ norm.{u_2} (E := A₂) (∑ x : Fin 4, HSMul.hSMul (β := A₂) (I ^ (↑x : ℕ)) ((f : (a : A₁) → A₂) (y x) : A₂)) ≤
    (↑(4 * C) : ℝ) * ‖x‖

Tactic:
apply norm_sum_le _ _ |>.trans

Premises used: LE.le.trans, norm_sum_le
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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
simp : ∑ x : Fin 4, norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (y x) : A₂) ≤ (↑(4 * C) : ℝ) * ‖x‖
⊢ ∑ i : Fin 4, ‖HSMul.hSMul (β := A₂) (I ^ (↑i : ℕ)) ((f : (a : A₁) → A₂) (y i) : A₂)‖ ≤ (↑(4 * C) : ℝ) * ‖x‖

Tactic:
simp only [norm_smul, norm_pow, norm_I, one_pow, one_mul]

Premises used: one_pow, norm_smul, norm_pow, Complex.norm_I, one_mul
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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, (↑C : ℝ) * ‖x‖ ≤ (↑(4 * C) : ℝ) * ‖x‖

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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
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
⊢ ∑ x : Fin 4, norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (y x) : A₂) ≤ (↑(4 * C) : ℝ) * ‖x‖

Tactic:
apply Finset.sum_le_sum (g := fun _ ↦ C * ‖x‖) (fun i _ ↦ ?_) |>.trans <| by simp [mul_assoc]

Premises used: Finset.sum_le_sum, LE.le.trans
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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
apply : (↑C : ℝ) * ‖y i‖ ≤ (fun (x_1 : Fin 4) ↦ (↑C : ℝ) * ‖x‖) i
⊢ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (y i) : A₂) ≤ (fun (x_1 : Fin 4) ↦ (↑C : ℝ) * ‖x‖) i

Tactic:
apply hmain _ (hy_nonneg i) |>.trans

Premises used: LE.le.trans
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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
hbc : ‖y i‖ ≤ ‖x‖
⊢ (↑C : ℝ) * ‖y i‖ ≤ (↑C : ℝ) * ‖x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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
⊢ ‖y i‖ ≤ ‖x‖

Tactic:
hy_norm i
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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
⊢ ‖y i‖ ≤ ‖x‖

Tactic:
exact hy_norm i
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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₂
suffices : ∃ (C : ℝ≥0), ∀ (a : A₁), 0 ≤ a → norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖
⊢ ∃ (C : ℝ≥0), ∀ (a : 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
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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₂
by_contra! :
  ∀ (hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)),
    False
⊢ ∃ (C : ℝ≥0), ∀ (a : A₁), 0 ≤ a → norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖

Tactic:
by_contra! hcontra
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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 : ℕ
⊢ 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₂)) ⋯

Tactic:
obtain ⟨hx₁, hx₂⟩ := Classical.choose_spec (hcontra (2 ^ (2 * n)))

Premises used: HMul.hMul, Classical.choose_spec, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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₂)) ⋯
⊢ (↑(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₂))
          ⋯‖ <
    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₂))
            ⋯) :
        A₂)

Tactic:
obtain ⟨hx₁, hx₂⟩ := Classical.choose_spec (hcontra (2 ^ (2 * n)))

Premises used: HMul.hMul, Classical.choose_spec, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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₂)) ⋯
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₂))
          ⋯‖ <
    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₂))
            ⋯) :
        A₂)
⊢ let x :=
    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₂)) ⋯;
  0 ≤ x

Tactic:
set x := Classical.choose (hcontra (2 ^ (2 * n)))

Premises used: HMul.hMul, HPow.hPow, Classical.choose, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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₂)) ⋯
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₂))
          ⋯‖ <
    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₂))
            ⋯) :
        A₂)
hx₃ :
  let x :=
    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₂)) ⋯;
  0 ≤ x
⊢ let x :=
    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₂)) ⋯;
  (↑(HPow.hPow (α := ℝ≥0) 2 (2 * n)) : ℝ) * ‖x‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)

Tactic:
set x := Classical.choose (hcontra (2 ^ (2 * n)))

Premises used: HMul.hMul, HPow.hPow, Classical.choose, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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 : x = 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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₂)
⊢ 0 < ‖x‖

Tactic:
have hx := (eq_zero_or_norm_pos x).resolve_left (fun hx ↦ by simp_all)
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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‖
⊢ 0 ≤ ‖x‖⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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
refine_2 : HPow.hPow (α := ℝ) 2 (2 * n) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (‖x‖⁻¹ • x) : A₂)
⊢ ∃ (x : A₁), 0 ≤ x ∧ ‖x‖ = 1 ∧ HPow.hPow (α := ℝ) 2 (2 * n) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)

Tactic:
refine ⟨‖x‖⁻¹ • x, smul_nonneg (by positivity) hx₁, ?_, ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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‖⁻¹ • x‖ = 1

Tactic:
simp [norm_smul, inv_mul_cancel₀ hx.ne']

Premises used: norm_smul, LT.lt.ne', inv_mul_cancel₀
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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‖
⊢ HPow.hPow (α := ℝ) 2 (2 * n) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (‖x‖⁻¹ • x) : A₂)

Tactic:
simpa [norm_smul] using (lt_inv_mul_iff₀' hx).mpr hx₂

Premises used: Iff.mpr, norm_smul, lt_inv_mul_iff₀'
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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₂)

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₂
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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₂)
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
⊢ False

Tactic:
choose x hx using this
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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₂)
⊢ (∀ (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

Premises used: forall_and
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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₂)
⊢ ∀ (x_1 : ℕ), 0 ≤ x x_1

Tactic:
obtain ⟨hx_nonneg, hx_norm, hx⟩ := hx
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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
⊢ ∀ (x_1 : ℕ), ‖x x_1‖ = 1

Tactic:
obtain ⟨hx_nonneg, hx_norm, hx⟩ := hx
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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
⊢ ∀ (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
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
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

Tactic:
Summable.of_norm ?_

Premises used: Summable.of_norm