mathlib-initiative/mathlib-tactics huggingface dataset:
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
e : V ≃ₗ[K] V
f : Dual K V
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
hfu : f u = 1
hu : u ∉ (↑e).fixedSubmodule
⊢ finrank K (V ⧸ (↑(auxTransvection hf * e)).fixedSubmodule) + 1 = finrank K (V ⧸ (↑e).fixedSubmodule)

Tactic:
rw [auxTransvection_mul_fixed hfu]

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
e : V ≃ₗ[K] V
f : Dual K V
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
hfu : f u = 1
hu : u ∉ (↑e).fixedSubmodule
⊢ finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ u) + 1 = finrank K (V ⧸ (↑e).fixedSubmodule)
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ generateFrom (squareCylinders fun i ↦ {s | MeasurableSet s}) = MeasurableSpace.pi

Tactic:
apply le_antisymm

Goal state after:
case a
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ generateFrom (squareCylinders fun i ↦ {s | MeasurableSet s}) ≤ MeasurableSpace.pi

case a
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ MeasurableSpace.pi ≤ generateFrom (squareCylinders fun i ↦ {s | MeasurableSet s})
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case a
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ ((fun t ↦ {i}.pi t) '' univ.pi fun i ↦ {s | MeasurableSet s}) ⊆ squareCylinders fun i ↦ {s | MeasurableSet s}

Tactic:
rw [← Finset.coe_singleton, squareCylinders_eq_iUnion_image]

Goal state after:
case a
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ ((fun t ↦ (↑{i}).pi t) '' univ.pi fun i ↦ {s | MeasurableSet s}) ⊆
    ⋃ s, (fun t ↦ (↑s).pi t) '' univ.pi fun i ↦ {s | MeasurableSet s}
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
⊢ (∃ P, ↑P.parts ⊆ C) → s ∈ supClosure C

Tactic:
by
    intro ⟨P, hP⟩
    rw [← P.sup_parts, sup_id_set_eq_sUnion]
    exact supClosed_supClosure.sSup_mem
      (Finset.finite_toSet _)
      (subset_supClosure hC.empty_mem)
      (hP.trans subset_supClosure)

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ generateFrom (measurableCylinders α) = MeasurableSpace.pi

Tactic:
apply le_antisymm

Goal state after:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ generateFrom (measurableCylinders α) ≤ MeasurableSpace.pi

case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ MeasurableSpace.pi ≤ generateFrom (measurableCylinders α)
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
t : Finset ℕ
S : Set ((i : ↥t) → X ↑i)
mS : MeasurableSet S
⊢ cylinder t S ∈ {cylinder (Finset.Iic (t.sup id)) (Finset.restrict₂ ⋯ ⁻¹' S)}

Tactic:
unfold cylinder

Goal state after:
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
t : Finset ℕ
S : Set ((i : ↥t) → X ↑i)
mS : MeasurableSet S
⊢ t.restrict ⁻¹' S ∈ {(Finset.Iic (t.sup id)).restrict ⁻¹' Finset.restrict₂ ⋯ ⁻¹' S}
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ Disjoint t (⋃₀ ↑(hC.disjointOfDiff hs ht))

Tactic:
rw [hC.sUnion_disjointOfDiff]
  exact disjoint_sdiff_right

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
inst✝ : Unique ι
⊢ Measurable fun x ↦ x

Tactic:
exact measurable_id

Goal state after:
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case inr
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
⊢ SecondCountableTopology (WithTop ι)

Tactic:
obtain ⟨c', c'_count, hc'⟩ : ∃ c' : Set ι, c'.Countable ∧ Dense c' :=
    SeparableSpace.exists_countable_dense

Goal state after:
case inr
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
⊢ SecondCountableTopology (WithTop ι)
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case inr
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
⊢ instWithTopOfOrderTopology = generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}

Tactic:
apply le_antisymm

Goal state after:
case inr.a
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
⊢ instWithTopOfOrderTopology ≤ generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}

case a
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
⊢ generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} ≤ instWithTopOfOrderTopology
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Nonempty α
⊢ ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v},
    ∀ t ∈ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v},
      ∃ I, ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} ∧ (↑I).PairwiseDisjoint id ∧ s \ t = ⋃₀ ↑I

Tactic:
rintro s ⟨u, v, huv, rfl⟩ t ⟨u', v', hu'v', rfl⟩
    rcases le_or_gt u' u with hu | hu
    · rcases Ioc_mem_ofPred_Ioc_le (max u v') v with ⟨u'', v'', h'', heq⟩
      exists {Set.Ioc u'' v''}
      grind [coe_singleton, pairwiseDisjoint_singleton]
    rcases le_or_gt v v' with hv | hv
    · rcases Ioc_mem_ofPred_Ioc_le u (min u' v) with ⟨u'', v'', h'', heq⟩
      exists {Set.Ioc u'' v''}
      grind [coe_singleton, pairwiseDisjoint_singleton]
    rw [show Set.Ioc u v \ Set.Ioc u' v' = Set.Ioc u u' ∪ Set.Ioc v' v by grind]
    refine ⟨{Set.Ioc u u', Set.Ioc v' v}, by grind, ?_, by simp⟩
    intro a ha b hb hab
    simp [Function.onFun]
    grind

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

Goal state before:
pp: case h_dis
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ ↑(Finset.image f a)
⊢ (↑(Finset.image f a)).PairwiseDisjoint id

pp: case h_mem
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ ↑(Finset.image f a)
⊢ ⋃₀ ↑(Finset.image f a) ∈ C

pp: α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ ↑(Finset.image f a)
⊢ ∑ u ∈ Finset.image f a, m u = ∑ i ∈ a, m (f i)

Tactic:
· simpa using! h_dis.image

Goal state after:
case h_mem
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ ↑(Finset.image f a)
⊢ ⋃₀ ↑(Finset.image f a) ∈ C

α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ ↑(Finset.image f a)
⊢ ∑ u ∈ Finset.image f a, m u = ∑ i ∈ a, m (f i)
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
e : V ≃ₗ[K] V
f g : Dual K V
v : V
a b : K
hv : ∀ (s t : K), s • (↑e).fixedSubmodule.mkQ v + t • e.fixedReduce ((↑e).fixedSubmodule.mkQ v) = 0 → s = 0 ∧ t = 0
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha : ∀ (v_1 : V), (auxTransvection hf * e) v_1 - a • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb : ∀ (v_1 : V), (auxTransvection hg * e) v_1 - b • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
c : K := b - a
hc : c = b - a
key : ∀ (x : V), g (e x) • (v - e v) - c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hc0 : c = 0
y : V
hy : -y ∈ (↑e).fixedSubmodule
k : K
hk : y + k • v = v - e v
⊢ (k - 1) • v + 1 • e v = -y

Tactic:
rw [eq_comm, ← sub_eq_iff_eq_add] at hk

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
e : V ≃ₗ[K] V
f g : Dual K V
v : V
a b : K
hv : ∀ (s t : K), s • (↑e).fixedSubmodule.mkQ v + t • e.fixedReduce ((↑e).fixedSubmodule.mkQ v) = 0 → s = 0 ∧ t = 0
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha : ∀ (v_1 : V), (auxTransvection hf * e) v_1 - a • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb : ∀ (v_1 : V), (auxTransvection hg * e) v_1 - b • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
c : K := b - a
hc : c = b - a
key : ∀ (x : V), g (e x) • (v - e v) - c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hc0 : c = 0
y : V
hy : -y ∈ (↑e).fixedSubmodule
k : K
hk : v - e v - k • v = y
⊢ (k - 1) • v + 1 • e v = -y
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case inr
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 g : Dual K V
v : V
a b : K
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
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha : ∀ (v_1 : V), (auxTransvection hf * e) v_1 - a • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb : ∀ (v_1 : V), (auxTransvection hg * e) v_1 - b • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
c : K := b - a
hc : c = b - a
key : ∀ (x : V), g (e x) • (v - e v) - c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hc0 : c ≠ 0
⊢ (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v = ⊤

Tactic:
eq_top_iff

Goal state after:
case inr
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 g : Dual K V
v : V
a b : K
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
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha : ∀ (v_1 : V), (auxTransvection hf * e) v_1 - a • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb : ∀ (v_1 : V), (auxTransvection hg * e) v_1 - b • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
c : K := b - a
hc : c = b - a
key : ∀ (x : V), g (e x) • (v - e v) - c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hc0 : c ≠ 0
⊢ ⊤ ≤ (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case refine_2
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, m s ≠ ∞
hm_tendsto : ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n ↦ m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n ↦ (⋃ i, f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
⊢ (⋂ i, ⋃ i, f i) ∩ ⋂ i, (accumulate f i)ᶜ = ∅

Tactic:
Set.iInter_const,

Goal state after:
case refine_2
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, m s ≠ ∞
hm_tendsto : ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n ↦ m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n ↦ (⋃ i, f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
⊢ (⋃ i, f i) ∩ ⋂ i, (accumulate f i)ᶜ = ∅
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ
hε : 0 < ε
hε2 : 0 < ε / 2
δ₁ : ℝ
hδ₁_pos : 0 < δ₁
hfδ₁ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
δ₂ : ℝ
hδ₂_pos : 0 < δ₂
hgδ₂ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
⊢ ENNReal.ofReal ε = ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2)

Tactic:
rw [← ENNReal.ofReal_add hε2.le hε2.le, add_halves]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
x : α
hx : x ∈ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
⊢ x ∈ {x | eLpNormEssSup f μ < ↑‖f x‖₊}

Tactic:
Set.mem_ofPred_eq,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
x : α
hx : x ∈ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
⊢ eLpNormEssSup f μ < ↑‖f x‖₊
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
this : {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ⊆ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
hle : μ {a | ¬‖f a‖ₑ ≤ eLpNormEssSup f μ} = 0
⊢ μ {x | eLpNormEssSup f μ < ↑‖f x‖₊} ≤ 0

Tactic:
not_le

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
this : {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ⊆ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
hle : μ {a | eLpNormEssSup f μ < ‖f a‖ₑ} = 0
⊢ μ {x | eLpNormEssSup f μ < ↑‖f x‖₊} ≤ 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
⊢ toSignedMeasure 0 = 0

Tactic:
ext i hi

Goal state after:
α : Type u_1
m : MeasurableSpace α
i : Set α
hi : MeasurableSet i
⊢ (toSignedMeasure 0) i = 0 i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ (μ + ν).toSignedMeasure = μ.toSignedMeasure + ν.toSignedMeasure

Tactic:
ext i hi

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0
⊢ (r • μ).toSignedMeasure = r • μ.toSignedMeasure

Tactic:
ext i hi

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ (r • μ).toSignedMeasure i = (r • μ.toSignedMeasure) i
Module: Mathlib.MeasureTheory.Measure.Complex

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
R : Type u_2
inst✝³ : Semiring R
inst✝² : Module R ℝ
inst✝¹ : ContinuousConstSMul R ℝ
inst✝ : ContinuousConstSMul R ℂ
⊢ ∀ (m_1 : R) (x : ComplexMeasure α),
    equivSignedMeasure.toFun (m_1 • x) = (RingHom.id R) m_1 • equivSignedMeasure.toFun x

Tactic:
by
      intro r c
      dsimp
      ext
      · simp [Complex.smul_re]
      · simp [Complex.smul_im]

Goal state after:
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Ω
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : ⋃ i, sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), μ (sets x) < ∞
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x
this : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), a ∈ sets i → μ[fun ω ↦ (B (f ω)) (g ω) | m] a = (B (f a)) (μ[g | m] a)
ω : Ω
hω : ∀ (i : ℕ), ω ∈ sets i → μ[fun ω ↦ (B (f ω)) (g ω) | m] ω = (B (f ω)) (μ[g | m] ω)
⊢ ∃ i, ω ∈ sets i

Tactic:
have h_mem : ω ∈ ⋃ i, sets i := by rw [h_univ]; exact Set.mem_univ _

Goal state after:
Ω : 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)
sets : ℕ → Set Ω
h_univ : ⋃ i, sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), μ (sets x) < ∞
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x
this : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), a ∈ sets i → μ[fun ω ↦ (B (f ω)) (g ω) | m] a = (B (f a)) (μ[g | m] a)
ω : Ω
hω : ∀ (i : ℕ), ω ∈ sets i → μ[fun ω ↦ (B (f ω)) (g ω) | m] ω = (B (f ω)) (μ[g | m] ω)
h_mem : ω ∈ ⋃ i, sets i
⊢ ∃ i, ω ∈ sets i
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

Tactic:
ext i hi

Goal state after:
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
i : Set β
hi : MeasurableSet i
⊢ (map 0 f) i = 0 i
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
i : Set β
hi : MeasurableSet i
⊢ (map 0 f) i = 0 i

Tactic:
map_apply _ hf hi,

Goal state after:
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
i : Set β
hi : MeasurableSet i
⊢ 0 (f ⁻¹' i) = 0 i
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
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
hf : Measurable f
⊢ (v + w).map f = v.map f + w.map f

Tactic:
ext i hi

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
hf : Measurable f
i : Set β
hi : MeasurableSet i
⊢ ((v + w).map f) i = (v.map f + w.map f) i
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
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : Measurable f
⊢ (c • v).map f = c • v.map f

Tactic:
ext i hi

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : Measurable f
i : Set β
hi : MeasurableSet i
⊢ ((c • v).map f) i = (c • v.map f) i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : s v + s (w \ v) = 0
h₁ : 0 ≤ s v
⊢ s v = 0

Tactic:
have h₂ : 0 ≤ s (w \ v) :=
    nonneg_of_zero_le_restrict _
      (restrict_le_restrict_subset _ _ hu hsu (sdiff_subset.trans hw₂))

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : s v + s (w \ v) = 0
h₁ : 0 ≤ s v
h₂ : 0 ≤ s (w \ v)
⊢ s v = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hw₁ : s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : s w = 0 → w ⊆ u → v ⊆ w → s v = 0
⊢ s v = 0

Tactic:
exact this hw₁ hw₂ hwt

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0

Tactic:
have hi₁ : MeasurableSet i := by_contradiction fun h => ne_of_lt hi <| s.not_measurable h

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case intro.refine_1
α : Type u_1
β : Type u_2
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
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), v ≤[f b] w
val✝ : Encodable β
n : ℕ
⊢ MeasurableSet (⋃ b ∈ Encodable.decode₂ β n, f b)

Tactic:
measurability

Goal state after: