mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R✝ : Type u_1
X : Type u_2
M✝ : Type u_3
N✝ : Type u_4
P✝ : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
N : Type u_10
P : Type u_11
w : StdSimplex R M
x✝ : M
inst✝ : IsStrictOrderedRing R
x y : M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
⊢ 0 ≤ Finsupp.single x s

Tactic:
by simpa

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R✝ : Type u_1
X : Type u_2
M✝ : Type u_3
N✝ : Type u_4
P✝ : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
N : Type u_10
P : Type u_11
w : StdSimplex R M
x✝ : M
inst✝ : IsStrictOrderedRing R
x y : M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
⊢ 0 ≤ Finsupp.single y t

Tactic:
by simpa

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
J : I → Type u_9
s : StdSimplex R I
f : (i : I) → StdSimplex R (J i)
g : (i : I) → J i → M
⊢ (iConvexComb s fun i ↦ iConvexComb (f i) (g i)) =
    iConvexComb (iConvexComb s fun i ↦ map (fun x ↦ ⟨i, x⟩) (f i)) (Sigma.uncurry g)

Tactic:
simp only [iConvexComb]

Goal state after:
R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
J : I → Type u_9
s : StdSimplex R I
f : (i : I) → StdSimplex R (J i)
g : (i : I) → J i → M
⊢ sConvexComb (map (fun i ↦ sConvexComb (map (g i) (f i))) s) =
    sConvexComb (map (Sigma.uncurry g) (sConvexComb (map (fun i ↦ map (fun x ↦ ⟨i, x⟩) (f i)) s)))
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : I → J → M
⊢ (iConvexComb s fun i ↦ iConvexComb (f i) (g i)) =
    iConvexComb (iConvexComb s fun i ↦ map (fun x ↦ (i, x)) (f i)) (Function.uncurry g)

Tactic:
simp only [iConvexComb]

Goal state after:
R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : I → J → M
⊢ sConvexComb (map (fun i ↦ sConvexComb (map (g i) (f i))) s) =
    sConvexComb (map (Function.uncurry g) (sConvexComb (map (fun i ↦ map (fun x ↦ (i, x)) (f i)) s)))
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : J → M
⊢ (iConvexComb s fun i ↦ iConvexComb (f i) g) = iConvexComb (iConvexComb s f) g

Tactic:
simp only [iConvexComb]

Goal state after:
R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : J → M
⊢ sConvexComb (map (fun i ↦ sConvexComb (map g (f i))) s) = sConvexComb (map g (sConvexComb (map f s)))
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
X : Type u_2
ι : Sort u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
s : ι → Set X
hs : ∀ (i : ι), IsStarConvexSet R x (s i)
⊢ ∀ s_1 ∈ range fun i ↦ s i, IsStarConvexSet R x s_1

Tactic:
by simpa

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
ι : Sort u_7
s : ι → Set X
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
hs' : ∀ (i : ι), IsConvexSet R (s i)
⊢ ∀ s_1 ∈ range fun i ↦ s i, IsConvexSet R s_1

Tactic:
by simpa

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set Y
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R X
hw : ↑w.weights.support ⊆ f ⁻¹' s
x : X
hx : w.weights x ≠ 0
⊢ x ∈ ↑w.weights.support

Tactic:
by simpa

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
I : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
s : StdSimplex R I
f : I → P
p : P := ⋯.some
this : ((Finsupp.mapDomain f s.weights).sum fun x r ↦ r • (x -ᵥ p)) = s.weights.sum fun x r ↦ r • (f x -ᵥ p)
⊢ (((StdSimplex.map f s).weights.support.weightedVSubOfPoint id p) fun i ↦
        (fun x r ↦ r) i ((StdSimplex.map f s).weights i)) +ᵥ
      p =
    ((s.weights.support.weightedVSubOfPoint f p) fun i ↦ (fun x r ↦ r) i (s.weights i)) +ᵥ p

Tactic:
by simpa

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: K : Type u_4
X : Type u_5
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t✝ : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄, ↑t ⊆ s → t = w.weights.support → sConvexComb w ∈ s
w : StdSimplex K X
hw : ↑(Finset.cons x t hx) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : w.weights x ≠ 0
hwx' : ∃ y, y ≠ x ∧ w.weights y ≠ 0
⊢ ∃ x_1 ∈ {x}, w.weights x_1 ≠ 0

Tactic:
by simpa

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : ∑ e ∈ s, w e • f e = 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0
hI : 0 < ∑ i ∈ I, w i
⊢ ∑ i ∈ J, w i • f i + ∑ i ∈ I, w i • f i = 0

Tactic:
by
    simpa only [← h_vsum, not_lt] using sum_filter_add_sum_filter_not s (fun i ↦ w i < 0) _

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

Goal state before:
pp: I : Type u_1
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x : X
f : StdSimplex ℝ I
g : I → X
⊢ dist x (iConvexComb f g) ≤ iConvexComb f fun i ↦ dist x (g i)

Tactic:
by
  simpa using dist_iConvexComb_le f (fun _ ↦ x) g

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: F : Type u_1
R : Type u_2
M : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : IsStrictOrderedRing R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : SetLike F M
inst✝³ : AddSubmonoidClass F M
inst✝² : SMulMemClass F R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
S : F
w : StdSimplex R M
hw : ↑w.weights.support ⊆ ↑S
m : M
hm : w.weights m ≠ 0
⊢ m ∈ ↑w.weights.support

Tactic:
by simpa

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x : M
s : Set M
hs : IsStarConvexSet R x s
⊢ IsStarConvexSet R (-x) (-s)

Tactic:
by
  rw [← Set.image_neg_eq_neg]; exact hs.image (by fun_prop)

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
h_nonempty : Nonempty ι
I : Finset ι
⊢ (⋂ i ∈ I, F i).Nonempty

Tactic:
apply helly_theorem' (s := I) (𝕜 := 𝕜) (by simp [h_convex])

Goal state after:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
h_nonempty : Nonempty ι
I : Finset ι
⊢ ∀ I_1 ⊆ I, #I_1 ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I_1, F i).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case refine_2
V : Type u
inst✝¹ : Fintype V
inst✝ : DecidableEq V
Adj : V → V → Prop
hs : Std.Symm Adj
hi : Std.Irrefl Adj
⊢ ∀ (x : V), (fun v w ↦ decide (Adj v w)) x x = false

pp: case refine_3
V : Type u
inst✝¹ : Fintype V
inst✝ : DecidableEq V
Adj : V → V → Prop
hs : Std.Symm Adj
hi : Std.Irrefl Adj
⊢ SimpleGraph.mk' ⟨fun v w ↦ decide (Adj v w), ⋯⟩ = { Adj := Adj, symm := hs, loopless := hi }

Tactic:
· intro v; simp [hi.irrefl v]

Goal state after:
case refine_3
V : Type u
inst✝¹ : Fintype V
inst✝ : DecidableEq V
Adj : V → V → Prop
hs : Std.Symm Adj
hi : Std.Irrefl Adj
⊢ SimpleGraph.mk' ⟨fun v w ↦ decide (Adj v w), ⋯⟩ = { Adj := Adj, symm := hs, loopless := hi }
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
x✝ : G.Adj v w
⊢ s(v, w) ∈ G.edgeSet ∧ v ∈ s(v, w) ∧ w ∈ s(v, w)

Tactic:
by simpa

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
h : G.IsUniversal v
⊢ Gᶜᶜ.IsUniversal v

Tactic:
by simpa

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

Goal state before:
pp: E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
r : ℝ
x y : PE
hxy : dist x y = r * dist x x
hyz : dist y x = (1 - r) * dist x x
this : y -ᵥ x ∈ [0 -[ℝ] x -ᵥ x]
⊢ y = x

Tactic:
by simpa

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

Goal state before:
pp: case inr.refine_2
𝕜 : 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
⊢ (w i)⁻¹ < (1 - ε) / ε + (w i)⁻¹

Tactic:
· exact lt_add_of_pos_left _ <| by positivity

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

Goal state before:
pp: V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
s : Set V
x : V
hx : x ∉ (convexHull ℝ) s
ι : Type
w✝ : Fintype ι
w : ι → ℝ
a : ι → V
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i, w i = 1
ha : ∀ (i : ι), a i ∈ s
hy : ∑ i, w i • a i ∈ (convexHull ℝ) s
hxy : IsVisible ℝ ((convexHull ℝ) s) x (∑ i, w i • a i)
i : ι
hi : i ∈ {i | w i ≠ 0}
⊢ ∀ i ∈ Finset.univ, a i ∈ s

Tactic:
by simpa

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

Goal state before:
pp: V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
x : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed[inst✝²] ((convexHull ℝ) s)
hx : x ∉ (convexHull ℝ) s
⊢ -x +ᵥ ↑(affineSpan ℝ ({x} ∪ {y | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y})) =
    ↑(span ℝ (-x +ᵥ {y | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y}))

Tactic:
simp [← AffineSubspace.coe_pointwise_vadd, AffineSubspace.pointwise_vadd_span,
        vadd_set_insert, affineSpan_insert_zero]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
this : 0 ≤ (‖x‖ - 1) ^ 2
⊢ 1 + ‖x‖ ≤ √(2 * (1 + ‖x‖ ^ 2))

Tactic:
apply le_sqrt_of_sq_le

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
this : 0 ≤ (‖x‖ - 1) ^ 2
⊢ (1 + ‖x‖) ^ 2 ≤ 2 * (1 + ‖x‖ ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 1 < t
⊢ t ^ (-r⁻¹) - 1 < 0

Tactic:
sub_neg

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 1 < t
⊢ t ^ (-r⁻¹) < 1
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[volume.restrict (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[volume.restrict (Ioc 0 t)] G
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
have G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t := by
    refine fun t t_pos => ⟨(g_intble t t_pos).1.congr_fun_ae (g_eq_G_on t), ?_⟩
    rw [Ioc_eq_empty_of_le t_pos.lt.le]
    exact integrableOn_empty

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[volume.restrict (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[volume.restrict (Ioc 0 t)] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
⊢ T.rayleighQuotient '' {0}ᶜ = T.rayleighQuotient '' sphere 0 r

Tactic:
ext a
  constructor
  · rintro ⟨x, hx : x ≠ 0, hxT⟩
    let c : 𝕜 := ‖x‖⁻¹ * r
    have : c ≠ 0 := by simp [c, hx, hr.ne']
    refine ⟨c • x, ?_, ?_⟩
    · simp [field, c, norm_smul, abs_of_pos hr]
    · rw [T.rayleigh_smul x this]
      exact hxT
  · rintro ⟨x, hx, hxT⟩
    exact ⟨x, ne_zero_of_mem_sphere hr.ne' ⟨x, hx⟩, hxT⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
⊢ ‖⟪T x, x⟫_𝕜‖ / ‖x‖ ^ 2 ≤ ‖T‖

Tactic:
norm_inner_le_norm,

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
⊢ ‖T x‖ * ‖x‖ / ‖x‖ ^ 2 ≤ ‖T‖
Module: Mathlib.Analysis.Distribution.TestFunction

Goal state before:
pp: E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
m : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
f : 𝓓^{n}(Ω, F)
H : IntegrableOn (fun x ↦ 1) (tsupport ⇑f) μ
this : IntegrableOn (⇑(1 • f)) (tsupport ⇑f) μ
⊢ IntegrableOn (⇑f) (tsupport ⇑f) μ

Tactic:
by simpa

Goal state after:
Module: Mathlib.Analysis.Distribution.TestFunction

Goal state before:
pp: case pos
𝕜 : Type u_1
𝕂 : Type u_2
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
F' : Type u_5
inst✝¹⁴ : NormedAddCommGroup F'
inst✝¹³ : NormedSpace ℝ F'
inst✝¹² : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
m : MeasurableSpace E
inst✝¹¹ : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst✝¹⁰ : NormedAddCommGroup F₁
inst✝⁹ : NormedSpace 𝕜 F₁
inst✝⁸ : NormedSpace ℝ F₁
inst✝⁷ : NormedAddCommGroup F₂
inst✝⁶ : NormedSpace 𝕜 F₂
inst✝⁵ : NormedAddCommGroup F₃
inst✝⁴ : NormedSpace 𝕜 F₃
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : IsScalarTower ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
K : Compacts E
K_sub_Ω : ↑K ⊆ ↑Ω
f : 𝓓^{n}_{K}(E, F₁)
h : LocallyIntegrableOn φ (↑Ω) μ
⊢ ∫ (x : E), (B ((ofSupportedIn K_sub_Ω f) x)) (φ x) ∂μ = (ContDiffMapSupportedIn.integralAgainstBilinCLM B μ φ) f

Tactic:
simp [h.integrableOn_compact_subset K_sub_Ω K.2]

Goal state after:
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
⊢ ∫ (x : E), ‖x‖ ^ k * ‖f x‖ ∂μ ≤ (2 ^ μ.integrablePower * ∫ (x : E), (1 + ‖x‖) ^ (-↑μ.integrablePower) ∂μ) * (C₁ + C₂)

Tactic:
← integral_const_mul,

Goal state after:
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
⊢ ∫ (x : E), ‖x‖ ^ k * ‖f x‖ ∂μ ≤ (∫ (a : E), 2 ^ μ.integrablePower * (1 + ‖a‖) ^ (-↑μ.integrablePower) ∂μ) * (C₁ + C₂)
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‖
⊢ ‖(T - μ • 1) (η • x)‖ < ε

Tactic:
map_smul,

Goal state after:
𝕜 : 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‖
⊢ ‖η • (T - μ • 1) x‖ < ε
Module: Mathlib.Data.Fin.Tuple.Sort

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : Monotone (f ∘ ⇑σ) ∧ ∀ (i j : Fin n), i < j → f (σ i) = f (σ j) → σ i < σ j
i j : Fin n
hij : i < j
⊢ (Equiv.trans σ (graphEquiv₁ f)) i < (Equiv.trans σ (graphEquiv₁ f)) j

Tactic:
obtain he | hl := (h.1 hij.le).eq_or_lt <;> apply Prod.Lex.toLex_lt_toLex.2

Goal state after:
case refine_2.inl
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : Monotone (f ∘ ⇑σ) ∧ ∀ (i j : Fin n), i < j → f (σ i) = f (σ j) → σ i < σ j
i j : Fin n
hij : i < j
he : (f ∘ ⇑σ) i = (f ∘ ⇑σ) j
⊢ (f (σ i), σ i).1 < (f (σ j), σ j).1 ∨ (f (σ i), σ i).1 = (f (σ j), σ j).1 ∧ (f (σ i), σ i).2 < (f (σ j), σ j).2

case refine_2.inr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : Monotone (f ∘ ⇑σ) ∧ ∀ (i j : Fin n), i < j → f (σ i) = f (σ j) → σ i < σ j
i j : Fin n
hij : i < j
hl : (f ∘ ⇑σ) i < (f ∘ ⇑σ) j
⊢ (f (σ i), σ i).1 < (f (σ j), σ j).1 ∨ (f (σ i), σ i).1 = (f (σ j), σ j).1 ∧ (f (σ i), σ i).2 < (f (σ j), σ j).2
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, T (w.ofLp x • (hT.eigenvectorBasis hn) x) = ∑ x, (↑(hT.eigenvalues hn x) * w.ofLp x) • (hT.eigenvectorBasis hn) x

Tactic:
map_smul,

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)
⊢ ∑ x, w.ofLp x • T ((hT.eigenvectorBasis hn) x) = ∑ x, (↑(hT.eigenvalues hn x) * w.ofLp x) • (hT.eigenvectorBasis hn) x
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
X : Type u_5
inst✝ : TopologicalSpace X
φ : X → 𝓓^{n}_{K}(E, F)
⊢ (∀ (i : ℕ), Continuous[inst✝, _] (⇑(structureMapCLM ℝ n i) ∘ φ)) ↔
    ∀ (i : ℕ), ↑i ≤ n → Continuous[inst✝, _] (⇑(structureMapCLM ℝ n i) ∘ φ)

Tactic:
congrm (∀ i, ?_)

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
X : Type u_5
inst✝ : TopologicalSpace X
φ : X → 𝓓^{n}_{K}(E, F)
i : ℕ
⊢ Continuous[inst✝, _] (⇑(structureMapCLM ℝ n i) ∘ φ) ↔ ↑i ≤ n → Continuous[inst✝, _] (⇑(structureMapCLM ℝ n i) ∘ φ)
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Finite n
m : Type u_3
inst✝ : Finite m
x : Matrix n n 𝕜
y : Matrix m m 𝕜
hx : x.PosSemidef
hy : y.PosSemidef
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) x y).PosSemidef

Tactic:
have := Fintype.ofFinite n

Goal state after:
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Finite n
m : Type u_3
inst✝ : Finite m
x : Matrix n n 𝕜
y : Matrix m m 𝕜
hx : x.PosSemidef
hy : y.PosSemidef
this : Fintype n
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) x y).PosSemidef
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Finite n
m : Type u_3
inst✝ : Finite m
x : Matrix n n 𝕜
y : Matrix m m 𝕜
hx : x.PosDef
hy : y.PosDef
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) x y).PosDef

Tactic:
have := Fintype.ofFinite n

Goal state after:
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Finite n
m : Type u_3
inst✝ : Finite m
x : Matrix n n 𝕜
y : Matrix m m 𝕜
hx : x.PosDef
hy : y.PosDef
this : Fintype n
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) x y).PosDef
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
hAs : (A.submatrix Subtype.val Subtype.val).PosDef
hBs : (B.submatrix Subtype.val Subtype.val).PosDef
y : ↥x.support → 𝕜
hy : y ≠ 0
⊢ (diagonal y).vec ≠ 0

Tactic:
by simpa

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

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Finite n
v : n → E
⊢ (gram 𝕜 v).PosSemidef

Tactic:
have := Fintype.ofFinite n

Goal state after:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Finite n
v : n → E
this : Fintype n
⊢ (gram 𝕜 v).PosSemidef
Module: Mathlib.Analysis.InnerProductSpace.GramMatrix

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Finite n
v : n → E
h_gram : (gram 𝕜 v).PosDef
⊢ LinearIndependent 𝕜 v

Tactic:
have := Fintype.ofFinite n

Goal state after:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Finite n
v : n → E
h_gram : (gram 𝕜 v).PosDef
this : Fintype n
⊢ LinearIndependent 𝕜 v