mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
e : SymmetricAlgebra R M ≃ₐ[R] A
he : ↑↑e ∘ₗ SymmetricAlgebra.ι R M = f
h : ↑e = SymmetricAlgebra.lift f
⊢ IsSymmetricAlgebra f

Tactic:
change Function.Bijective _

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
e : SymmetricAlgebra R M ≃ₐ[R] A
he : ↑↑e ∘ₗ SymmetricAlgebra.ι R M = f
h : ↑e = SymmetricAlgebra.lift f
⊢ Function.Bijective ⇑(SymmetricAlgebra.lift f)
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
i : ℕ
x : TensorAlgebra R M
hx : x ∈ (ι R).range ^ i
⊢ ((lift R) (GradedAlgebra.ι R M)) x = (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) i) ⟨x, hx⟩

Tactic:
induction hx using Submodule.pow_induction_on_left' with
    | algebraMap r =>
      rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
    | add x y i hx hy ihx ihy =>
      rw [map_add, ihx, ihy, ← map_add]
      rfl
    | mem_mul m hm i x hx ih =>
      obtain ⟨_, rfl⟩ := hm
      rw [map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.of_mul_of]
      exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)

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
he : ∀ (u : V), u ∈ (↑e).fixedSubmodule
⊢ False

Tactic:
← Submodule.eq_top_iff'

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
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
he : (↑e).fixedSubmodule = ⊤
⊢ False
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case pos
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
hi₂ : i ∈ s₂
⊢ t₂' i ∈ C i

pp: case neg
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
hi₂ : i ∉ s₂
⊢ t₂' i ∈ C i

Tactic:
· rw [← h2 i hi₂]
        exact h₂ i (mem_univ _)

Goal state after:
case neg
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
hi₂ : i ∉ s₂
⊢ t₂' i ∈ C i
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case insert.inr
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
a✝ : s ∉ S
ih : ↑S ⊆ C → ∃ P, ↑P.parts ⊆ C
hsC : s ∈ C
hSC : ↑S ⊆ C
P : Finpartition (S.sup id)
hP : ↑P.parts ⊆ C
hs : s ≠ ⊥
Q : (t : Set α) → t ∈ (P.avoid s).parts → Finpartition t
hQ : ∀ (t : Set α) (a : t ∈ (P.avoid s).parts), ↑(Q t a).parts ⊆ C
⊢ insert s ↑((P.avoid s).bind Q).parts ⊆ C

Tactic:
insert_subset_iff,

Goal state after:
case insert.inr
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
a✝ : s ∉ S
ih : ↑S ⊆ C → ∃ P, ↑P.parts ⊆ C
hsC : s ∈ C
hSC : ↑S ⊆ C
P : Finpartition (S.sup id)
hP : ↑P.parts ⊆ C
hs : s ≠ ⊥
Q : (t : Set α) → t ∈ (P.avoid s).parts → Finpartition t
hQ : ∀ (t : Set α) (a : t ∈ (P.avoid s).parts), ↑(Q t a).parts ⊆ C
⊢ s ∈ C ∧ ↑((P.avoid s).bind Q).parts ⊆ C
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:
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.SetSemiring

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

Tactic:
by
  conv_rhs => rw [← union_sdiff_cancel hst, ← hC.sUnion_disjointOfDiff hs ht]
  simp only [sUnion_insert]

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ∀ t ∈ ↑(hC.disjointOfDiffUnion hs hI), t ⊆ s \ ⋃₀ ↑I

Tactic:
rw [← sUnion_subset_iff, hC.sdiff_sUnion_eq_sUnion_disjointOfDiffUnion hs hI]

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

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
I : Finset ι
t : (i : ι) → Set (α i)
⊢ (↑I).pi t = (↑I).domRestrict ⁻¹' univ.pi fun i ↦ t ↑i

Tactic:
ext; simp

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

Goal state before:
pp: case a.inl.coe.top.inr.refine_1
ι : 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₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a : ι
hb✝ : ⊤ ∈ Ioi ↑a
ha : (Ioi a).Nonempty
b : ι
bc' : b ∈ c'
hb : b ∈ Ioi a
⊢ Ioi ↑b ⊆ Ioi ↑a

Tactic:
apply Ioi_subset_Ioi
            simpa using hb.le

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

Goal state before:
pp: case pos
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
hn_pos : n > 0
he' : auxTransvection hf * e ∈ transvections K V ^ n * dilatransvections K V
⊢ ∃ x ∈ transvections K V, ∃ y ∈ transvections K V ^ n * dilatransvections K V, x * y = e

pp: case neg
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
hn_pos : n > 0
he' : auxTransvection hf * e ∉ transvections K V ^ n * dilatransvections K V
⊢ ∃ x ∈ transvections K V, ∃ y ∈ transvections K V ^ n * dilatransvections K V, x * y = e

Tactic:
· -- This is the easy case where one knows that `auxTransvection hf * e` is
        -- the product of at most `n + 1` transvections
        refine ⟨(auxTransvection hf)⁻¹, ?_, auxTransvection hf * e, he', by simp⟩
        rw [inv_mem_transvections_iff]
        apply mem_transvections

Goal state after:
case neg
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
hn_pos : n > 0
he' : auxTransvection hf * e ∉ transvections K V ^ n * dilatransvections K V
⊢ ∃ x ∈ transvections K V, ∃ y ∈ transvections K V ^ n * dilatransvections K V, x * y = e
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‖₊}
⊢ μ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} = 0

Tactic:
rw [← nonpos_iff_eq_zero]

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‖₊}
⊢ μ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ≤ 0
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
inst✝ : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
⊢ Tendsto (fun n ↦ v (s n)) atTop (𝓝 (v (⋂ n, s n)))

Tactic:
have I n : v (s n) = v univ - v (s n)ᶜ := by simp [of_compl (hs n)]

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
inst✝ : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
I : ∀ (n : ℕ), v (s n) = v univ - v (s n)ᶜ
⊢ Tendsto (fun n ↦ v (s n)) atTop (𝓝 (v (⋂ n, s n)))
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
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)
sets : ℕ → Set Ω
sets_prop : ∀ (n : ℕ), MeasurableSet (sets n) ∧ μ (sets n) < ∞ ∧ ∀ x ∈ sets n, ‖f x‖ ≤ ↑n
h_univ : ⋃ i, sets i = Set.univ
⊢ μ[fun ω ↦ (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω ↦ (B (f ω)) (μ[g | m] ω)

Tactic:
simp_rw [forall_and] at sets_prop

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)
sets : ℕ → Set Ω
h_univ : ⋃ i, sets i = Set.univ
sets_prop : (∀ (x : ℕ), MeasurableSet (sets x)) ∧ (∀ (x : ℕ), μ (sets x) < ∞) ∧ ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x
⊢ μ[fun ω ↦ (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω ↦ (B (f ω)) (μ[g | m] ω)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : TopologicalSpace M
N : Type u_4
inst✝⁶ : AddCommMonoid N
inst✝⁵ : TopologicalSpace N
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousConstSMul R N
v : VectorMeasure α M
f : M →ₗ[R] N
hf : Continuous[inst✝⁷, inst✝⁵] ⇑f
c : R
⊢ (c • v).mapRange f.toAddMonoidHom hf = c • v.mapRange f.toAddMonoidHom hf

Tactic:
ext; simp

Goal state after:
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
⊢ v ≤[⋃ n, f n] w

Tactic:
refine restrict_le_restrict_of_subset_le v w fun a ha₁ 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
⊢ v a ≤ w a
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
    refine Set.disjoint_iUnion_left.mpr fun _ => ?_
    refine Set.disjoint_iUnion_right.mpr fun _ => ?_
    exact restrictNonposSeq_disjoint hab

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∞
inst✝ : Subsingleton ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
hι : ¬Nonempty ι
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
· exact ⟨1, zero_lt_one, fun i => False.elim <| hι <| Nonempty.intro i⟩

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

Goal state before:
pp: case refine_2
α : 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₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ w t = 0

Tactic:
(_ : t = uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t),

Goal state after:
case refine_2
α : 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₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ w (uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t) = 0

α : 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₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ t = uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s.totalVariation ≪ μ.ennrealToMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ S = 0
⊢ s S = 0

Tactic:
← VectorMeasure.ennrealToMeasure_apply hS₁

Goal state after:
case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s.totalVariation ≪ μ.ennrealToMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ.ennrealToMeasure S = 0
⊢ s 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 : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
this : ∀ (n : ℕ), eLpNorm (f n - g) p μ = eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g ⋯) p μ
⊢ ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), f n x = AEStronglyMeasurable.mk (f n) ⋯ x

Tactic:
rw [ae_all_iff]

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 : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
this : ∀ (n : ℕ), eLpNorm (f n - g) p μ = eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g ⋯) p μ
⊢ ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, f i a = AEStronglyMeasurable.mk (f i) ⋯ a
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
hp₀ : p ≠ 0
hp : p ≠ ∞
c : E
⊢ lpNorm (fun _x ↦ c) p μ = ‖c‖ * μ.real Set.univ ^ p.toReal⁻¹

Tactic:
by
  simp [lpNorm, eLpNorm_const' c hp₀ hp, Measure.real, ENNReal.toReal_rpow,
    aestronglyMeasurable_const]

Goal state after:
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
hf : MemLp f p μ
hp : 1 ≤ p
hg : ¬MemLp g p μ
hfg : MemLp (f + g) p μ
⊢ MemLp g p μ

Tactic:
simpa using hfg.sub hf

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : ¬Integrable f μ
⊢ t = s.singularPart μ

Tactic:
rw [withDensityᵥ, dif_neg hfi, add_zero] at hadd
    refine eq_singularPart' t measurable_zero (integrable_zero _ _ μ) htμ ?_
    rwa [withDensityᵥ_zero, add_zero]

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

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f μ
h : 0 < μ {x | ↑R < |μ[f | m] x|}
⊢ False

Tactic:
suffices μ.real {x | ↑R < |(μ[f|m]) x|} * ↑R < μ.real {x | ↑R < |(μ[f|m]) x|} * ↑R by
    exact this.ne rfl

Goal state after:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f μ
h : 0 < μ {x | ↑R < |μ[f | m] x|}
⊢ μ.real {x | ↑R < |μ[f | m] x|} * ↑R < μ.real {x | ↑R < |μ[f | m] x|} * ↑R
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ μ.restrict univ = μ

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Surjective g
h : iIndepSets (π ∘ g) κ μ
⊢ iIndepSets π κ μ

Tactic:
obtain ⟨g', hg'⟩ := hg.hasRightInverse

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Surjective g
h : iIndepSets (π ∘ g) κ μ
g' : ι → ι'
hg' : Function.RightInverse g' g
⊢ iIndepSets π κ μ
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
hyp : ∀ (n : ι), IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht2 : t2 ∈ s'
n : ι
ht1 : t1 ∈ s n
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
exact hyp n t1 t2 ht1 ht2

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr.basic
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
t : Set Ω
ht : t ∈ p1
⊢ MeasurableSet t

Tactic:
rw [hpm1]

Goal state after:
case inr.basic
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
t : Set Ω
ht : t ∈ p1
⊢ MeasurableSet t