mathlib-initiative/mathlib-tactics huggingface dataset:
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
I : Finset (Set α)
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
h_mem : ⋃₀ ↑I ∈ C
⊢ m (⋃₀ ↑I) = ∑ u ∈ I, extend (fun x x_1 ↦ m x) u

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
I : Finset (Set α)
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
h_mem : ⋃₀ ↑I ∈ C
⊢ ⋃₀ ↑I ∈ C

Tactic:
]

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
I : Finset (Set α)
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
h_mem : ⋃₀ ↑I ∈ C
⊢ m (⋃₀ ↑I) = ∑ u ∈ I, extend (fun x x_1 ↦ m x) u

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
I : Finset (Set α)
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
h_mem : ⋃₀ ↑I ∈ C
⊢ ⋃₀ ↑I ∈ C
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
I : Finset (Set α)
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
h_mem : ⋃₀ ↑I ∈ C
⊢ ∑ u ∈ I, m u = ∑ u ∈ I, extend (fun x x_1 ↦ m x) u

Tactic:
]

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
I : Finset (Set α)
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
h_mem : ⋃₀ ↑I ∈ C
⊢ ∑ u ∈ I, m u = ∑ u ∈ I, extend (fun x x_1 ↦ m x) u
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
I : Finset (Set α)
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
h_mem : ⋃₀ ↑I ∈ C
s : Set α
hs : s ∈ I
⊢ m s = m s

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
I : Finset (Set α)
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
h_mem : ⋃₀ ↑I ∈ C
s : Set α
hs : s ∈ I
⊢ s ∈ C

Tactic:
]

Goal state after:
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
I : Finset (Set α)
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
h_mem : ⋃₀ ↑I ∈ C
s : Set α
hs : s ∈ I
⊢ s ∈ C
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case inl.refine_2
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
hn0 : n = 0
⊢ 1 ≤ 1

Tactic:
]

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 α
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
⊢ ∃ a, ∀ (b_1 : ℕ), a ≤ b_1 → M * r₁ (f b_1) ≤ r₂ (f b_1) → Disjoint (b b_1) (W ∩ B b_1)

Tactic:
]

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
⊢ ∃ a, ∀ (b_1 : ℕ), a ≤ b_1 → M * r₁ (f b_1) ≤ r₂ (f b_1) → Disjoint (b b_1) (W ∩ B b_1)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
hs : s ∈ C
⊢ m s = m s

pp: case h
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
hs : s ∈ C
⊢ s ∈ C

Tactic:
]

Goal state after:
case h
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
hs : s ∈ C
⊢ s ∈ C
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
hs : s ∉ C
⊢ ∞ = ∞

pp: case h
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
hs : s ∉ C
⊢ s ∉ C

Tactic:
]

Goal state after:
case h
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
hs : s ∉ C
⊢ s ∉ C
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case insert
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → (↑S).PairwiseDisjoint s → m (⋃ i ∈ S, s i) = ∑ i ∈ S, m (s i)
hs : ∀ n ∈ insert i S, s n ∈ C
hS : (↑(insert i S)).PairwiseDisjoint s
⊢ m (⋃ i_1 ∈ insert i S, s i_1) = m (s i) + ∑ x ∈ S, m (s x)

Tactic:
]

Goal state after:
case insert
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → (↑S).PairwiseDisjoint s → m (⋃ i ∈ S, s i) = ∑ i ∈ S, m (s i)
hs : ∀ n ∈ insert i S, s n ∈ C
hS : (↑(insert i S)).PairwiseDisjoint s
⊢ m (⋃ i_1 ∈ insert i S, s i_1) = m (s i) + ∑ x ∈ S, m (s x)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case insert
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → (↑S).PairwiseDisjoint s → m (⋃ i ∈ S, s i) = ∑ i ∈ S, m (s i)
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
hS : (↑S).PairwiseDisjoint s ∧ ∀ j ∈ ↑S, i ≠ j → Disjoint (s i) (s j)
⊢ m (s i ∪ ⋃ x ∈ ↑S, s x) = m (s i) + m (⋃ i ∈ S, s i)

Tactic:
]

Goal state after:
case insert
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → (↑S).PairwiseDisjoint s → m (⋃ i ∈ S, s i) = ∑ i ∈ S, m (s i)
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
hS : (↑S).PairwiseDisjoint s ∧ ∀ j ∈ ↑S, i ≠ j → Disjoint (s i) (s j)
⊢ m (s i ∪ ⋃ x ∈ ↑S, s x) = m (s i) + m (⋃ i ∈ S, s i)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case insert
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → (↑S).PairwiseDisjoint s → m (⋃ i ∈ S, s i) = ∑ i ∈ S, m (s i)
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
hS : (↑S).PairwiseDisjoint s ∧ ∀ j ∈ ↑S, i ≠ j → Disjoint (s i) (s j)
⊢ ∀ i_1 ∈ ↑S, Disjoint (s i) (s i_1)

Tactic:
]

Goal state after:
case insert
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → (↑S).PairwiseDisjoint s → m (⋃ i ∈ S, s i) = ∑ i ∈ S, m (s i)
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
hS : (↑S).PairwiseDisjoint s ∧ ∀ j ∈ ↑S, i ≠ j → Disjoint (s i) (s j)
⊢ ∀ i_1 ∈ ↑S, Disjoint (s i) (s i_1)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case succ
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetRing C
s : ℕ → Set α
hs_disj : Pairwise (Disjoint on s)
hsC : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : m (accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i)
⊢ m (accumulate s n) + m (s (n + 1)) = m (accumulate s n) + m (s (n + 1))

pp: case succ
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetRing C
s : ℕ → Set α
hs_disj : Pairwise (Disjoint on s)
hsC : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : m (accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i)
⊢ Disjoint (accumulate s n) (s (n + 1))

pp: α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetRing C
s : ℕ → Set α
hs_disj : Pairwise (Disjoint on s)
hsC : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : m (accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i)
⊢ accumulate s n ∈ C

Tactic:
]

Goal state after:
case succ
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetRing C
s : ℕ → Set α
hs_disj : Pairwise (Disjoint on s)
hsC : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : m (accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i)
⊢ Disjoint (accumulate s n) (s (n + 1))

α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetRing C
s : ℕ → Set α
hs_disj : Pairwise (Disjoint on s)
hsC : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : m (accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i)
⊢ accumulate s n ∈ 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
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
j : ℕ
hj : i ≤ j
hj' : M * r₁ (f j) ≤ r₂ (f j)
⊢ b j ⊆ Z i

Tactic:
]

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 : ℕ
hj : i ≤ j
hj' : M * r₁ (f j) ≤ r₂ (f j)
⊢ b j ⊆ Z i
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:
]

Goal state after:
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
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
⊢ auxTransvection hf ∈ transvections K V

Tactic:
]

Goal state after:
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
⊢ auxTransvection hf ∈ transvections K V
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 : s ∈ C ∧ ↑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:
]

Goal state after:
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 : s ∈ C ∧ ↑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
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 : s ∈ C ∧ ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id ∧ ∀ j ∈ ↑I, Disjoint (id s) (id j)
h_mem : ⋃₀ insert s ↑I ∈ C
⊢ m (⋃₀ insert s ↑I) = ∑ u ∈ insert s I, m u

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 : s ∈ C ∧ ↑I ⊆ C
h_dis : (insert s ↑I).PairwiseDisjoint id
h_mem : ⋃₀ insert s ↑I ∈ C
⊢ s ∉ ↑I

Tactic:
]

Goal state after:
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 : s ∈ C ∧ ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id ∧ ∀ j ∈ ↑I, Disjoint (id s) (id j)
h_mem : ⋃₀ insert s ↑I ∈ C
⊢ m (⋃₀ insert s ↑I) = ∑ u ∈ insert s I, m u

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 : s ∈ C ∧ ↑I ⊆ C
h_dis : (insert s ↑I).PairwiseDisjoint id
h_mem : ⋃₀ insert s ↑I ∈ C
⊢ s ∉ ↑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
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
⊢ (↑e).fixedSubmodule ⊔ K ∙ v ⊔ K ∙ (e v - v) < ⊤

Tactic:
]

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 : ∀ (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
⊢ (↑e).fixedSubmodule ⊔ K ∙ v ⊔ K ∙ (e v - v) < ⊤