mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
hki' : P.pairingIn ℤ k i < 0
hkj' : 0 < P.pairingIn ℤ k j
this✝² : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : P.IsNotG2
this : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hlj_mem : P.root l - P.root j ∈ range ⇑P.root
⊢ ¬(chainBotCoeff i m = 1 ∧ chainBotCoeff j (-l) = 0)

Tactic:
suffices ¬ (P.pairingIn ℤ m i = 0 ∧ P.pairingIn ℤ l j ≠ 0) by
    contrapose this
    rcases ne_or_eq (P.pairingIn ℤ m i) 0 with hmi | hmi
    · simpa [hmi, this.1, P.pairingIn_eq_zero_iff (i := i)] using chainBotCoeff_if_one_zero him_mem
    refine ⟨hmi, fun hlj ↦ ?_⟩
    rw [chainBotCoeff_if_one_zero hjl_mem] at this
    simp [P.pairingIn_eq_zero_iff (i := j), hlj] at this

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
hki' : P.pairingIn ℤ k i < 0
hkj' : 0 < P.pairingIn ℤ k j
this✝² : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : P.IsNotG2
this : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hlj_mem : P.root l - P.root j ∈ range ⇑P.root
⊢ ¬(P.pairingIn ℤ m i = 0 ∧ P.pairingIn ℤ l j ≠ 0)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
i j : ↥b.support
⊢ ⁅⟨h j, ⋯⟩, ⟨f i, ⋯⟩⁆ = -b.cartanMatrix i j • ⟨f i, ⋯⟩

Tactic:
by simp [Subtype.ext_iff, lie_h_f]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ (TensorAlgebra.ι R) m ∈ (TensorAlgebra.ι R).range ^ 1

Tactic:
by simpa only [pow_one] using LinearMap.mem_range_self _ m

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
⊢ onIocAux f ∅ = 0

Tactic:
onIocAux,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
⊢ (if h : ∃ p, p.1 ≤ p.2 ∧ ∅ = Set.Ioc p.1 p.2 then f h.choose.2 - f h.choose.1 else 0) = 0
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
m : AddContent G C
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ m (s ∪ t) ≤ m s + m t

Tactic:
rw [← union_sdiff_self, addContent_union hC hs (hC.sdiff_mem ht hs)]

Goal state after:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
m : AddContent G C
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ m s + m (t \ s) ≤ m s + m t

α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
m : AddContent G C
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ Disjoint s (t \ s)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M ↦ {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
⊢ ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ

Tactic:
intro M

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M ↦ {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
M : ℕ
⊢ AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ v (A ∪ B) = v A + v B

Tactic:
Set.union_eq_iUnion,

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ v (⋃ b, bif b then A else B) = v A + v B
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
A : Set α
hA : MeasurableSet A
⊢ v Aᶜ = v univ - v A

Tactic:
simpa [compl_eq_univ_sdiff] using of_sdiff hA .univ (v := v) (subset_univ _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
x✝ : Set α
hi : ¬MeasurableSet x✝
⊢ (⇑v - ⇑w) x✝ = 0

Tactic:
Pi.sub_apply,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
x✝ : Set α
hi : ¬MeasurableSet x✝
⊢ v x✝ - w x✝ = 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: Ω : 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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
hm : ¬m ≤ mΩ
⊢ ∀ (a : Ω), μ[fun ω ↦ (B (f ω)) (g ω) | m] a = (fun ω ↦ (B (f ω)) (μ[g | m] ω)) a

Tactic:
simp [condExp_of_not_le hm]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
i : Set α
hi : MeasurableSet i
⊢ (μ + ν).toENNRealVectorMeasure i = (μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) i

Tactic:
toENNRealVectorMeasure_apply_measurable hi,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
i : Set α
hi : MeasurableSet i
⊢ (μ + ν) i = (μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
i : Set α
hi : MeasurableSet i
⊢ μ i + ν i = μ.toENNRealVectorMeasure i + ν.toENNRealVectorMeasure i

Tactic:
toENNRealVectorMeasure_apply_measurable hi,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
i : Set α
hi : MeasurableSet i
⊢ μ i + ν i = μ i + ν.toENNRealVectorMeasure i
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: case neg
Ω : 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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[fun ω ↦ (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω ↦ (B (f ω)) (μ[g | m] ω)

pp: case pos
Ω : 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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
⊢ μ[fun ω ↦ (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω ↦ (B (f ω)) (μ[g | m] ω)

Tactic:
· exact ae_of_all _ <| by simp [condExp_of_not_sigmaFinite hm hμm]

Goal state after:
case pos
Ω : 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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
⊢ μ[fun ω ↦ (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω ↦ (B (f ω)) (μ[g | m] ω)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
f : α → β
hf : Measurable f
⊢ map 0 f = 0

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
f : α → β
hf : ¬Measurable f
⊢ map 0 f = 0

Tactic:
· ext i hi
    rw [map_apply _ hf hi, zero_apply, zero_apply]

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
f : α → β
hf : ¬Measurable f
⊢ map 0 f = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
ha₃ : ⋃ n, a ∩ disjointed f n = a
ha₄ : Pairwise (Disjoint on fun n ↦ a ∩ disjointed f n)
⊢ ∑' (i : ℕ), v (a ∩ disjointed f i) ≤ w (⋃ n, a ∩ disjointed f n)

pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
ha₃ : ⋃ n, a ∩ disjointed f n = a
ha₄ : Pairwise (Disjoint on fun n ↦ a ∩ disjointed f n)
⊢ ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)

Tactic:
w.of_disjoint_iUnion _ ha₄

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
ha₃ : ⋃ n, a ∩ disjointed f n = a
ha₄ : Pairwise (Disjoint on fun n ↦ a ∩ disjointed f n)
⊢ ∑' (i : ℕ), v (a ∩ disjointed f i) ≤ ∑' (i : ℕ), w (a ∩ disjointed f i)

α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
ha₃ : ⋃ n, a ∩ disjointed f n = a
ha₄ : Pairwise (Disjoint on fun n ↦ a ∩ disjointed f n)
⊢ ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)

α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
ha₃ : ⋃ n, a ∩ disjointed f n = a
ha₄ : Pairwise (Disjoint on fun n ↦ a ∩ disjointed f n)
⊢ ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → w s = 0 → v s = 0
⊢ v ≪ᵥ w

Tactic:
intro s hs
  by_cases hmeas : MeasurableSet s
  · exact h hmeas hs
  · exact not_measurable v hmeas

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

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

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

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (a : α) in i, (s.toJordanDecomposition.posPart.rnDeriv μ a).toReal ∂μ -
      ∫ (a : α) in i, (s.toJordanDecomposition.negPart.rnDeriv μ a).toReal ∂μ =
    s i

pp: case hf
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (fun x ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) (μ.restrict i)

pp: case hg
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (fun x ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) (μ.restrict i)

Tactic:
setIntegral_toReal_rnDeriv h.1 i,

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ s.toJordanDecomposition.posPart.real i - ∫ (a : α) in i, (s.toJordanDecomposition.negPart.rnDeriv μ a).toReal ∂μ = s i

case hf
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (fun x ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) (μ.restrict i)

case hg
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (fun x ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) (μ.restrict i)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

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

Tactic:
← toReal_eLpNorm (hf.add hg).aestronglyMeasurable,

Goal state after:
case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
hg : MemLp g p μ
⊢ (eLpNorm (f + g) p μ).toReal ≤ lpNorm f p μ + lpNorm g p μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case a.μ
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| (r • s).toJordanDecomposition.negPart.singularPart μ

Tactic:
rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_negPart_neg _ _ hr, singularPart_smul]

Goal state after:
case a.μ
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| (-r).toNNReal • s.toJordanDecomposition.posPart.singularPart μ
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Goal state before:
pp: case h.refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
F : Set X
hF : IsClosed[inst✝¹] F
key :
  ∀ (x : X),
    Tendsto (fun i ↦ (thickenedIndicator ⋯ F) x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F).indicator (fun x ↦ 1) x))
x : X
⊢ Tendsto (fun i ↦ ((fun n ↦ thickenedIndicator ⋯ F) i) x) atTop (𝓝 (F.indicator (fun x ↦ 1) x))

Tactic:
← IsClosed.closure_eq hF

Goal state after:
case h.refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
F : Set X
hF : IsClosed[inst✝¹] F
key :
  ∀ (x : X),
    Tendsto (fun i ↦ (thickenedIndicator ⋯ F) x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F).indicator (fun x ↦ 1) x))
x : X
⊢ Tendsto (fun i ↦ ((fun n ↦ thickenedIndicator ⋯ F) i) x) atTop (𝓝 ((closure[inst✝¹] F).indicator (fun x ↦ 1) x))
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ
hp : 1 ≤ p
f : α → E
s : Set α
hs : MeasurableSet s
hf : Integrable (fun x ↦ ‖f x‖ ^ p) μ
⊢ ∫ (x : α) in s, ‖μ[f | m] x‖ ^ p ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ^ p ∂μ

Tactic:
have hp' : p ≠ 0 := by linarith

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ
hp : 1 ≤ p
f : α → E
s : Set α
hs : MeasurableSet s
hf : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : p ≠ 0
⊢ ∫ (x : α) in s, ‖μ[f | m] x‖ ^ p ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ^ p ∂μ
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ testAgainstNN 0 f = 0

Tactic:
simp only [testAgainstNN, toMeasure_zero, lintegral_zero_measure, ENNReal.toNNReal_zero]

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 μ
h✝ : NeZero μ
hp' : 0 < p
hm : ¬m ≤ m0
⊢ lpNorm μ[f | m] p μ ≤ lpNorm f p μ

Tactic:
simp [condExp_of_not_le hm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
ℐ : ℝ≥0 → ι
δ : ℝ≥0
hδpos : 0 < ↑δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal ↑δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal ↑δ < μ {x | C ≤ ‖f (ℐ C) x‖₊}
C : ℝ≥0
⊢ C • μ {x | C ≤ ‖f (ℐ C) x‖₊} ^ (1 / p.toReal) ≤ eLpNorm ({x | C ≤ ‖f (ℐ C) x‖₊}.indicator (f (ℐ C))) p μ

Tactic:
refine le_eLpNorm_of_bddBelow hp hp' _
            (measurableSet_le measurable_const (hf _).nnnorm.measurable)
            (Eventually.of_forall fun x hx => ?_)

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
ℐ : ℝ≥0 → ι
δ : ℝ≥0
hδpos : 0 < ↑δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal ↑δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal ↑δ < μ {x | C ≤ ‖f (ℐ C) x‖₊}
C : ℝ≥0
x : α
hx : x ∈ {x | C ≤ ‖f (ℐ C) x‖₊}
⊢ C ≤ ‖{x | C ≤ ‖f (ℐ C) x‖₊}.indicator (f (ℐ C)) x‖₊
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case refine_1
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SFinite μ
s : Set Ω
Rs : ℕ → ℝ
left✝ : StrictAnti Rs
Rs_pos : ∀ (n : ℕ), 0 < Rs n
Rs_lim : Tendsto Rs atTop (𝓝 0)
obs : ∀ (n : ℕ), ∃ r ∈ Ioo 0 (Rs n), μ (frontier (Metric.thickening r s)) = 0
⊢ Tendsto (fun n ↦ ⋯.choose) atTop (𝓝 0)

pp: case refine_2
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SFinite μ
s : Set Ω
Rs : ℕ → ℝ
left✝ : StrictAnti Rs
Rs_pos : ∀ (n : ℕ), 0 < Rs n
Rs_lim : Tendsto Rs atTop (𝓝 0)
obs : ∀ (n : ℕ), ∃ r ∈ Ioo 0 (Rs n), μ (frontier (Metric.thickening r s)) = 0
⊢ ∀ (n : ℕ), 0 < (fun n ↦ ⋯.choose) n ∧ μ (frontier (Metric.thickening ((fun n ↦ ⋯.choose) n) s)) = 0

Tactic:
· exact tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds Rs_lim
      (fun n ↦ (obs n).choose_spec.1.1.le) fun n ↦ (obs n).choose_spec.1.2.le

Goal state after:
case refine_2
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SFinite μ
s : Set Ω
Rs : ℕ → ℝ
left✝ : StrictAnti Rs
Rs_pos : ∀ (n : ℕ), 0 < Rs n
Rs_lim : Tendsto Rs atTop (𝓝 0)
obs : ∀ (n : ℕ), ∃ r ∈ Ioo 0 (Rs n), μ (frontier (Metric.thickening r s)) = 0
⊢ ∀ (n : ℕ), 0 < (fun n ↦ ⋯.choose) n ∧ μ (frontier (Metric.thickening ((fun n ↦ ⋯.choose) n) s)) = 0
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr.inr
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
h : IsMarkovKernel κ
a : α
ht : t = univ
⊢ (κ a) s = (κ a) s * 1

Tactic:
mul_one

Goal state after:
case inr.inr
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
h : IsMarkovKernel κ
a : α
ht : t = univ
⊢ (κ a) s = (κ a) s
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
π : ι → Set (Set Ω)
x✝ : MeasurableSpace Ω
μ : Measure Ω
h : iIndepSets π μ
⊢ μ univ = 1

Tactic:
by simpa using h ∅ (f := fun _ ↦ univ)

Goal state after: