Theorem: MeasureTheory.Measure.ext_iff_singleton (Carleson/ToMathlib/MeasureReal.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
⊢ μ1 = μ2 ↔ ∀ (x : S), μ1 {x} = μ2 {x}
Tactic:
constructor
State after:
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
⊢ μ1 = μ2 → ∀ (x : S), μ1 {x} = μ2 {x}

case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
⊢ (∀ (x : S), μ1 {x} = μ2 {x}) → μ1 = μ2

State before:
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
⊢ μ1 = μ2 → ∀ (x : S), μ1 {x} = μ2 {x}
Tactic:
rintro rfl
State after:
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 : Measure S
⊢ ∀ (x : S), μ1 {x} = μ1 {x}

State before:
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 : Measure S
⊢ ∀ (x : S), μ1 {x} = μ1 {x}
Tactic:
simp
State after:
no goals

State before:
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
⊢ (∀ (x : S), μ1 {x} = μ2 {x}) → μ1 = μ2
Tactic:
intro h
State after:
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
h : ∀ (x : S), μ1 {x} = μ2 {x}
⊢ μ1 = μ2

State before:
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
h : ∀ (x : S), μ1 {x} = μ2 {x}
⊢ μ1 = μ2
Tactic:
ext s
State after:
case mpr.h
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
h : ∀ (x : S), μ1 {x} = μ2 {x}
s : Set S
a✝ : MeasurableSet s
⊢ μ1 s = μ2 s

State before:
case mpr.h
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
h : ∀ (x : S), μ1 {x} = μ2 {x}
s : Set S
a✝ : MeasurableSet s
⊢ μ1 s = μ2 s
Tactic:
have hs : Set.Finite s := Set.toFinite s
State after:
case mpr.h
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
h : ∀ (x : S), μ1 {x} = μ2 {x}
s : Set S
a✝ : MeasurableSet s
hs : s.Finite
⊢ μ1 s = μ2 s

State before:
case mpr.h
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
h : ∀ (x : S), μ1 {x} = μ2 {x}
s : Set S
a✝ : MeasurableSet s
hs : s.Finite
⊢ μ1 s = μ2 s
Tactic:
rw [← hs.coe_toFinset, ← Finset.sum_measure_singleton μ1, ← Finset.sum_measure_singleton μ2]
State after:
case mpr.h
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
h : ∀ (x : S), μ1 {x} = μ2 {x}
s : Set S
a✝ : MeasurableSet s
hs : s.Finite
⊢ ∑ x ∈ hs.toFinset, μ1 {x} = ∑ x ∈ hs.toFinset, μ2 {x}

State before:
case mpr.h
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
S : Type u_4
inst✝² : Fintype S
inst✝¹ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ1 μ2 : Measure S
h : ∀ (x : S), μ1 {x} = μ2 {x}
s : Set S
a✝ : MeasurableSet s
hs : s.Finite
⊢ ∑ x ∈ hs.toFinset, μ1 {x} = ∑ x ∈ hs.toFinset, μ2 {x}
Tactic:
simp_rw [h]
State after:
no goals