-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem mkMetric_apply (m : ℝ≥0∞ → ℝ≥0∞) (s : Set X) :
    mkMetric m s =
      ⨆ (r : ℝ≥0∞) (_ : 0 < r),
        ⨅ (t : ℕ → Set X) (_ : s ⊆ iUnion t) (_ : ∀ n, diam (t n) ≤ r),
          ∑' n, ⨆ _ : (t n).Nonempty, m (diam (t n))

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
⊢ ∑' (n : ℕ), ⨆ (_ : (id t n).Nonempty), ⨅ (_ : diam (id t n) ≤ r), m (diam (id t n)) =
    ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ id r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n))

Tactic:
dsimp

Result:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ r), m (diam (t n)) =
    ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n))

Proof state:
case neg
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ¬∀ (n : ℕ), diam (t n) ≤ r
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ r), m (diam (t n)) = ⊤

Tactic:
push_neg at htr

Result:
case neg
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ∃ n, r < diam (t n)
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ r), m (diam (t n)) = ⊤

Proof state:
case pos
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ∀ (n : ℕ), diam (t n) ≤ r
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ r), m (diam (t n)) =
    ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n))

Tactic:
rw [iInf_eq_if, if_pos htr]

Result:
case pos
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ∀ (n : ℕ), diam (t n) ≤ r
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ r), m (diam (t n)) =
    ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n))

Proof state:
case pos
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ∀ (n : ℕ), diam (t n) ≤ r
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ r), m (diam (t n)) =
    ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n))

Tactic:
congr 1 with n : 1

Result:
case pos.e_f.h
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ∀ (n : ℕ), diam (t n) ≤ r
n : ℕ
⊢ ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ r), m (diam (t n)) = ⨆ (_ : (t n).Nonempty), m (diam (t n))

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
⊢ ⨆ i,
      ⨆ (_ : i > 0),
        ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ i), m (diam (t n)) =
    ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t, ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n))

Tactic:
refine
  surjective_id.iSup_congr id fun r =>
    iSup_congr_Prop Iff.rfl fun _ =>
      surjective_id.iInf_congr _ fun t => iInf_congr_Prop Iff.rfl fun ht => ?_

Result:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
⊢ ∑' (n : ℕ), ⨆ (_ : (id t n).Nonempty), ⨅ (_ : diam (id t n) ≤ r), m (diam (id t n)) =
    ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ id r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n))

Proof state:
case neg
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ∃ n, r < diam (t n)
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ r), m (diam (t n)) = ⊤

Tactic:
rcases htr with ⟨n, hn⟩

Result:
case neg.intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
n : ℕ
hn : r < diam (t n)
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ r), m (diam (t n)) = ⊤

Proof state:
case neg.intro.hc
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
n : ℕ
hn : r < diam (t n)
⊢ (t n).Nonempty

Tactic:
rcases diam_pos_iff.1 ((zero_le r).trans_lt hn) with ⟨x, hx, -⟩

Result:
case neg.intro.hc.intro.intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
n : ℕ
hn : r < diam (t n)
x : X
hx : x ∈ t n
⊢ (t n).Nonempty

Proof state:
case neg
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ¬∀ (n : ℕ), diam (t n) ≤ r
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ r), m (diam (t n)) =
    ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n))

Tactic:
rw [iInf_eq_if, if_neg htr]

Result:
case neg
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ¬∀ (n : ℕ), diam (t n) ≤ r
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ r), m (diam (t n)) = ⊤

Proof state:
case neg.intro.hc.intro.intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
n : ℕ
hn : r < diam (t n)
x : X
hx : x ∈ t n
⊢ (t n).Nonempty

Tactic:
exact ⟨x, hx⟩

Result:
no goals

Proof state:
case pos.e_f.h
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ∀ (n : ℕ), diam (t n) ≤ r
n : ℕ
⊢ ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ r), m (diam (t n)) = ⨆ (_ : (t n).Nonempty), m (diam (t n))

Tactic:
simp only [iInf_eq_if, htr n, id, if_true, iSup_and']

Result:
no goals

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
⊢ (mkMetric m) s =
    ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t, ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n))

Tactic:
simp only [← OuterMeasure.coe_mkMetric, OuterMeasure.mkMetric, OuterMeasure.mkMetric',
  OuterMeasure.iSup_apply, OuterMeasure.mkMetric'.pre, OuterMeasure.boundedBy_apply, extend]

Result:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
⊢ ⨆ i,
      ⨆ (_ : i > 0),
        ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ i), m (diam (t n)) =
    ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t, ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n))

Proof state:
case neg.intro.hnc
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
n : ℕ
hn : r < diam (t n)
⊢ ¬diam (t n) ≤ r

Tactic:
exact hn.not_le

Result:
no goals