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

Goal state before:
pp: case h₁
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := ⋯
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
⊢ ∀ i ∈ b.support, ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b i ∈ U → ∃ j, u j ∈ U

pp: case h₂
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := ⋯
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
⊢ ∀ (i j k : ι),
    P.root k = P.root i + P.root j →
      (∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b i ∈ U → ∃ j, u j ∈ U) →
        j ∈ b.support → ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b k ∈ U → ∃ j, u j ∈ U

Tactic:
· intro j hj U hj'
      let f' : lieAlgebra b := ⟨f ⟨j, hj⟩, f_mem_lieAlgebra _⟩
      have : ⁅f', v b j⁆ = u ⟨j, hj⟩ := f_lie_v_same ⟨j, hj⟩
      replace this : u ⟨j, hj⟩ ∈ U := by
        rw [← this]
        exact U.lie_mem (x := f') hj'
      exact ⟨⟨j, hj⟩, this⟩

Goal state after:
case h₂
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := ⋯
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
⊢ ∀ (i j k : ι),
    P.root k = P.root i + P.root j →
      (∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b i ∈ U → ∃ j, u j ∈ U) →
        j ∈ b.support → ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b k ∈ U → ∃ j, u j ∈ U
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
⊢ Function.Bijective ⇑(SymmetricAlgebra.lift f)

Tactic:
exact h ▸ e.bijective

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Matrix

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
ι : Type u_7
κ : Type u_8
τ : Type u_9
inst✝¹² : DecidableEq ι
inst✝¹¹ : DecidableEq κ
inst✝¹⁰ : DecidableEq τ
inst✝⁹ : Fintype ι
inst✝⁸ : Fintype κ
inst✝⁷ : Fintype τ
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
⊢ (toMatrix ((bM.tensorProduct bN).tensorProduct bP) (bM.tensorProduct (bN.tensorProduct bP)))
      ↑(TensorProduct.assoc R M N P) =
    submatrix 1 _root_.id ⇑(Equiv.prodAssoc ι κ τ)

Tactic:
by
  ext ⟨i, j, k⟩ ⟨⟨i', j'⟩, k'⟩
  simp only [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe, assoc_tmul,
    Basis.tensorProduct_repr_tmul_apply, Basis.repr_self, Finsupp.single_apply, @eq_comm _ k',
    @eq_comm _ j', smul_eq_mul, mul_ite, mul_one, mul_zero, ← ite_and, @eq_comm _ i',
    submatrix_apply, Matrix.one_apply, id_eq, Equiv.prodAssoc_apply, Prod.mk.injEq]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
hJI : J ⊆ I
this : univ = Finset.restrict₂ hJI ⁻¹' univ
⊢ (Measure.map (Finset.restrict₂ hJI) (P I)) univ = (P J) univ

pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
hJI : J ⊆ I
this : univ = Finset.restrict₂ hJI ⁻¹' univ
⊢ MeasurableSpace ((i : ↥J) → α ↑i)

pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
hJI : J ⊆ I
this : univ = Finset.restrict₂ hJI ⁻¹' univ
⊢ Measurable (Finset.restrict₂ hJI)

Tactic:
· rw [hP I J hJI]

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
hJI : J ⊆ I
this : univ = Finset.restrict₂ hJI ⁻¹' univ
⊢ Measurable (Finset.restrict₂ hJI)
Module: Mathlib.MeasureTheory.Constructions.Projective

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
hP : IsProjectiveMeasureFamily P
I J : Finset ι
⊢ (P I) univ = (P J) univ

Tactic:
by
  classical
  rw [← hP.measure_univ_eq_of_subset I.subset_union_left,
    ← hP.measure_univ_eq_of_subset (I.subset_union_right (s₂ := J))]

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

Goal state before:
pp: case pos
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
hji : j = i
⊢ MeasurableSet ((fun j ↦ if hji : j = i then ⋯.mpr t else univ) j)

pp: case neg
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
hji : ¬j = i
⊢ MeasurableSet ((fun j ↦ if hji : j = i then ⋯.mpr t else univ) j)

Tactic:
· simp only [hji, eq_mpr_eq_cast, dif_pos]
      convert! ht
      simp only [cast_heq]

Goal state after:
case neg
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
hji : ¬j = i
⊢ MeasurableSet ((fun j ↦ if hji : j = i then ⋯.mpr t else univ) j)
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
⊢ SecondCountableTopology (WithTop ι)

Tactic:
rcases isEmpty_or_nonempty ι with hι | ⟨⟨x₀⟩⟩

Goal state after:
case inl
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
hι : IsEmpty ι
⊢ SecondCountableTopology (WithTop ι)

case inr
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
⊢ SecondCountableTopology (WithTop ι)
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case refine_2
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
⊢ ∀ (t : Set ((a : ι) → α a)),
    MeasurableSet t →
      (∃ I t_1, I.Countable ∧ t = I.domRestrict ⁻¹' t_1) → ∃ I t_1, I.Countable ∧ tᶜ = I.domRestrict ⁻¹' t_1

pp: case refine_3
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
⊢ ∀ (f : ℕ → Set ((a : ι) → α a)),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) →
        (∀ (i : ℕ), ∃ I t, I.Countable ∧ f i = I.domRestrict ⁻¹' t) →
          ∃ I t, I.Countable ∧ ⋃ i, f i = I.domRestrict ⁻¹' t

Tactic:
· rintro - - ⟨I, t, hI, rfl⟩
    exact ⟨I, tᶜ, hI, by simp⟩

Goal state after:
case refine_3
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
⊢ ∀ (f : ℕ → Set ((a : ι) → α a)),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) →
        (∀ (i : ℕ), ∃ I t, I.Countable ∧ f i = I.domRestrict ⁻¹' t) →
          ∃ I t, I.Countable ∧ ⋃ i, f i = I.domRestrict ⁻¹' t
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
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ∑ u ∈ insert s (hC.disjointOfDiff ht hs), m u = m s + ∑ i ∈ hC.disjointOfDiff ht hs, m i

Tactic:
rw [sum_insert]
    exact hC.notMem_disjointOfDiff ht hs

Goal state after:
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' m : AddContent G C
hC : IsSetSemiring C
⊢ m ∅ = 0

Tactic:
addContent_empty

Goal state after:
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' m : AddContent G C
hC : IsSetSemiring C
⊢ 0 = 0
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')
x✝ : IsEmpty ((i : ι) → α i) ∨ Nonempty ((i : ι) → α i)
⊢ (P (I ∪ J)) (S' ∪ T') = (P (I ∪ J)) S' + (P (I ∪ J)) T'

Tactic:
cases isEmpty_or_nonempty (Π i, α i) with

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

Goal state before:
pp: case h
α : 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
j : Fin #J
⊢ (m.supClosure hC) (f j) ≤ (m.supClosure hC) ↑(J.equivFin.symm j)

Tactic:
exact addContent_mono hC.isSetRing_supClosure.isSetSemiring (h1 j)
    (subset_supClosure (h_ss (J.equivFin.symm j).2)) (disjointed_subset _ j)

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

Goal state before:
pp: case a.inr.coe.coe.refine_1.coe
ι : 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 b : ι
hb✝ : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
w : ι
hw : ↑w ∈ ((⋂ z ∈ f, Ioi ↑z) ∩ ⋂ z ∈ g, Iio ↑z) ∩ Iio ⊤
⊢ ↑w ∈ Iio ↑a

Tactic:
simp only [mem_Iio, WithTop.coe_lt_coe]

Goal state after:
case a.inr.coe.coe.refine_1.coe
ι : 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 b : ι
hb✝ : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
w : ι
hw : ↑w ∈ ((⋂ z ∈ f, Ioi ↑z) ∩ ⋂ z ∈ g, Iio ↑z) ∩ Iio ⊤
⊢ w < a
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
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
⊢ m ∅ = 0

pp: case h
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
⊢ ∅ ∈ C

Tactic:
addContent_empty

Goal state after:
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
⊢ 0 = 0

case h
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
⊢ ∅ ∈ C
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 α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun i ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun i ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun i ↦ ⋃ j, ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬μ W = 0
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (fun j ↦ μ (W ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : ℕ → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun j ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun j ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
⊢ ∀ᶠ (j : ℕ) in atTop, μ (W ∩ closedBall (w j) (r₁ (f j))) / μ (closedBall (w j) (r₁ (f j))) ≤ ↑(1 - C⁻¹)

Tactic:
have h₂ : ∀ j, W ∩ B j ⊆ B j := fun j => inter_subset_right

Goal state after:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun i ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun i ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun i ↦ ⋃ j, ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬μ W = 0
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (fun j ↦ μ (W ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : ℕ → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun j ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun j ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
⊢ ∀ᶠ (j : ℕ) in atTop, μ (W ∩ closedBall (w j) (r₁ (f j))) / μ (closedBall (w j) (r₁ (f j))) ≤ ↑(1 - C⁻¹)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case insert
α : Type u_1
C : Set (Set α)
s✝ t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α}, s ∈ C → t ∈ C → Disjoint s t → m (s ∪ t) = m s + m t
s : Set α
I : Finset (Set α)
hsI : s ∉ I
h : ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → m (⋃₀ ↑I) = ∑ u ∈ I, m u
h_ss : ↑(insert s I) ⊆ C
h_dis : (↑(insert s I)).PairwiseDisjoint id
h_mem : ⋃₀ ↑(insert s I) ∈ C
⊢ m (⋃₀ ↑(insert s I)) = ∑ u ∈ insert s I, m u

Tactic:
rw [Finset.coe_insert] at *
      rw [Set.insert_subset_iff] at h_ss
      rw [Set.pairwiseDisjoint_insert_of_notMem] at h_dis
      swap; · exact hsI
      have h_sUnion_mem : ⋃₀ ↑I ∈ C := by
        rw [Set.sUnion_eq_biUnion]
        apply hC.biUnion_mem
        intro n hn
        exact h_ss.2 hn
      rw [Set.sUnion_insert, m_add h_ss.1 h_sUnion_mem (Set.disjoint_sUnion_right.mpr h_dis.2),
        Finset.sum_insert hsI, h h_ss.2 h_dis.1]
      rwa [Set.sUnion_insert] at h_mem

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 β
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 δ₁ δ₂)
⊢ eLpNorm (s.indicator (f i + g i)) p μ ≤ ENNReal.ofReal ε

Tactic:
Set.indicator_add'

Goal state after:
α : 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 δ₁ δ₂)
⊢ eLpNorm (s.indicator (f i) + s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
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‖}
⊢ (eLpNormEssSup f μ).toReal < ‖f x‖

Tactic:
refine lt_of_lt_of_le ?_ hx

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 μ).toReal < (eLpNormEssSup f μ + 1).toReal
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 α
hA : MeasurableSet A
hB : MeasurableSet B
h' : v (B \ A) = 0
⊢ v (A \ B ∪ A ∩ B) = v (A \ B) + v (A ∩ B)

Tactic:
by
      rw [of_union]
      · rw [disjoint_comm]
        exact Set.disjoint_of_subset_left A.inter_subset_right disjoint_sdiff_self_right
      · exact hA.diff hB
      · exact hA.inter hB

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (v.map f) s = v (f ⁻¹' s)

Tactic:
map,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (if hf : Measurable f then
        { measureOf' := fun s ↦ if MeasurableSet s then v (f ⁻¹' s) else 0, empty' := ⋯, not_measurable' := ⋯,
          m_iUnion' := ⋯ }
      else 0)
      s =
    v (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε

pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
· refine ⟨1, zero_lt_one, fun s _ _ => ?_⟩
    rw [(_ : f = 0)]
    · simp
    · ext x
      rw [Pi.zero_apply, ← norm_le_zero_iff]
      exact (lt_of_lt_of_le (hf x) hM).le

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h : n ≠ m
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅

Tactic:
rcases lt_or_gt_of_ne h with (h | h)

Goal state after:
case inl
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h✝ : n ≠ m
h : n < m
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅

case inr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h✝ : n ≠ m
h : m < n
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
i : Set α
hi : MeasurableSet i
⊢ (posPart 0).real i - (negPart 0).real i = 0 i

Tactic:
zero_posPart,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
i : Set α
hi : MeasurableSet i
⊢ Measure.real 0 i - (negPart 0).real i = 0 i