awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
m : ℕ := max (max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))) (z.fst (β := fun (n : ℕ) ↦ X n))
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hz : z.fst (β := fun (n : ℕ) ↦ X n) ≤ m
⊢ inductiveLimitDist (X := X) f x z =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hz (fun {k : ℕ} ↦ f k) (z.snd (β := fun (n : ℕ) ↦ X n)))

Tactic:
inductiveLimitDist_eq_dist I x z m hx hz

Premises used: Metric.inductiveLimitDist_eq_dist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
m : ℕ := max (max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))) (z.fst (β := fun (n : ℕ) ↦ X n))
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hz : z.fst (β := fun (n : ℕ) ↦ X n) ≤ m
⊢ dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hz (fun {k : ℕ} ↦ f k) (z.snd (β := fun (n : ℕ) ↦ X n))) ≤
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) +
      dist (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hz (fun {k : ℕ} ↦ f k) (z.snd (β := fun (n : ℕ) ↦ X n)))

Tactic:
(dist_triangle _ _ _)

Premises used: dist_triangle
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
m : ℕ := max (max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))) (z.fst (β := fun (n : ℕ) ↦ X n))
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hz : z.fst (β := fun (n : ℕ) ↦ X n) ≤ m
rw :
  dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) +
      dist (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hz (fun {k : ℕ} ↦ f k) (z.snd (β := fun (n : ℕ) ↦ X n))) =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) +
      inductiveLimitDist (X := X) f y z
rw₁ rw₂ :
  dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) +
      dist (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hz (fun {k : ℕ} ↦ f k) (z.snd (β := fun (n : ℕ) ↦ X n))) =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) +
      dist (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hz (fun {k : ℕ} ↦ f k) (z.snd (β := fun (n : ℕ) ↦ X n)))
⊢ dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) +
      dist (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hz (fun {k : ℕ} ↦ f k) (z.snd (β := fun (n : ℕ) ↦ X n))) =
    inductiveLimitDist (X := X) f x y + inductiveLimitDist (X := X) f y z

Tactic:
rw [inductiveLimitDist_eq_dist I x y m hx hy, inductiveLimitDist_eq_dist I y z m hy hz]

Premises used: Metric.inductiveLimitDist_eq_dist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
m : ℕ := max (max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))) (z.fst (β := fun (n : ℕ) ↦ X n))
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hz : z.fst (β := fun (n : ℕ) ↦ X n) ≤ m
inductiveLimitDist :
  dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) +
      dist (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hz (fun {k : ℕ} ↦ f k) (z.snd (β := fun (n : ℕ) ↦ X n))) =
    Metric.inductiveLimitDist (X := X) f x y + Metric.inductiveLimitDist (X := X) f y z
⊢ Metric.inductiveLimitDist (X := X) f x z ≤
    Metric.inductiveLimitDist (X := X) f x y + Metric.inductiveLimitDist (X := X) f y z

Tactic:
calc
      inductiveLimitDist f x z = dist (leRecOn hx (f _) x.2 : X m) (leRecOn hz (f _) z.2 : X m) :=
        inductiveLimitDist_eq_dist I x z m hx hz
      _ ≤ dist (leRecOn hx (f _) x.2 : X m) (leRecOn hy (f _) y.2 : X m) +
            dist (leRecOn hy (f _) y.2 : X m) (leRecOn hz (f _) z.2 : X m) :=
        (dist_triangle _ _ _)
      _ = inductiveLimitDist f x y + inductiveLimitDist f y z := by
        rw [inductiveLimitDist_eq_dist I x y m hx hy, inductiveLimitDist_eq_dist I y z m hy hz]

Premises used: dist_triangle, Metric.inductiveLimitDist, Nat.leRecOn, Metric.inductiveLimitDist_eq_dist, Dist.dist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x y : X n
change :
  inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x) (Sigma.mk (β := fun (n : ℕ) ↦ X n) n y) =
    dist x y
⊢ dist (toInductiveLimit (X := X) I n x) (toInductiveLimit (X := X) I n y) = dist x y

Tactic:
change inductiveLimitDist f ⟨n, x⟩ ⟨n, y⟩ = dist x y

Premises used: Metric.inductiveLimitDist, Sigma.mk, Dist.dist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x y : X n
rw :
  dist
      (leRecOn (C := fun (x : ℕ) ↦ X x) ⋯ (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) ⋯ (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) n y).snd (β := fun (n : ℕ) ↦ X n))) =
    dist x y
rw₁ :
  dist ((Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).snd (β := fun (n : ℕ) ↦ X n))
      (leRecOn (C := fun (x : ℕ) ↦ X x) ⋯ (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) n y).snd (β := fun (n : ℕ) ↦ X n))) =
    dist x y
rw₂ rw₃ :
  dist ((Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).snd (β := fun (n : ℕ) ↦ X n))
      ((Sigma.mk (β := fun (n : ℕ) ↦ X n) n y).snd (β := fun (n : ℕ) ↦ X n)) =
    dist x y
⊢ inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x) (Sigma.mk (β := fun (n : ℕ) ↦ X n) n y) =
    dist x y

Tactic:
rw [inductiveLimitDist_eq_dist I ⟨n, x⟩ ⟨n, y⟩ n (le_refl n) (le_refl n), leRecOn_self,
      leRecOn_self]

Premises used: le_refl, Nat.leRecOn_self, Metric.inductiveLimitDist_eq_dist, Sigma.mk
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric (X := X) I
x : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace
h₁ : ∀ (x : X n), (toInductiveLimit (X := X) I n.succ ∘ f n) x = toInductiveLimit (X := X) I n x
⊢ toInductiveLimit (X := X) I n.succ ∘ f n = toInductiveLimit (X := X) I n

Tactic:
funext x
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric (X := X) I
x_1 : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace
x : X n
⊢ Eq (α := InductiveLimit (X := X) I) (Quotient.mk'' (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x)))
    (Quotient.mk'' (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x))

Tactic:
SeparationQuotient.mk_eq_mk.2 (Metric.inseparable_iff.2 ?_)

Premises used: Iff.mpr, SeparationQuotient.mk_eq_mk, Metric.inseparable_iff, Metric.InductiveLimit, SeparationQuotient.mk
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric (X := X) I
x_1 : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace
x : X n
h₁ : dist (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x)) (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x) = 0
⊢ Eq (α := InductiveLimit (X := X) I) (Quotient.mk'' (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x)))
    (Quotient.mk'' (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x))

Tactic:
refine SeparationQuotient.mk_eq_mk.2 (Metric.inseparable_iff.2 ?_)

Premises used: Iff.mpr, SeparationQuotient.mk_eq_mk, Metric.inseparable_iff
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric (X := X) I
x_1 : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace
x : X n
h₁ :
  inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x))
      (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x) =
    0
⊢ dist (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x)) (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x) = 0

Tactic:
change inductiveLimitDist f ⟨n.succ, f n x⟩ ⟨n, x⟩ = 0

Premises used: Metric.inductiveLimitDist, Sigma.mk, Nat.succ
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric (X := X) I
x_1 : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace
x : X n
h₁ :
  (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).fst (β := fun (n : ℕ) ↦ X n) ≤
    (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).fst (β := fun (n : ℕ) ↦ X n)
h₂ :
  (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x)).fst (β := fun (n : ℕ) ↦ X n) ≤
    (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x)).fst (β := fun (n : ℕ) ↦ X n)
h₃ : (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).fst (β := fun (n : ℕ) ↦ X n) ≤ n.succ
⊢ inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x))
      (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x) =
    0

Tactic:
rw [inductiveLimitDist_eq_dist I ⟨n.succ, f n x⟩ ⟨n, x⟩ n.succ, leRecOn_self,
    leRecOn_succ, leRecOn_self, dist_self]

Premises used: Nat.leRecOn_succ, dist_self, Nat.leRecOn_self, Metric.inductiveLimitDist_eq_dist, Sigma.mk, Nat.succ
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric (X := X) I
x_1 : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace
x : X n
⊢ (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).fst (β := fun (n : ℕ) ↦ X n) ≤
    (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).fst (β := fun (n : ℕ) ↦ X n)

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric (X := X) I
x_1 : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace
x : X n
⊢ (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x)).fst (β := fun (n : ℕ) ↦ X n) ≤
    (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x)).fst (β := fun (n : ℕ) ↦ X n)

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric (X := X) I
x_1 : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace
x : X n
⊢ (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).fst (β := fun (n : ℕ) ↦ X n) ≤ n.succ

Tactic:
le_succ _

Premises used: Nat.le_succ
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric (X := X) I
x_1 : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace
x : X n
⊢ (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).fst (β := fun (n : ℕ) ↦ X n) ≤ n.succ

Tactic:
exact le_succ _

Premises used: Nat.le_succ
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
⊢ Dense.{u} (X := InductiveLimit (X := X) I) (⋃ (i : ℕ), range (toInductiveLimit (X := X) I i))

Tactic:
dense_univ.mono ?_

Premises used: dense_univ, Dense.mono
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
refine : Subset.{u} (α := Set (InductiveLimit (X := X) I)) univ (⋃ (i : ℕ), range (toInductiveLimit (X := X) I i))
⊢ Dense.{u} (X := InductiveLimit (X := X) I) (⋃ (i : ℕ), range (toInductiveLimit (X := X) I i))

Tactic:
refine dense_univ.mono ?_

Premises used: dense_univ, Dense.mono
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
a : InductiveLimit (X := X) I
n : ℕ
x : X n
h :
  Membership.mem (γ := Set (InductiveLimit (X := X) I)) univ
    (Quot.mk (⇑(inseparableSetoid ((n : ℕ) × X n)) : (n : ℕ) × X n → (n : ℕ) × X n → Prop)
      (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x))
⊢ Membership.mem (γ := Set (InductiveLimit (X := X) I)) (⋃ (i : ℕ), range (toInductiveLimit (X := X) I i))
    (Quot.mk (⇑(inseparableSetoid ((n : ℕ) × X n)) : (n : ℕ) × X n → (n : ℕ) × X n → Prop)
      (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x))

Tactic:
mem_iUnion.2 ⟨n, mem_range.2 ⟨x, rfl⟩⟩

Premises used: Iff.mpr, Set.mem_range, Set.mem_iUnion, Exists.intro, rfl
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
a : InductiveLimit (X := X) I
n : ℕ
x : X n
h :
  Membership.mem (γ := Set (InductiveLimit (X := X) I)) univ
    (Quot.mk (⇑(inseparableSetoid ((n : ℕ) × X n)) : (n : ℕ) × X n → (n : ℕ) × X n → Prop)
      (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x))
⊢ Membership.mem (γ := Set (InductiveLimit (X := X) I)) (⋃ (i : ℕ), range (toInductiveLimit (X := X) I i))
    (Quot.mk (⇑(inseparableSetoid ((n : ℕ) × X n)) : (n : ℕ) × X n → (n : ℕ) × X n → Prop)
      (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x))

Tactic:
refine mem_iUnion.2 ⟨n, mem_range.2 ⟨x, rfl⟩⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
hs : ∀ (n : ℕ), TopologicalSpace.SeparableSpace.{u} (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
choose :
  ∀ (hsX : (n : ℕ) → Set (X n)) (hcX : ∀ (n : ℕ), (hsX n).Countable) (hdX : ∀ (n : ℕ), Dense (hsX n)),
    TopologicalSpace.SeparableSpace.{u} (InductiveLimit (X := X) I)
⊢ TopologicalSpace.SeparableSpace.{u} (InductiveLimit (X := X) I)

Tactic:
choose hsX hcX hdX using (fun n ↦ TopologicalSpace.exists_countable_dense (X n))

Premises used: TopologicalSpace.exists_countable_dense
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
hs : ∀ (n : ℕ), TopologicalSpace.SeparableSpace.{u} (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
hsX : (n : ℕ) → Set (X n)
hcX : ∀ (n : ℕ), (hsX n).Countable
hdX : ∀ (n : ℕ), Dense (hsX n)
s : Set (InductiveLimit (X := X) I) := ⋃ (i : ℕ), toInductiveLimit (X := X) I i '' hsX i
⊢ TopologicalSpace.SeparableSpace.{u} (InductiveLimit (X := X) I)

Tactic:
⟨s, countable_iUnion (fun n => (hcX n).image _), ?_⟩

Premises used: Set.Countable.image, Set.countable_iUnion, Metric.toInductiveLimit, And.intro, Exists.intro, TopologicalSpace.SeparableSpace.mk
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
hs : ∀ (n : ℕ), TopologicalSpace.SeparableSpace.{u} (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
hsX : (n : ℕ) → Set (X n)
hcX : ∀ (n : ℕ), (hsX n).Countable
hdX : ∀ (n : ℕ), Dense (hsX n)
s : Set (InductiveLimit (X := X) I) := ⋃ (i : ℕ), toInductiveLimit (X := X) I i '' hsX i
refine : Dense s
⊢ TopologicalSpace.SeparableSpace.{u} (InductiveLimit (X := X) I)

Tactic:
refine ⟨s, countable_iUnion (fun n => (hcX n).image _), ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
hs : ∀ (n : ℕ), TopologicalSpace.SeparableSpace.{u} (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
hsX : (n : ℕ) → Set (X n)
hcX : ∀ (n : ℕ), (hsX n).Countable
hdX : ∀ (n : ℕ), Dense (hsX n)
s : Set (InductiveLimit (X := X) I) := ⋃ (i : ℕ), toInductiveLimit (X := X) I i '' hsX i
⊢ Dense s

Tactic:
.of_closure <| (dense_iUnion_range_toInductiveLimit I).mono <| iUnion_subset fun i ↦ ?_

Premises used: Set.iUnion_subset, Metric.dense_iUnion_range_toInductiveLimit, Dense.of_closure, Dense.mono
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
hs : ∀ (n : ℕ), TopologicalSpace.SeparableSpace.{u} (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
hsX : (n : ℕ) → Set (X n)
hcX : ∀ (n : ℕ), (hsX n).Countable
hdX : ∀ (n : ℕ), Dense (hsX n)
s : Set (InductiveLimit (X := X) I) := ⋃ (i : ℕ), toInductiveLimit (X := X) I i '' hsX i
refine : ∀ (i : ℕ), range (toInductiveLimit (X := X) I i) ⊆ closure s
⊢ Dense s

Tactic:
refine .of_closure <| (dense_iUnion_range_toInductiveLimit I).mono <| iUnion_subset fun i ↦ ?_

Premises used: Set.iUnion_subset, Metric.dense_iUnion_range_toInductiveLimit, Dense.mono
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
hs : ∀ (n : ℕ), TopologicalSpace.SeparableSpace.{u} (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
hsX : (n : ℕ) → Set (X n)
hcX : ∀ (n : ℕ), (hsX n).Countable
hdX : ∀ (n : ℕ), Dense (hsX n)
s : Set (InductiveLimit (X := X) I) := ⋃ (i : ℕ), toInductiveLimit (X := X) I i '' hsX i
i : ℕ
⊢ range (toInductiveLimit (X := X) I i) ⊆ closure (toInductiveLimit (X := X) I i '' hsX i)

Tactic:
(toInductiveLimit_isometry I i |>.continuous).range_subset_closure_image_dense (hdX i)

Premises used: Continuous.range_subset_closure_image_dense, Isometry.continuous, Metric.toInductiveLimit_isometry
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
hs : ∀ (n : ℕ), TopologicalSpace.SeparableSpace.{u} (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
hsX : (n : ℕ) → Set (X n)
hcX : ∀ (n : ℕ), (hsX n).Countable
hdX : ∀ (n : ℕ), Dense (hsX n)
s : Set (InductiveLimit (X := X) I) := ⋃ (i : ℕ), toInductiveLimit (X := X) I i '' hsX i
i : ℕ
⊢ closure (toInductiveLimit (X := X) I i '' hsX i) ⊆ closure s

Tactic:
closure_mono <| subset_iUnion (fun j ↦ toInductiveLimit I j '' hsX j) i

Premises used: closure_mono, Set.subset_iUnion, Metric.toInductiveLimit, Set.image
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
hs : ∀ (n : ℕ), TopologicalSpace.SeparableSpace.{u} (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
hsX : (n : ℕ) → Set (X n)
hcX : ∀ (n : ℕ), (hsX n).Countable
hdX : ∀ (n : ℕ), Dense (hsX n)
s : Set (InductiveLimit (X := X) I) := ⋃ (i : ℕ), toInductiveLimit (X := X) I i '' hsX i
i : ℕ
⊢ range (toInductiveLimit (X := X) I i) ⊆ closure s

Tactic:
calc
    range (toInductiveLimit I i) ⊆ closure (toInductiveLimit I i '' (hsX i)) :=
      (toInductiveLimit_isometry I i |>.continuous).range_subset_closure_image_dense (hdX i)
    _ ⊆ closure s := closure_mono <| subset_iUnion (fun j ↦ toInductiveLimit I j '' hsX j) i

Premises used: Continuous.range_subset_closure_image_dense, closure_mono, Set.subset_iUnion, Isometry.continuous, Metric.toInductiveLimit, closure, Metric.toInductiveLimit_isometry, Set.image, Set.range
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
⊢ Equivalence IsometryRel

Tactic:
⟨fun _ => Nonempty.intro (IsometryEquiv.refl _), fun ⟨e⟩ => ⟨e.symm⟩, fun ⟨e⟩ ⟨f⟩ => ⟨e.trans f⟩⟩

Premises used: _private.0.GromovHausdorff.equivalence_isometryRel.match_1, Membership.mem, Subtype, IsometryEquiv.symm, Nonempty.intro, IsometryEquiv.refl, IsometryEquiv.trans, Equivalence.mk, _private.0.GromovHausdorff.IsometryRel
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
simp :
  (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
      p (NonemptyCompacts.kuratowskiEmbedding X) ↔
    ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ ⟦p⟧ = toGHSpace X ↔ ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))

Tactic:
simp only [toGHSpace, Quotient.eq]

Premises used: GromovHausdorff.toGHSpace, Quotient.eq
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
⊢ (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
      p (NonemptyCompacts.kuratowskiEmbedding X) ↔
    ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
refine_1 :
  ∀
    (h :
      (IsometryRel.setoid :
          NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
        p (NonemptyCompacts.kuratowskiEmbedding X)),
    ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
refine_2 :
  (∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) →
    (IsometryRel.setoid :
        NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
      p (NonemptyCompacts.kuratowskiEmbedding X)
⊢ (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
      p (NonemptyCompacts.kuratowskiEmbedding X) ↔
    ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))

Tactic:
refine ⟨fun h => ?_, ?_⟩