awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
refine : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) (‖x.1‖ + ‖x.2‖) 2
⊢ ‖x‖ ≤ ‖x.1‖ + ‖x.2‖

Tactic:
refine abs_le_of_sq_le_sq' ?_ (by positivity) |>.2

Premises used: abs_le_of_sq_le_sq', And.right
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖⟪x.1, x.1⟫_A‖ + ‖⟪x.2, x.2⟫_A‖ = HPow.hPow (β := ℕ) ‖x.1‖ 2 + 0 + HPow.hPow (β := ℕ) ‖x.2‖ 2

Tactic:
simp [norm_sq_eq A]

Premises used: CStarModule.norm_sq_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
bc : 0 ≤ 2 * ‖x.1‖ * ‖x.2‖
⊢ HPow.hPow (β := ℕ) ‖x.1‖ 2 + 0 + HPow.hPow (β := ℕ) ‖x.2‖ 2 ≤
    HPow.hPow (β := ℕ) ‖x.1‖ 2 + 2 * ‖x.1‖ * ‖x.2‖ + HPow.hPow (β := ℕ) ‖x.2‖ 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ 0 ≤ 2 * ‖x.1‖ * ‖x.2‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ HPow.hPow (β := ℕ) ‖x.1‖ 2 + 2 * ‖x.1‖ * ‖x.2‖ + HPow.hPow (β := ℕ) ‖x.2‖ 2 = HPow.hPow (β := ℕ) (‖x.1‖ + ‖x.2‖) 2

Tactic:
ring
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
calc : ‖⟪x.1, x.1⟫_A‖ + ‖⟪x.2, x.2⟫_A‖ = HPow.hPow (β := ℕ) ‖x.1‖ 2 + 0 + HPow.hPow (β := ℕ) ‖x.2‖ 2
calc₁ :
  HPow.hPow (β := ℕ) ‖x.1‖ 2 + 0 + HPow.hPow (β := ℕ) ‖x.2‖ 2 ≤
    HPow.hPow (β := ℕ) ‖x.1‖ 2 + 2 * ‖x.1‖ * ‖x.2‖ + HPow.hPow (β := ℕ) ‖x.2‖ 2
calc₂ :
  HPow.hPow (β := ℕ) ‖x.1‖ 2 + 2 * ‖x.1‖ * ‖x.2‖ + HPow.hPow (β := ℕ) ‖x.2‖ 2 = HPow.hPow (β := ℕ) (‖x.1‖ + ‖x.2‖) 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) (‖x.1‖ + ‖x.2‖) 2

Tactic:
calc ‖x‖ ^ 2 ≤ ‖⟪x.1, x.1⟫_A‖ + ‖⟪x.2, x.2⟫_A‖ := prod_norm_sq x ▸ norm_add_le _ _
    _ = ‖x.1‖ ^ 2 + 0 + ‖x.2‖ ^ 2 := by simp [norm_sq_eq A]
    _ ≤ ‖x.1‖ ^ 2 + 2 * ‖x.1‖ * ‖x.2‖ + ‖x.2‖ ^ 2 := by gcongr; positivity
    _ = (‖x.1‖ + ‖x.2‖) ^ 2 := by ring

Premises used: Norm.norm, Prod.fst, HAdd.hAdd, Prod.snd
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x y z : C⋆ᵐᵒᵈ(A, E × F)
⊢ ⟪x.1, (y + z).1⟫_A + ⟪x.2, (y + z).2⟫_A = ⟪x.1, y.1⟫_A + ⟪x.2, y.2⟫_A + (⟪x.1, z.1⟫_A + ⟪x.2, z.2⟫_A)

Tactic:
simpa using add_add_add_comm ..

Premises used: add_add_add_comm
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
h : x = 0
⊢ ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0

Tactic:
simp [h]
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
refine : ∀ (h : ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0), x = 0
⊢ ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0 ↔ x = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
h : ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0
a :
  Eq (α := E × F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)
    ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) 0 : E × F)
⊢ x = 0

Tactic:
apply equiv A (E × F) |>.injective

Premises used: WithCStarModule.equiv, Equiv.injective, Prod
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
h : ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0
a :
  Eq.{u_2 + 1} (α := E) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).1
    ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) 0).1
a₁ :
  Eq.{u_3 + 1} (α := F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).2
    ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) 0).2
⊢ Eq (α := E × F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)
    ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) 0 : E × F)

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
h : ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0
⊢ Eq.{u_2 + 1} (α := E) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).1
    ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) 0).1

Tactic:
inner_self.mp <| le_antisymm ?_ (inner_self_nonneg (A := A))

Premises used: CStarModule.inner_self, le_antisymm, Iff.mp, CStarModule.inner_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
h : ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0
a :
  inner.{u_1, u_2} A (E := E) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).1
      ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).1 ≤
    0
⊢ Eq.{u_2 + 1} (α := E) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).1
    ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) 0).1

Tactic:
refine inner_self.mp <| le_antisymm ?_ (inner_self_nonneg (A := A))

Premises used: CStarModule.inner_self, le_antisymm, Iff.mp, CStarModule.inner_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
h : ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0
⊢ inner.{u_1, u_2} A (E := E) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).1
      ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).1 ≤
    0

Tactic:
le_add_of_nonneg_right CStarModule.inner_self_nonneg |>.trans_eq h

Premises used: LE.le.trans_eq, le_add_of_nonneg_right
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
h : ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0
⊢ inner.{u_1, u_2} A (E := E) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).1
      ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).1 ≤
    0

Tactic:
exact le_add_of_nonneg_right CStarModule.inner_self_nonneg |>.trans_eq h

Premises used: LE.le.trans_eq, le_add_of_nonneg_right
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
h : ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0
⊢ Eq.{u_3 + 1} (α := F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).2
    ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) 0).2

Tactic:
inner_self.mp <| le_antisymm ?_ (inner_self_nonneg (A := A))

Premises used: CStarModule.inner_self, le_antisymm, Iff.mp, CStarModule.inner_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
h : ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0
a :
  inner.{u_1, u_3} A (E := F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).2
      ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).2 ≤
    0
⊢ Eq.{u_3 + 1} (α := F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).2
    ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) 0).2

Tactic:
refine inner_self.mp <| le_antisymm ?_ (inner_self_nonneg (A := A))

Premises used: CStarModule.inner_self, le_antisymm, Iff.mp, CStarModule.inner_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
h : ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0
⊢ inner.{u_1, u_3} A (E := F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).2
      ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).2 ≤
    0

Tactic:
le_add_of_nonneg_left CStarModule.inner_self_nonneg |>.trans_eq h

Premises used: LE.le.trans_eq, le_add_of_nonneg_left
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
h : ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0
⊢ inner.{u_1, u_3} A (E := F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).2
      ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x).2 ≤
    0

Tactic:
exact le_add_of_nonneg_left CStarModule.inner_self_nonneg |>.trans_eq h

Premises used: LE.le.trans_eq, le_add_of_nonneg_left
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
⊢ ∀ {a : A} {x y : C⋆ᵐᵒᵈ(A, E × F)}, ⟪x.1, (a • y).1⟫_A + ⟪x.2, (a • y).2⟫_A = a * (⟪x.1, y.1⟫_A + ⟪x.2, y.2⟫_A)

Tactic:
simp [mul_add]

Premises used: mul_add
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
⊢ ∀ {z : ℂ} {x y : C⋆ᵐᵒᵈ(A, E × F)}, ⟪x.1, (z • y).1⟫_A + ⟪x.2, (z • y).2⟫_A = z • (⟪x.1, y.1⟫_A + ⟪x.2, y.2⟫_A)

Tactic:
simp [smul_add]

Premises used: smul_add
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x y : C⋆ᵐᵒᵈ(A, E × F)
⊢ star (⟪x.1, y.1⟫_A + ⟪x.2, y.2⟫_A) = ⟪y.1, x.1⟫_A + ⟪y.2, x.2⟫_A

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖x‖ = √‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Tactic:
rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖x‖ = √‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x y : C⋆ᵐᵒᵈ(A, E × F)
⊢ ⟪x, y⟫_A = ⟪x.1, y.1⟫_A + ⟪x.2, y.2⟫_A

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
simp : ‖⟪x.1, x.1⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖ ∧ ‖⟪x.2, x.2⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖
⊢ max ‖x.1‖ ‖x.2‖ ≤ √‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Tactic:
simp only [norm_eq_sqrt_norm_inner_self (A := A) (E := E),
    norm_eq_sqrt_norm_inner_self (A := A) (E := F), max_le_iff, norm_nonneg,
    Real.sqrt_le_sqrt_iff]

Premises used: Real.sqrt_le_sqrt_iff, CStarModule.norm_eq_sqrt_norm_inner_self, max_le_iff, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
left : ‖⟪x.1, x.1⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖
right : ‖⟪x.2, x.2⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖
⊢ ‖⟪x.1, x.1⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖ ∧ ‖⟪x.2, x.2⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Tactic:
constructor
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖⟪x.1, x.1⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Tactic:
CStarAlgebra.norm_le_norm_of_nonneg_of_le (A := A) ?_ ?_

Premises used: CStarAlgebra.norm_le_norm_of_nonneg_of_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
left : 0 ≤ ⟪x.1, x.1⟫_A
left₁ : ⟪x.1, x.1⟫_A ≤ ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A
⊢ ‖⟪x.1, x.1⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Tactic:
refine CStarAlgebra.norm_le_norm_of_nonneg_of_le (A := A) ?_ ?_

Premises used: CStarAlgebra.norm_le_norm_of_nonneg_of_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ 0 ≤ ⟪x.1, x.1⟫_A

Tactic:
aesop (add safe apply CStarModule.inner_self_nonneg)

Premises used: CStarModule.inner_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ⟪x.1, x.1⟫_A ≤ ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A

Tactic:
aesop (add safe apply CStarModule.inner_self_nonneg)

Premises used: CStarModule.inner_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖⟪x.2, x.2⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Tactic:
CStarAlgebra.norm_le_norm_of_nonneg_of_le (A := A) ?_ ?_

Premises used: CStarAlgebra.norm_le_norm_of_nonneg_of_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
right : 0 ≤ ⟪x.2, x.2⟫_A
right₁ : ⟪x.2, x.2⟫_A ≤ ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A
⊢ ‖⟪x.2, x.2⟫_A‖ ≤ ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Tactic:
refine CStarAlgebra.norm_le_norm_of_nonneg_of_le (A := A) ?_ ?_

Premises used: CStarAlgebra.norm_le_norm_of_nonneg_of_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ 0 ≤ ⟪x.2, x.2⟫_A

Tactic:
aesop (add safe apply CStarModule.inner_self_nonneg)

Premises used: CStarModule.inner_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ⟪x.2, x.2⟫_A ≤ ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A

Tactic:
aesop (add safe apply CStarModule.inner_self_nonneg)

Premises used: CStarModule.inner_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ Norm.norm (E := E × F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F) ≤ ‖x‖

Tactic:
max_le_prod_norm x

Premises used: WithCStarModule.max_le_prod_norm
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
apply :
  ‖x.1‖ + ‖x.2‖ ≤
    (↑2 : ℝ) *
      Norm.norm (E := E × F)
        (((linearEquiv ℂ A (E × F) : C⋆ᵐᵒᵈ(A, E × F) ≃ₗ[ℂ] E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)
⊢ ‖x‖ ≤
    (↑2 : ℝ) *
      Norm.norm (E := E × F)
        (((linearEquiv ℂ A (E × F) : C⋆ᵐᵒᵈ(A, E × F) ≃ₗ[ℂ] E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)

Tactic:
apply prod_norm_le_norm_add x |>.trans

Premises used: WithCStarModule.prod_norm_le_norm_add, LE.le.trans
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
simp :
  ‖x.1‖ + ‖x.2‖ ≤
    Norm.norm (E := E × F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F) +
      Norm.norm (E := E × F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)
⊢ ‖x.1‖ + ‖x.2‖ ≤
    (↑2 : ℝ) *
      Norm.norm (E := E × F)
        (((linearEquiv ℂ A (E × F) : C⋆ᵐᵒᵈ(A, E × F) ≃ₗ[ℂ] E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)

Tactic:
simp only [NNReal.coe_ofNat, linearEquiv_apply, two_mul]

Premises used: two_mul, WithCStarModule.linearEquiv_apply, NNReal.coe_ofNat