-- Mathlib/Topology/MetricSpace/Gluing.lean
theorem inductiveLimitDist_eq_dist (I : ∀ n, Isometry (f n)) (x y : Σn, X n) :
    ∀ m (hx : x.1 ≤ m) (hy : y.1 ≤ m), inductiveLimitDist f x y =
      dist (leRecOn hx (f _) x.2 : X m) (leRecOn hy (f _) y.2 : X m)
  | 0, hx, hy => by
    obtain ⟨i, x⟩ := x; obtain ⟨j, y⟩ := y
    obtain rfl : i = 0 := nonpos_iff_eq_zero.1 hx
    obtain rfl : j = 0 := nonpos_iff_eq_zero.1 hy
    rfl
  | (m + 1), hx, hy => by
    by_cases h : max x.1 y.1 = (m + 1)
    · generalize m + 1 = m' at *
      subst m'
      rfl
    · have : max x.1 y.1 ≤ succ m

Proof state:
case neg
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 ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬x.fst ⊔ y.fst = m + 1
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd)

Tactic:
have : max x.1 y.1 ≤ succ m := by simp [hx, hy]

Result:
case neg
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 ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬x.fst ⊔ y.fst = m + 1
this : x.fst ⊔ y.fst ≤ m.succ
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd)

Proof state:
case neg
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 ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬x.fst ⊔ y.fst = m + 1
this✝ : x.fst ⊔ y.fst ≤ m.succ
this : x.fst ⊔ y.fst ≤ m
xm : x.fst ≤ m
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd)

Tactic:
have ym : y.1 ≤ m := le_trans (le_max_right _ _) this

Result:
case neg
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 ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬x.fst ⊔ y.fst = m + 1
this✝ : x.fst ⊔ y.fst ≤ m.succ
this : x.fst ⊔ y.fst ≤ m
xm : x.fst ≤ m
ym : y.fst ≤ m
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd)

Proof state:
case neg
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 ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬x.fst ⊔ y.fst = m + 1
this✝ : x.fst ⊔ y.fst ≤ m.succ
this : x.fst ⊔ y.fst ≤ m
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd)

Tactic:
have xm : x.1 ≤ m := le_trans (le_max_left _ _) this

Result:
case neg
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 ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬x.fst ⊔ y.fst = m + 1
this✝ : x.fst ⊔ y.fst ≤ m.succ
this : x.fst ⊔ y.fst ≤ m
xm : x.fst ≤ m
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd)

Proof state:
case mk
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 ≤ 0
i : ℕ
x : X i
hx : ⟨i, x⟩.fst ≤ 0
⊢ inductiveLimitDist f ⟨i, x⟩ y = dist (leRecOn hx (fun {k} => f k) ⟨i, x⟩.snd) (leRecOn hy (fun {k} => f k) y.snd)

Tactic:
obtain ⟨j, y⟩ := y

Result:
case mk.mk
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 : ⟨i, x⟩.fst ≤ 0
j : ℕ
y : X j
hy : ⟨j, y⟩.fst ≤ 0
⊢ inductiveLimitDist f ⟨i, x⟩ ⟨j, y⟩ =
    dist (leRecOn hx (fun {k} => f k) ⟨i, x⟩.snd) (leRecOn hy (fun {k} => f k) ⟨j, y⟩.snd)

Proof state:
case neg
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 ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬x.fst ⊔ y.fst = m + 1
this : x.fst ⊔ y.fst ≤ m.succ
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd)

Tactic:
have : max x.1 y.1 ≤ m := by simpa [h] using of_le_succ this

Result:
case neg
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 ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬x.fst ⊔ y.fst = m + 1
this✝ : x.fst ⊔ y.fst ≤ m.succ
this : x.fst ⊔ y.fst ≤ m
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd)