mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
x : EuclideanSpace 𝕜 n
⊢ 0 ≤ ‖T x‖

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
x : EuclideanSpace 𝕜 n
⊢ 0 ≤ ‖v‖ * ‖x‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
⊢ EqOn (↑(e.subtypeRestr hV).symm) (inclusion hUV ∘ ↑(e.subtypeRestr hU).symm) (e.subtypeRestr hU).target

Tactic:
set i := Set.inclusion hUV

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
⊢ EqOn (↑(e.subtypeRestr hV).symm) (i ∘ ↑(e.subtypeRestr hU).symm) (e.subtypeRestr hU).target
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: case right
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
⊢ EqOn (↑((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j))) (↑(Z.trivChange i j).toPartialEquiv)
    ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source

Tactic:
rintro ⟨x, v⟩ hx
    simp only [trivChange, localTrivAsPartialEquiv, PartialEquiv.symm,
      Prod.mk_inj, prodMk_mem_set_prod_eq, PartialEquiv.trans_source, mem_inter_iff,
      mem_preimage, proj, mem_univ, (· ∘ ·),
      PartialEquiv.coe_trans] at hx ⊢
    simp only [Z.coordChange_comp, hx, mem_inter_iff, and_self_iff, mem_baseSet_at]

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
ht :
  ∃ i i_1,
    IsOpen[instTopologicalSpaceProd] i_1 ∧
      t = (Z.localTrivAsPartialEquiv i).source ∩ ↑(Z.localTrivAsPartialEquiv i) ⁻¹' i_1
⊢ IsOpen[instTopologicalSpaceProd] ((Z.localTrivAsPartialEquiv i).target ∩ (Z.localTrivAsPartialEquiv i).invFun ⁻¹' t)

Tactic:
obtain ⟨j, s, s_open, ts⟩ : ∃ j s, IsOpen s ∧
      t = (localTrivAsPartialEquiv Z j).source ∩ localTrivAsPartialEquiv Z j ⁻¹' s := ht

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s
⊢ IsOpen[instTopologicalSpaceProd] ((Z.localTrivAsPartialEquiv i).target ∩ (Z.localTrivAsPartialEquiv i).invFun ⁻¹' t)
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
this : FiberBundle F E := a.toFiberBundle
⊢ Continuous[a.totalSpaceTopology, inst✝²] TotalSpace.proj

Tactic:
exact FiberBundle.continuous_proj F E

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

Goal state before:
pp: case succ
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
k : ℕ
hk : ∀ (x y : A), (a.toProd.2 ^ k) x * y = x * (a.toProd.1 ^ k) y
x y : A
⊢ a.toProd.2 ((a.toProd.2 ^ k) x) * y = x * (a.toProd.1 ^ (k + 1)) y

Tactic:
a.central,

Goal state after:
case succ
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
k : ℕ
hk : ∀ (x y : A), (a.toProd.2 ^ k) x * y = x * (a.toProd.1 ^ k) y
x y : A
⊢ (a.toProd.2 ^ k) x * a.toProd.1 y = x * (a.toProd.1 ^ (k + 1)) y
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
⊢ CompleteSpace 𝓜(𝕜, A)

Tactic:
completeSpace_iff_isComplete_range isUniformEmbedding_toProdMulOpposite.isUniformInducing

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
⊢ IsComplete (Set.range toProdMulOpposite)
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case refine_3
E : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace X
f : E → X
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
F : PartialEquiv E (X × ι) :=
  { toFun := fun e ↦ (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι),
    invFun := fun x ↦ if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1, source := f ⁻¹' V,
    target := V ×ˢ Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }
open_preim : ∀ {W : Set X}, W ⊆ V → IsOpen[inst✝⁴] W → IsOpen[inst✝⁵] (f ⁻¹' W)
open_source : IsOpen[inst✝⁵] F.source
cont_f : ContinuousOn f F.source
i : ι
⊢ ContinuousOn (fun x ↦ if h : x ∈ V then inv i ⋯ else Classical.arbitrary (X → E) x) {a | a ∈ V ∧ i ∈ Set.univ}

Tactic:
Set.mem_univ,

Goal state after:
case refine_3
E : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace X
f : E → X
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
F : PartialEquiv E (X × ι) :=
  { toFun := fun e ↦ (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι),
    invFun := fun x ↦ if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1, source := f ⁻¹' V,
    target := V ×ˢ Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }
open_preim : ∀ {W : Set X}, W ⊆ V → IsOpen[inst✝⁴] W → IsOpen[inst✝⁵] (f ⁻¹' W)
open_source : IsOpen[inst✝⁵] F.source
cont_f : ContinuousOn f F.source
i : ι
⊢ ContinuousOn (fun x ↦ if h : x ∈ V then inv i ⋯ else Classical.arbitrary (X → E) x) {a | a ∈ V ∧ True}
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
t : ↑unitInterval
⊢ ↑((x.path y) t) = ↑((⇑exp ∘ ⇑(Path.segment (↑x).arg (x.angleDiff y + (↑x).arg))) t)

Tactic:
rw [path_apply, comp_apply]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
z : ℂ
hz : z ∈ spectrum ℂ u
⊢ 0 ≤ ‖u - 1‖

Tactic:
positivity

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

Goal state before:
pp: x y : Circle
hne : x ≠ y
⊢ 2⁻¹ ∈ unitInterval

Tactic:
simp only [mem_Icc, inv_nonneg, Nat.ofNat_nonneg, true_and]

Goal state after:
x y : Circle
hne : x ≠ y
⊢ 2⁻¹ ≤ 1
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case inr
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this✝¹ : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
this✝ : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ e, V' e
h✝ : Nonempty ↑(f ⁻¹' {x})
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst✝¹] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ e, f '' V' e
this : Finite ↑(f ⁻¹' {x})
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})

Tactic:
have hU' : IsOpen U' := hU.inter <| isOpen_iInter_of_finite fun e ↦ by
    convert! ← (φ e).isOpen_image_of_subset_source (hV' _) inter_subset_right; exact (hφ e).2

Goal state after:
case inr
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this✝¹ : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
this✝ : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ e, V' e
h✝ : Nonempty ↑(f ⁻¹' {x})
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst✝¹] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ e, f '' V' e
this : Finite ↑(f ⁻¹' {x})
hU' : IsOpen[inst✝¹] U'
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
⊢ 0 ≤ ‖u - 1‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
⊢ 0 ≤ 2

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
a✝ : Nontrivial A
y : ℝ
hy : y ∈ spectrum ℝ ↑x
⊢ 0 ≤ |y|

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
⊢ 0 ≤ ‖↑(expUnitary x) - 1‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
⊢ 0 ≤ 2

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
⊢ 0 ≤ ‖x‖

Tactic:
positivity

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

Goal state before:
pp: T : ℝ
hT : T ≠ 0
⊢ 2 * π ≠ 0

Tactic:
positivity

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

Goal state before:
pp: x✝¹ : ℕ
x✝ : True
⊢ 0 < π / 2 ^ (x✝¹ + 1)

Tactic:
positivity

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

Goal state before:
pp: r x : ℝ
⊢ x ∈ {x | |x| < r} ↔ x ∈ Ioo (-r) r

Tactic:
simp [abs_lt]

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

Goal state before:
pp: z : Circle
hz : ∀ n > 0, z ^ n ∈ centeredArc (π / 2)
hz1 : z ∈ centeredArc (π / 2)
n : ℕ
ih : z ∈ centeredArc (π / 2 ^ (n + 1))
⊢ 2 ^ (n + 1) > 0

Tactic:
positivity

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

Goal state before:
pp: n : ℤ
inst✝ : NeZero n
hn : IsUnit ↑n
e : AddCircle 1 ≃ₜ Circle := homeomorphCircle ⋯
x✝ : AddCircle 1
⊢ x✝ ∈ ⇑e ⁻¹' ↑(zpowGroupHom n).ker ↔ x✝ ∈ {x | n • x = 0}

Tactic:
simp [e, homeomorphCircle_apply, ← toCircle_zsmul, ← (injective_toCircle one_ne_zero).eq_iff]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ 0 ≤ ‖a‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
⊢ 0 ≤ π

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
⊢ 0 ≤ ‖argSelfAdjoint u‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : t ∈ Set.Icc 0 1
hu : ‖↑u - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
⊢ 0 ≤ ‖↑(expUnitary (t • argSelfAdjoint u)) - 1‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : t ∈ Set.Icc 0 1
hu : ‖↑u - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
⊢ 0 ≤ ‖↑u - 1‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : t ∈ Set.Icc 0 1
hu : ‖↑u - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
⊢ 0 ≤ ‖t • argSelfAdjoint u‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
⊢ 0 ≤ dist u 1

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
⊢ 0 ≤ 2

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : dist u 1 ^ 2 < ε
hε2 : ε < 2 ^ 2
⊢ 0 ≤ dist u 1 ^ 2

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : dist u 1 ^ 2 < ε
hε2 : ε < 2 ^ 2
hε : 0 < ε
huε' : dist u 1 < √ε
v : ↥(unitary A)
hv : v ∈ closedBall 1 √ε
z : ℂ
hz : z ∈ spectrum ℂ ↑v
⊢ 0 ≤ ‖↑v - 1‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : dist u 1 ^ 2 < ε
hε2 : ε < 2 ^ 2
hε : 0 < ε
huε' : dist u 1 < √ε
v : ↥(unitary A)
hv : v ∈ closedBall 1 √ε
z : ℂ
hz : z ∈ spectrum ℂ ↑v
⊢ 0 ≤ ε

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
⊢ 0 ≤ ‖↑u - 1‖ ^ 2 / 2

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
⊢ 0 ≤ ‖↑(expUnitary x) - 1‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
⊢ 0 ≤ 2

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
⊢ 0 ≤ ‖↑x‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
y : F
x : E
w✝ : ↥(↑A).range
⊢ 0 ≤ (fun w ↦ ‖y - ↑w‖) w✝

Tactic:
positivity

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
⊢ ↑(s.restrict S hS).centroid = s.centroid

Tactic:
by
  rw [eq_comm]
  have := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
  have hf : Function.Injective (S.subtype) := by
    simp only [coe_subtype, Subtype.val_injective]
  exact (s.restrict S hS).centroid_map S.subtype hf

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
x✝ : ∃ y, y • 1 = ↑(↑g).symm ∘SL ↑↑f
y : 𝕜
h : y • 1 = ↑(↑g).symm ∘SL ↑↑f
hy : y ≠ 0
hfg : ↑↑f = y • ↑↑g
hgf : ↑↑g = star y • ↑↑f
this : ↑↑g = ((starRingEnd 𝕜) y * y) • ↑↑g
⊢ ∃ α, ∀ (x : H), f x = (α • g) x

Tactic:
← one_smul 𝕜 (g : H →L[𝕜] K)

Goal state after:
case neg
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
x✝ : ∃ y, y • 1 = ↑(↑g).symm ∘SL ↑↑f
y : 𝕜
h : y • 1 = ↑(↑g).symm ∘SL ↑↑f
hy : y ≠ 0
hfg : ↑↑f = y • ↑↑g
hgf : ↑↑g = star y • ↑↑f
this : 1 • ↑↑g = ((starRingEnd 𝕜) y * y) • ↑↑g
⊢ ∃ α, ∀ (x : H), f x = (α • g) x
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
⊢ p -ᵥ s.centroid = 0

Tactic:
let s' : Finset (Fin (n + 1)) := {i₀}ᶜ

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
⊢ p -ᵥ s.centroid = 0
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : (i : α) → E i
⊢ Memℓp f p ↔ Summable fun i ↦ ‖f i‖ ^ p.toReal

Tactic:
by
  rw [ENNReal.toReal_pos_iff] at hp
  dsimp [Memℓp]
  rw [if_neg hp.1.ne', if_neg hp.2.ne]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case h.h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
b : α
⊢ 0 ≤ ‖f b‖ ^ p.toReal

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hf : Summable fun i ↦ ‖f i‖ ^ p.toReal
i✝ : α
⊢ 0 ≤ ‖f i✝‖ ^ p.toReal

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hf : Summable fun i ↦ ‖f i‖ ^ p.toReal
⊢ ∀ (i : α), 0 ≤ ‖f i‖ ^ p.toReal

Tactic:
intro; positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hp : 0 < p.toReal
hf : Memℓp f p
i : α
⊢ 0 ≤ ‖f i‖ ^ p.toReal

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ BddAbove (Set.range fun i ↦ 0)

Tactic:
exact bddAbove_singleton.mono Set.range_const_subset

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hg : Summable fun i ↦ ‖g i‖ ^ p.toReal
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hp : 0 < p.toReal
i : α
⊢ 0 ≤ ‖f i‖ ^ p.toReal

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < q.toReal
hpq : q ≤ ∞
A : ℝ
hA : A ∈ upperBounds (Set.range fun i ↦ ‖f i‖ ^ q.toReal)
i : α
⊢ 0 ≤ ‖f i‖ ^ q.toReal

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable fun i ↦ ‖f i‖ ^ q.toReal
i : α
hi : ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal
⊢ 0 ≤ ‖f i‖ ^ p.toReal

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)
⊢ Summable fun i ↦ ‖(f + g) i‖ ^ p.toReal

Tactic:
refine .of_nonneg_of_le ?_ (fun i => ?_) (((hf.summable hp).add (hg.summable hp)).mul_left C)

Goal state after:
case inr.inr.refine_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)
⊢ ∀ (b : α), 0 ≤ ‖(f + g) b‖ ^ p.toReal

case inr.inr.refine_2
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)
i : α
⊢ ‖(f + g) i‖ ^ p.toReal ≤ C * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr.refine_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)
b✝ : α
⊢ 0 ≤ ‖(f + g) b✝‖ ^ p.toReal

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr.refine_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)
⊢ ∀ (b : α), 0 ≤ ‖(f + g) b‖ ^ p.toReal

Tactic:
intro; positivity

Goal state after: