mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Covering.AddCircle

Goal state before:
pp: case e'_8
𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℕ
hn : IsUnit ↑n
e_6✝ : ↥(nsmulAddMonoidHom n).ker = ↥(zsmulAddGroupHom ↑n).ker
e_7✝ : (nsmulAddMonoidHom n).ker.toAddGroup ≍ (zsmulAddGroupHom ↑n).ker.toAddGroup
x✝ : 𝕜
⊢ ((nsmulAddMonoidHom n).comp (QuotientAddGroup.mk' (AddSubgroup.zmultiples p))) x✝ =
    ((zsmulAddGroupHom ↑n).comp (QuotientAddGroup.mk' (AddSubgroup.zmultiples p))) x✝

Tactic:
simp

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)
inst✝¹ : Algebra ℚ 𝕜
n : ℤ
inst✝ : NeZero n
⊢ ↑n = (algebraMap ℚ 𝕜) ↑n

Tactic:
simp

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
E' : Type u_3
inst✝ : TopologicalSpace E'
g : E' ≃ₜ E
h : IsCoveringMapOn (f ∘ ⇑g) s
x✝ : E
⊢ f x✝ = ((f ∘ ⇑g) ∘ ⇑g.symm) x✝

Tactic:
simp

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)
inst✝¹ : Algebra ℚ 𝕜
n : ℕ
inst✝ : NeZero n
⊢ ↑n = (algebraMap ℚ 𝕜) ↑n

Tactic:
simp

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

Goal state before:
pp: case e'_5
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMapOn (⇑g ∘ f) (⇑g.symm ⁻¹' s)
x✝ : E
⊢ f x✝ = (⇑g.symm ∘ ⇑g ∘ f) x✝

Tactic:
simp

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

Goal state before:
pp: case e'_6
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMapOn (⇑g ∘ f) (⇑g.symm ⁻¹' s)
x✝ : X
⊢ x✝ ∈ s ↔ x✝ ∈ ⇑g.symm.symm ⁻¹' ⇑g.symm ⁻¹' s

Tactic:
simp

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
E' : Type u_3
inst✝ : TopologicalSpace E'
g : E' ≃ₜ E
h : IsCoveringMap (f ∘ ⇑g)
x✝ : E
⊢ f x✝ = ((f ∘ ⇑g) ∘ ⇑g.symm) x✝

Tactic:
simp

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
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMap (⇑g ∘ f)
x✝ : E
⊢ f x✝ = (⇑g.symm ∘ ⇑g ∘ f) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: case funProp.discharger
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ ∀ x ∈ Real.exp '' spectrum ℝ a, x ≠ 0

Tactic:
simp

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

Goal state before:
pp: n : ℤ
⊢ ↑(exp (↑n * (2 * π))) = ↑1

Tactic:
simp

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

Goal state before:
pp: case pos
x y : Circle
hxy : (↑(exp (↑x).arg)).arg ≤ (↑y).arg
⊢ exp ((↑y).arg - (↑(exp (↑x).arg)).arg + (↑x).arg) = y

Tactic:
simp

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

Goal state before:
pp: case neg
x y : Circle
hxy : ¬(↑(exp (↑x).arg)).arg ≤ (↑y).arg
⊢ exp (2 * π + (↑y).arg - (↑(exp (↑x).arg)).arg + (↑x).arg) = y

Tactic:
simp

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

Goal state before:
pp: x✝ y✝ x y : Circle
⊢ x = exp (↑x).arg

Tactic:
simp

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

Goal state before:
pp: x✝ y✝ x y : Circle
⊢ y = exp (x.angleDiff y + (↑x).arg)

Tactic:
simp

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:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ ⇑exp '' (Ioc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ Ioc (↑y).arg (y.angleDiff x + (↑y).arg)) = univ

Tactic:
Ioc_union_Ioc_angleDiff_add_arg h,

Goal state after:
x y : Circle
h : x ≠ y
⊢ ⇑exp '' Ioc (min (↑x).arg (↑y).arg) (min (↑x).arg (↑y).arg + 2 * π) = univ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x).arg (x.angleDiff y + (↑x).arg)) (Ioc (↑y).arg (y.angleDiff x + (↑y).arg))
a : ℝ
ha : a ∈ Ioc (↑x).arg (x.angleDiff y + (↑x).arg)
b : ℝ
hb : b ∈ Ioc (↑y).arg (y.angleDiff x + (↑y).arg)
⊢ min (↑x).arg (↑y).arg + 2 * π - min (↑x).arg (↑y).arg ≤ 2 * π

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ 0 < 1

Tactic:
simp

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
⊢ spectrum ℂ u = ∅

Tactic:
simp

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

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ x ∉ {x}ᶜ

Tactic:
simp

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

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ 0 ≤ 1

Tactic:
simp

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
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h✝ : Nontrivial A
h_eqOn : Set.EqOn (fun z ↦ ‖z - 1‖ ^ 2) (fun z ↦ 2 * (1 - z.re)) (spectrum ℂ u)
h₂ : IsGreatest ((fun z ↦ 2 * (1 - z.re)) '' spectrum ℂ u) (2 * (1 - x))
⊢ (fun x ↦ ‖x - 1‖) '' spectrum ℂ u ⊆ {x | 0 ≤ x}

Tactic:
simp

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

Goal state before:
pp: case inl
⊢ Periodic (fun x ↦ Circle.exp (2 * π / 0 * x)) 0

Tactic:
simp

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
h : -‖↑x‖ ∈ spectrum ℝ ↑x
⊢ (fun a ↦ Real.cos a) (-‖↑x‖) = Real.cos ‖x‖

Tactic:
simp

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

Goal state before:
pp: case zero
T : ℝ
x : AddCircle T
⊢ (0 • x).toCircle = x.toCircle ^ 0

Tactic:
simp

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

Goal state before:
pp: case convert_2
⊢ 2 * π ≠ 0

Tactic:
simp

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

Goal state before:
pp: ⊢ ∀ᶠ (i : ℕ) in Filter.atTop, True

Tactic:
simp

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

Goal state before:
pp: case e'_5
n : ℤ
inst✝ : NeZero n
hn : IsUnit ↑n
e : AddCircle 1 ≃ₜ Circle := ⋯
x✝ : AddCircle 1
⊢ ↑((⇑(zpowGroupHom n) ∘ ⇑e) x✝) = ↑((⇑e ∘ fun x ↦ n • x) x✝)

Tactic:
simp [zpowGroupHom, e, homeomorphCircle_apply, toCircle_zsmul]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : CStarRing A
inst✝² : Ring R
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
x✝ : A
⊢ (let __spread.0 := (Units.mulLeftLinearEquiv R A) (toUnits 1);
      { toLinearEquiv := __spread.0, norm_map' := ⋯ })
      x✝ =
    1 x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : CStarRing A
inst✝² : Ring R
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
x✝² x✝¹ : ↥(unitary A)
x✝ : A
⊢ (let __spread.0 := (Units.mulLeftLinearEquiv R A) (toUnits (x✝² * x✝¹));
      { toLinearEquiv := __spread.0, norm_map' := ⋯ })
      x✝ =
    ((let __spread.0 := (Units.mulLeftLinearEquiv R A) (toUnits x✝²);
        { toLinearEquiv := __spread.0, norm_map' := ⋯ }) *
        let __spread.0 := (Units.mulLeftLinearEquiv R A) (toUnits x✝¹);
        { toLinearEquiv := __spread.0, norm_map' := ⋯ })
      x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : CStarRing A
inst✝² : Ring R
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
u v : ↥(unitary A)
x : A
⊢ ((mulLeft R A) (u * v)) x = ((mulLeft R A) u) (((mulLeft R A) v) x)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : CStarRing A
inst✝² : Ring R
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
x✝ : A
⊢ (mulRight R 1) x✝ = (LinearIsometryEquiv.refl R A) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Normalize

Goal state before:
pp: case inr.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
⊢ normalize (0 • x) = ↑(SignType.sign 0) • normalize x

Tactic:
simp

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
A : E →L[𝕜] F
x : E
y : F
⊢ ⟪(adjointAux A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x✝¹ : (A : Type ?u.39) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
x✝ : ∀ (A : Type ?u.41) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
⊢ 0 = ∑ i, 0 i • ↑(![1, -1, 1, -1] i) ∧ ∀ (i : Fin 4), ‖0 i‖ ≤ ‖0‖ / 2

Tactic:
simp

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
⊢ adjoint (ContinuousLinearMap.id 𝕜 E) = ContinuousLinearMap.id 𝕜 E

Tactic:
simp

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
⊢ adjoint 1 = 1

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u v : ↥(unitary A)
⊢ ‖(↑u * ↑(star v) - 1) * ↑v‖ = ‖↑(u * star v) - 1‖

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
⊢ expUnitary (↑0 • x) = 1

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
⊢ expUnitary (↑1 • x) = expUnitary x

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u v : ↥(unitary A)
huv : ‖↑v - ↑u‖ < 2
⊢ ↑(expUnitary (↑0 • argSelfAdjoint (v * star u)) * u) = ↑u

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
⊢ (fun y ↦ (List.map expUnitary y).prod) [] = 1

Tactic:
simp

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

Goal state before:
pp: case mpr.nil
A : Type u_1
inst✝ : CStarAlgebra A
⊢ (List.map expUnitary []).prod ∈ pathComponent 1

Tactic:
simp

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
T : E →L[𝕜] F
⊢ (↑T).rangeᗮ = (↑(adjoint (adjoint T))).range.topologicalClosureᗮ

Tactic:
simp

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
⊢ A x ∈ (↑A).range

Tactic:
simp

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
hb : BddBelow (Set.range fun w ↦ ‖y - ↑w‖)
⊢ (∀ (z : E), ‖y - A x‖ ≤ ‖y - A z‖) ↔ ∀ (i : ↥(↑A).range), ‖y - A x‖ ≤ ‖y - ↑i‖

Tactic:
simp

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
T U : E →L[𝕜] E
hT : (↑T).IsSymmetric
hU : (↑U).IsSymmetric
⊢ (↑U).ker ≤ (↑T).ker ↔ (↑T).range ≤ (↑U).range

Tactic:
refine ⟨fun h ↦ ?_, LinearMap.ker_le_ker_of_range hT hU⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T U : E →L[𝕜] E
hT : (↑T).IsSymmetric
hU : (↑U).IsSymmetric
h : (↑U).ker ≤ (↑T).ker
⊢ (↑T).range ≤ (↑U).range
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
⊢ ‖adjoint A ∘SL A‖ = ‖A‖ * ‖A‖

Tactic:
by
  refine le_antisymm ?_ ?_
  · calc
      ‖A† ∘L A‖ ≤ ‖A†‖ * ‖A‖ := opNorm_comp_le _ _
      _ = ‖A‖ * ‖A‖ := by rw [LinearIsometryEquiv.norm_map]
  · rw [← sq, ← Real.sqrt_le_sqrt_iff (norm_nonneg _), Real.sqrt_sq (norm_nonneg _)]
    refine opNorm_le_bound _ (Real.sqrt_nonneg _) fun x => ?_
    have :=
      calc
        re ⟪(A† ∘L A) x, x⟫ ≤ ‖(A† ∘L A) x‖ * ‖x‖ := re_inner_le_norm _ _
        _ ≤ ‖A† ∘L A‖ * ‖x‖ * ‖x‖ := by gcongr; exact le_opNorm _ _
    calc
      ‖A x‖ = √(re ⟪(A† ∘L A) x, x⟫) := by rw [apply_norm_eq_sqrt_inner_adjoint_left]
      _ ≤ √(‖A† ∘L A‖ * ‖x‖ * ‖x‖) := Real.sqrt_le_sqrt this
      _ = √‖A† ∘L A‖ * ‖x‖ := by
        simp_rw [mul_assoc, Real.sqrt_mul (norm_nonneg _) (‖x‖ * ‖x‖),
          Real.sqrt_mul_self (norm_nonneg x)]

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
x : E
y : F
⊢ adjoint (((rankOne 𝕜) x) y) = ((rankOne 𝕜) y) x

Tactic:
simp [rankOne_def', adjoint_comp, ← adjoint_innerSL_apply]

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
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ (∀ (x : E), ‖(1 - T) (T x)‖ = 0) ↔ ∀ (x : E), ‖(T - T * T) x‖ = 0

Tactic:
simp

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
w✝¹ : Submodule 𝕜 E
w✝ : w✝¹.HasOrthogonalProjection
⊢ IsStarProjection w✝¹.starProjection

Tactic:
simp

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
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
⊢ univ.Nonempty

Tactic:
simp

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
⊢ adjoint id = id

Tactic:
simp

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
⊢ adjoint 1 = 1

Tactic:
simp

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
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
⊢ i ∈ univ

Tactic:
simp

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
p : P
⊢ univ.Nonempty

Tactic:
simp

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
p : P
p✝ : Fin (n + 1) → V
⊢ univ.Nonempty

Tactic:
simp

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
⊢ finrank 𝕜 ↥(adjoint A).ker + finrank 𝕜 ↥A.range - finrank 𝕜 ↥(adjoint A).ker = finrank 𝕜 ↥A.range

Tactic:
simp

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

Goal state before:
pp: case e'_3
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 : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ ↑fs = Set.range ⇑(fs.orderEmbOfFin h).toEmbedding

Tactic:
simp

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
ι₁ : 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₁ : ι₁
i₂ : ι₂
⊢ ⟪A (b₁ i₁), b₂ i₂⟫_𝕜 = ⟪(adjoint B) (b₁ i₁), b₂ i₂⟫_𝕜

Tactic:
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
n : ℕ
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ {i}ᶜ ≠ Set.univ

Tactic:
simp

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

Goal state before:
pp: case hw.h
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
V₂ : Type u_4
P₂ : Type u_5
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective ⇑f
⊢ #univ ≠ 0

Tactic:
simp

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✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i✝ i : Fin (n + 1)
⊢ ∑ j ∈ {i}ᶜ, (↑n)⁻¹ • (s.points j -ᵥ s.points i) =
    ∑ i_1 ∈ {i}ᶜ, (↑n)⁻¹ • (s.points i_1 -ᵥ s.points i) + ∑ i_1 ∈ {i}, (↑n)⁻¹ • (s.points i_1 -ᵥ s.points i)

Tactic:
simp

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✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i✝ j i : Fin (n + 1)
⊢ ∀ x ∈ univ, s.points x -ᵥ s.points i = s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0)

Tactic:
simp

Goal state after:
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
e : H ≃ₗᵢ[𝕜] K
⊢ adjoint ↑↑e = adjoint ↑↑e ∘SL ↑↑e ∘SL ↑↑e.symm

Tactic:
simp

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✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i j : Fin (n + 1)
h1 : ∀ (i : Fin (n + 1)), ∑ x, (s.points x -ᵥ s.points i) = ∑ x, (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0))
⊢ s.points i -ᵥ s.points j = -(s.points j -ᵥ s.points i)

Tactic:
simp

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✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ (↑n + 1)⁻¹ = 1 * (↑n + 1)⁻¹

Tactic:
simp

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

Goal state before:
pp: case hw.h
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
V₂ : Type u_4
P₂ : Type u_5
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AffineSpace V₂ P₂
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective ⇑f
i : Fin (n + 1)
⊢ #univ ≠ 0

Tactic:
simp

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

Goal state before:
pp: case inl
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑∅ ⊆ ↑(affineSpan k ↑t)
⊢ #∅ ≤ #t

Tactic:
simp

Goal state after: