mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G₁ G₂ : SimpleGraph V
⊢ (G₁ ⊔ G₂).edgeSet = G₁.edgeSet ∪ G₂.edgeSet

Tactic:
ext ⟨x, y⟩
  rfl

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

Goal state before:
pp: V : Type u
G₁ G₂ : SimpleGraph V
⊢ (G₁ ⊓ G₂).edgeSet = G₁.edgeSet ∩ G₂.edgeSet

Tactic:
ext ⟨x, y⟩
  rfl

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

Goal state before:
pp: V : Type u
G₁ G₂ : SimpleGraph V
⊢ (G₁ \ G₂).edgeSet = G₁.edgeSet \ G₂.edgeSet

Tactic:
ext ⟨x, y⟩
  rfl

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow

Goal state before:
pp: p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
h₁ : StrictConvexOn ℝ≥0 univ ⇑f
h₂ : ∀ (x : ℝ≥0), f.symm x = x ^ p
x : ℝ≥0
mx : x ∈ univ
y : ℝ≥0
my : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • (fun x ↦ x ^ p) x + b • (fun x ↦ x ^ p) y < (fun x ↦ x ^ p) (a • x + b • y)

Tactic:
simp only [← h₂]

Goal state after:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
h₁ : StrictConvexOn ℝ≥0 univ ⇑f
h₂ : ∀ (x : ℝ≥0), f.symm x = x ^ p
x : ℝ≥0
mx : x ∈ univ
y : ℝ≥0
my : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f.symm x + b • f.symm y < f.symm (a • x + b • y)
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ G.neighborSet v ∪ Gᶜ.neighborSet v = {v}ᶜ

Tactic:
by
  ext w
  have h := @ne_of_adj _ G
  simp_rw [Set.mem_union, mem_neighborSet, compl_adj, Set.mem_compl_iff, Set.mem_singleton_iff]
  tauto

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G = ⊤ ↔ ∀ (v : V), G.IsUniversal v

Tactic:
simp [eq_top_iff_forall_ne_adj, IsUniversal]

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

Goal state before:
pp: case mp
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
⊢ s.WSameSide x y → x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

pp: case mpr
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
⊢ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) → s.WSameSide x y

Tactic:
· rintro ⟨p₁', hp₁', p₂', hp₂', h0 | h0 | ⟨r₁, r₂, hr₁, hr₂, hr⟩⟩
    · rw [vsub_eq_zero_iff_eq] at h0
      rw [h0]
      exact Or.inl hp₁'
    · refine Or.inr ⟨p₂', hp₂', ?_⟩
      rw [h0]
      exact SameRay.zero_right _
    · refine Or.inr ⟨(r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂', s.smul_vsub_vadd_mem _ h hp₁' hp₂',
        Or.inr (Or.inr ⟨r₁, r₂, hr₁, hr₂, ?_⟩)⟩
      rw [vsub_vadd_eq_vsub_sub, smul_sub, ← hr, smul_smul, mul_div_cancel₀ _ hr₂.ne.symm,
        ← smul_sub, vsub_sub_vsub_cancel_right]

Goal state after:
case mpr
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
⊢ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) → s.WSameSide x y
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
this : dist a b + dist b c = dist a c ↔ b -ᵥ a ∈ affineSegment ℝ (a -ᵥ a) (c -ᵥ a)
⊢ dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c

Tactic:
← affineSegment_vsub_const_image

Goal state after:
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
this : dist a b + dist b c = dist a c ↔ b -ᵥ a ∈ (fun x ↦ x -ᵥ a) '' affineSegment ℝ a c
⊢ dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c
Module: Mathlib.Analysis.Convex.StoneSeparation

Goal state before:
pp: case inr.inr.refine_4
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
⊢ (az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q) ∈
    (convexHull 𝕜) {p, q, az • x + bz • y}

Tactic:
classical
    let w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
    let z : Fin 3 → E := ![p, q, az • x + bz • y]
    have hw₀ : ∀ i, 0 ≤ w i := by
      rintro i
      fin_cases i
      · exact mul_nonneg (mul_nonneg haz hav) hbu
      · exact mul_nonneg (mul_nonneg hbz hau) hbv
      · exact mul_nonneg hau hav
    have hw : ∑ i, w i = az * av + bz * au := by
      trans az * av * bu + (bz * au * bv + au * av)
      · simp [w, Fin.sum_univ_succ]
      linear_combination (au * bv - 1 * au) * habz + (-(1 * az * au) + au) * habv + az * av * habu
    have hz : ∀ i, z i ∈ ({p, q, az • x + bz • y} : Set E) := fun i => by fin_cases i <;> simp [z]
    convert!
      (Finset.centerMass_mem_convexHull (Finset.univ : Finset (Fin 3)) (fun i _ => hw₀ i)
          (by rwa [hw]) fun i _ => hz i :
        Finset.univ.centerMass w z ∈ _)
    rw [Finset.centerMass, hw]
    trans (az * av + bz * au)⁻¹ •
      ((az * av * bu) • p + ((bz * au * bv) • q + (au * av) • (az • x + bz • y)))
    · module
    congr 3
    simp [w, z]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
a b m : ℝ
x y : E
f : E → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * (f x - m / 2 * ‖x‖ ^ 2) + b * (f y - m / 2 * ‖y‖ ^ 2) +
      m / 2 * (‖a • x‖ ^ 2 + 2 * inner ℝ (a • x) (b • y) + ‖b • y‖ ^ 2) =
    a * f x + b * f y - m / 2 * a * b * ‖x - y‖ ^ 2

Tactic:
norm_sub_sq_real,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
a b m : ℝ
x y : E
f : E → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * (f x - m / 2 * ‖x‖ ^ 2) + b * (f y - m / 2 * ‖y‖ ^ 2) +
      m / 2 * (‖a • x‖ ^ 2 + 2 * inner ℝ (a • x) (b • y) + ‖b • y‖ ^ 2) =
    a * f x + b * f y - m / 2 * a * b * (‖x‖ ^ 2 - 2 * inner ℝ x y + ‖y‖ ^ 2)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: 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
⊢ IsPreconnected {y | s.WOppSide x y}

Tactic:
by
  rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)
  · rw [coe_eq_bot_iff] at h
    simp only [h, not_wOppSide_bot]
    exact isPreconnected_empty
  · exact (isConnected_setOfPred_wOppSide x h).isPreconnected

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

Goal state before:
pp: α : Type u_1
𝕜 : 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✝¹ : MulActionWithZero 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ (eLpNorm (↑↑(f • g)) r μ).toReal ≤ (eLpNorm (↑↑f) p μ * eLpNorm (↑↑g) q μ).toReal

Tactic:
refine ENNReal.toReal_mono (by finiteness) ?_

Goal state after:
α : Type u_1
𝕜 : 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✝¹ : MulActionWithZero 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ eLpNorm (↑↑(f • g)) r μ ≤ eLpNorm (↑↑f) p μ * eLpNorm (↑↑g) q μ
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case refine_1.inl
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)
h :
  (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)
⊢ False

Tactic:
exact (s.sSameSide_affineSpan_faceOpposite_of_sign_eq hw₁ hw₂ hs h0).wSameSide.not_sOppSide h

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
x : E
f : 𝓓^{n}(Ω, ℝ)
⊢ (delta x) f = f x

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: case mk
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
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
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
⊢ Function.uncurry (fun x y ↦ (Ioc 0 (f x)).indicator (fun t ↦ ENNReal.ofReal (g t)) y) (p_fst, p_snd) =
    {p | p.2 ∈ Ioc 0 (f p.1)}.indicator (fun p ↦ ENNReal.ofReal (g p.2)) (p_fst, p_snd)

Tactic:
| mk p_fst p_snd =>

Goal state after:
case mk
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
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
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
⊢ Function.uncurry (fun x y ↦ (Ioc 0 (f x)).indicator (fun t ↦ ENNReal.ofReal (g t)) y) (p_fst, p_snd) =
    {p | p.2 ∈ Ioc 0 (f p.1)}.indicator (fun p ↦ ENNReal.ofReal (g p.2)) (p_fst, p_snd)
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
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
obtain ⟨F, F_mble, F_nn, f_eq_F⟩ : ∃ F : α → ℝ, Measurable F ∧ 0 ≤ F ∧ f =ᵐ[μ] F := by
    refine ⟨fun ω ↦ max (f_mble.mk f ω) 0, f_mble.measurable_mk.max measurable_const,
        fun ω ↦ le_max_right _ _, ?_⟩
    filter_upwards [f_mble.ae_eq_mk, f_nn] with ω hω h'ω
    rw [← hω]
    exact (max_eq_left h'ω).symm

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
F : α → ℝ
F_mble : Measurable F
F_nn : 0 ≤ F
f_eq_F : f =ᵐ[μ] F
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
cst : ℝ → ℝ := fun x ↦ 1
cst_intble : ∀ t > 0, IntervalIntegrable cst volume 0 t
key : ∫⁻ (ω : α), ENNReal.ofReal (∫ (x : ℝ) in 0..f ω, 1) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a}
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a}

Tactic:
rw [← key]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
cst : ℝ → ℝ := fun x ↦ 1
cst_intble : ∀ t > 0, IntervalIntegrable cst volume 0 t
key : ∫⁻ (ω : α), ENNReal.ofReal (∫ (x : ℝ) in 0..f ω, 1) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a}
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (x : ℝ) in 0..f ω, 1) ∂μ
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
t : ℝ
ht : 0 < t
hT' : (algebraMap ℝ 𝕜) t ∈ resolventSet 𝕜 T
hT0 : ¬T = 0
c : ℝ
hc0 : c > 0
x : E
hc : (c * ‖x‖) ^ 2 ≤ ‖(algebraMap ℝ 𝕜) t • x‖ ^ 2 - 2 * re ⟪T x, (algebraMap ℝ 𝕜) t • x⟫_𝕜 + ‖T x‖ ^ 2
hx : ¬x = 0
⊢ re ⟪T x, x⟫_𝕜 / ‖x‖ ^ 2 ≤ (t ^ 2 + ‖T‖ ^ 2) / (2 * t) - c ^ 2 / (2 * t)

Tactic:
le_opNorm

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
t : ℝ
ht : 0 < t
hT' : (algebraMap ℝ 𝕜) t ∈ resolventSet 𝕜 T
hT0 : ¬T = 0
c : ℝ
hc0 : c > 0
x : E
hc : (c * ‖x‖) ^ 2 ≤ ‖(algebraMap ℝ 𝕜) t • x‖ ^ 2 - 2 * re ⟪T x, (algebraMap ℝ 𝕜) t • x⟫_𝕜 + (‖T‖ * ‖x‖) ^ 2
hx : ¬x = 0
⊢ re ⟪T x, x⟫_𝕜 / ‖x‖ ^ 2 ≤ (t ^ 2 + ‖T‖ ^ 2) / (2 * t) - c ^ 2 / (2 * t)
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‖
c : ℝ
hc₀ : c > 0
hc : ∀ ε > 0, ∃ x, ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ ‖(T - μ • 1) x‖ < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : ℕ → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), ‖(T - μ • 1) (x n)‖ < φ n
hx_lim : Tendsto (fun n ↦ (T - μ • 1) (x n)) atTop (𝓝 0)
y_ : ℕ → X := fun n ↦ T (x n)
hy_lower : ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
K : Set X
hK : IsCompact K
hK' : ⇑↑T '' Metric.closedBall 0 1 ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 y)
⊢ Tendsto (fun n ↦ (T - μ • 1) (y_ n)) atTop (𝓝 0)

Tactic:
simpa [Function.comp_def] using T.continuous.continuousAt.tendsto.comp hx_lim

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
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
f : C(↑(spectrum ℝ A), ℝ)
hf : ↑hA.cfcAux f = 0
h2 : diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩) = 0
i : n
hx : hA.eigenvalues i ∈ spectrum ℝ A
⊢ f ⟨hA.eigenvalues i, hx⟩ = 0

Tactic:
← diagonal_zero

Goal state after:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
f : C(↑(spectrum ℝ A), ℝ)
hf : ↑hA.cfcAux f = 0
h2 : diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩) = diagonal fun x ↦ 0
i : n
hx : hA.eigenvalues i ∈ spectrum ℝ A
⊢ f ⟨hA.eigenvalues i, hx⟩ = 0
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
hT : T.IsSymmetric
μ : 𝕜
hμ : HasEigenvalue T μ
⊢ (starRingEnd 𝕜) μ = μ

Tactic:
by
  obtain ⟨v, hv₁, hv₂⟩ := hμ.exists_hasEigenvector
  rw [mem_eigenspace_iff] at hv₁
  simpa [hv₂, inner_smul_left, inner_smul_right, hv₁] using hT v v

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
inst✝ : Nontrivial (Matrix n n 𝕜)
a : Matrix n n 𝕜
ha : IsSelfAdjoint a
⊢ (spectrum ℝ a).Nonempty

Tactic:
obtain (h | h) := isEmpty_or_nonempty n

Goal state after:
case inl
n : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
inst✝ : Nontrivial (Matrix n n 𝕜)
a : Matrix n n 𝕜
ha : IsSelfAdjoint a
h : IsEmpty n
⊢ (spectrum ℝ a).Nonempty

case inr
n : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
inst✝ : Nontrivial (Matrix n n 𝕜)
a : Matrix n n 𝕜
ha : IsSelfAdjoint a
h : Nonempty n
⊢ (spectrum ℝ a).Nonempty
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 : ℝ → ℝ
hA' : IsSelfAdjoint A
this : cfcHom hA' = hA.cfcAux
⊢ ContinuousOn f (spectrum ℝ A)

Tactic:
rw [continuousOn_iff_continuous_domRestrict]; fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : M.PosDef
x : Matrix n n 𝕜
hx : inner 𝕜 x x = 0
⊢ x = 0

Tactic:
obtain ⟨y, hy, rfl⟩ := CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self.mp
        hM.isStrictlyPositive

Goal state after:
𝕜 : Type u_1
n : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : Fintype n
x y : Matrix n n 𝕜
hy : IsUnit y
hM : (star y * y).PosDef
__spread✝⁻⁰ : PreInnerProductSpace.Core 𝕜 (Matrix n n 𝕜) := ⋯.matrixPreInnerProductSpace
hx : inner 𝕜 x x = 0
⊢ x = 0
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions

Goal state before:
pp: case e'_3
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SecondCountableTopologyEither α E
inst✝⁵ : CompactSpace α
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
this : Function.Surjective ⇑(linearIsometryBoundedOfCompact α E 𝕜)
⊢ ↑(Lp.boundedContinuousFunction E p μ) = Set.range ⇑(BoundedContinuousFunction.toLp p μ 𝕜)

Tactic:
← BoundedContinuousFunction.range_toLp p μ (𝕜 := 𝕜),

Goal state after:
case e'_3
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SecondCountableTopologyEither α E
inst✝⁵ : CompactSpace α
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
this : Function.Surjective ⇑(linearIsometryBoundedOfCompact α E 𝕜)
⊢ ↑(↑(BoundedContinuousFunction.toLp p μ 𝕜)).range.toAddSubgroup = Set.range ⇑(BoundedContinuousFunction.toLp p μ 𝕜)
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
x : α
⊢ ‖⟪↑↑f x, ↑↑g x⟫‖ ≤ ‖‖↑↑f x‖ ^ ↑2 + ‖↑↑g x‖ ^ ↑2‖

Tactic:
Real.rpow_natCast,

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
x : α
⊢ ‖⟪↑↑f x, ↑↑g x⟫‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ ↑2‖
Module: Mathlib.Geometry.Manifold.SmoothApprox

Goal state before:
pp: case neg
E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst✝⁴, _] ε
ε_pos : ∀ (x : M), 0 < ε x
S U : Set M
hS : IsClosed[inst✝⁴] S
hU : U ∈ 𝓝ˢ S
hfU : ContMDiffOn I 𝓘(ℝ, F) (↑n) f U
dist_f_f : ∀ (x : M), dist (f x) (f x) < ε x
t : M → Set F := fun x ↦ {y | dist y (f x) < ε x ∧ (x ∈ S → y = f x) ∧ (f x = 0 → y = 0)}
t_conv : ∀ (x : M), Convex ℝ (t x)
x : M
hx : x ∉ S
⊢ ∃ U ∈ 𝓝 x, ∃ g, ContMDiffOn I 𝓘(ℝ, F) (↑n) g U ∧ ∀ y ∈ U, g y ∈ t y

Tactic:
have : ∀ᶠ y in 𝓝 x, y ∉ S ∧ dist (f x) (f y) < ε y := (hS.isOpen_compl.eventually_mem hx).and
      ((continuous_const.dist f_cont).continuousAt.eventually_lt ε_cont.continuousAt (dist_f_f x))

Goal state after:
case neg
E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst✝⁴, _] ε
ε_pos : ∀ (x : M), 0 < ε x
S U : Set M
hS : IsClosed[inst✝⁴] S
hU : U ∈ 𝓝ˢ S
hfU : ContMDiffOn I 𝓘(ℝ, F) (↑n) f U
dist_f_f : ∀ (x : M), dist (f x) (f x) < ε x
t : M → Set F := fun x ↦ {y | dist y (f x) < ε x ∧ (x ∈ S → y = f x) ∧ (f x = 0 → y = 0)}
t_conv : ∀ (x : M), Convex ℝ (t x)
x : M
hx : x ∉ S
this : ∀ᶠ (y : M) in 𝓝 x, y ∉ S ∧ dist (f x) (f y) < ε y
⊢ ∃ U ∈ 𝓝 x, ∃ g, ContMDiffOn I 𝓘(ℝ, F) (↑n) g U ∧ ∀ y ∈ U, g y ∈ t y
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
inst✝¹ : RCLike 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
⊢ (fun a ↦ ⟪↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) a, ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) a⟫) =ᵐ[μ]
    fun a ↦ g a * (starRingEnd 𝕜) (f a)

Tactic:
have hf_ae := f.coeFn_toLp 2 μ 𝕜

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
inst✝¹ : RCLike 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᵐ[μ] ⇑f
⊢ (fun a ↦ ⟪↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) a, ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) a⟫) =ᵐ[μ]
    fun a ↦ g a * (starRingEnd 𝕜) (f a)
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝¹⁰ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝⁹ : NormedAddCommGroup F₁
inst✝⁸ : NormedSpace 𝕜 F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace 𝕜 F₃
inst✝² : SMulCommClass ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
⊢ (integralAgainstBilinLM B μ φ) f = if IntegrableOn φ (↑K) μ then ∫ (x : E), (B (f x)) (φ x) ∂μ else 0

Tactic:
by
  rfl

Goal state after: