-- Mathlib/MeasureTheory/Measure/Dirac.lean
/-- Dirac delta measures at two points are equal if every measurable set contains either both or
neither of the points. -/
lemma dirac_eq_dirac_iff_forall_mem_iff_mem {x y : α} :
    Measure.dirac x = Measure.dirac y ↔ ∀ A, MeasurableSet A → (x ∈ A ↔ y ∈ A)

Proof state:
case mpr.h
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
⊢ (dirac x) A = (dirac y) A

Tactic:
by_cases x_in_A : x ∈ A

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∈ A
⊢ (dirac x) A = (dirac y) A

case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∉ A
⊢ (dirac x) A = (dirac y) A

Proof state:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
⊢ dirac x = dirac y → ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)

Tactic:
intro h A A_mble

Result:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
⊢ x ∈ A ↔ y ∈ A

Proof state:
case mpr
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
⊢ (∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)) → dirac x = dirac y

Tactic:
intro h

Result:
case mpr
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
⊢ dirac x = dirac y

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
obs : A.indicator 1 x = A.indicator 1 y
x_in_A : x ∈ A
⊢ x ∈ A ↔ y ∈ A

Tactic:
simpa only [x_in_A, indicator_of_mem, Pi.one_apply, true_iff, Eq.comm (a := (1 : ℝ≥0∞)),
            indicator_eq_one_iff_mem] using obs

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
⊢ dirac x = dirac y

Tactic:
ext A A_mble

Result:
case mpr.h
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
⊢ (dirac x) A = (dirac y) A

Proof state:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
obs : (fun μ => μ A) (dirac x) = (fun μ => μ A) (dirac y)
⊢ x ∈ A ↔ y ∈ A

Tactic:
simp only [Measure.dirac_apply' _ A_mble] at obs

Result:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
obs : A.indicator 1 x = A.indicator 1 y
⊢ x ∈ A ↔ y ∈ A

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
⊢ dirac x = dirac y ↔ ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
⊢ dirac x = dirac y → ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)

case mpr
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
⊢ (∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)) → dirac x = dirac y

Proof state:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
obs : A.indicator 1 x = A.indicator 1 y
⊢ x ∈ A ↔ y ∈ A

Tactic:
by_cases x_in_A : x ∈ A

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
obs : A.indicator 1 x = A.indicator 1 y
x_in_A : x ∈ A
⊢ x ∈ A ↔ y ∈ A

case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
obs : A.indicator 1 x = A.indicator 1 y
x_in_A : x ∉ A
⊢ x ∈ A ↔ y ∈ A

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∉ A
y_notin_A : y ∉ A
⊢ (dirac x) A = (dirac y) A

Tactic:
simp only [Measure.dirac_apply' _ A_mble, x_in_A, y_notin_A,
           not_false_eq_true, indicator_of_not_mem]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
obs : A.indicator 1 x = A.indicator 1 y
x_in_A : x ∉ A
⊢ x ∈ A ↔ y ∈ A

Tactic:
simpa only [x_in_A, indicator_of_not_mem, Eq.comm (a := (0 : ℝ≥0∞)), indicator_apply_eq_zero,
            false_iff, not_false_eq_true, Pi.one_apply, one_ne_zero, imp_false] using obs

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∈ A
⊢ (dirac x) A = (dirac y) A

Tactic:
simp only [Measure.dirac_apply' _ A_mble, x_in_A, indicator_of_mem, Pi.one_apply,
           (h A A_mble).mp x_in_A]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∉ A
⊢ y ∉ A

Tactic:
simp_all only [false_iff, not_false_eq_true]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∉ A
⊢ (dirac x) A = (dirac y) A

Tactic:
have y_notin_A : y ∉ A := by simp_all only [false_iff, not_false_eq_true]

Result:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∉ A
y_notin_A : y ∉ A
⊢ (dirac x) A = (dirac y) A

Proof state:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
⊢ x ∈ A ↔ y ∈ A

Tactic:
have obs := congr_arg (fun μ ↦ μ A) h

Result:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
obs : (fun μ => μ A) (dirac x) = (fun μ => μ A) (dirac y)
⊢ x ∈ A ↔ y ∈ A