n✝ m✝ m n : ℕ
C : Fin (m + n) → Sort u_1
hleft : (i : Fin m) → C (↑(castAdd n) i)
hright : (i : Fin n) → C (↑(natAdd m) i)
i : Fin n
this : ¬↑(↑(natAdd m) i) < m
⊢ addCases hleft hright (↑(natAdd m) i) = hright i
n✝ m✝ m n : ℕ
C : Fin (m + n) → Sort u_1
hleft : (i : Fin m) → C (↑(castAdd n) i)
hright : (i : Fin n) → C (↑(natAdd m) i)
i : Fin n
⊢ addCases hleft hright (↑(natAdd m) i) = hright i
have : ¬(natAdd m i : ℕ) < m := (le_coe_natAdd _ _).not_lt
n✝ m✝ m n : ℕ
C : Fin (m + n) → Sort u_1
hleft : (i : Fin m) → C (↑(castAdd n) i)
hright : (i : Fin n) → C (↑(natAdd m) i)
i : Fin n
this : ¬↑(↑(natAdd m) i) < m
⊢ (_ :
        ↑(natAdd m) (subNat m (↑(cast (_ : m + n = n + m)) (↑(natAdd m) i)) (_ : m ≤ ↑(↑(natAdd m) i))) =
          ↑(natAdd m) i) ▸
      hright (subNat m (↑(cast (_ : m + n = n + m)) (↑(natAdd m) i)) (_ : m ≤ ↑(↑(natAdd m) i))) =
    hright i
n✝ m✝ m n : ℕ
C : Fin (m + n) → Sort u_1
hleft : (i : Fin m) → C (↑(castAdd n) i)
hright : (i : Fin n) → C (↑(natAdd m) i)
i : Fin n
this : ¬↑(↑(natAdd m) i) < m
⊢ addCases hleft hright (↑(natAdd m) i) = hright i
rw [addCases, dif_neg this]
n✝ m✝ m n : ℕ
C : Fin (m + n) → Sort u_1
hleft : (i : Fin m) → C (↑(castAdd n) i)
hright : (i : Fin n) → C (↑(natAdd m) i)
i : Fin n
this : ¬↑(↑(natAdd m) i) < m
⊢ HEq (hright (subNat m (↑(cast (_ : m + n = n + m)) (↑(natAdd m) i)) (_ : m ≤ ↑(↑(natAdd m) i)))) (hright i)
n✝ m✝ m n : ℕ
C : Fin (m + n) → Sort u_1
hleft : (i : Fin m) → C (↑(castAdd n) i)
hright : (i : Fin n) → C (↑(natAdd m) i)
i : Fin n
this : ¬↑(↑(natAdd m) i) < m
⊢ (_ :
        ↑(natAdd m) (subNat m (↑(cast (_ : m + n = n + m)) (↑(natAdd m) i)) (_ : m ≤ ↑(↑(natAdd m) i))) =
          ↑(natAdd m) i) ▸
      hright (subNat m (↑(cast (_ : m + n = n + m)) (↑(natAdd m) i)) (_ : m ≤ ↑(↑(natAdd m) i))) =
    hright i
refine' eq_of_heq ((eq_rec_heq _ _).trans _)
case e_1
n✝ m✝ m n : ℕ
C : Fin (m + n) → Sort u_1
hleft : (i : Fin m) → C (↑(castAdd n) i)
hright : (i : Fin n) → C (↑(natAdd m) i)
i : Fin n
this : ¬↑(↑(natAdd m) i) < m
⊢ subNat m (↑(cast (_ : m + n = n + m)) (↑(natAdd m) i)) (_ : m ≤ ↑(↑(natAdd m) i)) = i
n✝ m✝ m n : ℕ
C : Fin (m + n) → Sort u_1
hleft : (i : Fin m) → C (↑(castAdd n) i)
hright : (i : Fin n) → C (↑(natAdd m) i)
i : Fin n
this : ¬↑(↑(natAdd m) i) < m
⊢ HEq (hright (subNat m (↑(cast (_ : m + n = n + m)) (↑(natAdd m) i)) (_ : m ≤ ↑(↑(natAdd m) i)))) (hright i)
congr 1
no goals
case e_1
n✝ m✝ m n : ℕ
C : Fin (m + n) → Sort u_1
hleft : (i : Fin m) → C (↑(castAdd n) i)
hright : (i : Fin n) → C (↑(natAdd m) i)
i : Fin n
this : ¬↑(↑(natAdd m) i) < m
⊢ subNat m (↑(cast (_ : m + n = n + m)) (↑(natAdd m) i)) (_ : m ≤ ↑(↑(natAdd m) i)) = i
simp