mathlib-initiative/mathlib-tactics huggingface dataset:
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'
⊢ cylinder I S = cylinder (I ∪ J) S'

Tactic:
;

Goal state after:
ι : 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'
⊢ cylinder I S = cylinder (I ∪ J) S'
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'
⊢ cylinder J T = cylinder (I ∪ J) T'

Tactic:
;

Goal state after:
ι : 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'
⊢ cylinder J T = cylinder (I ∪ J) T'
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
t : Set α
ht : t ∈ J'
this : t = ⋃ s ∈ J, s ∩ t
⊢ (↑J).PairwiseDisjoint fun i ↦ i ∩ t

Tactic:
exact hJdisj.mono fun _ ↦ by simp

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'
⊢ cylinder I S ∪ cylinder J T = cylinder (I ∪ J) (S' ∪ T')

Tactic:
;

Goal state after:
ι : 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'
⊢ cylinder I S ∪ cylinder J T = cylinder (I ∪ J) (S' ∪ T')
Module: Mathlib.MeasureTheory.Constructions.SimpleGraph

Goal state before:
pp: case mk
V : Type u_1
a✝ : Sym2 V
u v : V
⊢ Measurable fun x ↦ Quot.mk (Sym2.Rel V) (u, v) ∈ x.edgeSet

Tactic:
;

Goal state after:
case mk
V : Type u_1
a✝ : Sym2 V
u v : V
⊢ Measurable fun x ↦ Quot.mk (Sym2.Rel V) (u, v) ∈ x.edgeSet
Module: Mathlib.MeasureTheory.Constructions.SimpleGraph

Goal state before:
pp: case mk
V : Type u_1
a✝ : Sym2 V
u v : V
⊢ Measurable fun x ↦ x.Adj u v

Tactic:
;

Goal state after:
case mk
V : Type u_1
a✝ : Sym2 V
u v : V
⊢ Measurable fun x ↦ x.Adj u v
Module: Mathlib.MeasureTheory.Constructions.SimpleGraph

Goal state before:
pp: V : Type u_1
⊢ ∀ (u v : V), Measurable fun ω ↦ s(u, v) ∈ ω ∧ ¬u = v

Tactic:
;

Goal state after:
V : Type u_1
⊢ ∀ (u v : V), Measurable fun ω ↦ s(u, v) ∈ ω ∧ ¬u = v
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inr.coe.coe.refine_2.hs
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
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
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] ((⋂ z ∈ f, Ioi ↑z) ∩ ⋂ z ∈ g, Iio ↑z)

pp: case a.inr.coe.coe.refine_2.ht
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
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
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio ⊤)

Tactic:
;

Goal state after:
case a.inr.coe.coe.refine_2.hs
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
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
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] ((⋂ z ∈ f, Ioi ↑z) ∩ ⋂ z ∈ g, Iio ↑z)

case a.inr.coe.coe.refine_2.ht
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
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
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio ⊤)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
i : ℕ
left✝¹ : i ∈ ↑I
j : ℕ
left✝ : j ∈ ↑I
hst : f i ≠ f j
h_eq : i = j
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
i : ℕ
left✝¹ : i ∈ ↑I
j : ℕ
left✝ : j ∈ ↑I
hst : f i ≠ f j
h_eq : i = j
⊢ False
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
i : ℕ
left✝¹ : i ∈ ↑I
j : ℕ
left✝ : j ∈ ↑I
hst : f j ≠ f j
h_eq : i = j
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
i : ℕ
left✝¹ : i ∈ ↑I
j : ℕ
left✝ : j ∈ ↑I
hst : f j ≠ f j
h_eq : i = j
⊢ False
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
⊢ IsOpen[TopologicalSpace.instWithTopOfOrderTopology] (Iio ⊤)

Tactic:
;

Goal state after:
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
⊢ IsOpen[TopologicalSpace.instWithTopOfOrderTopology] (Iio ⊤)
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : OrderTop ι
x✝ : WithTop ι
⊢ x✝ ∈ {⊤} ↔ x✝ ∈ Ioi ↑⊤

Tactic:
;

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : OrderTop ι
x✝ : WithTop ι
⊢ x✝ ∈ {⊤} ↔ x✝ ∈ Ioi ↑⊤
Module: Mathlib.MeasureTheory.Function.AEEqFun.DomAct

Goal state before:
pp: case mk
M : Type u_3
N : Type u_1
α : Type u_4
β : Type u_2
inst✝⁷ : MeasurableSpace N
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : SMul M α
inst✝³ : MeasurableConstSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : SMul N β
inst✝ : ContinuousConstSMul N β
m✝ : Mᵈᵐᵃ
n✝ : N
a✝¹ : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ m✝ • n✝ • Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝ = n✝ • m✝ • Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝

Tactic:
;

Goal state after:
case mk
M : Type u_3
N : Type u_1
α : Type u_4
β : Type u_2
inst✝⁷ : MeasurableSpace N
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : SMul M α
inst✝³ : MeasurableConstSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : SMul N β
inst✝ : ContinuousConstSMul N β
m✝ : Mᵈᵐᵃ
n✝ : N
a✝¹ : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ m✝ • n✝ • Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝ = n✝ • m✝ • Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝
Module: Mathlib.MeasureTheory.Function.AEEqFun.DomAct

Goal state before:
pp: case mk.mk
M : Type ?u.15
N : Type ?u.6
α : Type ?u.8
β : Type ?u.12
inst✝⁷ : MeasurableSpace N
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : SMul M α
inst✝³ : MeasurableConstSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : AddMonoid β
inst✝ : ContinuousAdd β
a✝² : Mᵈᵐᵃ
x✝ : α →ₘ[μ] β
a✝¹ : { f // AEStronglyMeasurable f μ }
y✝ : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ a✝² • (Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝¹ + Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝) =
    a✝² • Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝¹ + a✝² • Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝

Tactic:
;

Goal state after:
case mk.mk
M : Type ?u.15
N : Type ?u.6
α : Type ?u.8
β : Type ?u.12
inst✝⁷ : MeasurableSpace N
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : SMul M α
inst✝³ : MeasurableConstSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : AddMonoid β
inst✝ : ContinuousAdd β
a✝² : Mᵈᵐᵃ
x✝ : α →ₘ[μ] β
a✝¹ : { f // AEStronglyMeasurable f μ }
y✝ : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ a✝² • (Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝¹ + Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝) =
    a✝² • Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝¹ + a✝² • Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝
Module: Mathlib.MeasureTheory.Function.AEEqFun.DomAct

Goal state before:
pp: case mk.mk
M : Type ?u.14
N : Type ?u.6
α : Type ?u.8
β : Type ?u.12
inst✝⁸ : MeasurableSpace N
inst✝⁷ : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : Monoid M
inst✝⁴ : MulAction M α
inst✝³ : MeasurableConstSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : Monoid β
inst✝ : ContinuousMul β
r✝ : Mᵈᵐᵃ
x✝ : α →ₘ[μ] β
a✝¹ : { f // AEStronglyMeasurable f μ }
y✝ : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ r✝ • (Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝¹ * Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝) =
    r✝ • Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝¹ * r✝ • Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝

Tactic:
;

Goal state after:
case mk.mk
M : Type ?u.14
N : Type ?u.6
α : Type ?u.8
β : Type ?u.12
inst✝⁸ : MeasurableSpace N
inst✝⁷ : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : Monoid M
inst✝⁴ : MulAction M α
inst✝³ : MeasurableConstSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : Monoid β
inst✝ : ContinuousMul β
r✝ : Mᵈᵐᵃ
x✝ : α →ₘ[μ] β
a✝¹ : { f // AEStronglyMeasurable f μ }
y✝ : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ r✝ • (Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝¹ * Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝) =
    r✝ • Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝¹ * r✝ • Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
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:
;

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
⊢ ∅ ∈ C
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
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

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

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
⊢ ⋃₀ ↑I ∈ C

α : 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
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
⊢ s ∉ ↑I

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

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
⊢ s ∉ ↑I

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
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
⊢ 1 < n + 1

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
⊢ 1 < n + 1
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case refine_1
α : 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
⊢ Antitone s

Tactic:
intro i j hij x hxj

Goal state after:
case refine_1
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, m s ≠ ∞
hm_tendsto : ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n ↦ m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n ↦ (⋃ i, f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
i j : ℕ
hij : i ≤ j
x : α
hxj : x ∈ s j
⊢ x ∈ s i
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
hm : m ≤ mΩ
inst✝ : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun x ↦ (fs x) ω) atTop (𝓝 (f ω))
hμ : μ = 0
⊢ 0[fun ω ↦ (B (f ω)) (g ω) | m] =ᶠ[⊥] fun ω ↦ (B (f ω)) (0[g | m] ω)

Tactic:
;

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
hm : m ≤ mΩ
inst✝ : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun x ↦ (fs x) ω) atTop (𝓝 (f ω))
hμ : μ = 0
⊢ 0[fun ω ↦ (B (f ω)) (g ω) | m] =ᶠ[⊥] fun ω ↦ (B (f ω)) (0[g | m] ω)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M ↦ {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x ↦ ‖f x‖) μ
⊢ Tendsto (fun n ↦ ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a - 0‖ ∂μ) atTop (𝓝 0)

Tactic:
refine tendsto_lintegral_norm_of_dominated_convergence hmeas hbound ?_ htendsto

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M ↦ {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x ↦ ‖f x‖) μ
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a‖ ≤ ‖f a‖