[GOAL]
m n : ℕ
⊢ (fun b => bif b then 1 else 0) (Matrix.vecCons false ![true] 0) = 0 ∧
    (fun b => bif b then 1 else 0) (Matrix.vecCons false ![true] 1) = 1
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
⊢ Matrix.vecCons false ![true] ((fun b => bif b then 1 else 0) false) = false ∧
    Matrix.vecCons false ![true] ((fun b => bif b then 1 else 0) true) = true
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
α : Fin 2 → Type u
s : Set (α 0)
t : Set (α 1)
⊢ (fun f => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.pi Set.univ (cons s (cons t finZeroElim))
[PROOFSTEP]
ext f
[GOAL]
case h
m n : ℕ
α : Fin 2 → Type u
s : Set (α 0)
t : Set (α 1)
f : (i : Fin 2) → α i
⊢ f ∈ (fun f => (f 0, f 1)) ⁻¹' s ×ˢ t ↔ f ∈ Set.pi Set.univ (cons s (cons t finZeroElim))
[PROOFSTEP]
simp [Fin.forall_fin_two]
[GOAL]
m n : ℕ
i x : Fin (n + 1)
⊢ (fun x => Option.casesOn' x i (Fin.succAbove i)) (Fin.insertNth i none some i) = i
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
i x : Fin (n + 1)
j : Fin n
⊢ (fun x => Option.casesOn' x i (Fin.succAbove i)) (Fin.insertNth i none some (Fin.succAbove i j)) = Fin.succAbove i j
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
i : Fin (n + 1)
x : Option (Fin n)
⊢ Fin.insertNth i none some ((fun x => Option.casesOn' x i (Fin.succAbove i)) x) = x
[PROOFSTEP]
cases x
[GOAL]
case none
m n : ℕ
i : Fin (n + 1)
⊢ Fin.insertNth i none some ((fun x => Option.casesOn' x i (Fin.succAbove i)) none) = none
[PROOFSTEP]
dsimp
[GOAL]
case some
m n : ℕ
i : Fin (n + 1)
val✝ : Fin n
⊢ Fin.insertNth i none some ((fun x => Option.casesOn' x i (Fin.succAbove i)) (some val✝)) = some val✝
[PROOFSTEP]
dsimp
[GOAL]
case none
m n : ℕ
i : Fin (n + 1)
⊢ Fin.insertNth i none some i = none
[PROOFSTEP]
simp
[GOAL]
case some
m n : ℕ
i : Fin (n + 1)
val✝ : Fin n
⊢ Fin.insertNth i none some (Fin.succAbove i val✝) = some val✝
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
i : Fin (n + 1)
⊢ ↑(finSuccEquiv' i) i = none
[PROOFSTEP]
simp [finSuccEquiv']
[GOAL]
m✝ n : ℕ
i : Fin (n + 1)
m : Fin n
h : Fin.castSucc m < i
⊢ ↑(finSuccEquiv' i) (Fin.castSucc m) = some m
[PROOFSTEP]
rw [← Fin.succAbove_below _ _ h, finSuccEquiv'_succAbove]
[GOAL]
m✝ n : ℕ
i : Fin (n + 1)
m : Fin n
h : i ≤ Fin.castSucc m
⊢ ↑(finSuccEquiv' i) (Fin.succ m) = some m
[PROOFSTEP]
rw [← Fin.succAbove_above _ _ h, finSuccEquiv'_succAbove]
[GOAL]
m n : ℕ
i : Fin n
⊢ ↑(finSuccEquiv' (Fin.last n)) (Fin.castSucc i) = some i
[PROOFSTEP]
rw [← Fin.succAbove_last, finSuccEquiv'_succAbove]
[GOAL]
m n : ℕ
i : Fin (n + 1)
h : i ≠ Fin.last n
⊢ ↑(finSuccEquiv' (Fin.last n)) i = some (Fin.castLT i (_ : ↑i < n))
[PROOFSTEP]
rcases Fin.exists_castSucc_eq.2 h with ⟨i, rfl⟩
[GOAL]
case intro
m n : ℕ
i : Fin n
h : Fin.castSucc i ≠ Fin.last n
⊢ ↑(finSuccEquiv' (Fin.last n)) (Fin.castSucc i) = some (Fin.castLT (Fin.castSucc i) (_ : ↑(Fin.castSucc i) < n))
[PROOFSTEP]
rw [finSuccEquiv'_last_apply_castSucc]
[GOAL]
case intro
m n : ℕ
i : Fin n
h : Fin.castSucc i ≠ Fin.last n
⊢ some i = some (Fin.castLT (Fin.castSucc i) (_ : ↑(Fin.castSucc i) < n))
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
i j : Fin (n + 1)
hi : i ≠ Fin.last n
hj : j ≠ i
⊢ ↑(finSuccEquiv' i) j = some (Fin.predAbove (Fin.castLT i (_ : ↑i < n)) j)
[PROOFSTEP]
rcases Fin.exists_succAbove_eq hj with ⟨j, rfl⟩
[GOAL]
case intro
m n : ℕ
i : Fin (n + 1)
hi : i ≠ Fin.last n
j : Fin n
hj : Fin.succAbove i j ≠ i
⊢ ↑(finSuccEquiv' i) (Fin.succAbove i j) = some (Fin.predAbove (Fin.castLT i (_ : ↑i < n)) (Fin.succAbove i j))
[PROOFSTEP]
rcases Fin.exists_castSucc_eq.2 hi with ⟨i, rfl⟩
[GOAL]
case intro.intro
m n : ℕ
j i : Fin n
hi : Fin.castSucc i ≠ Fin.last n
hj : Fin.succAbove (Fin.castSucc i) j ≠ Fin.castSucc i
⊢ ↑(finSuccEquiv' (Fin.castSucc i)) (Fin.succAbove (Fin.castSucc i) j) =
    some (Fin.predAbove (Fin.castLT (Fin.castSucc i) (_ : ↑(Fin.castSucc i) < n)) (Fin.succAbove (Fin.castSucc i) j))
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
x : { x // x ≠ Fin.last n }
⊢ ↑(OrderIso.symm (finSuccAboveEquiv (Fin.last n))) x = Fin.castLT ↑x (_ : ↑↑x < n)
[PROOFSTEP]
rw [← Option.some_inj]
[GOAL]
m n : ℕ
x : { x // x ≠ Fin.last n }
⊢ some (↑(OrderIso.symm (finSuccAboveEquiv (Fin.last n))) x) = some (Fin.castLT ↑x (_ : ↑↑x < n))
[PROOFSTEP]
simpa [finSuccAboveEquiv, OrderIso.symm] using finSuccEquiv'_last_apply x.property
[GOAL]
m n : ℕ
p : Fin (n + 1)
h : p ≠ Fin.last n
x : { x // x ≠ p }
⊢ ↑(OrderIso.symm (finSuccAboveEquiv p)) x = Fin.predAbove (Fin.castLT p (_ : ↑p < n)) ↑x
[PROOFSTEP]
rw [← Option.some_inj]
[GOAL]
m n : ℕ
p : Fin (n + 1)
h : p ≠ Fin.last n
x : { x // x ≠ p }
⊢ some (↑(OrderIso.symm (finSuccAboveEquiv p)) x) = some (Fin.predAbove (Fin.castLT p (_ : ↑p < n)) ↑x)
[PROOFSTEP]
simpa [finSuccAboveEquiv, OrderIso.symm] using finSuccEquiv'_ne_last_apply h x.property
[GOAL]
m n : ℕ
⊢ ↑finSuccEquivLast (Fin.last n) = none
[PROOFSTEP]
simp [finSuccEquivLast]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
i : Fin (n + 1)
f : (j : Fin (n + 1)) → α j
⊢ (fun f => Fin.insertNth i f.fst f.snd) ((fun f => (f i, fun j => f (Fin.succAbove i j))) f) = f
[PROOFSTEP]
simp [Fin.insertNth_eq_iff]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
i : Fin (n + 1)
f : α i × ((j : Fin n) → α (Fin.succAbove i j))
⊢ (fun f => (f i, fun j => f (Fin.succAbove i j))) ((fun f => Fin.insertNth i f.fst f.snd) f) = f
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
x : Fin m ⊕ Fin n
⊢ (fun i => Fin.addCases Sum.inl Sum.inr i) (Sum.elim (Fin.castAdd n) (Fin.natAdd m) x) = x
[PROOFSTEP]
cases' x with y y
[GOAL]
case inl
m n : ℕ
y : Fin m
⊢ (fun i => Fin.addCases Sum.inl Sum.inr i) (Sum.elim (Fin.castAdd n) (Fin.natAdd m) (Sum.inl y)) = Sum.inl y
[PROOFSTEP]
dsimp
[GOAL]
case inr
m n : ℕ
y : Fin n
⊢ (fun i => Fin.addCases Sum.inl Sum.inr i) (Sum.elim (Fin.castAdd n) (Fin.natAdd m) (Sum.inr y)) = Sum.inr y
[PROOFSTEP]
dsimp
[GOAL]
case inl
m n : ℕ
y : Fin m
⊢ Fin.addCases Sum.inl Sum.inr (Fin.castAdd n y) = Sum.inl y
[PROOFSTEP]
simp
[GOAL]
case inr
m n : ℕ
y : Fin n
⊢ Fin.addCases Sum.inl Sum.inr (Fin.natAdd m y) = Sum.inr y
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
x : Fin (m + n)
⊢ Sum.elim (Fin.castAdd n) (Fin.natAdd m) ((fun i => Fin.addCases Sum.inl Sum.inr i) x) = x
[PROOFSTEP]
refine' Fin.addCases (fun i => _) (fun i => _) x
[GOAL]
case refine'_1
m n : ℕ
x : Fin (m + n)
i : Fin m
⊢ Sum.elim (Fin.castAdd n) (Fin.natAdd m) ((fun i => Fin.addCases Sum.inl Sum.inr i) (Fin.castAdd n i)) =
    Fin.castAdd n i
[PROOFSTEP]
simp
[GOAL]
case refine'_2
m n : ℕ
x : Fin (m + n)
i : Fin n
⊢ Sum.elim (Fin.castAdd n) (Fin.natAdd m) ((fun i => Fin.addCases Sum.inl Sum.inr i) (Fin.natAdd m i)) = Fin.natAdd m i
[PROOFSTEP]
simp
[GOAL]
m n✝ : ℕ
k : Fin m
n : ℕ
⊢ ↑finAddFlip (Fin.castAdd n k) = Fin.natAdd n k
[PROOFSTEP]
simp [finAddFlip]
[GOAL]
m✝ n : ℕ
k : Fin n
m : ℕ
⊢ ↑finAddFlip (Fin.natAdd m k) = Fin.castAdd m k
[PROOFSTEP]
simp [finAddFlip]
[GOAL]
m n k : ℕ
h : k < m
hk : optParam (k < m + n) (_ : k < m + n)
hnk : optParam (n + k < n + m) (_ : n + k < n + m)
⊢ ↑finAddFlip { val := k, isLt := hk } = { val := n + k, isLt := hnk }
[PROOFSTEP]
convert finAddFlip_apply_castAdd ⟨k, h⟩ n
[GOAL]
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ ↑finAddFlip { val := k, isLt := h₂ } = { val := k - m, isLt := (_ : k - m < n + m) }
[PROOFSTEP]
convert @finAddFlip_apply_natAdd n ⟨k - m, (tsub_lt_iff_right h₁).2 ?_⟩ m
[GOAL]
case h.e'_2.h.e'_6.h.e'_2
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k = ↑(Fin.natAdd m { val := k - m, isLt := (_ : k - m < n) })
[PROOFSTEP]
simp [add_tsub_cancel_of_le h₁]
[GOAL]
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k < n + m
[PROOFSTEP]
rwa [add_comm]
[GOAL]
m n k : ℕ
h : k < n
⊢ ↑(finRotate (n + 1)) { val := k, isLt := (_ : k < n + 1) } = { val := k + 1, isLt := (_ : Nat.succ k < Nat.succ n) }
[PROOFSTEP]
ext
[GOAL]
case h
m n k : ℕ
h : k < n
⊢ ↑(↑(finRotate (n + 1)) { val := k, isLt := (_ : k < n + 1) }) =
    ↑{ val := k + 1, isLt := (_ : Nat.succ k < Nat.succ n) }
[PROOFSTEP]
dsimp [finRotate_succ]
[GOAL]
case h
m n k : ℕ
h : k < n
⊢ ↑(↑finAddFlip { val := k, isLt := (_ : k < n + 1) }) = k + 1
[PROOFSTEP]
simp [finAddFlip_apply_mk_left h, add_comm]
[GOAL]
m n : ℕ
⊢ ↑(finRotate (n + 1)) { val := n, isLt := (_ : n < n + 1) } = { val := 0, isLt := (_ : 0 < Nat.succ n) }
[PROOFSTEP]
dsimp [finRotate_succ]
[GOAL]
m n : ℕ
⊢ ↑(finCongr (_ : 1 + n = n + 1)) (↑finAddFlip { val := n, isLt := (_ : n < n + 1) }) = 0
[PROOFSTEP]
rw [finAddFlip_apply_mk_right le_rfl]
[GOAL]
m n : ℕ
⊢ ↑(finCongr (_ : 1 + n = n + 1)) { val := n - n, isLt := (_ : n - n < 1 + n) } = 0
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
⊢ snoc v a = fun i => cons a v (↑(finRotate (n + 1)) i)
[PROOFSTEP]
ext ⟨i, h⟩
[GOAL]
case h.mk
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
⊢ snoc v a { val := i, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := i, isLt := h })
[PROOFSTEP]
by_cases h' : i < n
[GOAL]
case pos
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ snoc v a { val := i, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := i, isLt := h })
[PROOFSTEP]
rw [finRotate_of_lt h', Fin.snoc, Fin.cons, dif_pos h']
[GOAL]
case pos
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ _root_.cast (_ : α = α) (v (castLT { val := i, isLt := h } h')) =
    cases a v { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
[PROOFSTEP]
rfl
[GOAL]
case neg
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ snoc v a { val := i, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := i, isLt := h })
[PROOFSTEP]
have h'' : n = i := by
  simp only [not_lt] at h' 
  exact (Nat.eq_of_le_of_lt_succ h' h).symm
[GOAL]
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ n = i
[PROOFSTEP]
simp only [not_lt] at h' 
[GOAL]
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : n ≤ i
⊢ n = i
[PROOFSTEP]
exact (Nat.eq_of_le_of_lt_succ h' h).symm
[GOAL]
case neg
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
h'' : n = i
⊢ snoc v a { val := i, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := i, isLt := h })
[PROOFSTEP]
subst h''
[GOAL]
case neg
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ snoc v a { val := n, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := n, isLt := h })
[PROOFSTEP]
rw [finRotate_last', Fin.snoc, Fin.cons, dif_neg (lt_irrefl _)]
[GOAL]
case neg
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ _root_.cast (_ : α = α) a = cases a v { val := 0, isLt := (_ : 0 < Nat.succ n) }
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
i : Fin (n + 1)
⊢ ↑(finRotate (n + 1)) i = i + 1
[PROOFSTEP]
cases n
[GOAL]
case zero
m : ℕ
i : Fin (Nat.zero + 1)
⊢ ↑(finRotate (Nat.zero + 1)) i = i + 1
[PROOFSTEP]
exact @Subsingleton.elim (Fin 1) _ _ _
[GOAL]
case succ
m n✝ : ℕ
i : Fin (Nat.succ n✝ + 1)
⊢ ↑(finRotate (Nat.succ n✝ + 1)) i = i + 1
[PROOFSTEP]
rcases i.le_last.eq_or_lt with (rfl | h)
[GOAL]
case succ.inl
m n✝ : ℕ
⊢ ↑(finRotate (Nat.succ n✝ + 1)) (Fin.last (n✝ + 1)) = Fin.last (n✝ + 1) + 1
[PROOFSTEP]
simp [finRotate_last]
[GOAL]
case succ.inr
m n✝ : ℕ
i : Fin (Nat.succ n✝ + 1)
h : i < Fin.last (n✝ + 1)
⊢ ↑(finRotate (Nat.succ n✝ + 1)) i = i + 1
[PROOFSTEP]
cases i
[GOAL]
case succ.inr.mk
m n✝ val✝ : ℕ
isLt✝ : val✝ < Nat.succ n✝ + 1
h : { val := val✝, isLt := isLt✝ } < Fin.last (n✝ + 1)
⊢ ↑(finRotate (Nat.succ n✝ + 1)) { val := val✝, isLt := isLt✝ } = { val := val✝, isLt := isLt✝ } + 1
[PROOFSTEP]
simp only [Fin.lt_iff_val_lt_val, Fin.val_last, Fin.val_mk] at h 
[GOAL]
case succ.inr.mk
m n✝ val✝ : ℕ
isLt✝ : val✝ < Nat.succ n✝ + 1
h : val✝ < n✝ + 1
⊢ ↑(finRotate (Nat.succ n✝ + 1)) { val := val✝, isLt := isLt✝ } = { val := val✝, isLt := isLt✝ } + 1
[PROOFSTEP]
simp [finRotate_of_lt h, Fin.eq_iff_veq, Fin.add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ h)]
[GOAL]
m n : ℕ
⊢ ↑(finRotate (Nat.succ n)) 0 = 1
[PROOFSTEP]
rw [finRotate_succ_apply, zero_add]
[GOAL]
m n : ℕ
i : Fin (Nat.succ n)
h : i ≠ Fin.last n
⊢ ↑(↑(finRotate (n + 1)) i) = ↑i + 1
[PROOFSTEP]
rw [finRotate_succ_apply]
[GOAL]
m n : ℕ
i : Fin (Nat.succ n)
h : i ≠ Fin.last n
⊢ ↑(i + 1) = ↑i + 1
[PROOFSTEP]
have : (i : ℕ) < n := Fin.val_lt_last h
[GOAL]
m n : ℕ
i : Fin (Nat.succ n)
h : i ≠ Fin.last n
this : ↑i < n
⊢ ↑(i + 1) = ↑i + 1
[PROOFSTEP]
exact Fin.val_add_one_of_lt this
[GOAL]
m n : ℕ
i : Fin (Nat.succ n)
⊢ ↑(↑(finRotate (Nat.succ n)) i) = if i = Fin.last n then 0 else ↑i + 1
[PROOFSTEP]
rw [finRotate_succ_apply, Fin.val_add_one i]
[GOAL]
m n : ℕ
x : Fin m × Fin n
⊢ ↑x.snd + n * ↑x.fst + 1 = ↑x.fst * n + ↑x.snd + 1
[PROOFSTEP]
ac_rfl
[GOAL]
m n : ℕ
x✝ : Fin m × Fin n
x : Fin m
y : Fin n
H : 0 < n
⊢ ↑y / n + ↑x = 0 + ↑x
[PROOFSTEP]
rw [Nat.div_eq_of_lt y.2]
[GOAL]
m n✝ n : ℕ
inst✝ : NeZero n
p : ℕ × Fin n
⊢ (fun a => (a / n, ↑a)) ((fun p => p.fst * n + ↑p.snd) p) = p
[PROOFSTEP]
refine' Prod.ext _ (Fin.ext <| Nat.mul_add_mod_of_lt p.2.is_lt)
[GOAL]
m n✝ n : ℕ
inst✝ : NeZero n
p : ℕ × Fin n
⊢ ((fun a => (a / n, ↑a)) ((fun p => p.fst * n + ↑p.snd) p)).fst = p.fst
[PROOFSTEP]
dsimp only
[GOAL]
m n✝ n : ℕ
inst✝ : NeZero n
p : ℕ × Fin n
⊢ (p.fst * n + ↑p.snd) / n = p.fst
[PROOFSTEP]
rw [add_comm, Nat.add_mul_div_right _ _ (NeZero.pos n), Nat.div_eq_of_lt p.2.is_lt, zero_add]
[GOAL]
m n✝ n : ℕ
inst✝ : NeZero n
a : ℤ
⊢ (fun p => p.fst * ↑n + ↑↑p.snd) ((fun a => (a / ↑n, ↑(natMod a ↑n))) a) = a
[PROOFSTEP]
simp_rw [Fin.coe_ofNat_eq_mod, Int.coe_nat_mod, Int.natMod, Int.toNat_of_nonneg (Int.emod_nonneg _ <| NeZero.ne ↑n),
  Int.emod_emod, Int.ediv_add_emod']
[GOAL]
m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
⊢ (fun a => (a / ↑n, ↑(natMod a ↑n))) ((fun p => p.fst * ↑n + ↑↑p.snd) (q, { val := r, isLt := hrn })) =
    (q, { val := r, isLt := hrn })
[PROOFSTEP]
simp only [Fin.val_mk, Prod.mk.inj_iff, Fin.ext_iff]
[GOAL]
m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
⊢ (q * ↑n + ↑r) / ↑n = q ∧ ↑↑(natMod (q * ↑n + ↑r) ↑n) = r
[PROOFSTEP]
obtain ⟨h1, h2⟩ := Int.coe_nat_nonneg r, Int.ofNat_lt.2 hrn
[GOAL]
m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
h1 : 0 ≤ ↑r
h2 : ↑r < ↑n
⊢ (q * ↑n + ↑r) / ↑n = q ∧ ↑↑(natMod (q * ↑n + ↑r) ↑n) = r
[PROOFSTEP]
rw [add_comm, Int.add_mul_ediv_right _ _ (NeZero.ne ↑n), Int.ediv_eq_zero_of_lt h1 h2, Int.natMod,
  Int.add_mul_emod_self, Int.emod_eq_of_lt h1 h2, Int.toNat_coe_nat]
[GOAL]
m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
h1 : 0 ≤ ↑r
h2 : ↑r < ↑n
⊢ 0 + q = q ∧ ↑↑r = r
[PROOFSTEP]
exact ⟨zero_add q, Fin.val_cast_of_lt hrn⟩
[GOAL]
m✝ n✝ n m : ℕ
h : n ≤ m
i : Fin n
⊢ ↑(castLE h i) < n
[PROOFSTEP]
simp
[GOAL]
m✝ n✝ n m : ℕ
h : n ≤ m
x✝ : Fin n
⊢ (fun i => { val := ↑↑i, isLt := (_ : ↑↑i < n) }) ((fun i => { val := castLE h i, property := (_ : ↑i < n) }) x✝) = x✝
[PROOFSTEP]
simp
[GOAL]
m✝ n✝ n m : ℕ
h : n ≤ m
x✝ : { i // ↑i < n }
⊢ (fun i => { val := castLE h i, property := (_ : ↑i < n) }) ((fun i => { val := ↑↑i, isLt := (_ : ↑↑i < n) }) x✝) = x✝
[PROOFSTEP]
simp
[GOAL]
m✝ n✝ n m : ℕ
h : n ≤ m
⊢ ∀ {a b : Fin n},
    ↑{ toFun := fun i => { val := castLE h i, property := (_ : ↑i < n) },
              invFun := fun i => { val := ↑↑i, isLt := (_ : ↑↑i < n) },
              left_inv := (_ : ∀ (x : Fin n), { val := ↑x, isLt := (_ : ↑x < n) } = x),
              right_inv :=
                (_ :
                  ∀ (x : { i // ↑i < n }),
                    { val := castLE h ((fun i => { val := ↑↑i, isLt := (_ : ↑↑i < n) }) x),
                        property := (_ : ↑((fun i => { val := ↑↑i, isLt := (_ : ↑↑i < n) }) x) < n) } =
                      x) }
          a ≤
        ↑{ toFun := fun i => { val := castLE h i, property := (_ : ↑i < n) },
              invFun := fun i => { val := ↑↑i, isLt := (_ : ↑↑i < n) },
              left_inv := (_ : ∀ (x : Fin n), { val := ↑x, isLt := (_ : ↑x < n) } = x),
              right_inv :=
                (_ :
                  ∀ (x : { i // ↑i < n }),
                    { val := castLE h ((fun i => { val := ↑↑i, isLt := (_ : ↑↑i < n) }) x),
                        property := (_ : ↑((fun i => { val := ↑↑i, isLt := (_ : ↑↑i < n) }) x) < n) } =
                      x) }
          b ↔
      a ≤ b
[PROOFSTEP]
simp [(strictMono_castLE h).le_iff_le]
