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

Goal state before:
pp: 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 : ∀ ⦃x_1 : X⦄, x_1 ∈ Set.range x ∪ Set.range y → ∀ ⦃y_1 : X⦄, y_1 ∈ Set.range x ∪ Set.range y → dist x_1 y_1 ≤ D
hD' : 0 < D
⊢ Continuous fun i ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)

Tactic:
replace hD := fun t₁ t₂ ↦ hD (.inl (Set.mem_range_self t₁)) (.inr (Set.mem_range_self t₂))

Goal state after:
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
⊢ Continuous fun i ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G H : SimpleGraph V
h : Disjoint G.support H.support
⊢ Disjoint G H

Tactic:
simp_rw [Set.disjoint_left, mem_support] at h
  rw [← disjoint_edgeSet, Set.disjoint_left, Sym2.forall]
  grind [mem_edgeSet]

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 y p₁ : P
h : p₁ ∈ s
⊢ s.WOppSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
by
  constructor
  · 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 [vadd_vsub_assoc, ← vsub_sub_vsub_cancel_right x p₁ p₁']
      linear_combination (norm := match_scalars <;> field) hr
  · rintro (h' | ⟨h₁, h₂, h₃⟩)
    · exact wOppSide_of_left_mem y h'
    · exact ⟨p₁, h, h₁, h₂, h₃⟩

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
⊢ s.WOppSide x y ↔ ∃ a ∈ Set.Iic 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
Set.mem_Iic

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 ↔ ∃ a ≤ 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
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
⊢ s.SOppSide x y ↔ ∃ a ∈ Set.Iio 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
Set.mem_Iio

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 ↔ ∃ a < 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
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}

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

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ Integrable (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-r / 2)) μ

Tactic:
by
  have hr : 0 < r := lt_of_le_of_lt (finrank ℝ E).cast_nonneg hnr
  refine ((integrable_one_add_norm hnr).const_mul <| (2 : ℝ) ^ (r / 2)).mono'
    ?_ (Eventually.of_forall fun x => ?_)
  · apply Measurable.aestronglyMeasurable (by fun_prop)
  refine (abs_of_pos ?_).trans_le (rpow_neg_one_add_norm_sq_le x hr)
  positivity

Goal state after:
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
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
n : ℕ
I : ν {a | f a ≤ M} = 0
J : μ {a | u n < f a} < ∞
⊢ ν {a | f a ≤ M} + ν {a | u n < f a} < ∞

Tactic:
I,

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
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
n : ℕ
I : ν {a | f a ≤ M} = 0
J : μ {a | u n < f a} < ∞
⊢ 0 + ν {a | u n < f a} < ∞
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 : ℕ
hk : ∀ n_1 ≤ n, iteratedFDeriv ℝ n_1 f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
F : E → (N : Fin (n + 1)) → E [×↑N]→L[ℝ] F✝ := fun x N ↦ iteratedFDeriv ℝ (↑N) f x
⊢ ∀ (i : ℕ) (h : i < n + 1), (fun x ↦ iteratedFDeriv ℝ i f x) =O[⊤] fun x ↦ (1 + ‖x‖) ^ k

Tactic:
Nat.lt_succ_iff

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
F : E → (N : Fin (n + 1)) → E [×↑N]→L[ℝ] F✝ := fun x N ↦ iteratedFDeriv ℝ (↑N) f x
⊢ ∀ (i : ℕ) (h : i ≤ n), (fun x ↦ iteratedFDeriv ℝ i f x) =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: case inr
α : 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
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
a : α
ha : M < f a
⊢ a ∈ ⋃ i, {a | f a ≤ M} ∪ {a | u i < f a}

Tactic:
obtain ⟨n, hn⟩ : ∃ n, u n < f a := ((tendsto_order.1 ulim).2 _ ha).exists

Goal state after:
case inr
α : 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
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
a : α
ha : M < f a
n : ℕ
hn : u n < f a
⊢ a ∈ ⋃ i, {a | f a ≤ M} ∪ {a | u i < f a}
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
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
this : SigmaFinite ν
meas : MeasurableSet {a | M < f a}
I : ∫⁻ (ω : α) in {a | M < f a}ᶜ, ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = 0
⊢ ∫⁻ (x : α) in {a | M < f a}, ENNReal.ofReal (∫ (t : ℝ) in 0..f x, g t) ∂μ +
      ∫⁻ (x : α) in {a | M < f a}ᶜ, ENNReal.ofReal (∫ (t : ℝ) in 0..f x, g t) ∂μ =
    ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂ν

Tactic:
I,

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
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
this : SigmaFinite ν
meas : MeasurableSet {a | M < f a}
I : ∫⁻ (ω : α) in {a | M < f a}ᶜ, ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = 0
⊢ ∫⁻ (x : α) in {a | M < f a}, ENNReal.ofReal (∫ (t : ℝ) in 0..f x, g t) ∂μ + 0 =
    ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂ν
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
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
this : SigmaFinite ν
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂ν
B1 :
  ∫⁻ (t : ℝ) in Ioc 0 M, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioc 0 M, ν {a | t ≤ f a} * ENNReal.ofReal (g t)
B2 :
  ∫⁻ (t : ℝ) in Ioi M, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioi M, ν {a | t ≤ f a} * ENNReal.ofReal (g t)
I : Ioi 0 = Ioc 0 M ∪ Ioi M
J : Disjoint (Ioc 0 M) (Ioi M)
⊢ ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioi 0, ν {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
I,

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
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
this : SigmaFinite ν
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂ν
B1 :
  ∫⁻ (t : ℝ) in Ioc 0 M, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioc 0 M, ν {a | t ≤ f a} * ENNReal.ofReal (g t)
B2 :
  ∫⁻ (t : ℝ) in Ioi M, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioi M, ν {a | t ≤ f a} * ENNReal.ofReal (g t)
I : Ioi 0 = Ioc 0 M ∪ Ioi M
J : Disjoint (Ioc 0 M) (Ioi M)
⊢ ∫⁻ (t : ℝ) in Ioc 0 M ∪ Ioi M, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioc 0 M ∪ Ioi M, ν {a | t ≤ f a} * ENNReal.ofReal (g t)
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
⊢ (fun a ↦ μ {a_1 | a ≤ f a_1} * ENNReal.ofReal (g a)) =ᵐ[volume.restrict (Ioi 0)] fun a ↦
    μ {a_1 | a < f a_1} * ENNReal.ofReal (g a)

Tactic:
filter_upwards [meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f]
    with t ht

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
t : ℝ
ht : μ {a | t ≤ f a} = μ {a | t < f a}
⊢ μ {a | t ≤ f a} * ENNReal.ofReal (g t) = μ {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 μ
⊢ (fun a ↦ μ {a_1 | a ≤ f a_1}) =ᵐ[volume.restrict (Ioi 0)] fun a ↦ μ {a_1 | a < f a_1}

Tactic:
filter_upwards [meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f]
    with t ht

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
t : ℝ
ht : μ {a | t ≤ f a} = μ {a | t < f a}
⊢ μ {a | t ≤ f a} = μ {a | t < f a}
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 : ℕ∞
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₁)
⊢ (if LocallyIntegrableOn φ (↑Ω) μ then ∫ (x : E), (B ((ofSupportedIn K_sub_Ω f) x)) (φ x) ∂μ else 0) =
    (if LocallyIntegrableOn φ (↑Ω) μ then ContDiffMapSupportedIn.integralAgainstBilinCLM B μ φ else 0) f

Tactic:
by
      split_ifs with h
      · simp [h.integrableOn_compact_subset K_sub_Ω K.2]
      · simp

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

Goal state before:
pp: C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ x ^ k * f = x ^ (-↑l) * (x ^ (k + l) * f)

Tactic:
by
      rw [← Real.rpow_natCast, ← Real.rpow_natCast, ← mul_assoc, ← Real.rpow_add (by positivity)]
      simp

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

Goal state before:
pp: case neg
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
c : ℝ := -b⁻¹ * a
hc : T x₀ = c • x₀
⊢ T x₀ = T.rayleighQuotient x₀ • x₀

Tactic:
convert hc

Goal state after:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
c : ℝ := -b⁻¹ * a
hc : T x₀ = c • x₀
⊢ T.rayleighQuotient x₀ = c
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
⊢ HasEigenvalue T ↑(RCLike.re (↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)))

Tactic:
let ⟨x, hx⟩ := hT.direct_sum_isInternal.subordinateOrthonormalBasisIndex hn i
    hT.orthogonalFamily_eigenspaces'

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
i : Fin n
x : 𝕜
hx : HasUnifEigenvalue T x 1
⊢ HasEigenvalue T ↑(RCLike.re (↑T ⟨x, hx⟩))
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f g : 𝓓^{n}_{K}(E, F)
⊢ (if hk : k + 1 ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0) =
    (if hk : k + 1 ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0) +
      if hk : k + 1 ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0

Tactic:
split_ifs with hk
    · have hk' : 0 < (n : ℕ∞ω) := mod_cast (add_pos_of_right zero_lt_one k).trans_le hk
      ext
      simp [fderiv_add (f.contDiff.differentiable hk'.ne').differentiableAt
                       (g.contDiff.differentiable hk'.ne').differentiableAt, FunLike.coe_add]
    · simp

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
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < RCLike.re ⟪x, T x⟫
v : E
hv₂ : v ≠ 0
hpos : 0 < ‖v‖ ^ 2
hv₁ : T v = ↑μ • v
this : RCLike.re ⟪v, T v⟫ = μ * ‖v‖ ^ 2
⊢ 0 < μ

Tactic:
exact (mul_pos_iff_of_pos_right hpos).mp (this ▸ hnn v)

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 : ℝ
hx : x ∈ spectrum ℝ A
⊢ 0 ≤ x

Tactic:
obtain ⟨i, rfl⟩ := Set.ext_iff.mp
      hA.posSemidef.1.spectrum_real_eq_range_eigenvalues x |>.mp hx

Goal state after:
𝕜 : Type u_1
n : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : Fintype n
A : Matrix n n 𝕜
hA : 0 ≤ A
i : n
hx : ⋯.eigenvalues i ∈ spectrum ℝ A
⊢ 0 ≤ ⋯.eigenvalues i
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
y : Matrix n n 𝕜
hx : (star y * y).PosSemidef
h : IsUnit (star y * y)
hv : y *ᵥ v = 0
⊢ v = 0

Tactic:
rw [← map_eq_zero_iff (f := (yᴴ * y).mulVecLin) (mulVec_injective_iff_isUnit.mpr h),
    mulVecLin_apply, ← mulVec_mulVec, hv, mulVec_zero]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
x : ι →₀ 𝕜
hAs : (A.submatrix Subtype.val Subtype.val).PosSemidef
hBs : (B.submatrix Subtype.val Subtype.val).PosSemidef
⊢ ((A ⊙ B).submatrix Subtype.val Subtype.val).PosSemidef

Tactic:
submatrix_hadamard,

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
x : ι →₀ 𝕜
hAs : (A.submatrix Subtype.val Subtype.val).PosSemidef
hBs : (B.submatrix Subtype.val Subtype.val).PosSemidef
⊢ (A.submatrix Subtype.val Subtype.val ⊙ B.submatrix Subtype.val Subtype.val).PosSemidef
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
⊢ ((A ⊙ B).submatrix Subtype.val Subtype.val).PosDef

Tactic:
submatrix_hadamard,

Goal state after:
𝕜 : 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
⊢ (A.submatrix Subtype.val Subtype.val ⊙ B.submatrix Subtype.val Subtype.val).PosDef
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
⊢ (abs a ^ 2) ^ x = (star a * a) ^ x

Tactic:
abs_nnrpow_two

Goal state after:
A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
⊢ (star a * a) ^ x = (star a * a) ^ x
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝¹⁸ : RCLike 𝕜
inst✝¹⁷ : NonUnitalRing A
inst✝¹⁶ : TopologicalSpace A
inst✝¹⁵ : Module 𝕜 A
inst✝¹⁴ : StarRing A
inst✝¹³ : PartialOrder A
inst✝¹² : StarOrderedRing A
inst✝¹¹ : IsScalarTower 𝕜 A A
inst✝¹⁰ : SMulCommClass 𝕜 A A
inst✝⁹ : Module ℝ A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : IsScalarTower ℝ A A
inst✝⁶ : NonnegSpectrumClass ℝ A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : StarModule 𝕜 A
inst✝¹ : StarModule ℝ A
inst✝ : IsScalarTower ℝ 𝕜 A
r : 𝕜
a : A
⊢ abs (r • a) = abs (‖r‖ • a)

Tactic:
simp only [abs, mul_smul_comm, smul_mul_assoc, star_smul, ← smul_assoc,
      RCLike.real_smul_eq_coe_smul (K := 𝕜)]
    simp [-algebraMap_smul, ← smul_mul_assoc, ← mul_comm (starRingEnd _ _), RCLike.conj_mul, sq]

Goal state after: