mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case intro
α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
a✝ : α
t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
a' : α
⊢ a' ∈ {a}.erase a + t → Acc (CutExpand r) {a'}

Tactic:
erase_singleton,

Goal state after:
case intro
α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
a✝ : α
t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
a' : α
⊢ a' ∈ 0 + t → Acc (CutExpand r) {a'}
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case left
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
f : Dual K V
v : V
hv : v ∉ (↑e).fixedSubmodule
hf : map f (↑e).fixedSubmodule = ⊥
hfv : f (v - e v) = 0
hfv' : f (e v) = 1
ht : (↑e).fixedSubmodule ≤ (↑(transvection hfv)).fixedSubmodule
x : V
hx : x ∈ (↑e).fixedSubmodule
⊢ ↑(transvection hfv) x = x

Tactic:
← mem_fixedSubmodule_iff

Goal state after:
case left
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
f : Dual K V
v : V
hv : v ∉ (↑e).fixedSubmodule
hf : map f (↑e).fixedSubmodule = ⊥
hfv : f (v - e v) = 0
hfv' : f (e v) = 1
ht : (↑e).fixedSubmodule ≤ (↑(transvection hfv)).fixedSubmodule
x : V
hx : x ∈ (↑e).fixedSubmodule
⊢ x ∈ (↑(transvection hfv)).fixedSubmodule
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
h1 : finrank K (V ⧸ W ⊔ K ∙ v) + finrank K ↥(W ⊔ K ∙ v) = finrank K V
h2 : finrank K (V ⧸ W) + finrank K ↥W = finrank K V
⊢ finrank K (V ⧸ W ⊔ K ∙ v) + 1 = finrank K (V ⧸ W)

Tactic:
rw [finrank_sup_span_singleton hv] at h1

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
h1 : finrank K (V ⧸ W ⊔ K ∙ v) + (finrank K ↥W + 1) = finrank K V
h2 : finrank K (V ⧸ W) + finrank K ↥W = finrank K V
⊢ finrank K (V ⧸ W ⊔ K ∙ v) + 1 = finrank K (V ⧸ W)
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hW : 1 < finrank K (V ⧸ W)
htop : W ⊔ K ∙ v = ⊤
h1 : finrank K (V ⧸ W) + finrank K ↥W = finrank K V
⊢ finrank K ↥(K ∙ v) ≤ 1

Tactic:
exact le_trans (finrank_span_le_card {v}) (by simp)

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
n✝ : ℕ
e : V ≃ₗ[K] V
he : e.fixedReduce = 1
n : ℕ
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
hind :
  ∀ {e : V ≃ₗ[K] V},
    e.fixedReduce = 1 → finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
f : Dual K V
v : V
hf : (↑e).fixedSubmodule ≤ ker f
hv : f v = 1
hv' : v ∈ (↑e).fixedSubmodule
⊢ False

Tactic:
by
        apply one_ne_zero' K
        rw [← hv, ← LinearMap.mem_ker]
        exact hf hv'

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
e : V ≃ₗ[K] V
u y : V
hy : y ∈ (↑e).fixedSubmodule
a : K
hu' : y + a • (e u - u) = e u
hu : ∀ (s t : K), s • (↑e).fixedSubmodule.mkQ u + t • e.fixedReduce ((↑e).fixedSubmodule.mkQ u) = 0 → s = 0 ∧ t = 0
⊢ a • (↑e).fixedSubmodule.mkQ u + (1 - a) • e.fixedReduce ((↑e).fixedSubmodule.mkQ u) = 0

Tactic:
simp only [← LinearMap.map_smul, ← LinearEquiv.map_smul]

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
e : V ≃ₗ[K] V
u y : V
hy : y ∈ (↑e).fixedSubmodule
a : K
hu' : y + a • (e u - u) = e u
hu : ∀ (s t : K), s • (↑e).fixedSubmodule.mkQ u + t • e.fixedReduce ((↑e).fixedSubmodule.mkQ u) = 0 → s = 0 ∧ t = 0
⊢ (↑e).fixedSubmodule.mkQ (a • u) + e.fixedReduce ((↑e).fixedSubmodule.mkQ ((1 - a) • u)) = 0
Module: Mathlib.MeasureTheory.Constructions.SimpleGraph

Goal state before:
pp: V : Type u_1
⊢ ∀ (a : Sym2 V), Measurable fun x ↦ a ∈ x.edgeSet

Tactic:
rintro ⟨u, v⟩; simp only [mem_edgeSet]; fun_prop

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case inl.refine_2
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
n✝ : ℕ
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn0 : n = 0
⊢ auxTransvection hf * e ∈ dilatransvections K V

Tactic:
mem_dilatransvections_iff_finrank_quotient,

Goal state after:
case inl.refine_2
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
n✝ : ℕ
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn0 : n = 0
⊢ finrank K (V ⧸ (↑(auxTransvection hf * e)).fixedSubmodule) ≤ 1
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: case refine_2
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝¹ : CompleteSpace E
hm : m ≤ mΩ
inst✝ : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun x ↦ (fs x) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), ‖(fs n) ω‖ ≤ c
⊢ Integrable (fun ω ↦ (B (f ω)) (μ[g | m] ω)) μ

Tactic:
exact B.integrable_of_bilin_of_bdd_left c (hf.mono hm).aestronglyMeasurable hf_bound
        integrable_condExp

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → v i = w i
⊢ ∀ (x : Set α), v x = w x

Tactic:
i

Goal state after:
case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → v i = w i
i : Set α
⊢ v i = w i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case convert_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ ∀ (i : ℕ), MeasurableSet (Function.extend e f (fun x ↦ ∅) i)

pp: case convert_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ Pairwise (Disjoint on Function.extend e f fun x ↦ ∅)

Tactic:
· simp [Function.apply_extend MeasurableSet, Function.comp_def, hm]

Goal state after:
case convert_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ Pairwise (Disjoint on Function.extend e f fun x ↦ ∅)
Module: Mathlib.MeasureTheory.Covering.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
⊢ blimsup (fun i ↦ thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ thickening (r i) (s i)) atTop p

Tactic:
let q : ℕ → Prop := fun i => p i ∧ 0 < r i
  have hq {u : ℕ → Set α} (hu : ∀ i, u i ≠ ∅ → 0 < r i) :
      blimsup u atTop p = blimsup u atTop q :=
    blimsup_congr' <| Eventually.of_forall fun i hi ↦ by simp [q, hu i hi]
  rw [hq fun i hi ↦ (thickening_nonempty_iff.1 <| nonempty_iff_ne_empty.2 hi).1,
    hq fun i hi ↦ (mul_pos_iff_of_pos_left hM).1 <|
      (thickening_nonempty_iff.1 <| nonempty_iff_ne_empty.2 hi).1]
  exact blimsup_thickening_mul_ae_eq_aux μ q s hM r hr (Eventually.of_forall fun i hi => hi.2)

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case neg.hd
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l)
⊢ Pairwise (Function.onFun Disjoint fun l ↦ ⋃ (_ : l < k), s.restrictNonposSeq i l)

Tactic:
intro a b hab

Goal state after:
case neg.hd
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l)
a b : ℕ
hab : a ≠ b
⊢ Function.onFun Disjoint (fun l ↦ ⋃ (_ : l < k), s.restrictNonposSeq i l) a b
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case mp.left
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
⊢ s.toJordanDecomposition.posPart ≪ μ

Tactic:
refine Measure.AbsolutelyContinuous.mk fun S _ hS₂ => ?_
      have := h hS₂
      rw [totalVariation, Measure.add_apply, add_eq_zero] at this

Goal state after:
case mp.left
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
this : s.toJordanDecomposition.posPart S = 0 ∧ s.toJordanDecomposition.negPart S = 0
⊢ s.toJordanDecomposition.posPart S = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case mp.right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
⊢ s.toJordanDecomposition.negPart ≪ μ

Tactic:
refine Measure.AbsolutelyContinuous.mk fun S _ hS₂ => ?_
      have := h hS₂
      rw [totalVariation, Measure.add_apply, add_eq_zero] at this

Goal state after:
case mp.right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : μ S = 0
this : s.toJordanDecomposition.posPart S = 0 ∧ s.toJordanDecomposition.negPart S = 0
⊢ s.toJordanDecomposition.negPart S = 0
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : ¬μ = 0
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
n : ℕ
hn : n ≥ N
hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
⊢ eLpNorm (tᶜ.indicator (f n - g)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)

Tactic:
specialize hN n hn

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : ¬μ = 0
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
N n : ℕ
hN : ∀ x ∈ tᶜ, dist (g x) (f n x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
hn : n ≥ N
hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
⊢ eLpNorm (tᶜ.indicator (f n - g)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
⊢ s.toMeasureOfZeroLE' i hi₂ ∅ ⋯ = 0

Tactic:
toMeasureOfZeroLE',

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
⊢ ↑(NNReal.mk ((VectorMeasure.restrict s i) ∅) ⋯) = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : 0 ≤[i] s
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ s.toMeasureOfZeroLE' i hi j hj₁ = ↑(NNReal.mk (s (i ∩ j)) ⋯)

Tactic:
toMeasureOfZeroLE',

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : 0 ≤[i] s
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ ↑(NNReal.mk ((VectorMeasure.restrict s i) j) ⋯) = ↑(NNReal.mk (s (i ∩ j)) ⋯)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hg : MemLp g p μ
hp : 1 ≤ p
⊢ lpNorm f p μ ≤ lpNorm (f + g) p μ + lpNorm g p μ

Tactic:
simpa using lpNorm_add_le' (f := f + g) hg.neg hp

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
g : α → ℝ
hg : MemLp g p μ
h : ∀ (x : α), ‖f x‖ ≤ g x
hf : ¬AEStronglyMeasurable f μ
⊢ lpNorm f p μ ≤ lpNorm g p μ

Tactic:
· simp [hf]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨C, hCpos, hC⟩ := h (ε / 2) (half_pos hε)

Goal state after:
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
h : ν s = 0
⊢ ↑ν s = 0

Tactic:
rw [← ennreal_coeFn_eq_coeFn_toMeasure, h, ENNReal.coe_zero]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
ν : FiniteMeasure Ω
s : Set Ω
h : ν s = 0
⊢ ↑ν s = 0

Tactic:
rw [← ennreal_coeFn_eq_coeFn_toMeasure, h, ENNReal.coe_zero]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 0)
⊢ Tendsto μs F (𝓝 0)

Tactic:
rw [tendsto_iff_forall_testAgainstNN_tendsto]
  intro f
  convert! tendsto_zero_testAgainstNN_of_tendsto_zero_mass mass_lim f
  rw [zero_testAgainstNN_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
p : ℝ≥0∞
hp : 1 ≤ p
hf : MemLp f p μ
⊢ eLpNorm μ[f | m] p μ ≤ eLpNorm f p μ

pp: case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
p : ℝ≥0∞
hp : 1 ≤ p
hf : ¬MemLp f p μ
⊢ eLpNorm μ[f | m] p μ ≤ eLpNorm f p μ

Tactic:
· rw [← ofReal_lpNorm hf, ← ofReal_lpNorm (hf.condExp hp)]
    exact ENNReal.ofReal_le_ofReal (hf.lpNorm_condExp_le_lpNorm hp)

Goal state after:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
p : ℝ≥0∞
hp : 1 ≤ p
hf : ¬MemLp f p μ
⊢ eLpNorm μ[f | m] p μ ≤ eLpNorm f p μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
⊢ UniformIntegrable (fun i ↦ μ[g | ℱ i]) 1 μ

Tactic:
have hmeas : ∀ n, ∀ C, MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} := fun n C =>
    measurableSet_le measurable_const (stronglyMeasurable_condExp.mono (hℱ n)).measurable.nnnorm

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖μ[g | ℱ n] x‖₊}
⊢ UniformIntegrable (fun i ↦ μ[g | ℱ i]) 1 μ
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
⊢ ∀ {f_1 : ι → Set Ω},
    (∀ i ∈ S, f_1 i ∈ (fun x ↦ {s | MeasurableSet s}) i) →
      ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f_1 i) = ∏ i ∈ S, (κ a) (f_1 i)

Tactic:
setsΩ

Goal state after:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
⊢ (∀ i ∈ S, setsΩ i ∈ (fun x ↦ {s | MeasurableSet s}) i) →
    ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, setsΩ i) = ∏ i ∈ S, (κ a) (setsΩ i)
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
𝒜 ℬ : Set (Set Ω)
h : ∀ A ∈ 𝒜, IndepSets {A} ℬ μ
⊢ IndepSets 𝒜 ℬ μ

Tactic:
by
    rw [← 𝒜.biUnion_of_singleton]
    exact IndepSets.biUnion h

Goal state after:
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case right
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → μ (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, μ (f i ⁻¹' sets i)
this : IsProbabilityMeasure μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ μ (⋂ i, f i ⁻¹' s i) = (Measure.map (fun ω i ↦ f i ω) μ) (univ.pi s)

Tactic:
Measure.map_apply_of_aemeasurable (aemeasurable_pi_lambda _ fun x ↦ hf x)
        (.univ_pi hm)

Goal state after:
case right
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → μ (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, μ (f i ⁻¹' sets i)
this : IsProbabilityMeasure μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ μ (⋂ i, f i ⁻¹' s i) = μ ((fun c x ↦ f x c) ⁻¹' univ.pi s)
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
h : ∀ (F : Set Ω), IsClosed[inst✝¹] F → limsup (fun i ↦ (μs i) F) atTop ≤ μ F
F : Set Ω
hF_closed : IsClosed[inst✝¹] F
⊢ limsup (fun i ↦ ↑(μs i) F) atTop ≤ ↑μ F

Tactic:
specialize h F hF_closed

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
F : Set Ω
h : limsup (fun i ↦ (μs i) F) atTop ≤ μ F
hF_closed : IsClosed[inst✝¹] F
⊢ limsup (fun i ↦ ↑(μs i) F) atTop ≤ ↑μ F