mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: case refine_3
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)
x₁ : F
hx₁ : x₁ ∈ t
x₂ : F
hx₂ : x₂ ∈ t
hx_snd : (x, y).2 ∈ openSegment 𝕜 x₁ x₂
⊢ (x, y) ∈ (fun y_1 ↦ ((x, y).1, y_1)) '' openSegment 𝕜 x₁ x₂

Tactic:
]

Goal state after:
case refine_3
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)
x₁ : F
hx₁ : x₁ ∈ t
x₂ : F
hx₂ : x₂ ∈ t
hx_snd : (x, y).2 ∈ openSegment 𝕜 x₁ x₂
⊢ (x, y) ∈ (fun y_1 ↦ ((x, y).1, y_1)) '' openSegment 𝕜 x₁ x₂
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: case refine_1.a
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module 𝕜 (M i)
s : (i : ι) → Set (M i)
x : (i : ι) → M i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → M i),
    (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x
i : ι
x₁ : M i
hx₁ : x₁ ∈ s i
x₂ : M i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
⊢ x ∈ update x i '' openSegment 𝕜 x₁ x₂

Tactic:
]

Goal state after:
case refine_1.a
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module 𝕜 (M i)
s : (i : ι) → Set (M i)
x : (i : ι) → M i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → M i),
    (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x
i : ι
x₁ : M i
hx₁ : x₁ ∈ s i
x₂ : M i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
⊢ x ∈ update x i '' openSegment 𝕜 x₁ x₂
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
⊢ (x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) ↔
    x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
⊢ (x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) ↔
    x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ (x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) → x ∈ insert x₁ (insert x₂ (openSegment 𝕜 x₁ x₂)) → x₁ = x ∨ x₂ = x

Tactic:
]

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ (x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) → x ∈ insert x₁ (insert x₂ (openSegment 𝕜 x₁ x₂)) → x₁ = x ∨ x₂ = x
Module: Mathlib.Analysis.InnerProductSpace.Completion

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 := { toFun := fun x ↦ ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }
this : Continuous fun p ↦ (inner' p.1) p.2
⊢ Continuous (⋯.extend (uncurry (inner 𝕜)))

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 := { toFun := fun x ↦ ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }
this : Continuous fun p ↦ (inner' p.1) p.2
⊢ Continuous (⋯.extend (uncurry (inner 𝕜)))
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : ∀ ⦃x_1 : E⦄, x_1 ∈ A \ {x} → ∀ ⦃y : E⦄, y ∈ A \ {x} → [x_1 -[𝕜] y] ⊆ A \ {x}
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ [x₁ -[𝕜] x₂]
⊢ x₁ = x ∨ x₂ = x

Tactic:
]

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : ∀ ⦃x_1 : E⦄, x_1 ∈ A \ {x} → ∀ ⦃y : E⦄, y ∈ A \ {x} → [x_1 -[𝕜] y] ⊆ A \ {x}
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ [x₁ -[𝕜] x₂]
⊢ x₁ = x ∨ x₂ = x
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
⊢ x ∈ A ∧ x ∉ (convexHull 𝕜) (A \ {x}) ↔ x ∈ A ∧ x ∉ (convexHull 𝕜) (A \ {x})

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hx : x ∈ (convexHull 𝕜) A ∧ Convex 𝕜 ((convexHull 𝕜) A \ {x})
⊢ x ∈ A

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hx : x ∈ (convexHull 𝕜) A ∧ Convex 𝕜 ((convexHull 𝕜) A \ {x})
⊢ x ∈ A
Module: Mathlib.Analysis.CStarAlgebra.Hom

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CStarAlgebra A
inst✝³ : CStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective ⇑φ
h_spec : spectrum ℝ ((StarAlgHom.restrictScalars ℝ ↑φ) a) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum ℝ (φ a)
f : C(ℝ, ℝ)
h_eqOn : Set.EqOn (⇑f) 0 (spectrum ℝ (φ a))
h_eqOn_x : Set.EqOn (⇑f) 1 {x}
this : Set.EqOn (⇑f) 0 (spectrum ℝ a)
⊢ False

Tactic:
]

Goal state after:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CStarAlgebra A
inst✝³ : CStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective ⇑φ
h_spec : spectrum ℝ ((StarAlgHom.restrictScalars ℝ ↑φ) a) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum ℝ (φ a)
f : C(ℝ, ℝ)
h_eqOn : Set.EqOn (⇑f) 0 (spectrum ℝ (φ a))
h_eqOn_x : Set.EqOn (⇑f) 1 {x}
this : Set.EqOn (⇑f) 0 (spectrum ℝ a)
⊢ False
Module: Mathlib.Analysis.CStarAlgebra.Hom

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a✝ : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
hψ : Function.Injective ⇑ψ
a : Unitization ℂ A
⊢ ‖ψ a‖ ^ 2 = ‖a‖ ^ 2

Tactic:
]

Goal state after:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a✝ : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
hψ : Function.Injective ⇑ψ
a : Unitization ℂ A
⊢ ‖ψ a‖ ^ 2 = ‖a‖ ^ 2
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
x✝² x✝¹ x✝ : f.PreGNS
⊢ f (star (f.ofPreGNS x✝²) * f.ofPreGNS x✝) + f (star (f.ofPreGNS x✝¹) * f.ofPreGNS x✝) =
    f (star (f.ofPreGNS x✝²) * f.ofPreGNS x✝) + f (star (f.ofPreGNS x✝¹) * f.ofPreGNS x✝)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a : A
x : f.PreGNS
⊢ f
      (star (f.ofPreGNS ((↑f.toPreGNS ∘ₗ ↑((ContinuousLinearMap.mul ℂ A) a) ∘ₗ ↑f.ofPreGNS) x)) *
        f.ofPreGNS ((↑f.toPreGNS ∘ₗ ↑((ContinuousLinearMap.mul ℂ A) a) ∘ₗ ↑f.ofPreGNS) x)) ≤
    ↑(‖a‖ ^ 2 * ‖x‖ ^ 2)

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a : A
x : f.PreGNS
⊢ f
      (star (f.ofPreGNS ((↑f.toPreGNS ∘ₗ ↑((ContinuousLinearMap.mul ℂ A) a) ∘ₗ ↑f.ofPreGNS) x)) *
        f.ofPreGNS ((↑f.toPreGNS ∘ₗ ↑((ContinuousLinearMap.mul ℂ A) a) ∘ₗ ↑f.ofPreGNS) x)) ≤
    ↑(‖a‖ ^ 2 * ‖x‖ ^ 2)
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a : A
x : f.PreGNS
⊢ star (f.ofPreGNS x) * (star a * a) * f.ofPreGNS x ≤ ‖star a * a‖ • (star (f.ofPreGNS x) * f.ofPreGNS x)

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a : A
x : f.PreGNS
⊢ star (f.ofPreGNS x) * (star a * a) * f.ofPreGNS x ≤ ‖star a * a‖ • (star (f.ofPreGNS x) * f.ofPreGNS x)
Module: Mathlib.Analysis.CStarAlgebra.Extreme

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
x✝ : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : ↑a ∈ Icc 0 1
hb01 : ↑b ∈ Icc 0 1
this : t • (↑e * (1 - ↑a) * ↑e) = 0
⊢ e * t • a * e = t • e

pp: case hae
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
x✝ : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : ↑a ∈ Icc 0 1
hb01 : ↑b ∈ Icc 0 1
this : t • (↑e * (1 - ↑a) * ↑e) = 0
⊢ t • a ≤ e

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
x✝ : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : ↑a ∈ Icc 0 1
hb01 : ↑b ∈ Icc 0 1
this : t • (↑e * (1 - ↑a) * ↑e) = 0
⊢ e * t • a * e = t • e

case hae
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
x✝ : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : ↑a ∈ Icc 0 1
hb01 : ↑b ∈ Icc 0 1
this : t • (↑e * (1 - ↑a) * ↑e) = 0
⊢ t • a ≤ e
Module: Mathlib.Analysis.CStarAlgebra.Extreme

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
x✝ :
  (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : ↑e ≤ 1
⊢ 2 ≤ 2

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Extreme

Goal state before:
pp: case refine_2.refine_1
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
x✝ :
  (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : 0 ≤ ↑(2 • e - e * e)
⊢ 1 ≤ 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Extreme

Goal state before:
pp: case refine_2.refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
x✝ :
  (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : 0 ≤ ↑(2 • e - e * e)
⊢ 0 ≤ 1 - ↑(2 • e - e * e)

Tactic:
]

Goal state after:
case refine_2.refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
x✝ :
  (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : 0 ≤ ↑(2 • e - e * e)
⊢ 0 ≤ 1 - ↑(2 • e - e * e)
Module: Mathlib.Analysis.CStarAlgebra.Projection

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
h : p ≤ q
⊢ p = p

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
h_x : ∃ a ∈ Finset.univ.val, ‖U i a‖ ^ 2 = x
⊢ 0 ≤ x

Tactic:
]

Goal state after:
case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
h_x : ∃ a ∈ Finset.univ.val, ‖U i a‖ ^ 2 = x
⊢ 0 ≤ x
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
a : n
h_a : a ∈ Finset.univ.val ∧ ‖U i a‖ ^ 2 = x
⊢ 0 ≤ ‖U i a‖ ^ 2

Tactic:
]

Goal state after:
case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
a : n
h_a : a ∈ Finset.univ.val ∧ ‖U i a‖ ^ 2 = x
⊢ 0 ≤ ‖U i a‖ ^ 2
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ ∃ a ∈ Finset.univ.val, ‖U i a‖ ^ 2 = ‖U i j‖ ^ 2

Tactic:
]

Goal state after:
case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ ∃ a ∈ Finset.univ.val, ‖U i a‖ ^ 2 = ‖U i j‖ ^ 2
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2
diag_eq_norm_sum :
  RCLike.re ((U * Uᴴ) i i) = RCLike.re ↑(∑ x, ‖U i x‖ ^ 2) ∧ RCLike.im ((U * Uᴴ) i i) = RCLike.im ↑(∑ x, ‖U i x‖ ^ 2)
⊢ RCLike.re ((U * Uᴴ) i i) = ∑ x, ‖U i x‖ ^ 2

Tactic:
]

Goal state after:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2
diag_eq_norm_sum :
  RCLike.re ((U * Uᴴ) i i) = RCLike.re ↑(∑ x, ‖U i x‖ ^ 2) ∧ RCLike.im ((U * Uᴴ) i i) = RCLike.im ↑(∑ x, ‖U i x‖ ^ 2)
⊢ RCLike.re ((U * Uᴴ) i i) = ∑ x, ‖U i x‖ ^ 2
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2
diag_eq_norm_sum :
  RCLike.re ((U * Uᴴ) i i) = RCLike.re ↑(∑ x, ‖U i x‖ ^ 2) ∧ RCLike.im ((U * Uᴴ) i i) = RCLike.im ↑(∑ x, ‖U i x‖ ^ 2)
⊢ RCLike.re ↑(∑ x, ‖U i x‖ ^ 2) = ∑ x, ‖U i x‖ ^ 2

Tactic:
]

Goal state after:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2
diag_eq_norm_sum :
  RCLike.re ((U * Uᴴ) i i) = RCLike.re ↑(∑ x, ‖U i x‖ ^ 2) ∧ RCLike.im ((U * Uᴴ) i i) = RCLike.im ↑(∑ x, ‖U i x‖ ^ 2)
⊢ RCLike.re ↑(∑ x, ‖U i x‖ ^ 2) = ∑ x, ‖U i x‖ ^ 2
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x, ‖U i x‖ ^ 2)
re_diag_eq_norm_sum : RCLike.re ((U * Uᴴ) i i) = ∑ x, ‖U i x‖ ^ 2
mul_eq_one : U * Uᴴ = 1
diag_eq_one : RCLike.re ((U * Uᴴ) i i) = 1
⊢ ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2

Tactic:
]

Goal state after:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x, ‖U i x‖ ^ 2)
re_diag_eq_norm_sum : RCLike.re ((U * Uᴴ) i i) = ∑ x, ‖U i x‖ ^ 2
mul_eq_one : U * Uᴴ = 1
diag_eq_one : RCLike.re ((U * Uᴴ) i i) = 1
⊢ ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2
Module: Mathlib.Analysis.Normed.Field.UnitBall

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NonUnitalSeminormedRing 𝕜
a✝ b✝ : 𝕜
hx : ‖a✝‖ < 1
hy : ‖b✝‖ < 1
⊢ ‖a✝ * b✝‖ < 1

Tactic:
]

Goal state after:
𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NonUnitalSeminormedRing 𝕜
a✝ b✝ : 𝕜
hx : ‖a✝‖ < 1
hy : ‖b✝‖ < 1
⊢ ‖a✝ * b✝‖ < 1
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: case e_f
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℝ
x y : EuclideanSpace ℝ n
i : n
⊢ (∑ x, (∑ c, y.ofLp c * A x c) * Pi.single x 1 i) * x.ofLp i = (∑ c, y.ofLp c * A i c) * x.ofLp i

Tactic:
]

Goal state after:
case e_f
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℝ
x y : EuclideanSpace ℝ n
i : n
⊢ (∑ x, (∑ c, y.ofLp c * A x c) * Pi.single x 1 i) * x.ofLp i = (∑ c, y.ofLp c * A i c) * x.ofLp i
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: case e_2
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
normed_add_comm_group : NormedAddCommGroup (Matrix m n 𝕜) :=
  let __src := l2OpNormedAddCommGroupAux.replaceTopology ⋯;
  { toNorm := l2OpNormedAddCommGroupAux.toNorm, toAddCommGroup := addCommGroup, toMetricSpace := __src, dist_eq := ⋯ }
⊢ IsTopologicalAddGroup.rightUniformSpace (Matrix m n 𝕜) = PseudoEMetricSpace.toUniformSpace

Tactic:
]

Goal state after:
case e_2
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
normed_add_comm_group : NormedAddCommGroup (Matrix m n 𝕜) :=
  let __src := l2OpNormedAddCommGroupAux.replaceTopology ⋯;
  { toNorm := l2OpNormedAddCommGroupAux.toNorm, toAddCommGroup := addCommGroup, toMetricSpace := __src, dist_eq := ⋯ }
⊢ IsTopologicalAddGroup.rightUniformSpace (Matrix m n 𝕜) = PseudoEMetricSpace.toUniformSpace
Module: Mathlib.Analysis.Normed.Field.UnitBall

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NonUnitalSeminormedRing 𝕜
a✝ b✝ : 𝕜
hx : ‖a✝‖ ≤ 1
hy : ‖b✝‖ ≤ 1
⊢ ‖a✝ * b✝‖ ≤ 1

Tactic:
]

Goal state after:
𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NonUnitalSeminormedRing 𝕜
a✝ b✝ : 𝕜
hx : ‖a✝‖ ≤ 1
hy : ‖b✝‖ ≤ 1
⊢ ‖a✝ * b✝‖ ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: case e_2
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
normed_add_comm_group : NormedAddCommGroup (Matrix m n 𝕜) :=
  let __src := l2OpNormedAddCommGroupAux.replaceTopology ⋯;
  { toNorm := l2OpNormedAddCommGroupAux.toNorm, toAddCommGroup := addCommGroup, toMetricSpace := __src, dist_eq := ⋯ }
⊢ PseudoEMetricSpace.toUniformSpace = PseudoEMetricSpace.toUniformSpace

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.UnitBall

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : NormMulClass 𝕜
inst✝ : NormOneClass 𝕜
a✝ b✝ : 𝕜
hx : ‖a✝‖ = 1
hy : ‖b✝‖ = 1
⊢ ‖a✝ * b✝‖ = 1

Tactic:
]

Goal state after:
𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : NormMulClass 𝕜
inst✝ : NormOneClass 𝕜
a✝ b✝ : 𝕜
hx : ‖a✝‖ = 1
hy : ‖b✝‖ = 1
⊢ ‖a✝ * b✝‖ = 1
Module: Mathlib.Analysis.Normed.Field.UnitBall

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
x : ↑(sphere 0 1)
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.UnitBall

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
x y : ↑(sphere 0 1)
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.UnitBall

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
x : ↑(sphere 0 1)
n : ℤ
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix m n 𝕜
⊢ ‖ContinuousLinearMap.adjoint
        (toContinuousLinearMap
          ((toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis) A))‖ =
    ‖A‖

Tactic:
]

Goal state after:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix m n 𝕜
⊢ ‖ContinuousLinearMap.adjoint
        (toContinuousLinearMap
          ((toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis) A))‖ =
    ‖A‖
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: x : Circle
⊢ ↑x = 1 ↔ ↑x = 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: z : Circle
⊢ (starRingEnd ℂ) ↑z = (starRingEnd ℂ) ↑z

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: x y : Circle
z : ℂ
hz : z ≠ 0
⊢ 1 = 1

pp: x y : Circle
z : ℂ
hz : z ≠ 0
⊢ ‖z‖ ≠ 0

Tactic:
]

Goal state after:
x y : Circle
z : ℂ
hz : z ≠ 0
⊢ ‖z‖ ≠ 0
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: ⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ‖toContinuousLinearMap
        (adjoint ((toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis) A) ∘ₗ
          (toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis) A)‖ =
    ‖A‖ * ‖A‖

Tactic:
]

Goal state after:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ‖toContinuousLinearMap
        (adjoint ((toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis) A) ∘ₗ
          (toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis) A)‖ =
    ‖A‖ * ‖A‖
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: x : ℝ
n : ℕ
⊢ exp x ^ n = exp x ^ n

Tactic:
]

Goal state after: