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

Goal state before:
pp: A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
p : A
hp : IsIdempotentElem p
h : IsStarNormal p
x : ℂ
⊢ x ∈ quasispectrum ℂ p → x = ↑x.re

Tactic:
hx

Goal state after:
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
p : A
hp : IsIdempotentElem p
h : IsStarNormal p
x : ℂ
hx : x ∈ quasispectrum ℂ p
⊢ x = ↑x.re
Module: Mathlib.Analysis.Normed.Field.UnitBall

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

Tactic:
one_zpow

Goal state after:
𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
x : ↑(sphere 0 1)
n : ℤ
⊢ 1 = 1
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: case refine_1.e_a
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
x : X
⊢ x ∈ s → ∀ y ∈ e.source, ↑e x = ↑e y → x = y

Tactic:
hx

Goal state after:
case refine_1.e_a
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
x : X
hx : x ∈ s
⊢ ∀ y ∈ e.source, ↑e x = ↑e y → x = y
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
x : Y
⊢ x ∈ ((e.restr s).symm.trans e').source → (↑e' ∘ ↑e.symm) x = (↑e' ∘ ↑e.symm) x

Tactic:
hx

Goal state after:
case refine_2
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
x : Y
hx : x ∈ ((e.restr s).symm.trans e').source
⊢ (↑e' ∘ ↑e.symm) x = (↑e' ∘ ↑e.symm) x
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 : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y ∈ e.source

Tactic:
· have := OpenPartialHomeomorph.map_target _ hy
    rwa [e.subtypeRestr_source] at this

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

Goal state before:
pp: case neg
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : ¬Nonempty X
x : X'
⊢ x ∈ f '' e.source → ContinuousWithinAt (extend f ↑e fun x ↦ Classical.arbitrary Z) (f '' e.source) x

Tactic:
hx

Goal state after:
case neg
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : ¬Nonempty X
x : X'
hx : x ∈ f '' e.source
⊢ ContinuousWithinAt (extend f ↑e fun x ↦ Classical.arbitrary Z) (f '' e.source) x
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
b : B
x : E b
⊢ { proj := b, snd := x } ∈ (a.pretrivializationAt b).source

Tactic:
simp only [(a.pretrivializationAt b).source_eq, mem_preimage]

Goal state after:
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
b : B
x : E b
⊢ b ∈ (a.pretrivializationAt b).baseSet
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)
inst✝² : (x : B) → Zero (E x)
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : FiberBundle F E
x : B
v : E x
⊢ extend F v x = v

Tactic:
simp [extend, FiberBundle.mem_baseSet_trivializationAt' x]

Goal state after:
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
n : ℤ
x y : A
⊢ (↑n).2 x * y = x * (↑n).1 y

Tactic:
Prod.snd_intCast,

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
n : ℤ
x y : A
⊢ ↑n x * y = x * (↑n).1 y
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x✝ : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
x : B × F
⊢ x ∈ e.baseSet ×ˢ univ ⊓ e'.baseSet ×ˢ univ → x ∈ ⊥

Tactic:
hx

Goal state after:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x✝ : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
x : B × F
hx : x ∈ e.baseSet ×ˢ univ ⊓ e'.baseSet ×ˢ univ
⊢ x ∈ ⊥
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source
x : X
⊢ x ∈ s → ∃ e, x ∈ e.source ∧ f = ↑e

Tactic:
hx

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source
x : X
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ f = ↑e
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
hg : IsLocalHomeomorphOn g t
hf : IsLocalHomeomorphOn f s
h : Set.MapsTo f s t
x : X
⊢ x ∈ s → ∃ e, x ∈ e.source ∧ g ∘ f = ↑e

Tactic:
hx

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
hg : IsLocalHomeomorphOn g t
hf : IsLocalHomeomorphOn f s
h : Set.MapsTo f s t
x : X
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ g ∘ f = ↑e
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
x : X
h✝ : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[inst✝²] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
⊢ I ≃ₜ ↑(f ⁻¹' {x})

Tactic:
exact
  { toFun i := ⟨H.symm (⟨x, hxU⟩, i), by simp [← hH]⟩
    invFun e := (H ⟨e, by rwa [Set.mem_preimage, (e.2 : f e = x)]⟩).2
    left_inv _ := by simp
    right_inv e := Set.inclusion_injective (Set.preimage_mono (Set.singleton_subset_iff.mpr hxU)) <|
      H.injective <| Prod.ext (Subtype.ext <| by simpa [hH] using e.2.symm) (by simp)
    continuous_toFun := by fun_prop
    continuous_invFun := by fun_prop }

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CStarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : (Metric.closedBall 0 1).Nonempty
x y : A
⊢ ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖a.toProd.2 (star (a.toProd.1 (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊

Tactic:
hx

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CStarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : (Metric.closedBall 0 1).Nonempty
x y : A
hx : ‖x‖₊ ≤ 1
⊢ ‖y‖₊ ≤ 1 → ‖a.toProd.2 (star (a.toProd.1 (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
I : Type u_3
inst✝¹ : TopologicalSpace I
x : E
inst✝ : Nonempty I
h : IsEvenlyCovered f (f x) I
⊢ h.fiberHomeomorph.symm (↑h.toTrivialization x).2 = h.fiberHomeomorph.symm ⟨x, ⋯⟩

Tactic:
by
    simp [toTrivialization, toTrivialization', dif_pos h.2.choose_spec.1, fiberHomeomorph]

Goal state after:
Module: Mathlib.Topology.Covering.AddCircle

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℤ
hn : IsUnit ↑n
x✝ : 𝕜
⊢ ∀ ⦃a₂ : 𝕜⦄, ↑n * x✝ = ↑n * a₂ → x✝ = a₂

Tactic:
apply hn.isSMulRegular 𝕜

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

Goal state before:
pp: x y : Circle
hne : x ≠ y
⊢ (↑x).arg ≠ x.angleDiff y + (↑x).arg

Tactic:
by simp [angleDiff_pos hne |>.ne']

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

Goal state before:
pp: x y : Circle
hne : x ≠ y
⊢ Injective ⇑(x.path y)

Tactic:
rw [coe_path]
  refine (exp_injOn_Icc (a := x.val.arg) (b := angleDiff x y + x.val.arg)
    <| by simp [angleDiff_lt_two_pi]).injective_iff _ ?_ |>.mpr
    <| Path.segment_injective_of_ne <| by simp [angleDiff_pos hne |>.ne']
  rw [Path.range_segment, segment_eq_Icc (by simp)]

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

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ ⇑(x.path y) '' Ioc 0 1 ∪ ⇑(y.path x) '' Ioc 0 1 = univ

Tactic:
rw [path_image_Ioc_of_ne h, path_image_Ioc_of_ne h.symm, ← image_union,
    Ioc_union_Ioc_angleDiff_add_arg h, periodic_exp.image_Ioc two_pi_pos]
  exact exp_surjective.range_eq

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

Goal state before:
pp: case inl
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h✝ : Subsingleton A
⊢ False

Tactic:
apply hz.nonempty.of_image.ne_empty

Goal state after:
case inl
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h✝ : Subsingleton A
⊢ spectrum ℂ u = ∅
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
hxy : x ≠ y
⊢ ¬IsPreconnected {x, y}ᶜ

Tactic:
simp only [isPreconnected_iff_subset_of_disjoint_closed, not_forall, not_or, exists_and_left]
  refine ⟨range (path x y), ?_, range (path y x), (isCompact_range (path x y).continuous).isClosed,
    (isCompact_range (path y x).continuous).isClosed, ?_, ?_, ?_⟩
  · rw [compl_subset_iff_union, union_eq_right.mpr (by simp only [pair_subset_iff,
      (path x y).source_mem_range, (path x y).target_mem_range, and_self])]
    exact (range_path_ssubset_univ x y).ne
  · rw [range_path_union_range_path hxy]
    exact subset_univ _
  · rw [range_path_inter_range_path hxy]
    exact compl_inter_self {x, y}
  rw [compl_subset_iff_union, union_eq_right.mpr (by simp only [pair_subset_iff,
      (path y x).source_mem_range, (path y x).target_mem_range, and_self])]
  exact (range_path_ssubset_univ y x).ne

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
inst✝ : T2Space E
hf : IsClosedMap f
hs : ∀ x ∈ s, (f ⁻¹' {x}).Finite
h : IsLocalHomeomorphOn f (f ⁻¹' s)
x : X
⊢ x ∈ s → IsEvenlyCovered f x ↑(f ⁻¹' {x})

Tactic:
hx

Goal state after:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
inst✝ : T2Space E
hf : IsClosedMap f
hs : ∀ x ∈ s, (f ⁻¹' {x}).Finite
h : IsLocalHomeomorphOn f (f ⁻¹' s)
x : X
hx : x ∈ s
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
f : E → X
s : Set X
inst✝² : T2Space E
inst✝¹ : T2Space X
inst✝ : CompactSpace E
hf : Continuous[inst✝⁴, inst✝³] f
h : IsLocalHomeomorphOn f (f ⁻¹' s)
x : X
⊢ x ∈ s → IsEvenlyCovered f x ↑(f ⁻¹' {x})

Tactic:
hx

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
f : E → X
s : Set X
inst✝² : T2Space E
inst✝¹ : T2Space X
inst✝ : CompactSpace E
hf : Continuous[inst✝⁴, inst✝³] f
h : IsLocalHomeomorphOn f (f ⁻¹' s)
x : X
hx : x ∈ s
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: case inr
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
key : a + I • CFC.sqrt (1 - a ^ 2) = cfc (fun x ↦ ↑x.re + I * ↑√(1 - x.re ^ 2)) a
x : ℂ
⊢ x ∈ spectrum ℂ a → star (↑x.re + I * ↑√(1 - x.re ^ 2)) * (↑x.re + I * ↑√(1 - x.re ^ 2)) = 1

Tactic:
hx

Goal state after:
case inr
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
key : a + I • CFC.sqrt (1 - a ^ 2) = cfc (fun x ↦ ↑x.re + I * ↑√(1 - x.re ^ 2)) a
x : ℂ
hx : x ∈ spectrum ℂ a
⊢ star (↑x.re + I * ↑√(1 - x.re ^ 2)) * (↑x.re + I * ↑√(1 - x.re ^ 2)) = 1
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
⊢ 2 * (1 - z.re) ≤ ε

Tactic:
trans ‖(v - 1 : A)‖ ^ 2

Goal state after:
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
⊢ 2 * (1 - z.re) ≤ ‖↑v - 1‖ ^ 2

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
⊢ ‖↑v - 1‖ ^ 2 ≤ ε
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
x : E
⊢ ‖A x‖ ^ 2 = re ⟪x, (adjoint A ∘SL A) x⟫_𝕜

Tactic:
have h : ⟪x, (A† ∘L A) x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_right]; rfl
  rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
A : E →L[𝕜] E
hA : (↑A).IsSymmetric
⊢ adjoint A = A

Tactic:
rwa [eq_comm, eq_adjoint_iff A A]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
U : Submodule 𝕜 E
h : U ∈ invtSubmodule ↑(adjoint T)
⊢ Uᗮ ∈ invtSubmodule ↑T

Tactic:
simp only [mem_invtSubmodule_iff_forall_mem_of_mem, coe_coe, mem_orthogonal] at h ⊢

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
U : Submodule 𝕜 E
h : ∀ x ∈ U, (adjoint T) x ∈ U
⊢ ∀ (x : E), (∀ u ∈ U, ⟪u, x⟫_𝕜 = 0) → ∀ u ∈ U, ⟪u, T x⟫_𝕜 = 0
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
p : E →L[𝕜] E
⊢ IsStarProjection p ↔ ∃ (x : (↑p).range.HasOrthogonalProjection), p = (↑p).range.starProjection

Tactic:
simp_rw [p.isStarProjection_iff_isSymmetricProjection.eq,
    LinearMap.isSymmetricProjection_iff_eq_coe_starProjection_range, coe_inj]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
A : E →ₗ[𝕜] E
hA : A.IsSymmetric
⊢ adjoint A = A

Tactic:
rwa [eq_comm, eq_adjoint_iff A A]

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✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ A.rangeᗮ = (adjoint A).ker

Tactic:
have := FiniteDimensional.complete 𝕜 E
  have := FiniteDimensional.complete 𝕜 F
  simpa using! A.toContinuousLinearMap.orthogonal_range

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
n : ℕ
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ (↑n + 1) • (s.centroid -ᵥ s.points i) = ∑ x, (s.points x -ᵥ s.points i)

Tactic:
centroid_eq_smul_sum_vsub_vadd s 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✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ (↑n + 1) • (((↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ s.points i) +ᵥ s.points i) -ᵥ s.points i) =
    ∑ x, (s.points x -ᵥ s.points i)
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✝ : CharZero k
s : Simplex k P n
p : P
h : ∑ i, (s.points i -ᵥ p) = 0
x : Fin (n + 1)
⊢ x ∈ univ → s.points x -ᵥ p = s.points x -ᵥ s.centroid - (p -ᵥ s.centroid)

Tactic:
hx

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✝ : CharZero k
s : Simplex k P n
p : P
h : ∑ i, (s.points i -ᵥ p) = 0
x : Fin (n + 1)
hx : x ∈ univ
⊢ s.points x -ᵥ p = s.points x -ᵥ s.centroid - (p -ᵥ s.centroid)
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: case neg.inr
𝕜 : 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 = 0
⊢ ∃ α, ∀ (x : H), f x = (α • g) x

Tactic:
· exact ⟨1, fun x ↦ by simp [by simpa using congr($this x)]⟩

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

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
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
x : V
⊢ x ∈ (fun x ↦ x -ᵥ p₀) '' s → x ∈ ↑(k ∙ v)

Tactic:
hx

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
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
x : V
hx : x ∈ (fun x ↦ x -ᵥ p₀) '' s
⊢ x ∈ ↑(k ∙ v)
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
F : α → Type u_5
inst✝ : (i : α) → NormedAddCommGroup (F i)
p : ℝ≥0∞
hp : p ≠ 0
x : ↥(lp E p)
y : ↥(lp F p)
h : ∀ (i : α), ‖↑x i‖ ≤ ‖↑y i‖
⊢ ‖x‖ ≤ ‖y‖

Tactic:
obtain (rfl | rfl | hp) := p.trichotomy
  · exact hp rfl |>.elim
  · exact norm_le_of_forall_le (by positivity) fun i ↦ (h i).trans <| norm_apply_le_norm hp y i
  · exact norm_le_of_forall_sum_le hp (norm_nonneg' _) fun s ↦ calc
      ∑ i ∈ s, ‖x i‖ ^ p.toReal
      _ ≤ ∑ i ∈ s, ‖y i‖ ^ p.toReal := by gcongr with i _; exact h i
      _ ≤ ‖y‖ ^ p.toReal := sum_rpow_le_norm_rpow hp y s

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

Goal state before:
pp: α : Type u_3
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ↥(lp (fun x ↦ E) 1)
⊢ ∑' (i : α), ‖↑f i‖ = ‖f‖

Tactic:
by simp [norm_eq_tsum_rpow]

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

Goal state before:
pp: case inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hc : c ≠ 0
this : ‖c‖ * ‖c⁻¹ • c • f‖ ≤ ‖c‖ * (‖c⁻¹‖ * ‖c • f‖)
⊢ ‖c‖ * ‖f‖ ≤ ‖c • f‖

Tactic:
rwa [inv_smul_smul₀ hc, norm_inv, mul_inv_cancel_left₀ (norm_ne_zero_iff.mpr hc)] at this

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)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ := fun i ↦ ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal
hF : ∀ i ∉ s, F i = 0
i : α
hi : i ∈ s
⊢ F i = ‖↑f i‖ ^ p.toReal

Tactic:
simp only [F, coeFn_sum, lp.single_apply, if_pos hi, sub_self, coeFn_sub,
      Pi.sub_apply, Finset.sum_apply, Finset.sum_pi_single, sub_eq_self]

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ := fun i ↦ ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal
hF : ∀ i ∉ s, F i = 0
i : α
hi : i ∈ s
⊢ ‖0‖ ^ p.toReal = 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)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
⊢ HasSum (fun i ↦ lp.single p i (↑f i)) f

Tactic:
have hp₀ : 0 < p := zero_lt_one.trans_le Fact.out

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
⊢ HasSum (fun i ↦ lp.single p i (↑f i)) f