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

Goal state before:
pp: A : Type u_1
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace ℝ A
inst✝¹ : Nontrivial A
x : A
r : ℝ
inst✝ : StrictConvexSpace ℝ A
⊢ extremePoints ℝ (closedBall x r) = sphere x r

Tactic:
rw [(_root_.strictConvex_closedBall ℝ x r).extremePoints_eq_sdiff_interior, interior_closedBall',
    closedBall_sdiff_ball]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: ι : Sort u_1
V : Type u
G H : SimpleGraph V
a b c u v✝ w✝ : V
e : Sym2 V
inst✝ : DecidableEq V
v : V
x✝ : ↑(G.neighborSet v)
w : V
hw : w ∈ G.neighborSet v
⊢ (fun e ↦ ⟨G.otherVertexOfIncident ⋯, ⋯⟩) ((fun w ↦ ⟨s(v, ↑w), ⋯⟩) ⟨w, hw⟩) = ⟨w, hw⟩

Tactic:
simp only [Subtype.mk.injEq]
    exact incidence_other_neighbor_edge _ hw

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

Goal state before:
pp: case mp.inr.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
hr : r₁ • (x -ᵥ p₁') = r₂ • (y -ᵥ p₂')
⊢ r₁ • (x -ᵥ p₁) = r₂ • (y -ᵥ p₂') - r₂ • (r₁ / r₂) • (p₁ -ᵥ p₁')

Tactic:
← hr,

Goal state after:
case mp.inr.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
hr : r₁ • (x -ᵥ p₁') = r₂ • (y -ᵥ p₂')
⊢ r₁ • (x -ᵥ p₁) = r₁ • (x -ᵥ p₁') - r₂ • (r₁ / r₂) • (p₁ -ᵥ p₁')
Module: Mathlib.Analysis.Convex.StrictCombination

Goal state before:
pp: V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
t : Finset ι
w : ι → ℝ
p₀ : P
r : ℝ
p : ι → P
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : ∑ i ∈ t, w i = 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : p i ≠ p j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hp : ∀ i ∈ t, dist (p i) p₀ ≤ r
⊢ dist ((affineCombination ℝ t p) w) p₀ < r

Tactic:
rw [affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _ h1 p₀,
    weightedVSubOfPoint_apply, dist_vadd_left]
  simp_rw [dist_eq_norm_vsub] at hp
  exact norm_sum_lt_of_strictConvexSpace h0 h1 hi hj (by simpa using hij) hi0 hj0 hp

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ y ∈ {y | s.WSameSide x y} ↔ y ∈ Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) ↑s

Tactic:
Set.mem_ofPred,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ s.WSameSide x y ↔ y ∈ Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) ↑s
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ y ∈ {y | s.SSameSide x y} ↔ y ∈ Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) ↑s

Tactic:
Set.mem_ofPred,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ s.SSameSide x y ↔ y ∈ Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) ↑s
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ y ∈ {y | s.WOppSide x y} ↔ y ∈ Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Iic 0) ↑s

Tactic:
Set.mem_ofPred,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ s.WOppSide x y ↔ y ∈ Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Iic 0) ↑s
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ y ∈ {y | s.SOppSide x y} ↔ y ∈ Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Iio 0) ↑s

Tactic:
Set.mem_ofPred,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ s.SOppSide x y ↔ y ∈ Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Iio 0) ↑s
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case pos
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s).Nonempty
hx : x ∈ s
⊢ IsPreconnected {y | s.SSameSide x y}

pp: case neg
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s).Nonempty
hx : x ∉ s
⊢ IsPreconnected {y | s.SSameSide x y}

Tactic:
· simp only [hx, SSameSide, not_true, false_and, and_false]
      exact isPreconnected_empty

Goal state after:
case neg
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s).Nonempty
hx : x ∉ s
⊢ IsPreconnected {y | s.SSameSide x y}
Module: Mathlib.Analysis.Convex.Visible

Goal state before:
pp: case inr.refine_1.refine_1
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝¹ : 0 < w i
hwi✝ : w i < 1
ε : 𝕜
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
hε₁ : ε < 1
this✝ : 0 < 1 - ε
hwi : 0 < 1 - w i
this :
  Wbtw 𝕜 ((lineMap x (a i)) ε) ((lineMap x (∑ j ∈ t, w j • a j)) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)))
    (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j)
j : ι
⊢ j ∈ t.erase i → 0 ≤ w j / (1 - w i)

Tactic:
hj

Goal state after:
case inr.refine_1.refine_1
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝¹ : 0 < w i
hwi✝ : w i < 1
ε : 𝕜
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
hε₁ : ε < 1
this✝ : 0 < 1 - ε
hwi : 0 < 1 - w i
this :
  Wbtw 𝕜 ((lineMap x (a i)) ε) ((lineMap x (∑ j ∈ t, w j • a j)) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)))
    (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j)
j : ι
hj : j ∈ t.erase i
⊢ 0 ≤ w j / (1 - w i)
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ ‖holder r B f g‖ₑ ≤ ‖B‖ₑ * ‖f‖ₑ * ‖g‖ₑ

Tactic:
Lp.enorm_def

Goal state after:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ eLpNorm (↑↑(holder r B f g)) r μ ≤ ‖B‖ₑ * eLpNorm (↑↑f) p μ * eLpNorm (↑↑g) q μ
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
n : ℕ
⊢ ∃ k C, 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f x‖ ≤ C * (1 + ‖x‖) ^ k

Tactic:
rcases hf_temperate.isBigO_uniform n with ⟨k, hk⟩

Goal state after:
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
n k : ℕ
hk : ∀ n_1 ≤ n, iteratedFDeriv ℝ n_1 f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f x‖ ≤ C * (1 + ‖x‖) ^ k
Module: Mathlib.Analysis.Distribution.TestFunction

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
inst✝⁹ : NormedSpace 𝕜 F
n : ℕ∞
V : Type u_6
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
t : TopologicalSpace V
inst✝⁶ : IsTopologicalAddGroup V
inst✝⁵ : ContinuousSMul ℝ V
inst✝⁴ : LocallyConvexSpace ℝ V
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F
inst✝¹ : Module 𝕜 V
inst✝ : IsScalarTower ℝ 𝕜 V
f : 𝓓^{n}(Ω, F) →ₗ[𝕜] V
this✝¹ : IsTopologicalAddGroup 𝓓^{n}(Ω, F)
this✝ : ContinuousSMul ℝ 𝓓^{n}(Ω, F)
this : LocallyConvexSpace ℝ 𝓓^{n}(Ω, F)
⊢ topologicalSpace Ω F n ≤ induced (⇑(↑ℝ f)) t ↔
    ∀ (K : Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω), Continuous[_, t] (⇑(↑ℝ f) ∘ ofSupportedIn K_sub_Ω)

Tactic:
topologicalSpace_le_iff,

Goal state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
inst✝⁹ : NormedSpace 𝕜 F
n : ℕ∞
V : Type u_6
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
t : TopologicalSpace V
inst✝⁶ : IsTopologicalAddGroup V
inst✝⁵ : ContinuousSMul ℝ V
inst✝⁴ : LocallyConvexSpace ℝ V
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F
inst✝¹ : Module 𝕜 V
inst✝ : IsScalarTower ℝ 𝕜 V
f : 𝓓^{n}(Ω, F) →ₗ[𝕜] V
this✝¹ : IsTopologicalAddGroup 𝓓^{n}(Ω, F)
this✝ : ContinuousSMul ℝ 𝓓^{n}(Ω, F)
this : LocallyConvexSpace ℝ 𝓓^{n}(Ω, F)
⊢ originalTop Ω F n ≤ induced (⇑(↑ℝ f)) t ↔
    ∀ (K : Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω), Continuous[_, t] (⇑(↑ℝ f) ∘ ofSupportedIn K_sub_Ω)
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
T : F →L[ℝ] F
hT : (↑T).IsSymmetric
x₀ : F
⊢ HasStrictFDerivAt T.reApplyInnerSelf (2 • (innerSL ℝ) (T x₀)) x₀

Tactic:
convert! T.hasStrictFDerivAt.inner ℝ (hasStrictFDerivAt_id x₀) using 1
  ext y
  rw [smul_apply, ContinuousLinearMap.comp_apply, fderivInnerCLM_apply,
    ContinuousLinearMap.prod_apply, innerSL_apply_apply, id, ContinuousLinearMap.id_apply,
    hT.apply_clm x₀ y, real_inner_comm _ x₀, two_smul]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h : ∀ c > 0, ∃ x, ‖(T - μ • 1) x‖ < c * ‖x‖
hK : ∀ K > 0, ∃ x, ‖(T - μ • 1) x‖ < K * ‖x‖
C : 𝕜
hC : 1 < ‖C‖
ε : ℝ
hε : ε > 0
x : X
hx : ‖(T - μ • 1) x‖ < ε * ‖x‖
this : x ≠ 0
η : 𝕜
hη : η ≠ 0
h₁ : ‖η • x‖ < 1
h₂ : 1 / ‖C‖ ≤ ‖η • x‖
h₃ : ‖η‖⁻¹ ≤ 1⁻¹ * ‖C‖ * ‖x‖
⊢ ‖C‖⁻¹ ≤ ‖η • x‖

Tactic:
simpa using h₂

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Sort

Goal state before:
pp: case mpr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f))
this : graphEquiv₂ f = StrictMono.orderIsoOfSurjective (⇑(Equiv.trans σ (graphEquiv₁ f))) h ⋯
⊢ σ = sort f

Tactic:
ext1 x

Goal state after:
case mpr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f))
this : graphEquiv₂ f = StrictMono.orderIsoOfSurjective (⇑(Equiv.trans σ (graphEquiv₁ f))) h ⋯
x : Fin n
⊢ σ x = (sort f) x
Module: Mathlib.Analysis.Matrix.PosDef

Goal state before:
pp: n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.PosSemidef
i : n
x✝ : i ∈ Finset.univ
⊢ 0 ≤ ↑(⋯.eigenvalues i)

Tactic:
by simpa using hA.eigenvalues_nonneg i

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

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C(↑(spectrum ℝ a), ℝ)
⊢ spectrum ℝ (ha.cfcAux f) = Set.range ⇑f

Tactic:
apply Set.eq_of_subset_of_subset
      · rw [← ContinuousMap.spectrum_eq_range f]
        apply AlgHom.spectrum_apply_subset
      · rw [cfcAux_apply, conjStarAlgAut_apply, Unitary.spectrum_star_right_conjugate]
        rintro - ⟨x, rfl⟩
        apply spectrum.of_algebraMap_mem 𝕜
        simp only [Function.comp_apply, Set.mem_range, spectrum_diagonal]
        obtain ⟨x, hx⟩ := x
        obtain ⟨i, rfl⟩ := ha.spectrum_real_eq_range_eigenvalues ▸ hx
        exact ⟨i, rfl⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
v : E
μ : Eigenvalues T
⊢ (hT.diagonalization (T v)).ofLp μ = ↑T 1 μ • (hT.diagonalization v).ofLp μ

Tactic:
suffices
    ∀ w : PiLp 2 fun μ : Eigenvalues T => eigenspace T μ,
      T (hT.diagonalization.symm w) = hT.diagonalization.symm (toLp 2 fun μ => (μ : 𝕜) • w μ) by
    simpa only [LinearIsometryEquiv.symm_apply_apply, LinearIsometryEquiv.apply_symm_apply] using
      congr_arg (fun w => hT.diagonalization w μ) (this (hT.diagonalization v))

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
v : E
μ : Eigenvalues T
⊢ ∀ (w : PiLp 2 fun μ ↦ ↥(eigenspace T (↑T 1 μ))),
    T (hT.diagonalization.symm w) = hT.diagonalization.symm (toLp 2 fun μ ↦ ↑T 1 μ • w.ofLp μ)
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
i : Fin n
v : E := (hT.unsortedEigenvectorBasis hn) i
μ : 𝕜 := ↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
H₁ : v ∈ eigenspace T μ
⊢ v ≠ 0

Tactic:
simpa using (hT.unsortedEigenvectorBasis hn).toBasis.ne_zero i

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
⊢ ∑ x, w.ofLp x • ↑(hT.eigenvalues hn x) • (hT.eigenvectorBasis hn) x =
    ∑ x, (↑(hT.eigenvalues hn x) * w.ofLp x) • (hT.eigenvectorBasis hn) x

Tactic:
apply Fintype.sum_congr

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
⊢ ∀ (a : Fin n),
    w.ofLp a • ↑(hT.eigenvalues hn a) • (hT.eigenvectorBasis hn) a =
      (↑(hT.eigenvalues hn a) * w.ofLp a) • (hT.eigenvectorBasis hn) a
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
⊢ IsUniformInducing ⇑(ContinuousLinearMap.pi (structureMapCLM 𝕜 n))

Tactic:
simp_rw [isUniformInducing_iff_uniformSpace, ContDiffMapSupportedIn.uniformSpace_eq_iInf,
      Pi.uniformSpace_eq, comap_iInf, ← comap_comap]
    rfl

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : Fintype n
A : Matrix n n 𝕜
hA : 0 ≤ A
⊢ ∀ x ∈ quasispectrum ℝ A, 0 ≤ x

Tactic:
by
    classical
    simp only [quasispectrum_eq_spectrum_union_zero ℝ A, Set.union_singleton, Set.mem_insert_iff,
      forall_eq_or_imp, le_refl, true_and]
    intro x hx
    obtain ⟨i, rfl⟩ := Set.ext_iff.mp
      hA.posSemidef.1.spectrum_real_eq_range_eigenvalues x |>.mp hx
    exact hA.posSemidef.eigenvalues_nonneg _

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ (CFC.sqrt A).det = RCLike.sqrt A.det

Tactic:
CFC.sqrt_eq_cfc,

Goal state after:
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ (cfc (⇑NNReal.sqrt) A).det = RCLike.sqrt A.det
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓^{n}_{K}(E, F)
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) f ≤ C ↔ ↑i ≤ n → ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C

Tactic:
have : (∀ x, ‖iteratedFDeriv ℝ i f x‖ ≤ C) ↔ (∀ x ∈ K, ‖iteratedFDeriv ℝ i f x‖ ≤ C) := by
    congrm ∀ x, ?_
    by_cases hx : x ∈ K
    · simp [hx]
    · simp [hx, f.iteratedFDeriv_zero_on_compl hx, hC]
  by_cases hi : i ≤ n
  · simp [hi, forall_const, ContDiffMapSupportedIn.seminorm_apply, structureMapCLM_apply,
      BoundedContinuousFunction.norm_le hC, this]
  · push Not at hi
    simp [hi, ContDiffMapSupportedIn.seminorm_eq_bot_of_gt _ hi, hC]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : BorelSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : IsFiniteMeasure μ
inst✝ : Fact (1 ≤ p)
⊢ (toLpHom p μ).range = Lp.boundedContinuousFunction E p μ

Tactic:
by
  symm
  exact AddMonoidHom.addSubgroupOf_range_eq_of_le
      ((ContinuousMap.toAEEqFunAddHom μ).comp (toContinuousMapAddMonoidHom α E))
      (by rintro - ⟨f, rfl⟩; exact mem_Lp f : _ ≤ Lp E p μ)

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h : MemLp f 2 μ
⊢ Integrable (fun x ↦ f x ^ 2) μ

Tactic:
simpa [← memLp_one_iff_integrable] using h.norm_rpow two_ne_zero ENNReal.ofNat_ne_top

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: case e_f
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ (fun a ↦ ENNReal.ofReal (‖↑↑f a‖ ^ 2)) = fun a ↦ ↑(‖↑↑f a‖₊ ^ 2)

Tactic:
ext1 x

Goal state after:
case e_f
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
x : α
⊢ ENNReal.ofReal (‖↑↑f x‖ ^ 2) = ↑(‖↑↑f x‖₊ ^ 2)
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ hV : OrthogonalFamily 𝕜 G V
c : 𝕜
f : ↥(lp G 2)
⊢ ∑' (i : ι), (V i) (↑(c • f) i) = (RingHom.id 𝕜) c • ∑' (i : ι), (V i) (↑f i)

Tactic:
simpa only [LinearIsometry.map_smul, Pi.smul_apply, lp.coeFn_smul] using!
      (hV.summable_of_lp f).tsum_const_smul c

Goal state after:
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
⊢ ↑(Submonoid.closure (range fourier)) ⊆ ↑(span ℂ (range fourier))

Tactic:
refine Subset.trans ?_ Submodule.subset_span

Goal state after:
T : ℝ
⊢ ↑(Submonoid.closure (range fourier)) ⊆ range fourier
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x.toCircle = y.toCircle
⊢ x = y

Tactic:
exact injective_toCircle hT.elim.ne' hxy

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(E, F)
c : 𝕜
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • ⇑f) x‖ = ‖c‖ * ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖

Tactic:
mul_comm ‖c‖,

Goal state after:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(E, F)
c : 𝕜
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • ⇑f) x‖ = ‖x‖ ^ k * ‖c‖ * ‖iteratedFDeriv ℝ n (⇑f) x‖
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
M : ℝ
hMp : 0 ≤ M
hM : ∀ (x : ℝ), |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ M
⊢ (SchwartzMap.seminorm 𝕜 k n) f ≤ M

Tactic:
refine seminorm_le_bound 𝕜 k n f hMp ?_

Goal state after:
𝕜 : Type u_2
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
M : ℝ
hMp : 0 ≤ M
hM : ∀ (x : ℝ), |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ M
⊢ ∀ (x : ℝ), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ M