case refl
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
⊢ Function.Injective (leRecOn (_ : Nat.le n n) fun {k} => next)

case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
m : ℕ
hnm : Nat.le n m
ih : Function.Injective (leRecOn hnm fun {k} => next)
⊢ Function.Injective (leRecOn (_ : Nat.le n (succ m)) fun {k} => next)
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
⊢ Function.Injective (leRecOn hnm fun {k} => next)
induction' hnm with m hnm ih
case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
m : ℕ
hnm : Nat.le n m
ih : Function.Injective (leRecOn hnm fun {k} => next)
x y : C n
H : leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) x = leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) y
⊢ x = y
case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
m : ℕ
hnm : Nat.le n m
ih : Function.Injective (leRecOn hnm fun {k} => next)
⊢ Function.Injective (leRecOn (_ : Nat.le n (succ m)) fun {k} => next)
intro x y H
case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
m : ℕ
hnm : Nat.le n m
ih : Function.Injective (leRecOn hnm fun {k} => next)
x y : C n
H : next (leRecOn hnm (fun {k} => next) x) = next (leRecOn hnm (fun {k} => next) y)
⊢ x = y
case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
m : ℕ
hnm : Nat.le n m
ih : Function.Injective (leRecOn hnm fun {k} => next)
x y : C n
H : leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) x = leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) y
⊢ x = y
rw [leRecOn_succ hnm, leRecOn_succ hnm] at H
no goals
case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
m : ℕ
hnm : Nat.le n m
ih : Function.Injective (leRecOn hnm fun {k} => next)
x y : C n
H : next (leRecOn hnm (fun {k} => next) x) = next (leRecOn hnm (fun {k} => next) y)
⊢ x = y
exact ih (Hnext _ H)
case refl
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
x y : C n
H : leRecOn (_ : Nat.le n n) (fun {k} => next) x = leRecOn (_ : Nat.le n n) (fun {k} => next) y
⊢ x = y
case refl
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
⊢ Function.Injective (leRecOn (_ : Nat.le n n) fun {k} => next)
intro x y H
no goals
case refl
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
x y : C n
H : leRecOn (_ : Nat.le n n) (fun {k} => next) x = leRecOn (_ : Nat.le n n) (fun {k} => next) y
⊢ x = y
rwa [leRecOn_self, leRecOn_self] at H