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

Goal state before:
pp: n : Type u_4
α : Type u_5
ι : Type u_7
inst✝² : Fintype n
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : n → α
⊢ ‖replicateRow ι v‖₊ = ‖v‖₊

Tactic:
by
  simp [nnnorm_def, Pi.nnnorm_def]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ContinuousOn a t
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) t

Tactic:
ContinuousOn

Goal state after:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
⊢ ∀ x ∈ t, ContinuousWithinAt (fun x ↦ cfcₙ f (a x)) t x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ContinuousOn a t
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) t

Tactic:
ContinuousOn

Goal state after:
X : Type u_1
A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
⊢ ∀ x ∈ t, ContinuousWithinAt (fun x ↦ cfcₙ f (a x)) t x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra ℂ A
inst✝² : StarModule ℂ A
inst✝¹ : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝ : ContinuousMap.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf : ContinuousOn f ((fun x ↦ ↑x.re) '' spectrum ℂ a)
ha : IsStarNormal a
⊢ cfc f (cfc (fun x ↦ ↑x.re) a) = cfc (fun x ↦ f ↑x.re) a

Tactic:
← cfc_comp' ..

Goal state after:
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra ℂ A
inst✝² : StarModule ℂ A
inst✝¹ : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝ : ContinuousMap.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf : ContinuousOn f ((fun x ↦ ↑x.re) '' spectrum ℂ a)
ha : IsStarNormal a
⊢ cfc (fun x ↦ f ↑x.re) a = cfc (fun x ↦ f ↑x.re) a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra ℂ A
inst✝² : StarModule ℂ A
inst✝¹ : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝ : ContinuousMap.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf : ContinuousOn f ((fun x ↦ ↑x.im) '' spectrum ℂ a)
ha : IsStarNormal a
⊢ cfc f (cfc (fun x ↦ ↑x.im) a) = cfc (fun x ↦ f ↑x.im) a

Tactic:
← cfc_comp' ..

Goal state after:
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra ℂ A
inst✝² : StarModule ℂ A
inst✝¹ : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝ : ContinuousMap.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf : ContinuousOn f ((fun x ↦ ↑x.im) '' spectrum ℂ a)
ha : IsStarNormal a
⊢ cfc (fun x ↦ f ↑x.im) a = cfc (fun x ↦ f ↑x.im) a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℂ A
inst✝³ : StarModule ℂ A
inst✝² : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMap.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (spectrum ℝ ↑(ℜ a))
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.re) '' spectrum ℂ a)
| cfc (fun x ↦ ↑(f x.re)) (cfc (fun x ↦ ↑x.re) a)

Tactic:
← cfc_comp' ..

Goal state after:
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℂ A
inst✝³ : StarModule ℂ A
inst✝² : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMap.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (spectrum ℝ ↑(ℜ a))
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.re) '' spectrum ℂ a)
| cfc (fun x ↦ ↑(f (↑x.re).re)) a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℂ A
inst✝³ : StarModule ℂ A
inst✝² : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMap.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (spectrum ℝ ↑(ℑ a))
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.im) '' spectrum ℂ a)
| cfc (fun x ↦ ↑(f x.re)) (cfc (fun x ↦ ↑x.im) a)

Tactic:
← cfc_comp' ..

Goal state after:
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℂ A
inst✝³ : StarModule ℂ A
inst✝² : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMap.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (spectrum ℝ ↑(ℑ a))
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.im) '' spectrum ℂ a)
| cfc (fun x ↦ ↑(f (↑x.im).re)) a
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), ⟪f, w⟫ = (B v) w
⊢ ∀ (v_1 : E), ⟪f, v_1⟫ = ⟪B♯ v, v_1⟫

Tactic:
intro w

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), ⟪f, w⟫ = (B v) w
w : E
⊢ ⟪f, w⟫ = ⟪B♯ v, w⟫
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.toPreGNS ∘ₗ ↑((ContinuousLinearMap.mul ℂ A) a) ∘ₗ ↑f.ofPreGNS) x‖ ^ 2 ≤ ‖a‖ ^ 2 * ‖x‖ ^ 2

Tactic:
← RCLike.ofReal_le_ofReal (K := ℂ),

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

Goal state before:
pp: ⊢ cexp (↑0 * I) = ↑1

Tactic:
ofReal_zero,

Goal state after:
⊢ cexp (0 * I) = ↑1
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e f : Pretrivialization F proj
⊢ (f.symm.trans e.toPartialEquiv).source = (e.baseSet ∩ f.baseSet) ×ˢ univ

Tactic:
rw [PartialEquiv.trans_source, PartialEquiv.symm_source, e.target_inter_preimage_symm_source_eq]

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

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
⊢ (e.symm.trans e'.toPartialEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ univ

Tactic:
rw [PartialEquiv.trans_source, e'.source_eq, PartialEquiv.symm_source, e.target_eq, inter_comm,
    e.preimage_symm_proj_inter, inter_comm]

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h :
  ∀ (a b : X) (b_1 : f a = f b),
    ⟨(a, b), b_1⟩ ∈ Function.pullbackDiagonal f → ∃ t ∈ 𝓝 a ×ˢ 𝓝 b, Subtype.val ⁻¹' t ⊆ Function.pullbackDiagonal f
x : X
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
obtain ⟨t, ht, t_sub⟩ := h x x rfl rfl

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h :
  ∀ (a b : X) (b_1 : f a = f b),
    ⟨(a, b), b_1⟩ ∈ Function.pullbackDiagonal f → ∃ t ∈ 𝓝 a ×ˢ 𝓝 b, Subtype.val ⁻¹' t ⊆ Function.pullbackDiagonal f
x : X
t : Set (X × X)
ht : t ∈ 𝓝 x ×ˢ 𝓝 x
t_sub : Subtype.val ⁻¹' t ⊆ Function.pullbackDiagonal f
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case inr
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
p : Z
hp' : p ∈ e'.source
⊢ (↑(e.disjointUnion e'.toOpenPartialHomeomorph ⋯ ⋯) p).1 = proj p

Tactic:
change (e.source.piecewise e e' p).1 = proj p
      rw [piecewise_eq_of_notMem, e'.coe_fst hp']
      simp only [source_eq] at hp' ⊢
      exact fun h => H.le_bot ⟨h, hp'⟩

Goal state after:
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✝
T✝ : Trivialization F proj
z : Z
b : B
ι : Type u_5
inst✝² : TopologicalSpace ι
inst✝¹ : LocallyCompactPair ι ↑T✝.baseSet
γ : C(ι, ↑T✝.baseSet)
i : ι
e : ↑T✝.source
T : Trivialization F proj
inst✝ : LocallyCompactPair ι ↑T.baseSet
Ψ : C((↑T.source × C(ι, ↑T.baseSet)) × ι, C(ι, ↑T.baseSet) × ι) :=
  { toFun := fun eγt ↦ (eγt.1.2, eγt.2), continuous_toFun := ⋯ }
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun eγt ↦ (eγt.1.1, eγt.1.2 eγt.2)

Tactic:
simpa using ⟨by fun_prop, ContinuousEval.continuous_eval.comp Ψ.continuous⟩

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

Goal state before:
pp: case refine_1.inl
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
a✝ : Nontrivial A
h : ‖↑x‖ ∈ spectrum ℝ ↑x
⊢ Real.cos ‖x‖ ∈ (fun a ↦ Real.cos a) '' spectrum ℝ ↑x

Tactic:
| inl h =>

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
this : ContinuousOn arg (spectrum ℂ ↑u)
⊢ cfc (fun x ↦ NormedSpace.exp (I • x)) (cfc (fun x ↦ ↑x.arg) ↑u) = ↑u

Tactic:
← cfc_comp' ..

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
this : ContinuousOn arg (spectrum ℂ ↑u)
⊢ cfc (fun x ↦ NormedSpace.exp (I • ↑x.arg)) ↑u = ↑u
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
⊢ ContinuousOn argSelfAdjoint (ball 1 2)

Tactic:
rw [Topology.IsInducing.subtypeVal.continuousOn_iff]

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
⊢ ContinuousOn (Subtype.val ∘ argSelfAdjoint) (ball 1 2)
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : u ∈ ball 1 2
⊢ argSelfAdjoint u ∈ ball 0 π

Tactic:
simp only [mem_ball, Subtype.dist_eq, OneMemClass.coe_one, dist_eq_norm, sub_zero] at hu ⊢

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
⊢ ‖argSelfAdjoint u‖ < π
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
hT : IsSelfAdjoint T
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
⊢ IsSelfAdjoint (U.starProjection * T * U.starProjection)

Tactic:
exact hT.conjugate_self <| isSelfAdjoint_starProjection U

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
T : E →L[𝕜] E
inst✝ : CompleteSpace E
⊢ star T * T = T * star T ↔ ∀ (v : E), ‖T v‖ = ‖(adjoint T) v‖

Tactic:
← sub_eq_zero

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
⊢ star T * T - T * star T = 0 ↔ ∀ (v : E), ‖T v‖ = ‖(adjoint T) v‖
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ ∀ (x : E), ‖(T - star T * T) x‖ = 0

Tactic:
have :=
    calc (∀ x : E, ‖(T - star T * T) x‖ = 0) ↔ ∀ x, ‖(adjoint (1 - T)) (T x)‖ = 0 := by
          simp [star_eq_adjoint, one_def]
      _ ↔ ∀ x, ‖(1 - T) (T x)‖ = 0 := by
          simp only [isStarNormal_iff_norm_eq_adjoint.mp h.one_sub]
      _ ↔ ∀ x, ‖(T - T * T) x‖ = 0 := by simp
      _ ↔ T - T * T = 0 := by simp only [norm_eq_zero, ContinuousLinearMap.ext_iff, zero_apply]
      _ ↔ IsIdempotentElem T := by simp only [sub_eq_zero, IsIdempotentElem, eq_comm]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
hT : IsIdempotentElem T
h : IsStarNormal T
this : (∀ (x : E), ‖(T - star T * T) x‖ = 0) ↔ IsIdempotentElem T
⊢ ∀ (x : E), ‖(T - star T * T) x‖ = 0
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
t : Set (Fin (n + 1))
ht : t ≠ Set.univ
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : i ∈ Set.univ ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h : (affineCombination k univ s.points) w ∈ affineSpan k (s.points '' t)
wdef : w = centroidWeights k univ
hw : ∑ i, w i = 1
h1 : w i = 0
⊢ False

Tactic:
have h2 : w i = (1 : k) / (n + 1) := by
    simp [wdef, centroidWeights_apply, card_univ, Fintype.card_fin, Nat.cast_add,
      Nat.cast_one]

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
t : Set (Fin (n + 1))
ht : t ≠ Set.univ
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : i ∈ Set.univ ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h : (affineCombination k univ s.points) w ∈ affineSpan k (s.points '' t)
wdef : w = centroidWeights k univ
hw : ∑ i, w i = 1
h1 : w i = 0
h2 : w i = 1 / (↑n + 1)
⊢ False
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
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (i₁ : ι₁) (i₂ : ι₂), ⟪A (b₁ i₁), b₂ i₂⟫_𝕜 = ⟪b₁ i₁, B (b₂ i₂)⟫_𝕜
i₁ : ι₁
⊢ A (b₁ i₁) = (adjoint B) (b₁ i₁)

Tactic:
exact ext_inner_right_basis b₂ fun i₂ => by simp only [adjoint_inner_left, h i₁ i₂]

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✝
fs₁ fs₂ : Finset (Fin (n✝ + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h✝ :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
i : Fin (n✝ + 1)
ha :
  (↑fs₁).indicator (Function.const (Fin (n✝ + 1)) (↑(m₁ + 1))⁻¹) i =
    (↑fs₂).indicator (Function.const (Fin (n✝ + 1)) (↑(m₂ + 1))⁻¹) i
n : ℕ
h : ↑n + 1 = 0
⊢ False

Tactic:
norm_cast at h

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

Goal state before:
pp: case mp
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
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
i : Fin (n + 1)
ha :
  (↑fs₁).indicator (Function.const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) i =
    (↑fs₂).indicator (Function.const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) i
key : ∀ (n : ℕ), ↑n + 1 ≠ 0
hi : i ∈ fs₁
⊢ i ∈ fs₂

Tactic:
by_contra hni

Goal state after:
case mp
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
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
i : Fin (n + 1)
ha :
  (↑fs₁).indicator (Function.const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) i =
    (↑fs₂).indicator (Function.const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) i
key : ∀ (n : ℕ), ↑n + 1 ≠ 0
hi : i ∈ fs₁
hni : i ∉ fs₂
⊢ False
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: case mpr
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
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
i : Fin (n + 1)
ha :
  (↑fs₁).indicator (Function.const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) i =
    (↑fs₂).indicator (Function.const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) i
key : ∀ (n : ℕ), ↑n + 1 ≠ 0
hi : i ∈ fs₂
⊢ i ∈ fs₁

Tactic:
by_contra hni

Goal state after:
case mpr
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
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
i : Fin (n + 1)
ha :
  (↑fs₁).indicator (Function.const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) i =
    (↑fs₂).indicator (Function.const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) i
key : ∀ (n : ℕ), ↑n + 1 ≠ 0
hi : i ∈ fs₂
hni : i ∉ fs₁
⊢ False
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : 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
⊢ f.conjStarAlgEquiv = g.conjStarAlgEquiv ↔ ∃ α, f = α • g

Tactic:
conv_lhs => rw [eq_comm]

Goal state after:
𝕜 : 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
⊢ g.conjStarAlgEquiv = f.conjStarAlgEquiv ↔ ∃ α, f = α • g
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
i : Fin (n + 1)
⊢ (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i) =
    (↑n + 1) • ((↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i) - (s.centroid -ᵥ s.points i))

Tactic:
centroid_vsub_eq,

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
i : Fin (n + 1)
⊢ (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i) =
    (↑n + 1) • ((↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i) - (↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ s.points i))
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : 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
⊢ ↑((↑f).trans (↑g).symm) ∈ Subalgebra.center 𝕜 (H →L[𝕜] H) ↔ ∃ α, ∀ (x : H), f x = (α • g) x

Tactic:
Algebra.IsCentral.center_eq_bot,

Goal state after:
𝕜 : 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
⊢ ↑((↑f).trans (↑g).symm) ∈ ⊥ ↔ ∃ α, ∀ (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
i : Fin (n + 1)
⊢ ↑n • (s.centroid -ᵥ s.points i - (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i)) = s.points i -ᵥ s.centroid

Tactic:
centroid_vsub_eq,

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
i : Fin (n + 1)
⊢ ↑n • ((↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ s.points i) - (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i)) =
    s.points i -ᵥ s.centroid
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
i : Fin (n + 1)
⊢ ↑n • ((↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ s.points i) - (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i)) =
    -(s.centroid -ᵥ s.points i)

Tactic:
centroid_vsub_eq,

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
i : Fin (n + 1)
⊢ ↑n • ((↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ s.points i) - (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i)) =
    -((↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ s.points i))