-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem isometry_comap_mkMetric (m : ℝ≥0∞ → ℝ≥0∞) {f : X → Y} (hf : Isometry f)
    (H : Monotone m ∨ Surjective f) : comap f (mkMetric m) = mkMetric m

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
⊢ ⨆ i, ⨆ (_ : i > 0), (comap f) (boundedBy (extend fun s x => m (diam s))) =
    ⨆ r, ⨆ (_ : r > 0), boundedBy (extend fun s x => m (diam s))

Tactic:
refine surjective_id.iSup_congr id fun ε => surjective_id.iSup_congr id fun hε => ?_

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
⊢ (comap f) (boundedBy (extend fun s x => m (diam s))) = boundedBy (extend fun s x => m (diam s))

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
⊢ (boundedBy fun s => extend (fun s x => m (diam s)) (f '' s)) = boundedBy (extend fun s x => m (diam s))

Tactic:
congr with s : 1

Result:
case e_m.h
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
s : Set X
⊢ extend (fun s x => m (diam s)) (f '' s) = extend (fun s x => m (diam s)) s

Proof state:
case e_m.h.hP
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
s : Set X
⊢ diam (f '' s) ≤ ε ↔ diam s ≤ id ε

Tactic:
simp [hf.ediam_image]

Result:
no goals

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
⊢ Monotone m → Monotone fun s => extend (fun s x => m (diam s)) ↑s

Tactic:
intro h_mono s t hst

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
h_mono : Monotone m
s t : { s // s.Nonempty }
hst : s ≤ t
⊢ (fun s => extend (fun s x => m (diam s)) ↑s) s ≤ (fun s => extend (fun s x => m (diam s)) ↑s) t

Proof state:
case e_m.h.hm
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
s : Set X
ha✝ : diam (f '' s) ≤ ε
hb✝ : diam s ≤ id ε
⊢ m (diam (f '' s)) = m (diam s)

Tactic:
simp [hf.injective.subsingleton_image_iff, hf.ediam_image]

Result:
no goals

Proof state:
case e_m.h
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
s : Set X
⊢ extend (fun s x => m (diam s)) (f '' s) = extend (fun s x => m (diam s)) s

Tactic:
apply extend_congr

Result:
case e_m.h.hP
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
s : Set X
⊢ diam (f '' s) ≤ ε ↔ diam s ≤ id ε

case e_m.h.hm
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
s : Set X
⊢ diam (f '' s) ≤ ε → diam s ≤ id ε → m (diam (f '' s)) = m (diam s)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
⊢ (comap f) (boundedBy (extend fun s x => m (diam s))) = boundedBy (extend fun s x => m (diam s))

Tactic:
rw [comap_boundedBy _ (H.imp _ id)]

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
⊢ (boundedBy fun s => extend (fun s x => m (diam s)) (f '' s)) = boundedBy (extend fun s x => m (diam s))

X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
⊢ Monotone m → Monotone fun s => extend (fun s x => m (diam s)) ↑s

Proof state:
case e_m.h.hm
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
s : Set X
⊢ diam (f '' s) ≤ ε → diam s ≤ id ε → m (diam (f '' s)) = m (diam s)

Tactic:
intros

Result:
case e_m.h.hm
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
s : Set X
ha✝ : diam (f '' s) ≤ ε
hb✝ : diam s ≤ id ε
⊢ m (diam (f '' s)) = m (diam s)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
h_mono : Monotone m
s t : { s // s.Nonempty }
hst : s ≤ t
ht : diam ↑t ≤ ε
⊢ ⨅ (_ : diam ↑s ≤ ε), m (diam ↑s) ≤ m (diam ↑t)

Tactic:
apply le_trans _ (h_mono (diam_mono hst))

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
h_mono : Monotone m
s t : { s // s.Nonempty }
hst : s ≤ t
ht : diam ↑t ≤ ε
⊢ ⨅ (_ : diam ↑s ≤ ε), m (diam ↑s) ≤ m (diam ((fun a => ↑a) s))

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
h_mono : Monotone m
s t : { s // s.Nonempty }
hst : s ≤ t
⊢ (fun s => extend (fun s x => m (diam s)) ↑s) s ≤ (fun s => extend (fun s x => m (diam s)) ↑s) t

Tactic:
simp only [extend, le_iInf_iff]

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
h_mono : Monotone m
s t : { s // s.Nonempty }
hst : s ≤ t
⊢ diam ↑t ≤ ε → ⨅ (_ : diam ↑s ≤ ε), m (diam ↑s) ≤ m (diam ↑t)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
⊢ (comap f) (mkMetric m) = mkMetric m

Tactic:
simp only [mkMetric, mkMetric', mkMetric'.pre, inducedOuterMeasure, comap_iSup]

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
⊢ ⨆ i, ⨆ (_ : i > 0), (comap f) (boundedBy (extend fun s x => m (diam s))) =
    ⨆ r, ⨆ (_ : r > 0), boundedBy (extend fun s x => m (diam s))

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
h_mono : Monotone m
s t : { s // s.Nonempty }
hst : s ≤ t
⊢ diam ↑t ≤ ε → ⨅ (_ : diam ↑s ≤ ε), m (diam ↑s) ≤ m (diam ↑t)

Tactic:
intro ht

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
h_mono : Monotone m
s t : { s // s.Nonempty }
hst : s ≤ t
ht : diam ↑t ≤ ε
⊢ ⨅ (_ : diam ↑s ≤ ε), m (diam ↑s) ≤ m (diam ↑t)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
h_mono : Monotone m
s t : { s // s.Nonempty }
hst : s ≤ t
ht : diam ↑t ≤ ε
⊢ ⨅ (_ : diam ↑s ≤ ε), m (diam ↑s) ≤ m (diam ((fun a => ↑a) s))

Tactic:
simp only [(diam_mono hst).trans ht, le_refl, ciInf_pos]

Result:
no goals