mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case refine_2.inr.inr.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : ((s n).indicator fun x ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet t

Tactic:
heq

Goal state after:
case refine_2.inr.inr.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : (s n)ᶜ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet t
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case refine_2.inr.inr.inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : ((s n).indicator fun x ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = ∅
⊢ MeasurableSet t

Tactic:
heq

Goal state after:
case refine_2.inr.inr.inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : ∅ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = ∅
⊢ MeasurableSet t
Module: Mathlib.MeasureTheory.Function.Piecewise

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
⊢ StronglyMeasurable (hs.piecewise f)

Tactic:
let g (n : ℕ) (i : ι) : Fin (n + 1) :=
    if hi : ∃ m < n, i = e m then ⟨hi.choose, by grind⟩ else Fin.last n

Goal state after:
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
g : (n : ℕ) → ι → Fin (n + 1) := fun n i ↦ if hi : ∃ m < n, i = e m then ⟨hi.choose, ⋯⟩ else Fin.last n
⊢ StronglyMeasurable (hs.piecewise f)
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : Group G
inst✝¹ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst✝ : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u) F
g✝ h : G
s : Set X
g : G
⊢ ∀ (h : G), mean μ u F (g • s) ≤ mean μ u F (h • s)

Tactic:
h

Goal state after:
G : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : Group G
inst✝¹ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst✝ : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u) F
g✝ h✝ : G
s : Set X
g h : G
⊢ mean μ u F (g • s) ≤ mean μ u F (h • s)
Module: Mathlib.MeasureTheory.Integral.CircleTransform

Goal state before:
pp: R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
⊢ ∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B

Tactic:
obtain ⟨r, hr, hrx⟩ := exists_lt_mem_ball_of_mem_ball hx

Goal state after:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
⊢ ∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
f : α →C_c β
f' : α → β
h : f' = ⇑f
⊢ Continuous f'

Tactic:
h

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
f : α →C_c β
f' : α → β
h : f' = ⇑f
⊢ Continuous ⇑f
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
f : α →C_c β
f' : α → β
h : f' = ⇑f
⊢ HasCompactSupport f'

Tactic:
h

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
f : α →C_c β
f' : α → β
h : f' = ⇑f
⊢ HasCompactSupport ⇑f
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₚ[ℝ] ℝ
h : Λ₁ = Λ₂
⊢ toNNRealLinear Λ₁ = toNNRealLinear Λ₂

Tactic:
h

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₚ[ℝ] ℝ
h : Λ₁ = Λ₂
⊢ toNNRealLinear Λ₂ = toNNRealLinear Λ₂
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₚ[ℝ] ℝ
f : α →C_c ℝ
h : ∀ (x : α →C_c ℝ≥0), Λ₁ x.toReal = Λ₂ x.toReal
⊢ Λ₁ f.nnrealPart.toReal - Λ₁ (-f).nnrealPart.toReal = Λ₂ f.nnrealPart.toReal - Λ₂ (-f).nnrealPart.toReal

Tactic:
h

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

Goal state before:
pp: p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ 2 * π * ∫ (x : ℝ) in Ioi 0, x ^ (q + 1) * rexp (-x ^ p) = 2 * π / p * Real.Gamma ((q + 2) / p)

Tactic:
_root_.integral_rpow_mul_exp_neg_rpow (by linarith) (by linarith),

Goal state after:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ 2 * π * (1 / p * Real.Gamma ((q + 1 + 1) / p)) = 2 * π / p * Real.Gamma ((q + 2) / p)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x | deriv f x ≠ 0}
hsm : MeasurableSet s
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, s.indicator (fun x ↦ C) t

Tactic:
apply norm_sub_le_integral_of_norm_deriv_le_of_le hab hfc hfd

Goal state after:
case hfB
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := ⋯
hsm : MeasurableSet s
⊢ ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ s.indicator (fun x ↦ C) t

case hBi
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := ⋯
hsm : MeasurableSet s
⊢ IntervalIntegrable (s.indicator fun x ↦ C) volume a b
Module: Mathlib.MeasureTheory.Integral.Regular

Goal state before:
pp: case a
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : NormalSpace X
⊢ μ U ≤ ⨆ f, ⨆ (_ : Continuous f), ⨆ (_ : EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ)

Tactic:
apply le_of_forall_lt (fun r hr ↦ ?_)

Goal state after:
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : NormalSpace X
r : ENNReal
hr : r < μ U
⊢ r < ⨆ f, ⨆ (_ : Continuous f), ⨆ (_ : EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ)
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f₁ f₂ : X →C_c ℝ≥0
⊢ f₁ ≤ f₂ → Λ f₁ ≤ Λ f₂

Tactic:
h

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f₁ f₂ : X →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ Λ f₁ ≤ Λ f₂
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K₁ K₂ : Compacts X
h : K₁ ≤ K₂
⊢ rieszContentAux Λ K₁ ≤ rieszContentAux Λ K₂

Tactic:
unfold rieszContentAux
  gcongr
  apply rieszContentAux_image_nonempty

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: case pos
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint ↑K₁ ↑K₂
b : ℝ≥0
f : X →C_c ℝ≥0
hf : f ∈ {f | ∀ x ∈ K₁ ⊔ K₂, 1 ≤ f x}
Λf_eq_b : Λ f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, x ∈ support ⇑f
hsubsuppf : ↑K₁ ∪ ↑K₂ ⊆ tsupport ⇑f
g₁ g₂ : X →C_c ℝ≥0
hg₁ : EqOn (⇑g₁) 1 K₁.carrier
hg₂ : EqOn (⇑g₂) 1 K₂.carrier
sum_g : EqOn (⇑(g₁ + g₂)) 1 (tsupport f.toFun)
x : X
h : f x = 0
⊢ ↑(f x) = ↑((⇑g₁ + ⇑g₂) x) * ↑(f x)

Tactic:
h

Goal state after:
case pos
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint ↑K₁ ↑K₂
b : ℝ≥0
f : X →C_c ℝ≥0
hf : f ∈ {f | ∀ x ∈ K₁ ⊔ K₂, 1 ≤ f x}
Λf_eq_b : Λ f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, x ∈ support ⇑f
hsubsuppf : ↑K₁ ∪ ↑K₂ ⊆ tsupport ⇑f
g₁ g₂ : X →C_c ℝ≥0
hg₁ : EqOn (⇑g₁) 1 K₁.carrier
hg₂ : EqOn (⇑g₂) 1 K₂.carrier
sum_g : EqOn (⇑(g₁ + g₂)) 1 (tsupport f.toFun)
x : X
h : f x = 0
⊢ ↑0 = ↑((⇑g₁ + ⇑g₂) x) * ↑0
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: case pos
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint ↑K₁ ↑K₂
b : ℝ≥0
f : X →C_c ℝ≥0
hf : f ∈ {f | ∀ x ∈ K₁ ⊔ K₂, 1 ≤ f x}
Λf_eq_b : Λ f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, x ∈ support ⇑f
hsubsuppf : ↑K₁ ∪ ↑K₂ ⊆ tsupport ⇑f
g₁ g₂ : X →C_c ℝ≥0
hg₁ : EqOn (⇑g₁) 1 K₁.carrier
hg₂ : EqOn (⇑g₂) 1 K₂.carrier
sum_g : EqOn (⇑(g₁ + g₂)) 1 (tsupport f.toFun)
x : X
h : f x = 0
⊢ ↑0 = ↑((⇑g₁ + ⇑g₂) x) * ↑0

Tactic:
simp only [NNReal.coe_zero, mul_zero]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : X →C_c ℝ≥0
⊢ ∫ (x : X), ↑(f x) ∂rieszMeasure Λ = ∫ (x : X), f.toReal x ∂RealRMK.rieszMeasure (toRealPositiveLinear Λ)

Tactic:
simp [RealRMK.rieszMeasure, NNRealRMK.rieszMeasure]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
⊢ i ≤ j → generateMeasurableRec s i ⊆ generateMeasurableRec s j

Tactic:
h

Goal state after:
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h : i ≤ j
⊢ generateMeasurableRec s i ⊆ generateMeasurableRec s j
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: case inl.inr
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t✝ : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k✝ k : Ordinal.{u_1}
hk : k ≤ i
t : Set α
IH : ∀ j < k, ∀ t ∈ generateMeasurableRec s j, p t
ht : t ∈ compl '' ⋃ j, ⋃ (_ : j < k), generateMeasurableRec s j
⊢ p t

Tactic:
simp_rw [mem_image, mem_iUnion₂] at ht
    obtain ⟨u, ⟨⟨j, hj, hj'⟩, rfl⟩⟩ := ht
    exact hc u (IH j hj u hj') ⟨j, hj.trans_le hk, hj'⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case h.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range ⇑f ⊆ Ioo a (a + ↑N * ε)
b : ℝ := a + ↑N * ε
y : Fin N → ℝ := fun n ↦ a + ε * (↑↑n + 1)
hy : ∀ {n m : Fin N}, n < m → y n + ε ≤ y m
E : Fin N → Set X := fun n ↦ ⇑f ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport ⇑f
m : Fin N
a✝¹ : m ∈ univ
n : Fin N
a✝ : n ∈ univ
hmn : m ≠ n
x : X
hx : y m - ε < f x ∧ f x ≤ y m ∧ x ∈ tsupport ⇑f
⊢ (¬y n - ε < f x ∨ ¬f x ≤ y n) ∨ x ∉ tsupport ⇑f

Tactic:
not_lt,

Goal state after:
case h.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range ⇑f ⊆ Ioo a (a + ↑N * ε)
b : ℝ := a + ↑N * ε
y : Fin N → ℝ := fun n ↦ a + ε * (↑↑n + 1)
hy : ∀ {n m : Fin N}, n < m → y n + ε ≤ y m
E : Fin N → Set X := fun n ↦ ⇑f ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport ⇑f
m : Fin N
a✝¹ : m ∈ univ
n : Fin N
a✝ : n ∈ univ
hmn : m ≠ n
x : X
hx : y m - ε < f x ∧ f x ≤ y m ∧ x ∈ tsupport ⇑f
⊢ (f x ≤ y n - ε ∨ ¬f x ≤ y n) ∨ x ∉ tsupport ⇑f
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ max (#↑s) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
⊢ ∀ j < i, #↑(generateMeasurableRec s j) ≤ max (#↑s) 2 ^ ℵ₀

Tactic:
intro j hj
      exact IH j hj (hj.trans_le hi).le

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: case hf
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n) μ
x : Fin n → E
h : innerₗ E = ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)
hint' : ∀ (k : ℕ), ↑k ≤ ↑n → Integrable (fun x ↦ ‖x‖ ^ k * ‖1 x‖) μ
⊢ ContDiff ℝ (↑n) (fourierIntegral Real.fourierChar μ (innerₗ E) 1)

Tactic:
h

Goal state after:
case hf
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n) μ
x : Fin n → E
h : innerₗ E = ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)
hint' : ∀ (k : ℕ), ↑k ≤ ↑n → Integrable (fun x ↦ ‖x‖ ^ k * ‖1 x‖) μ
⊢ ContDiff ℝ (↑n) (fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)) 1)
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : OpensMeasurableSpace E
x t : E
⊢ charFun (Measure.dirac x) t = cexp (↑⟪x, t⟫ * I)

Tactic:
by
  rw [charFun_apply, integral_dirac]

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
inst✝ : R0Space X
x : X
K : Set X
hK : IsClosed[inst✝²] K
hx : x ∉ K
cx : IsClosed[inst✝²] (closure[inst✝²] {x})
a : X
hax : a ∈ closure[inst✝²] {x}
haK : a ∈ K
⊢ a ∈ ∅

Tactic:
exact hx ((specializes_iff_mem_closure.mpr hax).symm.mem_closed hK haK)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst✝⁸ : CompleteSpace E
inst✝⁷ : CompleteSpace F
inst✝⁶ : SecondCountableTopology E
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : BorelSpace E
inst✝³ : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (t : WithLp 2 (E × F)), charFun (Measure.map (toLp 2) ξ) t = charFun μ t.ofLp.1 * charFun ν t.ofLp.2

Tactic:
h

Goal state after:
E : Type u_4
F : Type u_5
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst✝⁸ : CompleteSpace E
inst✝⁷ : CompleteSpace F
inst✝⁶ : SecondCountableTopology E
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : BorelSpace E
inst✝³ : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (t : WithLp 2 (E × F)), charFun (Measure.map (toLp 2) (μ.prod ν)) t = charFun μ t.ofLp.1 * charFun ν t.ofLp.2
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: ι : Type u_6
inst✝⁷ : Fintype ι
E : ι → Type u_7
inst✝⁶ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst✝¹ : ∀ (i : ι), IsFiniteMeasure (μ i)
inst✝ : IsFiniteMeasure ν
h : ν = Measure.pi μ
⊢ ∀ (t : WithLp 2 ((i : ι) → E i)), charFun (Measure.map (toLp 2) ν) t = ∏ i, charFun (μ i) (t.ofLp i)

Tactic:
h

Goal state after:
ι : Type u_6
inst✝⁷ : Fintype ι
E : ι → Type u_7
inst✝⁶ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst✝¹ : ∀ (i : ι), IsFiniteMeasure (μ i)
inst✝ : IsFiniteMeasure ν
h : ν = Measure.pi μ
⊢ ∀ (t : WithLp 2 ((i : ι) → E i)), charFun (Measure.map (toLp 2) (Measure.pi μ)) t = ∏ i, charFun (μ i) (t.ofLp i)
Module: Mathlib.MeasureTheory.Measure.DiracProba

Goal state before:
pp: X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
x : X
⊢ diracProba x ∈ range diracProba

Tactic:
by exact mem_range_self x

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : BorelSpace F
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (L : StrongDual ℝ (E × F)),
    charFunDual ξ L =
      charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E F) * charFunDual ν (L ∘SL ContinuousLinearMap.inr ℝ E F)

Tactic:
h

Goal state after:
E : Type u_2
F : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : BorelSpace F
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (L : StrongDual ℝ (E × F)),
    charFunDual (μ.prod ν) L =
      charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E F) * charFunDual ν (L ∘SL ContinuousLinearMap.inr ℝ E F)
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : BorelSpace F
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (L : StrongDual ℝ (E × F)),
    charFunDual ξ L =
      charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E F) * charFunDual ν (L ∘SL ContinuousLinearMap.inr ℝ E F)

Tactic:
rw [h]; exact charFunDual_prod

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst✝⁹ : BorelSpace E
inst✝⁸ : SecondCountableTopology E
p : ℝ≥0∞
inst✝⁷ : Fact (1 ≤ p)
inst✝⁶ : BorelSpace F
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (L : StrongDual ℝ (WithLp p (E × F))),
    charFunDual (Measure.map (toLp p) ξ) L =
      charFunDual μ (L ∘SL ↑(prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inl ℝ E F) *
        charFunDual ν (L ∘SL ↑(prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inr ℝ E F)

Tactic:
h

Goal state after:
E : Type u_2
F : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst✝⁹ : BorelSpace E
inst✝⁸ : SecondCountableTopology E
p : ℝ≥0∞
inst✝⁷ : Fact (1 ≤ p)
inst✝⁶ : BorelSpace F
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (L : StrongDual ℝ (WithLp p (E × F))),
    charFunDual (Measure.map (toLp p) (μ.prod ν)) L =
      charFunDual μ (L ∘SL ↑(prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inl ℝ E F) *
        charFunDual ν (L ∘SL ↑(prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inr ℝ E F)