Theorem: MeasureTheory.ext_iff_measureReal_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
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
⊢ μ1 = μ2 ↔ ∀ (x : S), μ1.real {x} = μ2.real {x}
Tactic:
rw [Measure.ext_iff_singleton]
State after:
ι : 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
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
⊢ (∀ (x : S), μ1 {x} = μ2 {x}) ↔ ∀ (x : S), μ1.real {x} = μ2.real {x}

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
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
⊢ (∀ (x : S), μ1 {x} = μ2 {x}) ↔ ∀ (x : S), μ1.real {x} = μ2.real {x}
Tactic:
congr! with x
State after:
case a.h.a
ι : 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
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
⊢ μ1 {x} = μ2 {x} ↔ μ1.real {x} = μ2.real {x}

State before:
case a.h.a
ι : 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
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
⊢ μ1 {x} = μ2 {x} ↔ μ1.real {x} = μ2.real {x}
Tactic:
have h1 : μ1 {x} ≠ ⊤ := by finiteness
State after:
case a.h.a
ι : 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
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
h1 : μ1 {x} ≠ ⊤
⊢ μ1 {x} = μ2 {x} ↔ μ1.real {x} = μ2.real {x}

State before:
case a.h.a
ι : 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
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
h1 : μ1 {x} ≠ ⊤
⊢ μ1 {x} = μ2 {x} ↔ μ1.real {x} = μ2.real {x}
Tactic:
have h2 : μ2 {x} ≠ ⊤ := by finiteness
State after:
case a.h.a
ι : 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
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
h1 : μ1 {x} ≠ ⊤
h2 : μ2 {x} ≠ ⊤
⊢ μ1 {x} = μ2 {x} ↔ μ1.real {x} = μ2.real {x}

State before:
case a.h.a
ι : 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
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
h1 : μ1 {x} ≠ ⊤
h2 : μ2 {x} ≠ ⊤
⊢ μ1 {x} = μ2 {x} ↔ μ1.real {x} = μ2.real {x}
Tactic:
rw [measureReal_def, measureReal_def, ENNReal.toReal_eq_toReal_iff]
State after:
case a.h.a
ι : 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
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
h1 : μ1 {x} ≠ ⊤
h2 : μ2 {x} ≠ ⊤
⊢ μ1 {x} = μ2 {x} ↔ μ1 {x} = μ2 {x} ∨ μ1 {x} = 0 ∧ μ2 {x} = ⊤ ∨ μ1 {x} = ⊤ ∧ μ2 {x} = 0

State before:
case a.h.a
ι : 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
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
h1 : μ1 {x} ≠ ⊤
h2 : μ2 {x} ≠ ⊤
⊢ μ1 {x} = μ2 {x} ↔ μ1 {x} = μ2 {x} ∨ μ1 {x} = 0 ∧ μ2 {x} = ⊤ ∨ μ1 {x} = ⊤ ∧ μ2 {x} = 0
Tactic:
simp [h1, h2]
State after:
no goals

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
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
⊢ μ1 {x} ≠ ⊤
Tactic:
finiteness
State after:
no goals

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
inst✝¹ : IsFiniteMeasure μ1
inst✝ : IsFiniteMeasure μ2
x : S
h1 : μ1 {x} ≠ ⊤
⊢ μ2 {x} ≠ ⊤
Tactic:
finiteness
State after:
no goals