awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : Nonempty Z
inst_1 : MetricSpace Z
inst_2 : MetricSpace X
inst_3 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x : TopologicalSpace (X ⊕ Y) := UniformSpace.toTopologicalSpace
x_1 : Z
⊢ Eq (α := GlueSpace hΦ hΨ) (Quotient.mk'' (Sum.inl (Φ x_1))) (Quotient.mk'' (Sum.inr (Ψ x_1)))

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

Premises used: Iff.mpr, SeparationQuotient.mk_eq_mk, Metric.inseparable_iff, SeparationQuotient.mk, Metric.GlueSpace
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : Nonempty Z
inst_1 : MetricSpace Z
inst_2 : MetricSpace X
inst_3 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x : TopologicalSpace (X ⊕ Y) := UniformSpace.toTopologicalSpace
x_1 : Z
h : dist (Sum.inl (Φ x_1)) (Sum.inr (Ψ x_1)) = 0
⊢ Eq (α := GlueSpace hΦ hΨ) (Quotient.mk'' (Sum.inl (Φ x_1))) (Quotient.mk'' (Sum.inr (Ψ x_1)))

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
Y : Type v
Z : Type w
inst : Nonempty Z
inst_1 : MetricSpace Z
inst_2 : MetricSpace X
inst_3 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x : TopologicalSpace (X ⊕ Y) := UniformSpace.toTopologicalSpace
x_1 : Z
⊢ dist (Sum.inl (Φ x_1)) (Sum.inr (Ψ x_1)) = 0

Tactic:
glueDist_glued_points Φ Ψ 0 _

Premises used: Metric.glueDist_glued_points, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : Nonempty Z
inst_1 : MetricSpace Z
inst_2 : MetricSpace X
inst_3 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x : TopologicalSpace (X ⊕ Y) := UniformSpace.toTopologicalSpace
x_1 : Z
⊢ dist (Sum.inl (Φ x_1)) (Sum.inr (Ψ x_1)) = 0

Tactic:
exact glueDist_glued_points Φ Ψ 0 _

Premises used: Metric.glueDist_glued_points, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : Nonempty Z
inst_1 : MetricSpace Z
inst_2 : MetricSpace X
inst_3 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
⊢ Isometry (toGlueL hΦ hΨ)

Tactic:
Isometry.of_dist_eq fun _ _ => rfl

Premises used: Isometry.of_dist_eq, rfl
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : Nonempty Z
inst_1 : MetricSpace Z
inst_2 : MetricSpace X
inst_3 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
⊢ Isometry (toGlueR hΦ hΨ)

Tactic:
Isometry.of_dist_eq fun _ _ => rfl

Premises used: Isometry.of_dist_eq, 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)
x y : (n : ℕ) × X n
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ 0
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ 0
obtain :
  ∀ (i : ℕ) (x : X i) (hx : (Sigma.mk (β := fun (n : ℕ) ↦ X n) i x).fst (β := fun (n : ℕ) ↦ X n) ≤ 0),
    inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) i x) y =
      dist
        (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k)
          ((Sigma.mk (β := fun (n : ℕ) ↦ X n) i 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 x y =
    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)))

Tactic:
obtain ⟨i, x⟩ := 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)
y : (n : ℕ) × X n
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ 0
i : ℕ
x : X i
hx : (Sigma.mk (β := fun (n : ℕ) ↦ X n) i x).fst (β := fun (n : ℕ) ↦ X n) ≤ 0
obtain :
  ∀ (j : ℕ) (y : X j) (hy : (Sigma.mk (β := fun (n : ℕ) ↦ X n) j y).fst (β := fun (n : ℕ) ↦ X n) ≤ 0),
    inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) i x) (Sigma.mk (β := fun (n : ℕ) ↦ X n) j y) =
      dist
        (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k)
          ((Sigma.mk (β := fun (n : ℕ) ↦ X n) i x).snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k)
          ((Sigma.mk (β := fun (n : ℕ) ↦ X n) j y).snd (β := fun (n : ℕ) ↦ X n)))
⊢ inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) i x) y =
    dist
      (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) i x).snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))

Tactic:
obtain ⟨j, y⟩ := y
-- 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)
i : ℕ
x : X i
hx : (Sigma.mk (β := fun (n : ℕ) ↦ X n) i x).fst (β := fun (n : ℕ) ↦ X n) ≤ 0
j : ℕ
y : X j
hy : (Sigma.mk (β := fun (n : ℕ) ↦ X n) j y).fst (β := fun (n : ℕ) ↦ X n) ≤ 0
⊢ i = 0

Tactic:
nonpos_iff_eq_zero.1 hx

Premises used: Iff.mp, nonpos_iff_eq_zero
-- 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)
i : ℕ
x : X i
hx : (Sigma.mk (β := fun (n : ℕ) ↦ X n) i x).fst (β := fun (n : ℕ) ↦ X n) ≤ 0
j : ℕ
y : X j
hy : (Sigma.mk (β := fun (n : ℕ) ↦ X n) j y).fst (β := fun (n : ℕ) ↦ X n) ≤ 0
obtain :
  ∀ (x : X 0) (hx : (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x).fst (β := fun (n : ℕ) ↦ X n) ≤ 0),
    inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x) (Sigma.mk (β := fun (n : ℕ) ↦ X n) j y) =
      dist
        (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k)
          ((Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x).snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k)
          ((Sigma.mk (β := fun (n : ℕ) ↦ X n) j y).snd (β := fun (n : ℕ) ↦ X n)))
⊢ inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) i x) (Sigma.mk (β := fun (n : ℕ) ↦ X n) j y) =
    dist
      (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) i x).snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) j y).snd (β := fun (n : ℕ) ↦ X n)))

Tactic:
obtain rfl : i = 0 := nonpos_iff_eq_zero.1 hx

Premises used: Iff.mp, rfl, nonpos_iff_eq_zero
-- 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)
j : ℕ
y : X j
hy : (Sigma.mk (β := fun (n : ℕ) ↦ X n) j y).fst (β := fun (n : ℕ) ↦ X n) ≤ 0
x : X 0
hx : (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x).fst (β := fun (n : ℕ) ↦ X n) ≤ 0
⊢ j = 0

Tactic:
nonpos_iff_eq_zero.1 hy

Premises used: Iff.mp, nonpos_iff_eq_zero
-- 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)
j : ℕ
y : X j
hy : (Sigma.mk (β := fun (n : ℕ) ↦ X n) j y).fst (β := fun (n : ℕ) ↦ X n) ≤ 0
x : X 0
hx : (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x).fst (β := fun (n : ℕ) ↦ X n) ≤ 0
obtain :
  ∀ (y : X 0) (hy : (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 y).fst (β := fun (n : ℕ) ↦ X n) ≤ 0),
    inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x) (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 y) =
      dist
        (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k)
          ((Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x).snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k)
          ((Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 y).snd (β := fun (n : ℕ) ↦ X n)))
⊢ inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x) (Sigma.mk (β := fun (n : ℕ) ↦ X n) j y) =
    dist
      (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x).snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) j y).snd (β := fun (n : ℕ) ↦ X n)))

Tactic:
obtain rfl : j = 0 := nonpos_iff_eq_zero.1 hy

Premises used: Iff.mp, rfl, nonpos_iff_eq_zero
-- 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 : X 0
hx : (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x).fst (β := fun (n : ℕ) ↦ X n) ≤ 0
y : X 0
hy : (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 y).fst (β := fun (n : ℕ) ↦ X n) ≤ 0
⊢ inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x) (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 y) =
    dist
      (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x).snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 y).snd (β := 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)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
pos :
  ∀ (h : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1),
    inductiveLimitDist (X := X) f x y =
      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)))
neg :
  ∀ (h : ¬max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1),
    inductiveLimitDist (X := X) f x y =
      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 x y =
    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)))

Tactic:
by_cases h : max x.1 y.1 = (m + 1)

Premises used: Sigma.fst, HAdd.hAdd, Max.max, OfNat.ofNat
-- 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 : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
h : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1
pos :
  ∀ (m' : ℕ) (hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m') (hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m')
    (h : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m'),
    inductiveLimitDist (X := X) f x y =
      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 x y =
    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)))

Tactic:
generalize m + 1 = m' at *
-- 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 : (n : ℕ) × X n
m m' : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m'
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m'
h : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m'
pos :
  ∀ (hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)))
    (hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))),
    inductiveLimitDist (X := X) f x y =
      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 x y =
    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)))

Tactic:
subst m'
-- 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 : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))
⊢ inductiveLimitDist (X := X) f x y =
    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)))

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)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
h : ¬max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1
⊢ max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m.succ

Tactic:
simp [hx, hy]
-- 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 : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
h : ¬max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1
⊢ max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m.succ

Tactic:
have : max x.1 y.1 ≤ succ m := by simp [hx, hy]
-- 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 : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
h : ¬max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1
this : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m.succ
⊢ max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m

Tactic:
simpa [h] using of_le_succ this

Premises used: Nat.of_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)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
h : ¬max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1
this : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m.succ
⊢ max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m

Tactic:
have : max x.1 y.1 ≤ m := by simpa [h] using of_le_succ this
-- 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 : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
h : ¬max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1
this_1 : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m.succ
this : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m
⊢ x.fst (β := fun (n : ℕ) ↦ X n) ≤ m

Tactic:
have xm : x.1 ≤ m := le_trans (le_max_left _ _) this
-- 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 : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
h : ¬max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1
this_1 : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m.succ
this : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m
xm : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
⊢ y.fst (β := fun (n : ℕ) ↦ X n) ≤ m

Tactic:
have ym : y.1 ≤ m := le_trans (le_max_right _ _) this
-- 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 : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
h : ¬max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1
this_1 : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m.succ
this : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m
xm : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
ym : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m
neg :
  inductiveLimitDist (X := X) f x y =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) xm (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) ym (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
⊢ inductiveLimitDist (X := X) f x y =
    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)))

Tactic:
rw [leRecOn_succ xm, leRecOn_succ ym, (I m).dist_eq]

Premises used: Nat.leRecOn_succ, Isometry.dist_eq
-- 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 : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
h : ¬max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1
this_1 : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m.succ
this : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m
xm : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
ym : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m
⊢ inductiveLimitDist (X := X) f x y =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) xm (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) ym (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))

Tactic:
inductiveLimitDist_eq_dist I x y m xm ym
-- 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 : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
h : ¬max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1
this_1 : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m.succ
this : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m
xm : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
ym : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m
⊢ inductiveLimitDist (X := X) f x y =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) xm (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) ym (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))

Tactic:
exact inductiveLimitDist_eq_dist I x y m xm ym
-- 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 : (n : ℕ) × X n
⊢ inductiveLimitDist (X := X) f x x = 0

Tactic:
simp [inductiveLimitDist]

Premises used: Metric.inductiveLimitDist
-- 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 : (n : ℕ) × X n
m : ℕ := max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))
⊢ x.fst (β := fun (n : ℕ) ↦ X n) ≤ m

Tactic:
have hx : x.1 ≤ m := le_max_left _ _
-- 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 : (n : ℕ) × X n
m : ℕ := max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
⊢ y.fst (β := fun (n : ℕ) ↦ X n) ≤ m

Tactic:
have hy : y.1 ≤ m := le_max_right _ _
-- 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 : (n : ℕ) × X n
m : ℕ := max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hy : y.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))) =
    inductiveLimitDist (X := X) f y x
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) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
rw₂ rw₃ :
  dist (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.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) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
⊢ inductiveLimitDist (X := X) f x y = inductiveLimitDist (X := X) f y x

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

Premises used: dist_comm, 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))
⊢ x.fst (β := fun (n : ℕ) ↦ X n) ≤ m

Tactic:
have hx : x.1 ≤ m := le_trans (le_max_left _ _) (le_max_left _ _)
-- 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
⊢ y.fst (β := fun (n : ℕ) ↦ X n) ≤ m

Tactic:
have hy : y.1 ≤ m := le_trans (le_max_right _ _) (le_max_left _ _)
-- 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
⊢ z.fst (β := fun (n : ℕ) ↦ X n) ≤ m

Tactic:
have hz : z.1 ≤ m := le_max_right _ _