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

Goal state before:
pp: case neg.inl
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 0
⊢ Filter.Tendsto (fun i ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) (nhds t) (nhds (y t))

Tactic:
rw [Metric.nhds_basis_ball.tendsto_right_iff]

Goal state after:
case neg.inl
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 0
⊢ ∀ (i : ℝ),
    0 < i → ∀ᶠ (x_1 : T) in nhds t, convexCombPair (f x_1) (1 - f x_1) ⋯ ⋯ ⋯ (x x_1) (y x_1) ∈ Metric.ball (y t) i
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: case neg.inr
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
⊢ Filter.Tendsto (fun i ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)) (nhds t) (nhds (x t))

Tactic:
rw [Metric.nhds_basis_ball.tendsto_right_iff]

Goal state after:
case neg.inr
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
⊢ ∀ (i : ℝ),
    0 < i → ∀ᶠ (x_1 : T) in nhds t, convexCombPair (f x_1) (1 - f x_1) ⋯ ⋯ ⋯ (x x_1) (y x_1) ∈ Metric.ball (x t) i
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_card : finrank 𝕜 E + 1 ≤ #F
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ (⋂₀ ↑F).Nonempty

Tactic:
apply helly_theorem_set' h_convex

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_card : finrank 𝕜 E + 1 ≤ #F
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
a : V
h : G.Adj a a
⊢ False

Tactic:
exact G.irrefl h

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✝ : Subsingleton V
G : SimpleGraph V
⊢ G = ⊥

Tactic:
by ext a b; have := Subsingleton.elim a b; simp [this]

Goal state after:
Module: Mathlib.Analysis.Convex.Strict.Extreme

Goal state before:
pp: A : Type u_1
inst✝² : NormedAddCommGroup A
inst✝¹ : NormedSpace ℝ A
inst✝ : StrictConvexSpace ℝ A
a : A
r : ℝ
hr : r ≠ 0
x✝ : A
hx : x✝ ∈ sphere a r
⊢ x✝ ∈ extremePoints ℝ (closedBall a r)

Tactic:
rw [← frontier_closedBall _ hr, frontier, closure_closedBall] at hx
  exact (_root_.strictConvex_closedBall ℝ _ _).sdiff_interior_subset_extremePoints hx

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
⊢ G.incidenceSet v ∩ G.incidenceSet (Sym2.Mem.other h) = {e}

Tactic:
ext e'
  simp only [incidenceSet, Set.mem_sep_iff, Set.mem_inter_iff, Set.mem_singleton_iff]
  refine ⟨fun h' => ?_, ?_⟩
  · rw [← Sym2.other_spec h]
    exact (Sym2.mem_and_mem_iff (edge_other_ne G he h).symm).mp ⟨h'.1.2, h'.2.2⟩
  · rintro rfl
    exact ⟨⟨he, h⟩, he, Sym2.other_mem _⟩

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
⊢ dist a c < dist a b + dist b c ↔ ¬Wbtw ℝ a b c

Tactic:
by
  rw [← ne_iff_lt_iff_le.mpr (dist_triangle _ _ _), not_iff_not, eq_comm, dist_add_dist_eq_iff]

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedRing 𝕜
inst✝² : AddCommGroup V
inst✝¹ : Module 𝕜 V
inst✝ : AddTorsor V P
s : Set P
x : P
⊢ IsVisible 𝕜 s x x

Tactic:
by simp [IsVisible]

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 | s.SSameSide x y} = Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) ↑s

Tactic:
by
  ext y
  simp_rw [Set.mem_ofPred, Set.mem_image2, Set.mem_Ioi]
  constructor
  · rw [sSameSide_iff_exists_left hp]
    rintro ⟨-, hy, p₂, hp₂, h | h | ⟨r₁, r₂, hr₁, hr₂, h⟩⟩
    · rw [vsub_eq_zero_iff_eq] at h
      exact False.elim (hx (h.symm ▸ hp))
    · rw [vsub_eq_zero_iff_eq] at h
      exact False.elim (hy (h.symm ▸ hp₂))
    · refine ⟨r₁ / r₂, div_pos hr₁ hr₂, p₂, hp₂, ?_⟩
      rw [div_eq_inv_mul, ← smul_smul, h, smul_smul, inv_mul_cancel₀ hr₂.ne.symm, one_smul,
        vsub_vadd]
  · rintro ⟨t, ht, p', hp', rfl⟩
    exact sSameSide_smul_vsub_vadd_right hx hp hp' ht

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✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
j : Fin (n + 1)
hj : j ≠ i
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).WSameSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)

Tactic:
have hj' : s.points j ∈ affineSpan R (Set.range (s.faceOpposite i).points) := by
    simpa using hj

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✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
j : Fin (n + 1)
hj : j ≠ i
hj' : s.points j ∈ affineSpan R (Set.range (s.faceOpposite i).points)
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).WSameSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: α : Type u_1
𝕜' : Type u_2
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁹ : NormedRing 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : IsBoundedSMul 𝕜 E
inst✝⁵ : NormedRing 𝕜'
inst✝⁴ : Module 𝕜' E
inst✝³ : Module 𝕜' 𝕜
inst✝² : IsBoundedSMul 𝕜' E
inst✝¹ : IsBoundedSMul 𝕜' 𝕜
inst✝ : IsScalarTower 𝕜' 𝕜 E
c : 𝕜'
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ (c • f) • g = c • f • g

Tactic:
simp only [smul_def, ← MemLp.toLp_const_smul]

Goal state after:
α : Type u_1
𝕜' : Type u_2
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁹ : NormedRing 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : IsBoundedSMul 𝕜 E
inst✝⁵ : NormedRing 𝕜'
inst✝⁴ : Module 𝕜' E
inst✝³ : Module 𝕜' 𝕜
inst✝² : IsBoundedSMul 𝕜' E
inst✝¹ : IsBoundedSMul 𝕜' 𝕜
inst✝ : IsScalarTower 𝕜' 𝕜 E
c : 𝕜'
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ MemLp.toLp (↑↑(c • f) • ↑↑g) ⋯ = MemLp.toLp (c • ↑↑f • ↑↑g) ⋯
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: α : Type u_1
𝕜' : Type u_2
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁹ : NormedRing 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : IsBoundedSMul 𝕜 E
inst✝⁵ : NormedRing 𝕜'
inst✝⁴ : Module 𝕜' E
inst✝³ : Module 𝕜' 𝕜
inst✝² : IsBoundedSMul 𝕜' E
inst✝¹ : IsBoundedSMul 𝕜' 𝕜
inst✝ : SMulCommClass 𝕜' 𝕜 E
c : 𝕜'
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ c • f • g = f • c • g

Tactic:
simp only [smul_def, ← MemLp.toLp_const_smul]

Goal state after:
α : Type u_1
𝕜' : Type u_2
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁹ : NormedRing 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : IsBoundedSMul 𝕜 E
inst✝⁵ : NormedRing 𝕜'
inst✝⁴ : Module 𝕜' E
inst✝³ : Module 𝕜' 𝕜
inst✝² : IsBoundedSMul 𝕜' E
inst✝¹ : IsBoundedSMul 𝕜' 𝕜
inst✝ : SMulCommClass 𝕜' 𝕜 E
c : 𝕜'
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ MemLp.toLp (c • ↑↑f • ↑↑g) ⋯ = MemLp.toLp (↑↑f • ↑↑(c • g)) ⋯
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
s : ℝ
s_pos : s > 0
hs : 0 < ∫ (x : ℝ) in Ioc 0 s, g x ∂volume
h's : μ {a | s < f a} = ∞
A : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ∞
⊢ ∞ = ENNReal.ofReal (∫ (t : ℝ) in 0..s, g t) * ∞

Tactic:
rw [ENNReal.mul_top]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
s : ℝ
s_pos : s > 0
hs : 0 < ∫ (x : ℝ) in Ioc 0 s, g x ∂volume
h's : μ {a | s < f a} = ∞
A : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ∞
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..s, g t) ≠ 0
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
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
ω : α
hω : f ω = AEMeasurable.mk f f_mble ω
h'ω : 0 ω ≤ f ω
⊢ f ω = max (AEMeasurable.mk f f_mble ω) 0

Tactic:
rw [← hω]

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
ω : α
hω : f ω = AEMeasurable.mk f f_mble ω
h'ω : 0 ω ≤ f ω
⊢ f ω = max (f ω) 0
Module: Mathlib.Analysis.Distribution.TestFunction

Goal state before:
pp: 𝕜 : 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 : ℕ∞
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
toFun : 𝓓^{n}(Ω, F) → V
T : (K : Compacts E) → ↑K ⊆ ↑Ω → 𝓓^{n}_{K}(E, F) →L[𝕜] V
toFun_eq_T :
  ∀ (K : Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω) (f : 𝓓^{n}_{K}(E, F)), toFun (ofSupportedIn K_sub_Ω f) = (T K K_sub_Ω) f
f g : 𝓓^{n}(Ω, F)
K : Compacts E := { carrier := tsupport ⇑f ∪ tsupport ⇑g, isCompact' := ⋯ }
K_sub_Ω : ↑K ⊆ ↑Ω
f_K : 𝓓^{n}_{K}(E, F) := ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
g_K : 𝓓^{n}_{K}(E, F) := ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
⊢ toFun (ofSupportedIn K_sub_Ω (f_K + g_K)) = toFun (ofSupportedIn K_sub_Ω f_K) + toFun (ofSupportedIn K_sub_Ω g_K)

Tactic:
simp [toFun_eq_T]

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

Goal state before:
pp: 𝕜 : 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 : ℕ∞
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
toFun : 𝓓^{n}(Ω, F) → V
T : (K : Compacts E) → ↑K ⊆ ↑Ω → 𝓓^{n}_{K}(E, F) →L[𝕜] V
toFun_eq_T :
  ∀ (K : Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω) (f : 𝓓^{n}_{K}(E, F)), toFun (ofSupportedIn K_sub_Ω f) = (T K K_sub_Ω) f
toFun_add : ∀ (f g : 𝓓^{n}(Ω, F)), toFun (f + g) = toFun f + toFun g
c : 𝕜
f : 𝓓^{n}(Ω, F)
K : Compacts E := { carrier := tsupport ⇑f, isCompact' := ⋯ }
K_sub_Ω : ↑K ⊆ ↑Ω
f_K : 𝓓^{n}_{K}(E, F) := ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
⊢ toFun (ofSupportedIn K_sub_Ω (c • f_K)) = c • toFun (ofSupportedIn K_sub_Ω f_K)

Tactic:
simp [toFun_eq_T]

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
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : x₀ ∈ sphere 0 ‖x₀‖
⊢ ⨅ x, T.rayleighQuotient ↑x = T.rayleighQuotient x₀

Tactic:
refine IsMinOn.iInf_eq hx₀'' ?_

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : x₀ ∈ sphere 0 ‖x₀‖
⊢ IsMinOn T.rayleighQuotient (sphere 0 ‖x₀‖) x₀
Module: Mathlib.Analysis.Normed.Operator.Compact.Basic

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : IsUniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
⊢ IsClosed[ContinuousLinearMap.topologicalSpace] {f | IsCompactOperator ⇑f}

Tactic:
refine isClosed_of_closure_subset ?_
  rintro u hu
  rw [mem_closure_iff_nhds_zero] at hu
  suffices TotallyBounded (u '' Metric.closedBall 0 1) by
    change IsCompactOperator (u : M₁ →ₛₗ[σ₁₂] M₂)
    rw [isCompactOperator_iff_isCompact_closure_image_closedBall (u : M₁ →ₛₗ[σ₁₂] M₂) zero_lt_one]
    exact this.closure.isCompact_of_isClosed isClosed_closure
  rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero]
  intro U hU
  rcases exists_nhds_zero_half hU with ⟨V, hV, hVU⟩
  let SV : Set M₁ × Set M₂ := ⟨closedBall 0 1, -V⟩
  rcases hu { f | ∀ x ∈ SV.1, f x ∈ SV.2 }
      (ContinuousLinearMap.hasBasis_nhds_zero.mem_of_mem
        ⟨NormedSpace.isVonNBounded_closedBall _ _ _, neg_mem_nhds_zero M₂ hV⟩) with
    ⟨v, hv, huv⟩
  rcases totallyBounded_iff_subset_finite_iUnion_nhds_zero.mp
      (hv.isCompact_closure_image_closedBall 1).totallyBounded V hV with
    ⟨T, hT, hTv⟩
  have hTv : v '' closedBall 0 1 ⊆ _ := subset_closure.trans hTv
  refine ⟨T, hT, ?_⟩
  rw [image_subset_iff, preimage_iUnion₂] at hTv ⊢
  intro x hx
  specialize hTv hx
  rw [mem_iUnion₂] at hTv ⊢
  rcases hTv with ⟨t, ht, htx⟩
  refine ⟨t, ht, ?_⟩
  rw [mem_preimage, mem_vadd_set_iff_neg_vadd_mem, vadd_eq_add, neg_add_eq_sub] at htx ⊢
  convert! hVU _ htx _ (huv x hx) using 1
  rw [sub_apply]
  abel

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
μ : 𝕜
inst✝ : CompleteSpace X
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T) μ
S : X →L[𝕜] X := T - μ • 1
K : NNReal
hK : AntilipschitzWith K ⇑S
h₂ : ¬Function.Surjective ⇑S
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range (↑S ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ}, m ≤ n → f n ∈ (↑S ^ m).range
n m : ℕ
h : m ≤ n
⊢ S (f n) ∈ (↑S ∘ₗ ↑S ^ m).range

Tactic:
LinearMap.range_comp

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
inst✝ : CompleteSpace X
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T) μ
S : X →L[𝕜] X := T - μ • 1
K : NNReal
hK : AntilipschitzWith K ⇑S
h₂ : ¬Function.Surjective ⇑S
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range (↑S ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ}, m ≤ n → f n ∈ (↑S ^ m).range
n m : ℕ
h : m ≤ n
⊢ S (f n) ∈ Submodule.map (↑S) (LinearMap.range (↑S ^ m))
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
i : n
⊢ hA.eigenvalues i = RCLike.re (star (hA.eigenvectorBasis i).ofLp ⬝ᵥ A *ᵥ (hA.eigenvectorBasis i).ofLp)

Tactic:
by
  rw [dotProduct_comm]
  simp only [mulVec_eigenvectorBasis, smul_dotProduct, ← EuclideanSpace.inner_eq_star_dotProduct,
    inner_self_eq_norm_sq_to_K, RCLike.smul_re, hA.eigenvectorBasis.orthonormal.1 i,
    mul_one, algebraMap.coe_one, one_pow, RCLike.one_re]

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
f : C(↑(spectrum ℝ A), ℝ)
⊢ ((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary)
      (diagonal (RCLike.ofReal ∘ ⇑(star f) ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩)) =
    star
      (((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary)
        (diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩)))

Tactic:
by
    simp only [star_trivial, ← map_star, star_eq_conjTranspose, diagonal_conjTranspose, Pi.star_def,
      Function.comp_apply, RCLike.star_def, RCLike.conj_ofReal]
    rfl

Goal state after:
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)
x : E
⊢ ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C ↔ x ∈ K → ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C

Tactic:
by_cases hx : x ∈ K

Goal state after:
case pos
𝕜 : 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)
x : E
hx : x ∈ K
⊢ ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C ↔ x ∈ K → ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C

case neg
𝕜 : 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)
x : E
hx : x ∉ K
⊢ ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C ↔ x ∈ K → ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
hf_int : ∀ (c : E), ∫ (x : α), ⟪c, f x⟫ ∂μ = 0
⊢ ∫ (x : α), f x ∂μ = 0

Tactic:
specialize hf_int (∫ x, f x ∂μ); rwa [integral_inner hf, inner_self_eq_zero] at hf_int

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
inst✝ : CompleteSpace X
x : X
M : ℝ
hM : ∀ x_1 ∈ Set.range fun n ↦ (b.proj n) x, ‖x_1‖ ≤ M
⊢ ∃ C, ∀ (i : ℕ), ‖(b.proj i) x‖ ≤ C

Tactic:
exact ⟨M, Set.forall_mem_range.mp hM⟩

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

Goal state before:
pp: case neg.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
i j : ℕ
x : X
h : ¬i = j
h' : i > j
⊢ (P (j + 1)) x - (P (min i (j + 1))) x - ((P (min (i + 1) j)) x - (P j) x) = 0

Tactic:
min_eq_right (Nat.succ_le_of_lt h'),

Goal state after:
case neg.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
i j : ℕ
x : X
h : ¬i = j
h' : i > j
⊢ (P (j + 1)) x - (P j.succ) x - ((P (min (i + 1) j)) x - (P j) x) = 0
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g, ∫⁻ (x : α), ‖f x - g x‖ₑ ∂μ ≤ ε ∧ Integrable (⇑g) μ

Tactic:
simp only [← memLp_one_iff_integrable, ← eLpNorm_one_eq_lintegral_enorm] at hf ⊢
  exact hf.exists_boundedContinuous_eLpNorm_sub_le ENNReal.one_ne_top hε

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : AddCircle T → E
⊢ ∫ (t : AddCircle T), f t ∂haarAddCircle = T⁻¹ • T • ∫ (x : AddCircle T), f x ∂haarAddCircle

Tactic:
inv_smul_smul₀ hT.out.ne'

Goal state after:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : AddCircle T → E
⊢ ∫ (t : AddCircle T), f t ∂haarAddCircle = ∫ (x : AddCircle T), f x ∂haarAddCircle