case mp.zero
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n : ℕ
h✝ : res x n = res y n
h : res x Nat.zero = res y Nat.zero
⊢ ∀ ⦃m : ℕ⦄, m < Nat.zero → x m = y m

case mp.succ
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : res x n✝ = res y n✝
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
h : res x (Nat.succ n) = res y (Nat.succ n)
⊢ ∀ ⦃m : ℕ⦄, m < Nat.succ n → x m = y m

case mpr.zero
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n : ℕ
h✝ : ∀ ⦃m : ℕ⦄, m < n → x m = y m
h : ∀ ⦃m : ℕ⦄, m < Nat.zero → x m = y m
⊢ res x Nat.zero = res y Nat.zero

case mpr.succ
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : ∀ ⦃m : ℕ⦄, m < n✝ → x m = y m
n : ℕ
ih : (∀ ⦃m : ℕ⦄, m < n → x m = y m) → res x n = res y n
h : ∀ ⦃m : ℕ⦄, m < Nat.succ n → x m = y m
⊢ res x (Nat.succ n) = res y (Nat.succ n)
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n : ℕ
⊢ res x n = res y n ↔ ∀ ⦃m : ℕ⦄, m < n → x m = y m
constructor <;> intro h <;> induction' n with n ih
case mpr.succ
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : ∀ ⦃m : ℕ⦄, m < n✝ → x m = y m
n : ℕ
ih : (∀ ⦃m : ℕ⦄, m < n → x m = y m) → res x n = res y n
h : ∀ ⦃m : ℕ⦄, m < Nat.succ n → x m = y m
⊢ x n = y n ∧ res x n = res y n
case mpr.succ
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : ∀ ⦃m : ℕ⦄, m < n✝ → x m = y m
n : ℕ
ih : (∀ ⦃m : ℕ⦄, m < n → x m = y m) → res x n = res y n
h : ∀ ⦃m : ℕ⦄, m < Nat.succ n → x m = y m
⊢ res x (Nat.succ n) = res y (Nat.succ n)
simp only [res_succ, cons.injEq]
case mpr.succ
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : ∀ ⦃m : ℕ⦄, m < n✝ → x m = y m
n : ℕ
ih : (∀ ⦃m : ℕ⦄, m < n → x m = y m) → res x n = res y n
h : ∀ ⦃m : ℕ⦄, m < Nat.succ n → x m = y m
m : ℕ
hm : m < n
⊢ x m = y m
case mpr.succ
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : ∀ ⦃m : ℕ⦄, m < n✝ → x m = y m
n : ℕ
ih : (∀ ⦃m : ℕ⦄, m < n → x m = y m) → res x n = res y n
h : ∀ ⦃m : ℕ⦄, m < Nat.succ n → x m = y m
⊢ x n = y n ∧ res x n = res y n
refine' ⟨h (Nat.lt_succ_self _), ih fun m hm => _⟩
no goals
case mpr.succ
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : ∀ ⦃m : ℕ⦄, m < n✝ → x m = y m
n : ℕ
ih : (∀ ⦃m : ℕ⦄, m < n → x m = y m) → res x n = res y n
h : ∀ ⦃m : ℕ⦄, m < Nat.succ n → x m = y m
m : ℕ
hm : m < n
⊢ x m = y m
exact h (hm.trans (Nat.lt_succ_self _))
no goals
case mp.zero
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n : ℕ
h✝ : res x n = res y n
h : res x Nat.zero = res y Nat.zero
⊢ ∀ ⦃m : ℕ⦄, m < Nat.zero → x m = y m
simp
case mp.succ
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : res x n✝ = res y n✝
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
h : res x (Nat.succ n) = res y (Nat.succ n)
m : ℕ
hm : m < Nat.succ n
⊢ x m = y m
case mp.succ
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : res x n✝ = res y n✝
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
h : res x (Nat.succ n) = res y (Nat.succ n)
⊢ ∀ ⦃m : ℕ⦄, m < Nat.succ n → x m = y m
intro m hm
case mp.succ
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : res x n✝ = res y n✝
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
h : res x (Nat.succ n) = res y (Nat.succ n)
m : ℕ
hm : m < n ∨ m = n
⊢ x m = y m
case mp.succ
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : res x n✝ = res y n✝
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
h : res x (Nat.succ n) = res y (Nat.succ n)
m : ℕ
hm : m < Nat.succ n
⊢ x m = y m
rw [Nat.lt_succ_iff_lt_or_eq] at hm
case mp.succ
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : res x n✝ = res y n✝
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
hm : m < n ∨ m = n
h : x n = y n ∧ res x n = res y n
⊢ x m = y m
case mp.succ
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : res x n✝ = res y n✝
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
h : res x (Nat.succ n) = res y (Nat.succ n)
m : ℕ
hm : m < n ∨ m = n
⊢ x m = y m
simp only [res_succ, cons.injEq] at h
case mp.succ.inl
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : res x n✝ = res y n✝
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
h : x n = y n ∧ res x n = res y n
hm : m < n
⊢ x m = y m

case mp.succ.inr
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : res x n✝ = res y n✝
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
h : x n = y n ∧ res x n = res y n
hm : m = n
⊢ x m = y m
case mp.succ
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : res x n✝ = res y n✝
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
hm : m < n ∨ m = n
h : x n = y n ∧ res x n = res y n
⊢ x m = y m
cases' hm with hm hm
case mp.succ.inr
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : res x n✝ = res y n✝
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
h : x n = y n ∧ res x n = res y n
hm : m = n
⊢ x n = y n
case mp.succ.inr
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : res x n✝ = res y n✝
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
h : x n = y n ∧ res x n = res y n
hm : m = n
⊢ x m = y m
rw [hm]
no goals
case mp.succ.inr
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : res x n✝ = res y n✝
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
h : x n = y n ∧ res x n = res y n
hm : m = n
⊢ x n = y n
exact h.1
no goals
case mp.succ.inl
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n✝ : ℕ
h✝ : res x n✝ = res y n✝
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
h : x n = y n ∧ res x n = res y n
hm : m < n
⊢ x m = y m
exact ih h.2 hm
no goals
case mpr.zero
E : ℕ → Type ?u.20736
α : Type u_1
x y : ℕ → α
n : ℕ
h✝ : ∀ ⦃m : ℕ⦄, m < n → x m = y m
h : ∀ ⦃m : ℕ⦄, m < Nat.zero → x m = y m
⊢ res x Nat.zero = res y Nat.zero
simp