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

Goal state before:
pp: case algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : SymmetricAlgebra R M → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (SymmetricAlgebra R M)) r)
ι : ∀ (x : M), motive ((SymmetricAlgebra.ι R M) x)
mul : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a * b)
add : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a + b)
r : R
⊢ motive ((algHom R M) ((Algebra.algebraMap R (TensorAlgebra R M)) r))

Tactic:
AlgHom.commutes

Goal state after:
case algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : SymmetricAlgebra R M → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (SymmetricAlgebra R M)) r)
ι : ∀ (x : M), motive ((SymmetricAlgebra.ι R M) x)
mul : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a * b)
add : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a + b)
r : R
⊢ motive ((Algebra.algebraMap R (SymmetricAlgebra R M)) r)
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case inr.refine_2
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₂ + t
⊢ (s₁, (s₂ + t).erase a).1 + (s₁, (s₂ + t).erase a).2 = (s₁ + s₂ + t).erase a

Tactic:
· rw [add_assoc, erase_add_right_pos _ h]

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_notMem : v ∉ (↑e).fixedSubmodule
hv' : v - e v ∈ (↑e).fixedSubmodule
⊢ (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f

Tactic:
by
        simpa [hf] using hf (sub_mem_comm_iff.mp hv')

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α ↑i)
h : cylinder s S = ∅
hS : S ≠ ∅
⊢ False

Tactic:
← nonempty_iff_ne_empty

Goal state after:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
⊢ False
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case refine_3
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : Set α
hs : s ∈ C
t : Set α
ht : t ∈ C
⊢ s \ t = ⋃₀ ↑{s \ t}

Tactic:
· simp only [coe_singleton, sUnion_singleton]

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
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
⊢ ∃ v, LinearIndependent K ![v, e.fixedReduce v]

Tactic:
contrapose! he

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
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
he : ∀ (v : V ⧸ (↑e).fixedSubmodule), ¬LinearIndependent K ![v, e.fixedReduce v]
⊢ ∃ a, ∀ (x : V ⧸ (↑e).fixedSubmodule), e.fixedReduce x = a • x
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:
← sUnion_subset_iff,

Goal state after:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI) ⊆ s \ ⋃₀ ↑I
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
h_dis : (↑I).PairwiseDisjoint id
⊢ (↑I).PairwiseDisjoint id ∧
    (↑(hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id ∧
      ∀ ⦃i : Set α⦄, i ∈ ↑I → ∀ ⦃j : Set α⦄, j ∈ ↑(hC.disjointOfDiffUnion hs hI) → i ≠ j → Disjoint (id i) (id j)

Tactic:
refine ⟨h_dis, hC.pairwiseDisjoint_disjointOfDiffUnion hs hI, fun u hu v hv _ ↦ ?_⟩

Goal state after:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑I
v : Set α
hv : v ∈ ↑(hC.disjointOfDiffUnion hs hI)
x✝ : u ≠ v
⊢ Disjoint (id u) (id v)
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
hI_ss : ∀ t ∈ I, t ⊆ s
⊢ ⋃₀ (↑I ∪ ↑(hC.disjointOfDiffUnion hs hI)) = ⋃₀ ↑I ∪ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI)

Tactic:
sUnion_union

Goal state after:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
⊢ ⋃₀ ↑I ∪ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI) = ⋃₀ ↑I ∪ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI)
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case base
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
s t : Set α
t_mem : t ∈ 𝒜
⊢ t ∈ generateSetAlgebra ℬ

Tactic:
exact self_subset_generateSetAlgebra (h t_mem)

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

Goal state before:
pp: case inl
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
hmem : ∃ y ∈ (↑e).fixedSubmodule, ∃ a, y + a • v = v - e v
⊢ 1 = 0

Tactic:
obtain ⟨y, hy, k, hk⟩ := hmem

Goal state after:
case inl
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
⊢ 1 = 0
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
hC : IsSetSemiring C
m : AddContent G C
s : Set α
J : Finset (Set α)
hJ : ↑J ⊆ C
h'J : (↑J).PairwiseDisjoint id
hs : s = ⋃₀ ↑J
⊢ m.supClosureFun s = ∑ s ∈ J, m s

Tactic:
by
  have h : ∃ (J : Finset (Set α)), ↑J ⊆ C ∧ (PairwiseDisjoint (J : Set (Set α)) id) ∧ s = ⋃₀ ↑J :=
    ⟨J, hJ, h'J, hs⟩
  simp only [supClosureFun, h, ↓reduceDIte]
  apply sum_addContent_eq_of_sUnion_eq hC _ _ h.choose_spec.1 h.choose_spec.2.1 hJ h'J
  rw [← hs]
  exact h.choose_spec.2.2.symm

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
S' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' S
T' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' T
hS' : MeasurableSet S'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (I ∪ J) S'
h_eq2 : t = cylinder (I ∪ J) T'
h_eq3 : s ∪ t = cylinder (I ∪ J) (S' ∪ T')
⊢ (P (I ∪ J)) (S' ∪ T') = (P (I ∪ J)) S' + (P (I ∪ J)) T'

Tactic:
cases isEmpty_or_nonempty (Π i, α i) with
  | inl h => simp [hP.eq_zero_of_isEmpty]
  | inr h =>
    rw [measure_union _ hT']
    rwa [hs_eq, ht_eq, disjoint_cylinder_iff] at hst

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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
f : Fin #J → Set α := disjointed fun j ↦ ↑(J.equivFin.symm j)
htJ : t ⊆ ⋃ i, f i
h1 : ∀ (j : Fin #J), f j ∈ supClosure C
h2 : Pairwise (Disjoint on f)
h3 : ⋃ i, f i ∈ supClosure C
⊢ (m.supClosure hC) (⋃ i, f i) ≤ ∑ u ∈ J, m u

Tactic:
addContent_iUnion h1 h2 h3,

Goal state after:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
f : Fin #J → Set α := disjointed fun j ↦ ↑(J.equivFin.symm j)
htJ : t ⊆ ⋃ i, f i
h1 : ∀ (j : Fin #J), f j ∈ supClosure C
h2 : Pairwise (Disjoint on f)
h3 : ⋃ i, f i ∈ supClosure C
⊢ ∑ i, (m.supClosure hC) (f i) ≤ ∑ u ∈ J, m u
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
f : Fin #J → Set α := disjointed fun j ↦ ↑(J.equivFin.symm j)
htJ : t ⊆ ⋃ i, f i
h1 : ∀ (j : Fin #J), f j ∈ supClosure C
h2 : Pairwise (Disjoint on f)
h3 : ⋃ i, f i ∈ supClosure C
⊢ m t ≤ ∑ u ∈ J, m u

Tactic:
grw [← m.supClosure_apply_of_mem hC ht,
    addContent_mono hC.isSetRing_supClosure.isSetSemiring (subset_supClosure ht) h3 htJ,
    addContent_iUnion h1 h2 h3, ← J.sum_attach, Finset.attach_eq_univ, ← J.equivFin.symm.sum_comp]

Goal state after:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
f : Fin #J → Set α := disjointed fun j ↦ ↑(J.equivFin.symm j)
htJ : t ⊆ ⋃ i, f i
h1 : ∀ (j : Fin #J), f j ∈ supClosure C
h2 : Pairwise (Disjoint on f)
h3 : ⋃ i, f i ∈ supClosure C
⊢ ∑ i, (m.supClosure hC) (f i) ≤ ∑ i, m ↑(J.equivFin.symm i)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G✝ : Type u_2
inst✝² : AddCommMonoid G✝
m m' : AddContent G✝ C
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)),
    ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} →
      (↑I).PairwiseDisjoint id →
        ⋃₀ ↑I ∈ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} → #I = n → onIocAux f (⋃₀ ↑I) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I).PairwiseDisjoint id
hn : #I = n + 1
u : α
huv : u ≤ u
h'uv : ⋃₀ ↑I = Set.Ioc u u
⊢ onIocAux f (Set.Ioc u u) = ∑ u ∈ I, 0

Tactic:
simp [onIocAux_empty f]

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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
hm_ne_top : ∀ s ∈ C, m s ≠ ∞
s t : Set α
hs : s ∈ C
ht : t ∈ C
hts : t ⊆ s
⊢ m (s \ t) = m s - m t

Tactic:
by
  have h_union : m (t ∪ s \ t) = m t + m (s \ t) :=
    addContent_union hC ht (hC.sdiff_mem hs ht) disjoint_sdiff_self_right
  simp_rw [Set.union_sdiff_self, Set.union_eq_right.mpr hts] at h_union
  rw [h_union, ENNReal.add_sub_cancel_left (hm_ne_top _ ht)]

Goal state after:
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
⊢ ⋂ n, s n = ∅

Tactic:
· simp_rw [s, Set.sdiff_eq]
      rw [Set.iInter_inter_distrib, Set.iInter_const, ← Set.compl_iUnion, Set.iUnion_accumulate]
      exact Set.inter_compl_self _

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
e : V ≃ₗ[K] V
he :
  ¬1 < finrank K (V ⧸ (↑e).fixedSubmodule) ∨
    ¬e.fixedReduce ≠ 1 ∨ ¬∃ a, ∀ (x : V ⧸ (↑e).fixedSubmodule), e.fixedReduce x = a • x
⊢ e ∈ transvections K V ^ (finrank K (V ⧸ (↑e).fixedSubmodule) - 1) * dilatransvections K V

Tactic:
push Not at he

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
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1 ∨ e.fixedReduce = 1 ∨ ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
⊢ e ∈ transvections K V ^ (finrank K (V ⧸ (↑e).fixedSubmodule) - 1) * dilatransvections K V
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case hd
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
ι : Type u_4
s : Set ι
f : ι → Set α
hs : s.Countable
hd : s.Pairwise (Disjoint on f)
h : ∀ b ∈ s, MeasurableSet (f b)
this : Encodable ↑s
⊢ Pairwise (Disjoint on fun i ↦ f ↑i)

Tactic:
· exact hd.on_injective Subtype.coe_injective fun x => x.2

Goal state after:
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)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      blimsup (fun i ↦ cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ cthickening (r i) (s i)) atTop p
r' : ℕ → ℝ := fun i ↦ if 0 < r i then r i else 1 / (↑i + 1)
hr' : Tendsto r' atTop (𝓝[>] 0)
h₀ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)
h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)
h₂ : ∀ (i : ℕ), p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i)
hp : p = fun i ↦ p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0
⊢ ((blimsup (fun x ↦ cthickening (M * r' x) (s x)) atTop fun x ↦ p x ∧ 0 < r x) ∪
      blimsup (fun i ↦ cthickening (M * r i) (s i)) atTop fun i ↦ p i ∧ r i ≤ 0) =ᵐ[μ]
    (blimsup (fun x ↦ cthickening (r' x) (s x)) atTop fun x ↦ p x ∧ 0 < r x) ∪
      blimsup (fun i ↦ cthickening (r i) (s i)) atTop fun i ↦ p i ∧ r i ≤ 0

Tactic:
blimsup_congr (Eventually.of_forall h₂)

Goal state after:
α : 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)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      blimsup (fun i ↦ cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ cthickening (r i) (s i)) atTop p
r' : ℕ → ℝ := fun i ↦ if 0 < r i then r i else 1 / (↑i + 1)
hr' : Tendsto r' atTop (𝓝[>] 0)
h₀ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)
h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)
h₂ : ∀ (i : ℕ), p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i)
hp : p = fun i ↦ p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0
⊢ ((blimsup (fun x ↦ cthickening (M * r' x) (s x)) atTop fun x ↦ p x ∧ 0 < r x) ∪
      blimsup (fun x ↦ cthickening (r x) (s x)) atTop fun x ↦ p x ∧ r x ≤ 0) =ᵐ[μ]
    (blimsup (fun x ↦ cthickening (r' x) (s x)) atTop fun x ↦ p x ∧ 0 < r x) ∪
      blimsup (fun i ↦ cthickening (r i) (s i)) atTop fun i ↦ p i ∧ r i ≤ 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ HasSum (fun i ↦ (μ (f i)).toReal) (∑' (a : ℕ), (μ (f a)).toReal)

pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ ∀ (a : ℕ), μ (f a) ≠ ∞

Tactic:
exacts [(summable_measure_toReal hf₁ hf₂).hasSum, fun _ ↦ measure_ne_top _ _]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ :
  ∀ (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (f (Fin.last n))) p μ ≤ ENNReal.ofReal ε
i : Fin (n + 1)
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ↑i < n
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
(_ : f i = g ⟨i.val, hi⟩)

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ :
  ∀ (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (f (Fin.last n))) p μ ≤ ENNReal.ofReal ε
i : Fin (n + 1)
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ↑i < n
⊢ eLpNorm (s.indicator (g ⟨↑i, hi⟩)) p μ ≤ ENNReal.ofReal ε

α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ :
  ∀ (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (f (Fin.last n))) p μ ≤ ENNReal.ofReal ε
i : Fin (n + 1)
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ↑i < n
⊢ f i = g ⟨↑i, hi⟩
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : 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
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → v t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → w t = 0
t : Set α
hst : t ⊆ sᶜ
ht : ¬MeasurableSet t
⊢ w t = 0

Tactic:
· exact not_measurable w ht

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
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
hfint : ¬Integrable f μ
⊢ |μ[f | m]| ≤ᵐ[μ] μ[|f| | m]

pp: case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
hfint : Integrable f μ
⊢ |μ[f | m]| ≤ᵐ[μ] μ[|f| | m]

Tactic:
· simp only [condExp_of_not_integrable hfint, abs_zero]
    apply condExp_nonneg
    filter_upwards with a using abs_nonneg (f a)

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
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
hfint : Integrable f μ
⊢ |μ[f | m]| ≤ᵐ[μ] μ[|f| | m]
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
R : Type u_2
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0
c : R
μ : FiniteMeasure Ω
x✝ : Set Ω
⊢ (c • μ) x✝ = (c • ⇑μ) x✝

Tactic:
simp [← ENNReal.coe_inj, ENNReal.coe_smul]

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i ↦ ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))

Tactic:
simp [tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds,
    FiniteMeasure.tendsto_iff_forall_integral_tendsto]

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

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
f_le_g : ⇑f ≤ ⇑g
⊢ μ.testAgainstNN f ≤ μ.testAgainstNN g

Tactic:
simp only [← ENNReal.coe_le_coe, testAgainstNN_coe_eq]
  gcongr
  apply f_le_g

Goal state after:
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
f : α → E
p : ℝ≥0∞
hp : 1 ≤ p
hf : MemLp f p μ
⊢ lpNorm μ[f | m] p μ ≤ lpNorm f p μ

Tactic:
by_cases NeZero μ

Goal state after:
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 μ
⊢ lpNorm μ[f | m] p μ ≤ lpNorm f p μ

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