[GOAL]
n m : ℕ
α : Sort u_1
k l : ℕ
h : k = l
f : Fin k → α
g : Fin l → α
⊢ HEq f g ↔ ∀ (i : Fin k), f i = g { val := ↑i, isLt := (_ : ↑i < l) }
[PROOFSTEP]
subst h
[GOAL]
n m : ℕ
α : Sort u_1
k : ℕ
f g : Fin k → α
⊢ HEq f g ↔ ∀ (i : Fin k), f i = g { val := ↑i, isLt := (_ : ↑i < k) }
[PROOFSTEP]
simp [Function.funext_iff]
[GOAL]
n m : ℕ
α : Sort u_1
k l k' l' : ℕ
h : k = l
h' : k' = l'
f : Fin k → Fin k' → α
g : Fin l → Fin l' → α
⊢ HEq f g ↔
    ∀ (i : Fin k) (j : Fin k'), f i j = g { val := ↑i, isLt := (_ : ↑i < l) } { val := ↑j, isLt := (_ : ↑j < l') }
[PROOFSTEP]
subst h
[GOAL]
n m : ℕ
α : Sort u_1
k k' l' : ℕ
h' : k' = l'
f : Fin k → Fin k' → α
g : Fin k → Fin l' → α
⊢ HEq f g ↔
    ∀ (i : Fin k) (j : Fin k'), f i j = g { val := ↑i, isLt := (_ : ↑i < k) } { val := ↑j, isLt := (_ : ↑j < l') }
[PROOFSTEP]
subst h'
[GOAL]
n m : ℕ
α : Sort u_1
k k' : ℕ
f g : Fin k → Fin k' → α
⊢ HEq f g ↔
    ∀ (i : Fin k) (j : Fin k'), f i j = g { val := ↑i, isLt := (_ : ↑i < k) } { val := ↑j, isLt := (_ : ↑j < k') }
[PROOFSTEP]
simp [Function.funext_iff]
[GOAL]
n m k l : ℕ
h : k = l
i : Fin k
j : Fin l
⊢ HEq i j ↔ ↑i = ↑j
[PROOFSTEP]
subst h
[GOAL]
n m k : ℕ
i j : Fin k
⊢ HEq i j ↔ ↑i = ↑j
[PROOFSTEP]
simp [val_eq_val]
[GOAL]
n m : ℕ
a : Fin n
⊢ min (↑a) n = ↑a
[PROOFSTEP]
simp
[GOAL]
n m : ℕ
a : Fin n
⊢ max (↑a) n = n
[PROOFSTEP]
simp
[GOAL]
n✝ m n : ℕ
⊢ PartialOrder (Fin n)
[PROOFSTEP]
infer_instance
[GOAL]
n m : ℕ
⊢ Monotone ↑equivSubtype
[PROOFSTEP]
simp [Monotone]
[GOAL]
n m : ℕ
⊢ Monotone ↑equivSubtype.symm
[PROOFSTEP]
simp [Monotone]
[GOAL]
n m : ℕ
inst✝ : NeZero n
a : Fin n
⊢ 0 < a ↔ a ≠ 0
[PROOFSTEP]
rw [← val_fin_lt, val_zero', _root_.pos_iff_ne_zero, Ne.def, Ne.def, ext_iff, val_zero']
[GOAL]
n m : ℕ
i : Fin n
⊢ ↑((fun i => { val := n - (↑i + 1), isLt := (_ : n - (↑i + 1) < n) })
        ((fun i => { val := n - (↑i + 1), isLt := (_ : n - (↑i + 1) < n) }) i)) =
    ↑i
[PROOFSTEP]
dsimp only
[GOAL]
n m : ℕ
i : Fin n
⊢ n - (n - (↑i + 1) + 1) = ↑i
[PROOFSTEP]
rw [← tsub_tsub, tsub_tsub_cancel_of_le (Nat.add_one_le_iff.2 i.is_lt), add_tsub_cancel_right]
[GOAL]
n✝ m n a : ℕ
i : Fin (n + 1)
h : n = a + ↑i
⊢ ↑revPerm i = { val := a, isLt := (_ : a < Nat.succ n) }
[PROOFSTEP]
ext
[GOAL]
case h
n✝ m n a : ℕ
i : Fin (n + 1)
h : n = a + ↑i
⊢ ↑(↑revPerm i) = ↑{ val := a, isLt := (_ : a < Nat.succ n) }
[PROOFSTEP]
dsimp
[GOAL]
case h
n✝ m n a : ℕ
i : Fin (n + 1)
h : n = a + ↑i
⊢ n + 1 - (↑i + 1) = a
[PROOFSTEP]
conv_lhs =>
  congr
  rw [h]
[GOAL]
n✝ m n a : ℕ
i : Fin (n + 1)
h : n = a + ↑i
| n + 1 - (↑i + 1)
[PROOFSTEP]
  congr
  rw [h]
[GOAL]
n✝ m n a : ℕ
i : Fin (n + 1)
h : n = a + ↑i
| n + 1 - (↑i + 1)
[PROOFSTEP]
  congr
  rw [h]
[GOAL]
n✝ m n a : ℕ
i : Fin (n + 1)
h : n = a + ↑i
| n + 1 - (↑i + 1)
[PROOFSTEP]
congr
[GOAL]
case a
n✝ m n a : ℕ
i : Fin (n + 1)
h : n = a + ↑i
| n + 1
case a n✝ m n a : ℕ i : Fin (n + 1) h : n = a + ↑i | ↑i + 1
[PROOFSTEP]
rw [h]
[GOAL]
case h
n✝ m n a : ℕ
i : Fin (n + 1)
h : n = a + ↑i
⊢ a + ↑i + 1 - (↑i + 1) = a
[PROOFSTEP]
rw [add_assoc, add_tsub_cancel_right]
[GOAL]
n m : ℕ
i j : Fin n
⊢ ↑revPerm i ≤ ↑revPerm j ↔ j ≤ i
[PROOFSTEP]
simp only [le_iff_val_le_val, val_revPerm, tsub_le_tsub_iff_left (Nat.add_one_le_iff.2 j.is_lt), add_le_add_iff_right,
  iff_self]
[GOAL]
n m : ℕ
α : Type u_1
inst✝ : Preorder α
e : Fin n ≃o Fin m
i : Fin n
⊢ ↑(↑e i) = ↑i
[PROOFSTEP]
rcases i with ⟨i, hi⟩
[GOAL]
case mk
n m : ℕ
α : Type u_1
inst✝ : Preorder α
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
⊢ ↑(↑e { val := i, isLt := hi }) = ↑{ val := i, isLt := hi }
[PROOFSTEP]
dsimp only
[GOAL]
case mk
n m : ℕ
α : Type u_1
inst✝ : Preorder α
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
⊢ ↑(↑e { val := i, isLt := hi }) = i
[PROOFSTEP]
induction' i using Nat.strong_induction_on with i h
[GOAL]
case mk.h
n m : ℕ
α : Type u_1
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
⊢ ↑(↑e { val := i, isLt := hi }) = i
[PROOFSTEP]
refine' le_antisymm (forall_lt_iff_le.1 fun j hj => _) (forall_lt_iff_le.1 fun j hj => _)
[GOAL]
case mk.h.refine'_1
n m : ℕ
α : Type u_1
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
j : ℕ
hj : j < ↑(↑e { val := i, isLt := hi })
⊢ j < i
[PROOFSTEP]
have := e.symm.lt_iff_lt.2 (mk_lt_of_lt_val hj)
[GOAL]
case mk.h.refine'_1
n m : ℕ
α : Type u_1
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
j : ℕ
hj : j < ↑(↑e { val := i, isLt := hi })
this : ↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) } < ↑(OrderIso.symm e) (↑e { val := i, isLt := hi })
⊢ j < i
[PROOFSTEP]
rw [e.symm_apply_apply] at this
[GOAL]
case mk.h.refine'_1
n m : ℕ
α : Type u_1
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
j : ℕ
hj : j < ↑(↑e { val := i, isLt := hi })
this : ↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) } < { val := i, isLt := hi }
⊢ j < i
[PROOFSTEP]
have : _ < i := this
[GOAL]
case mk.h.refine'_1
n m : ℕ
α : Type u_1
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
j : ℕ
hj : j < ↑(↑e { val := i, isLt := hi })
this✝ : ↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) } < { val := i, isLt := hi }
this : ↑(↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) }) < i
⊢ j < i
[PROOFSTEP]
convert this
[GOAL]
case h.e'_3
n m : ℕ
α : Type u_1
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
j : ℕ
hj : j < ↑(↑e { val := i, isLt := hi })
this✝ : ↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) } < { val := i, isLt := hi }
this : ↑(↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) }) < i
⊢ j = ↑(↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) })
[PROOFSTEP]
simpa using h _ this (e.symm _).is_lt
[GOAL]
case mk.h.refine'_2
n m : ℕ
α : Type u_1
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
j : ℕ
hj : j < i
⊢ j < ↑(↑e { val := i, isLt := hi })
[PROOFSTEP]
rwa [← h j hj (hj.trans hi), ← lt_iff_val_lt_val, e.lt_iff_lt]
[GOAL]
n m : ℕ
α : Type u_1
inst✝ : Preorder α
e e' : Fin n ≃o α
⊢ e = e'
[PROOFSTEP]
ext i
[GOAL]
case h.h
n m : ℕ
α : Type u_1
inst✝ : Preorder α
e e' : Fin n ≃o α
i : Fin n
⊢ ↑e i = ↑e' i
[PROOFSTEP]
rw [← e.symm.apply_eq_iff_eq, e.symm_apply_apply, ← e'.trans_apply, ext_iff, coe_orderIso_apply]
[GOAL]
n✝ m n : ℕ
⊢ ↑0 ≠ ↑1
[PROOFSTEP]
simp only [val_one, val_zero]
[GOAL]
n m : ℕ
⊢ Nontrivial (Fin n) ↔ 2 ≤ n
[PROOFSTEP]
rcases n with (_ | _ | n)
[GOAL]
case zero
m : ℕ
⊢ Nontrivial (Fin zero) ↔ 2 ≤ zero
[PROOFSTEP]
simp [← Nat.one_eq_succ_zero, Fin.nontrivial, not_nontrivial, Nat.succ_le_iff]
  -- porting note: here and in the next lemma, had to use `←Nat.one_eq_succ_zero`.
[GOAL]
case succ.zero
m : ℕ
⊢ Nontrivial (Fin (Nat.succ zero)) ↔ 2 ≤ Nat.succ zero
[PROOFSTEP]
simp [← Nat.one_eq_succ_zero, Fin.nontrivial, not_nontrivial, Nat.succ_le_iff]
  -- porting note: here and in the next lemma, had to use `←Nat.one_eq_succ_zero`.
[GOAL]
case succ.succ
m n : ℕ
⊢ Nontrivial (Fin (Nat.succ (Nat.succ n))) ↔ 2 ≤ Nat.succ (Nat.succ n)
[PROOFSTEP]
simp [← Nat.one_eq_succ_zero, Fin.nontrivial, not_nontrivial, Nat.succ_le_iff]
  -- porting note: here and in the next lemma, had to use `←Nat.one_eq_succ_zero`.
[GOAL]
n✝ m n : ℕ
⊢ ∀ (a b c : Fin n), a + b + c = a + (b + c)
[PROOFSTEP]
simp [eq_iff_veq, add_def, add_assoc]
[GOAL]
n✝ m n : ℕ
⊢ ∀ (a b : Fin n), a + b = b + a
[PROOFSTEP]
simp [eq_iff_veq, add_def, add_comm]
[GOAL]
n m : ℕ
inst✝ : NeZero n
k : Fin n
⊢ k + 0 = k
[PROOFSTEP]
simp only [add_def, val_zero', add_zero, mod_eq_of_lt (is_lt k)]
[GOAL]
n m : ℕ
inst✝ : NeZero n
k : Fin n
⊢ 0 + k = k
[PROOFSTEP]
simp [eq_iff_veq, add_def, mod_eq_of_lt (is_lt k)]
[GOAL]
n✝ m n : ℕ
⊢ ∀ (a b c : Fin n), a + b + c = a + (b + c)
[PROOFSTEP]
simp [eq_iff_veq, add_def, add_assoc]
[GOAL]
n✝ m n : ℕ
⊢ ∀ (a b : Fin n), a + b = b + a
[PROOFSTEP]
simp [eq_iff_veq, add_def, add_comm]
[GOAL]
n✝ m n : ℕ
a b : Fin n
⊢ ↑(a + b) = if n ≤ ↑a + ↑b then ↑a + ↑b - n else ↑a + ↑b
[PROOFSTEP]
rw [Fin.val_add, Nat.add_mod_eq_ite, Nat.mod_eq_of_lt (show ↑a < n from a.2), Nat.mod_eq_of_lt (show ↑b < n from b.2)]
[GOAL]
n✝ m n : ℕ
k : Fin n
⊢ ↑(bit0 k) = bit0 ↑k % n
[PROOFSTEP]
cases k
[GOAL]
case mk
n✝ m n val✝ : ℕ
isLt✝ : val✝ < n
⊢ ↑(bit0 { val := val✝, isLt := isLt✝ }) = bit0 ↑{ val := val✝, isLt := isLt✝ } % n
[PROOFSTEP]
rfl
[GOAL]
n✝ m n : ℕ
inst✝ : NeZero n
k : Fin n
⊢ ↑(bit1 k) = bit1 ↑k % n
[PROOFSTEP]
cases n
[GOAL]
case zero
n m : ℕ
inst✝ : NeZero zero
k : Fin zero
⊢ ↑(bit1 k) = bit1 ↑k % zero
[PROOFSTEP]
cases' k with k h
[GOAL]
case zero.mk
n m : ℕ
inst✝ : NeZero zero
k : ℕ
h : k < zero
⊢ ↑(bit1 { val := k, isLt := h }) = bit1 ↑{ val := k, isLt := h } % zero
[PROOFSTEP]
cases k
[GOAL]
case zero.mk.zero
n m : ℕ
inst✝ : NeZero zero
h : zero < zero
⊢ ↑(bit1 { val := zero, isLt := h }) = bit1 ↑{ val := zero, isLt := h } % zero
[PROOFSTEP]
show _ % _ = _
[GOAL]
case zero.mk.zero
n m : ℕ
inst✝ : NeZero zero
h : zero < zero
⊢ ((zero + zero) % zero + 1 % zero) % zero = bit1 ↑{ val := zero, isLt := h } % zero
[PROOFSTEP]
simp
[GOAL]
case zero.mk.succ
n m : ℕ
inst✝ : NeZero zero
n✝ : ℕ
h : Nat.succ n✝ < zero
⊢ ↑(bit1 { val := Nat.succ n✝, isLt := h }) = bit1 ↑{ val := Nat.succ n✝, isLt := h } % zero
[PROOFSTEP]
cases' h with _ h
[GOAL]
case succ
n m n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
k : Fin (Nat.succ n✝)
⊢ ↑(bit1 k) = bit1 ↑k % Nat.succ n✝
[PROOFSTEP]
simp [bit1, Fin.val_bit0, Fin.val_add, Fin.val_one]
[GOAL]
n✝ m✝ m n : ℕ
inst✝ : NeZero n
h : bit1 m < n
⊢ { val := bit1 m, isLt := h } = bit1 { val := m, isLt := (_ : m < n) }
[PROOFSTEP]
ext
[GOAL]
case h
n✝ m✝ m n : ℕ
inst✝ : NeZero n
h : bit1 m < n
⊢ ↑{ val := bit1 m, isLt := h } = ↑(bit1 { val := m, isLt := (_ : m < n) })
[PROOFSTEP]
simp only [bit1, bit0] at h
[GOAL]
case h
n✝ m✝ m n : ℕ
inst✝ : NeZero n
h : m + m + 1 < n
⊢ ↑{ val := bit1 m, isLt := h } = ↑(bit1 { val := m, isLt := (_ : m < n) })
[PROOFSTEP]
simp only [bit1, bit0, val_add, val_one', ← Nat.add_mod, Nat.mod_eq_of_lt h]
[GOAL]
n✝ m n : ℕ
inst✝ : NeZero n
a : ℕ
h : a < n
⊢ ↑↑a = a
[PROOFSTEP]
rw [← ofNat_eq_val]
[GOAL]
n✝ m n : ℕ
inst✝ : NeZero n
a : ℕ
h : a < n
⊢ ↑(ofNat'' a) = a
[PROOFSTEP]
exact Nat.mod_eq_of_lt h
[GOAL]
n✝ m n : ℕ
inst✝ : NeZero n
a : Fin n
⊢ ↑↑a = a
[PROOFSTEP]
rw [Fin.eq_iff_veq]
[GOAL]
n✝ m n : ℕ
inst✝ : NeZero n
a : Fin n
⊢ ↑↑↑a = ↑a
[PROOFSTEP]
exact val_cast_of_lt a.isLt
[GOAL]
n✝ m n : ℕ
⊢ ↑n = last n
[PROOFSTEP]
rw [← Fin.ofNat_eq_val, Fin.ofNat'', Fin.last]
[GOAL]
n✝ m n : ℕ
⊢ { val := n % (n + 1), isLt := (_ : n % (n + 1) < n + 1) } = { val := n, isLt := (_ : n < Nat.succ n) }
[PROOFSTEP]
simp only [Nat.mod_eq_of_lt n.lt_succ_self]
[GOAL]
n m : ℕ
i : Fin (n + 1)
⊢ i ≤ ↑n
[PROOFSTEP]
rw [Fin.cast_nat_eq_last]
[GOAL]
n m : ℕ
i : Fin (n + 1)
⊢ i ≤ last n
[PROOFSTEP]
exact Fin.le_last i
[GOAL]
n m : ℕ
inst✝ : NeZero n
⊢ 0 = 1 ↔ n = 1
[PROOFSTEP]
constructor
[GOAL]
case mp
n m : ℕ
inst✝ : NeZero n
⊢ 0 = 1 → n = 1
[PROOFSTEP]
intro h
[GOAL]
case mp
n m : ℕ
inst✝ : NeZero n
h : 0 = 1
⊢ n = 1
[PROOFSTEP]
have := congr_arg ((↑) : Fin n → ℕ) h
[GOAL]
case mp
n m : ℕ
inst✝ : NeZero n
h : 0 = 1
this : ↑0 = ↑1
⊢ n = 1
[PROOFSTEP]
simp only [val_zero', val_one', @eq_comm _ 0, ← Nat.dvd_iff_mod_eq_zero] at this
[GOAL]
case mp
n m : ℕ
inst✝ : NeZero n
h : 0 = 1
this : n ∣ 1
⊢ n = 1
[PROOFSTEP]
exact eq_one_of_dvd_one this
[GOAL]
case mpr
n m : ℕ
inst✝ : NeZero n
⊢ n = 1 → 0 = 1
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
m : ℕ
inst✝ : NeZero 1
⊢ 0 = 1
[PROOFSTEP]
rfl
[GOAL]
n m : ℕ
inst✝ : NeZero n
⊢ 1 = 0 ↔ n = 1
[PROOFSTEP]
rw [eq_comm, zero_eq_one_iff]
[GOAL]
n m : ℕ
inst✝ : NeZero n
⊢ succ 0 = 1
[PROOFSTEP]
cases n
[GOAL]
case zero
m : ℕ
inst✝ : NeZero zero
⊢ succ 0 = 1
[PROOFSTEP]
exact (NeZero.ne 0 rfl).elim
[GOAL]
case succ
m n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
⊢ succ 0 = 1
[PROOFSTEP]
rfl
[GOAL]
n m : ℕ
inst✝ : NeZero n
⊢ succ 1 = 2
[PROOFSTEP]
cases n
[GOAL]
case zero
m : ℕ
inst✝ : NeZero zero
⊢ succ 1 = 2
[PROOFSTEP]
exact (NeZero.ne 0 rfl).elim
[GOAL]
case succ
m n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
⊢ succ 1 = 2
[PROOFSTEP]
rfl
[GOAL]
n✝ m n : ℕ
inst✝ : NeZero n
k : Fin n
h : k ≤ 0
⊢ ↑k = ↑0
[PROOFSTEP]
rw [Nat.eq_zero_of_le_zero h]
[GOAL]
n✝ m n : ℕ
inst✝ : NeZero n
k : Fin n
h : k ≤ 0
⊢ 0 = ↑0
[PROOFSTEP]
rfl
[GOAL]
n✝ m n : ℕ
inst✝ : NeZero n
k : Fin n
⊢ k = 0 → k ≤ 0
[PROOFSTEP]
rintro rfl
[GOAL]
n✝ m n : ℕ
inst✝ : NeZero n
⊢ 0 ≤ 0
[PROOFSTEP]
exact le_refl _
[GOAL]
n✝ m n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range ↑(castLEEmb h)
⊢ ↑(↑(Equiv.ofInjective ↑(castLEEmb h) (_ : Injective ↑(castLEEmb h))).symm { val := i, property := hi }) = ↑i
[PROOFSTEP]
rw [← coe_castLE h]
[GOAL]
n✝ m n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range ↑(castLEEmb h)
⊢ ↑(castLE h (↑(Equiv.ofInjective ↑(castLEEmb h) (_ : Injective ↑(castLEEmb h))).symm { val := i, property := hi })) =
    ↑i
[PROOFSTEP]
exact congr_arg Fin.val (Equiv.apply_ofInjective_symm _ _)
[GOAL]
n m : ℕ
h : n = m
⊢ OrderIso.symm (castIso h) = castIso (_ : m = n)
[PROOFSTEP]
simp
[GOAL]
n m : ℕ
h : n = m
i : Fin n
⊢ ↑(↑(castIso h) i) = ↑i
[PROOFSTEP]
simp
[GOAL]
n m n' : ℕ
inst✝ : NeZero n
h : n = n'
⊢ Fin n'
[PROOFSTEP]
{haveI : NeZero n' := by {rw [← h]; infer_instance
  };
  exact 0
}
[GOAL]
n m n' : ℕ
inst✝ : NeZero n
h : n = n'
⊢ Fin n'
[PROOFSTEP]
haveI : NeZero n' := by {rw [← h]; infer_instance
}
[GOAL]
n m n' : ℕ
inst✝ : NeZero n
h : n = n'
⊢ NeZero n'
[PROOFSTEP]
{rw [← h]; infer_instance
}
[GOAL]
n m n' : ℕ
inst✝ : NeZero n
h : n = n'
⊢ NeZero n'
[PROOFSTEP]
rw [← h]
[GOAL]
n m n' : ℕ
inst✝ : NeZero n
h : n = n'
⊢ NeZero n
[PROOFSTEP]
infer_instance
[GOAL]
n m n' : ℕ
inst✝ : NeZero n
h : n = n'
this : NeZero n'
⊢ Fin n'
[PROOFSTEP]
exact 0
[GOAL]
n m n' : ℕ
h : n + 1 = n' + 1
⊢ ↑(↑(castIso h) (last n)) = ↑(last n')
[PROOFSTEP]
rw [coe_castIso, val_last, val_last, Nat.succ_injective h]
[GOAL]
n m : ℕ
h : n = m
i : ℕ
hn : i < n
⊢ ↑(castIso h) { val := i, isLt := hn } = { val := i, isLt := (_ : i < m) }
[PROOFSTEP]
ext
[GOAL]
case h
n m : ℕ
h : n = m
i : ℕ
hn : i < n
⊢ ↑(↑(castIso h) { val := i, isLt := hn }) = ↑{ val := i, isLt := (_ : i < m) }
[PROOFSTEP]
simp
[GOAL]
n m k : ℕ
h : n = m
h' : m = k
i : Fin n
⊢ ↑(castIso h') (↑(castIso h) i) = ↑(castIso (_ : n = k)) i
[PROOFSTEP]
ext
[GOAL]
case h
n m k : ℕ
h : n = m
h' : m = k
i : Fin n
⊢ ↑(↑(castIso h') (↑(castIso h) i)) = ↑(↑(castIso (_ : n = k)) i)
[PROOFSTEP]
simp
[GOAL]
n m : ℕ
h : optParam (n = n) (_ : n = n)
⊢ castIso h = OrderIso.refl (Fin n)
[PROOFSTEP]
ext
[GOAL]
case h.h.h
n m : ℕ
h : optParam (n = n) (_ : n = n)
x✝ : Fin n
⊢ ↑(↑(castIso h) x✝) = ↑(↑(OrderIso.refl (Fin n)) x✝)
[PROOFSTEP]
simp
[GOAL]
n m : ℕ
h : n = m
⊢ (castIso h).toEquiv = Equiv.cast (_ : Fin n = Fin m)
[PROOFSTEP]
subst h
[GOAL]
n : ℕ
⊢ (castIso (_ : n = n)).toEquiv = Equiv.cast (_ : Fin n = Fin n)
[PROOFSTEP]
simp
[GOAL]
n✝ m✝ n n' m : ℕ
i : Fin n'
h : n' + m = n + m
⊢ ↑(castIso h) (castAdd m i) = castAdd m (↑(castIso (_ : n' = n)) i)
[PROOFSTEP]
ext
[GOAL]
case h
n✝ m✝ n n' m : ℕ
i : Fin n'
h : n' + m = n + m
⊢ ↑(↑(castIso h) (castAdd m i)) = ↑(castAdd m (↑(castIso (_ : n' = n)) i))
[PROOFSTEP]
simp
[GOAL]
n✝ m✝ n m m' : ℕ
i : Fin n
h : n + m' = n + m
⊢ ↑(castIso h) (castAdd m' i) = castAdd m i
[PROOFSTEP]
ext
[GOAL]
case h
n✝ m✝ n m m' : ℕ
i : Fin n
h : n + m' = n + m
⊢ ↑(↑(castIso h) (castAdd m' i)) = ↑(castAdd m i)
[PROOFSTEP]
simp
[GOAL]
n m n' : ℕ
i : Fin n
h : Nat.succ n = Nat.succ n'
⊢ ↑(↑(castIso h) (succ i)) = ↑(succ (↑(castIso (_ : n = n')) i))
[PROOFSTEP]
simp
[GOAL]
n m n' : ℕ
i : Fin n
h : n = n'
⊢ Nat.succ n = Nat.succ n'
[PROOFSTEP]
rw [h]
[GOAL]
n m n' : ℕ
i : Fin n
h : n = n'
⊢ ↑(succ (↑(castIso h) i)) = ↑(↑(castIso (_ : Nat.succ n = Nat.succ n')) (succ i))
[PROOFSTEP]
simp
[GOAL]
n m n' : ℕ
h : n + 1 = n' + 1
i : Fin n
⊢ ↑(castIso h) (castSucc i) = castSucc (↑(castIso (_ : n = n')) i)
[PROOFSTEP]
ext
[GOAL]
case h
n m n' : ℕ
h : n + 1 = n' + 1
i : Fin n
⊢ ↑(↑(castIso h) (castSucc i)) = ↑(castSucc (↑(castIso (_ : n = n')) i))
[PROOFSTEP]
simp only [coe_castIso, coe_castSucc]
[GOAL]
n m : ℕ
inst✝ : NeZero n
i : Fin n
h : 0 < i
⊢ 0 < castSucc i
[PROOFSTEP]
simpa [lt_iff_val_lt_val] using h
[GOAL]
n m : ℕ
inst✝ : NeZero n
a : Fin n
⊢ ↑a = ↑0 ↔ ↑(castSucc a) = ↑0
[PROOFSTEP]
simp
[GOAL]
n m : ℕ
a : Fin n
⊢ ↑↑a = castSucc a
[PROOFSTEP]
ext
[GOAL]
case h
n m : ℕ
a : Fin n
⊢ ↑↑↑a = ↑(castSucc a)
[PROOFSTEP]
exact val_cast_of_lt (Nat.lt.step a.is_lt)
[GOAL]
n✝ m n : ℕ
i : Fin (Nat.succ n)
hi : i ∈ Set.range castSucc
⊢ ↑(↑(Equiv.ofInjective castSucc (_ : Injective castSucc)).symm { val := i, property := hi }) = ↑i
[PROOFSTEP]
rw [← coe_castSucc]
[GOAL]
n✝ m n : ℕ
i : Fin (Nat.succ n)
hi : i ∈ Set.range castSucc
⊢ ↑(castSucc (↑(Equiv.ofInjective castSucc (_ : Injective castSucc)).symm { val := i, property := hi })) = ↑i
[PROOFSTEP]
exact congr_arg val (Equiv.apply_ofInjective_symm _ _)
[GOAL]
n✝ m✝ n n' m : ℕ
i : Fin n'
h : n' + m = n + m
⊢ ↑(castIso h) (addNat i m) = addNat (↑(castIso (_ : n' = n)) i) m
[PROOFSTEP]
ext
[GOAL]
case h
n✝ m✝ n n' m : ℕ
i : Fin n'
h : n' + m = n + m
⊢ ↑(↑(castIso h) (addNat i m)) = ↑(addNat (↑(castIso (_ : n' = n)) i) m)
[PROOFSTEP]
simp
[GOAL]
n✝ m✝ n n' m : ℕ
i : Fin n'
h : n' = n
⊢ natAdd m (↑(castIso h) i) = ↑(castIso (_ : m + n' = m + n)) (natAdd m i)
[PROOFSTEP]
ext
[GOAL]
case h
n✝ m✝ n n' m : ℕ
i : Fin n'
h : n' = n
⊢ ↑(natAdd m (↑(castIso h) i)) = ↑(↑(castIso (_ : m + n' = m + n)) (natAdd m i))
[PROOFSTEP]
simp
[GOAL]
n✝ m✝ n n' m : ℕ
i : Fin n'
h : m + n' = m + n
⊢ ↑(castIso h) (natAdd m i) = natAdd m (↑(castIso (_ : n' = n)) i)
[PROOFSTEP]
ext
[GOAL]
case h
n✝ m✝ n n' m : ℕ
i : Fin n'
h : m + n' = m + n
⊢ ↑(↑(castIso h) (natAdd m i)) = ↑(natAdd m (↑(castIso (_ : n' = n)) i))
[PROOFSTEP]
simp
[GOAL]
n m : ℕ
i : Fin (n + m)
h : n ≤ ↑i
⊢ natAdd n (subNat n (↑(castIso (_ : n + m = m + n)) i) h) = i
[PROOFSTEP]
simp [← castIso_addNat]
[GOAL]
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ ((fun x x_1 => x < x_1) ⇒ r) f f ↔ ∀ (i : Fin n), r (f (castSucc i)) (f (succ i))
[PROOFSTEP]
constructor
[GOAL]
case mp
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ ((fun x x_1 => x < x_1) ⇒ r) f f → ∀ (i : Fin n), r (f (castSucc i)) (f (succ i))
[PROOFSTEP]
intro H i
[GOAL]
case mp
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ((fun x x_1 => x < x_1) ⇒ r) f f
i : Fin n
⊢ r (f (castSucc i)) (f (succ i))
[PROOFSTEP]
exact H i.castSucc_lt_succ
[GOAL]
case mpr
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ (∀ (i : Fin n), r (f (castSucc i)) (f (succ i))) → ((fun x x_1 => x < x_1) ⇒ r) f f
[PROOFSTEP]
refine' fun H i => Fin.induction _ _
[GOAL]
case mpr.refine'_1
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f (castSucc i)) (f (succ i))
i : Fin (n + 1)
⊢ (fun x x_1 => x < x_1) i 0 → r (f i) (f 0)
[PROOFSTEP]
exact fun h => (h.not_le (zero_le i)).elim
[GOAL]
case mpr.refine'_2
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f (castSucc i)) (f (succ i))
i : Fin (n + 1)
⊢ ∀ (i_1 : Fin n),
    ((fun x x_1 => x < x_1) i (castSucc i_1) → r (f i) (f (castSucc i_1))) →
      (fun x x_1 => x < x_1) i (succ i_1) → r (f i) (f (succ i_1))
[PROOFSTEP]
intro j ihj hij
[GOAL]
case mpr.refine'_2
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f (castSucc i)) (f (succ i))
i : Fin (n + 1)
j : Fin n
ihj : (fun x x_1 => x < x_1) i (castSucc j) → r (f i) (f (castSucc j))
hij : i < succ j
⊢ r (f i) (f (succ j))
[PROOFSTEP]
rw [← le_castSucc_iff] at hij
[GOAL]
case mpr.refine'_2
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f (castSucc i)) (f (succ i))
i : Fin (n + 1)
j : Fin n
ihj : (fun x x_1 => x < x_1) i (castSucc j) → r (f i) (f (castSucc j))
hij : i ≤ castSucc j
⊢ r (f i) (f (succ j))
[PROOFSTEP]
rcases hij.eq_or_lt with (rfl | hlt)
[GOAL]
case mpr.refine'_2.inl
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f (castSucc i)) (f (succ i))
j : Fin n
ihj : (fun x x_1 => x < x_1) (castSucc j) (castSucc j) → r (f (castSucc j)) (f (castSucc j))
hij : castSucc j ≤ castSucc j
⊢ r (f (castSucc j)) (f (succ j))
case mpr.refine'_2.inr
n m : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f (castSucc i)) (f (succ i))
i : Fin (n + 1)
j : Fin n
ihj : (fun x x_1 => x < x_1) i (castSucc j) → r (f i) (f (castSucc j))
hij : i ≤ castSucc j
hlt : i < castSucc j
⊢ r (f i) (f (succ j))
[PROOFSTEP]
exacts [H j, _root_.trans (ihj hlt) (H j)]
[GOAL]
n✝ m n : ℕ
inst✝ : NeZero n
src✝¹ : AddCommMonoid (Fin n) := addCommMonoid n
src✝ : Neg (Fin n) := neg n
x✝¹ x✝ : Fin n
a : ℕ
ha : a < n
b : ℕ
hb : b < n
⊢ (a + (n - b)) % n = (a + (n - b) % n) % n
[PROOFSTEP]
simp
[GOAL]
n✝ m n : ℕ
inst✝ : NeZero n
src✝¹ : AddCommMonoid (Fin n) := addCommMonoid n
src✝ : Neg (Fin n) := neg n
x✝ : Fin n
a : ℕ
ha : a < n
⊢ (n - ↑{ val := a, isLt := ha } + a) % n = ↑0
[PROOFSTEP]
rw [Fin.val_zero', tsub_add_cancel_of_le, Nat.mod_self]
[GOAL]
n✝ m n : ℕ
inst✝ : NeZero n
src✝¹ : AddCommMonoid (Fin n) := addCommMonoid n
src✝ : Neg (Fin n) := neg n
x✝ : Fin n
a : ℕ
ha : a < n
⊢ ↑{ val := a, isLt := ha } ≤ n
[PROOFSTEP]
exact le_of_lt ha
[GOAL]
n m : ℕ
a b : Fin n
⊢ ↑(a - b) = (↑a + (n - ↑b)) % n
[PROOFSTEP]
cases a
[GOAL]
case mk
n m : ℕ
b : Fin n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ ↑({ val := val✝, isLt := isLt✝ } - b) = (↑{ val := val✝, isLt := isLt✝ } + (n - ↑b)) % n
[PROOFSTEP]
cases b
[GOAL]
case mk.mk
n m val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ ↑({ val := val✝¹, isLt := isLt✝¹ } - { val := val✝, isLt := isLt✝ }) =
    (↑{ val := val✝¹, isLt := isLt✝¹ } + (n - ↑{ val := val✝, isLt := isLt✝ })) % n
[PROOFSTEP]
rfl
[GOAL]
n m : ℕ
a : Fin 1
⊢ ↑a = 0
[PROOFSTEP]
simp [Subsingleton.elim a 0]
[GOAL]
n m : ℕ
⊢ ↑(-1) = n
[PROOFSTEP]
cases n
[GOAL]
case zero
m : ℕ
⊢ ↑(-1) = zero
[PROOFSTEP]
simp
[GOAL]
case succ
m n✝ : ℕ
⊢ ↑(-1) = Nat.succ n✝
[PROOFSTEP]
rw [Fin.coe_neg, Fin.val_one, Nat.succ_sub_one, Nat.mod_eq_of_lt]
[GOAL]
case succ
m n✝ : ℕ
⊢ n✝ + 1 < Nat.succ n✝ + 1
[PROOFSTEP]
constructor
[GOAL]
n✝ m n : ℕ
a : Fin (n + 1)
⊢ ↑(a - 1) = if a = 0 then n else ↑a - 1
[PROOFSTEP]
cases n
[GOAL]
case zero
n m : ℕ
a : Fin (zero + 1)
⊢ ↑(a - 1) = if a = 0 then zero else ↑a - 1
[PROOFSTEP]
simp
[GOAL]
case succ
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
⊢ ↑(a - 1) = if a = 0 then Nat.succ n✝ else ↑a - 1
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
h : a = 0
⊢ ↑(a - 1) = Nat.succ n✝
[PROOFSTEP]
simp [h]
[GOAL]
case neg
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
h : ¬a = 0
⊢ ↑(a - 1) = ↑a - 1
[PROOFSTEP]
rw [sub_eq_add_neg, val_add_eq_ite, coe_neg_one, if_pos, add_comm, add_tsub_add_eq_tsub_left]
[GOAL]
case neg.hc
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
h : ¬a = 0
⊢ Nat.succ n✝ + 1 ≤ ↑a + (n✝ + 1)
[PROOFSTEP]
conv_rhs => rw [add_comm]
[GOAL]
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
h : ¬a = 0
| ↑a + (n✝ + 1)
[PROOFSTEP]
rw [add_comm]
[GOAL]
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
h : ¬a = 0
| ↑a + (n✝ + 1)
[PROOFSTEP]
rw [add_comm]
[GOAL]
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
h : ¬a = 0
| ↑a + (n✝ + 1)
[PROOFSTEP]
rw [add_comm]
[GOAL]
case neg.hc
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
h : ¬a = 0
⊢ Nat.succ n✝ + 1 ≤ n✝ + 1 + ↑a
[PROOFSTEP]
rw [add_le_add_iff_left, Nat.one_le_iff_ne_zero]
[GOAL]
case neg.hc
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
h : ¬a = 0
⊢ ↑a ≠ 0
[PROOFSTEP]
rwa [Fin.ext_iff] at h
[GOAL]
n✝ m n : ℕ
a b : Fin n
⊢ ↑(a - b) = ↑a - ↑b ↔ b ≤ a
[PROOFSTEP]
cases n
[GOAL]
case zero
n m : ℕ
a b : Fin zero
⊢ ↑(a - b) = ↑a - ↑b ↔ b ≤ a
[PROOFSTEP]
exact @finZeroElim (fun _ => _) a
[GOAL]
case succ
n m n✝ : ℕ
a b : Fin (Nat.succ n✝)
⊢ ↑(a - b) = ↑a - ↑b ↔ b ≤ a
[PROOFSTEP]
rw [le_iff_val_le_val, Fin.coe_sub, ← add_tsub_assoc_of_le b.is_lt.le a]
[GOAL]
case succ
n m n✝ : ℕ
a b : Fin (Nat.succ n✝)
⊢ (↑a + Nat.succ n✝ - ↑b) % Nat.succ n✝ = ↑a - ↑b ↔ ↑b ≤ ↑a
[PROOFSTEP]
cases' le_or_lt (b : ℕ) a with h h
[GOAL]
case succ.inl
n m n✝ : ℕ
a b : Fin (Nat.succ n✝)
h : ↑b ≤ ↑a
⊢ (↑a + Nat.succ n✝ - ↑b) % Nat.succ n✝ = ↑a - ↑b ↔ ↑b ≤ ↑a
[PROOFSTEP]
simp [← tsub_add_eq_add_tsub h, val_fin_le.mp h, Nat.mod_eq_of_lt ((Nat.sub_le _ _).trans_lt a.is_lt)]
[GOAL]
case succ.inr
n m n✝ : ℕ
a b : Fin (Nat.succ n✝)
h : ↑a < ↑b
⊢ (↑a + Nat.succ n✝ - ↑b) % Nat.succ n✝ = ↑a - ↑b ↔ ↑b ≤ ↑a
[PROOFSTEP]
rw [Nat.mod_eq_of_lt, tsub_eq_zero_of_le h.le, tsub_eq_zero_iff_le, ← not_iff_not]
[GOAL]
case succ.inr
n m n✝ : ℕ
a b : Fin (Nat.succ n✝)
h : ↑a < ↑b
⊢ ¬↑a + Nat.succ n✝ ≤ ↑b ↔ ¬↑b ≤ ↑a
[PROOFSTEP]
simpa [b.is_lt.trans_le le_add_self] using h
[GOAL]
case succ.inr
n m n✝ : ℕ
a b : Fin (Nat.succ n✝)
h : ↑a < ↑b
⊢ ↑a + Nat.succ n✝ - ↑b < Nat.succ n✝
[PROOFSTEP]
rwa [tsub_lt_iff_left (b.is_lt.le.trans le_add_self), add_lt_add_iff_right]
[GOAL]
n✝ m n : ℕ
a b : Fin n
⊢ ↑(a - b) = n + ↑a - ↑b ↔ a < b
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
n m : ℕ
a b : Fin zero
⊢ ↑(a - b) = zero + ↑a - ↑b ↔ a < b
[PROOFSTEP]
exact @finZeroElim (fun _ => _) a
[GOAL]
case succ
n✝ m n : ℕ
a b : Fin (Nat.succ n)
⊢ ↑(a - b) = Nat.succ n + ↑a - ↑b ↔ a < b
[PROOFSTEP]
rw [lt_iff_val_lt_val, Fin.coe_sub, add_comm]
[GOAL]
case succ
n✝ m n : ℕ
a b : Fin (Nat.succ n)
⊢ (Nat.succ n - ↑b + ↑a) % Nat.succ n = Nat.succ n + ↑a - ↑b ↔ ↑a < ↑b
[PROOFSTEP]
cases' le_or_lt (b : ℕ) a with h h
[GOAL]
case succ.inl
n✝ m n : ℕ
a b : Fin (Nat.succ n)
h : ↑b ≤ ↑a
⊢ (Nat.succ n - ↑b + ↑a) % Nat.succ n = Nat.succ n + ↑a - ↑b ↔ ↑a < ↑b
[PROOFSTEP]
refine iff_of_false ?_ (not_lt_of_le h)
[GOAL]
case succ.inl
n✝ m n : ℕ
a b : Fin (Nat.succ n)
h : ↑b ≤ ↑a
⊢ ¬(Nat.succ n - ↑b + ↑a) % Nat.succ n = Nat.succ n + ↑a - ↑b
[PROOFSTEP]
simpa [add_tsub_assoc_of_le h] using ((Nat.mod_lt _ (Nat.succ_pos _)).trans_le le_self_add).ne
[GOAL]
case succ.inr
n✝ m n : ℕ
a b : Fin (Nat.succ n)
h : ↑a < ↑b
⊢ (Nat.succ n - ↑b + ↑a) % Nat.succ n = Nat.succ n + ↑a - ↑b ↔ ↑a < ↑b
[PROOFSTEP]
simp [← tsub_tsub_assoc b.is_lt.le h.le, ← tsub_add_eq_add_tsub b.is_lt.le,
  Nat.mod_eq_of_lt (tsub_lt_self (Nat.succ_pos _) (tsub_pos_of_lt h)), val_fin_le.mp _]
[GOAL]
case succ.inr
n✝ m n : ℕ
a b : Fin (Nat.succ n)
h : ↑a < ↑b
⊢ a < b
[PROOFSTEP]
exact h
[GOAL]
n✝ m n : ℕ
k : Fin (n + 2)
⊢ k < k - 1 ↔ k = 0
[PROOFSTEP]
rcases k with ⟨_ | k, hk⟩
[GOAL]
case mk.zero
n✝ m n : ℕ
hk : zero < n + 2
⊢ { val := zero, isLt := hk } < { val := zero, isLt := hk } - 1 ↔ { val := zero, isLt := hk } = 0
case mk.succ
n✝ m n k : ℕ
hk : Nat.succ k < n + 2
⊢ { val := Nat.succ k, isLt := hk } < { val := Nat.succ k, isLt := hk } - 1 ↔ { val := Nat.succ k, isLt := hk } = 0
[PROOFSTEP]
simp [lt_iff_val_lt_val]
[GOAL]
case mk.succ
n✝ m n k : ℕ
hk : Nat.succ k < n + 2
⊢ { val := Nat.succ k, isLt := hk } < { val := Nat.succ k, isLt := hk } - 1 ↔ { val := Nat.succ k, isLt := hk } = 0
[PROOFSTEP]
have : (k + 1 + (n + 1)) % (n + 2) = k % (n + 2) := by rw [add_right_comm, add_assoc, add_mod_right]
[GOAL]
n✝ m n k : ℕ
hk : Nat.succ k < n + 2
⊢ (k + 1 + (n + 1)) % (n + 2) = k % (n + 2)
[PROOFSTEP]
rw [add_right_comm, add_assoc, add_mod_right]
[GOAL]
case mk.succ
n✝ m n k : ℕ
hk : Nat.succ k < n + 2
this : (k + 1 + (n + 1)) % (n + 2) = k % (n + 2)
⊢ { val := Nat.succ k, isLt := hk } < { val := Nat.succ k, isLt := hk } - 1 ↔ { val := Nat.succ k, isLt := hk } = 0
[PROOFSTEP]
simp [lt_iff_val_lt_val, ext_iff, Fin.coe_sub, succ_eq_add_one, this, mod_eq_of_lt ((lt_succ_self _).trans hk)]
[GOAL]
n✝ m n : ℕ
k : Fin (n + 1)
⊢ k ≤ k - 1 ↔ k = 0
[PROOFSTEP]
cases n
[GOAL]
case zero
n m : ℕ
k : Fin (zero + 1)
⊢ k ≤ k - 1 ↔ k = 0
[PROOFSTEP]
simp [fin_one_eq_zero k]
[GOAL]
case succ
n m n✝ : ℕ
k : Fin (Nat.succ n✝ + 1)
⊢ k ≤ k - 1 ↔ k = 0
[PROOFSTEP]
rw [← lt_sub_one_iff, le_iff_lt_or_eq, lt_sub_one_iff, or_iff_left_iff_imp, eq_comm, sub_eq_iff_eq_add]
[GOAL]
case succ
n m n✝ : ℕ
k : Fin (Nat.succ n✝ + 1)
⊢ k = k + 1 → k = 0
[PROOFSTEP]
simp
[GOAL]
n✝ m n : ℕ
k : Fin (n + 1)
⊢ ¬k - 1 < k ↔ ¬0 < k
[PROOFSTEP]
simp only [not_lt, le_sub_one_iff, le_zero_iff]
[GOAL]
n m : ℕ
i : Fin (n + 1)
⊢ ↑(last n - i) = ↑(↑revPerm i)
[PROOFSTEP]
rw [coe_sub_iff_le.2 i.le_last, val_last, val_revPerm, Nat.succ_sub_succ_eq_sub]
[GOAL]
n m : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ succAbove a 0 = 0
[PROOFSTEP]
rw [Fin.succAbove_below]
[GOAL]
n m : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 = 0
[PROOFSTEP]
simp
[GOAL]
case h
n m : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 < a
[PROOFSTEP]
exact bot_lt_iff_ne_bot.mpr ha
[GOAL]
n m : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
b : Fin n
ha : a ≠ 0
⊢ succAbove a b = 0 ↔ b = 0
[PROOFSTEP]
simp only [← succAbove_ne_zero_zero ha, ← succAboveEmb_apply, OrderEmbedding.eq_iff_eq, iff_self]
[GOAL]
n m : ℕ
⊢ succAbove (last n) = castSucc
[PROOFSTEP]
ext
[GOAL]
case h.h
n m : ℕ
x✝ : Fin n
⊢ ↑(succAbove (last n) x✝) = ↑(castSucc x✝)
[PROOFSTEP]
simp only [succAbove_below, castSucc_lt_last]
[GOAL]
n m : ℕ
i : Fin n
⊢ succAbove (last n) i = castSucc i
[PROOFSTEP]
rw [succAbove_last]
[GOAL]
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : p ≤ castSucc i
⊢ succAbove p i = succ i
[PROOFSTEP]
simp [le_iff_val_le_val] at h
[GOAL]
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : ↑p ≤ ↑i
⊢ succAbove p i = succ i
[PROOFSTEP]
simp [succAbove, h.not_lt]
[GOAL]
n m : ℕ
p : Fin (n + 1)
i : Fin n
⊢ succAbove p i < p ↔ castSucc i < p
[PROOFSTEP]
refine' Iff.intro _ _
[GOAL]
case refine'_1
n m : ℕ
p : Fin (n + 1)
i : Fin n
⊢ succAbove p i < p → castSucc i < p
[PROOFSTEP]
intro h
[GOAL]
case refine'_1
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : succAbove p i < p
⊢ castSucc i < p
[PROOFSTEP]
cases' succAbove_lt_ge p i with H H
[GOAL]
case refine'_1.inl
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : succAbove p i < p
H : castSucc i < p
⊢ castSucc i < p
[PROOFSTEP]
exact H
[GOAL]
case refine'_1.inr
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : succAbove p i < p
H : p ≤ castSucc i
⊢ castSucc i < p
[PROOFSTEP]
rw [succAbove_above _ _ H] at h
[GOAL]
case refine'_1.inr
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : succ i < p
H : p ≤ castSucc i
⊢ castSucc i < p
[PROOFSTEP]
exact lt_trans (castSucc_lt_succ i) h
[GOAL]
case refine'_2
n m : ℕ
p : Fin (n + 1)
i : Fin n
⊢ castSucc i < p → succAbove p i < p
[PROOFSTEP]
intro h
[GOAL]
case refine'_2
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : castSucc i < p
⊢ succAbove p i < p
[PROOFSTEP]
rw [succAbove_below _ _ h]
[GOAL]
case refine'_2
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : castSucc i < p
⊢ castSucc i < p
[PROOFSTEP]
exact h
[GOAL]
n m : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p < succAbove p i ↔ p ≤ castSucc i
[PROOFSTEP]
refine' Iff.intro _ _
[GOAL]
case refine'_1
n m : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p < succAbove p i → p ≤ castSucc i
[PROOFSTEP]
intro h
[GOAL]
case refine'_1
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : p < succAbove p i
⊢ p ≤ castSucc i
[PROOFSTEP]
cases' succAbove_lt_ge p i with H H
[GOAL]
case refine'_1.inl
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : p < succAbove p i
H : castSucc i < p
⊢ p ≤ castSucc i
[PROOFSTEP]
rw [succAbove_below _ _ H] at h
[GOAL]
case refine'_1.inl
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : p < castSucc i
H : castSucc i < p
⊢ p ≤ castSucc i
[PROOFSTEP]
exact le_of_lt h
[GOAL]
case refine'_1.inr
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : p < succAbove p i
H : p ≤ castSucc i
⊢ p ≤ castSucc i
[PROOFSTEP]
exact H
[GOAL]
case refine'_2
n m : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p ≤ castSucc i → p < succAbove p i
[PROOFSTEP]
intro h
[GOAL]
case refine'_2
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : p ≤ castSucc i
⊢ p < succAbove p i
[PROOFSTEP]
rw [succAbove_above _ _ h]
[GOAL]
case refine'_2
n m : ℕ
p : Fin (n + 1)
i : Fin n
h : p ≤ castSucc i
⊢ p < succ i
[PROOFSTEP]
exact lt_of_le_of_lt h (castSucc_lt_succ i)
[GOAL]
n m : ℕ
p : Fin (n + 1)
i : Fin n
⊢ succAbove p i ≠ p
[PROOFSTEP]
intro eq
[GOAL]
n m : ℕ
p : Fin (n + 1)
i : Fin n
eq : succAbove p i = p
⊢ False
[PROOFSTEP]
by_cases H : castSucc i < p
[GOAL]
case pos
n m : ℕ
p : Fin (n + 1)
i : Fin n
eq : succAbove p i = p
H : castSucc i < p
⊢ False
[PROOFSTEP]
simp [lt_irrefl, ← succAbove_below _ _ H, eq] at H
[GOAL]
case neg
n m : ℕ
p : Fin (n + 1)
i : Fin n
eq : succAbove p i = p
H : ¬castSucc i < p
⊢ False
[PROOFSTEP]
simpa [← succAbove_above _ _ (le_of_not_lt H), eq, H] using castSucc_lt_succ i
[GOAL]
n m : ℕ
inst✝ : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
⊢ 0 < succAbove p i
[PROOFSTEP]
by_cases H : castSucc i < p
[GOAL]
case pos
n m : ℕ
inst✝ : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
H : castSucc i < p
⊢ 0 < succAbove p i
[PROOFSTEP]
simpa [succAbove_below _ _ H] using castSucc_pos' h
[GOAL]
case neg
n m : ℕ
inst✝ : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
H : ¬castSucc i < p
⊢ 0 < succAbove p i
[PROOFSTEP]
simp [succAbove_above _ _ (le_of_not_lt H)]
[GOAL]
n m : ℕ
x y : Fin (n + 1)
h : x < y
hx : optParam (↑x < n) (_ : ↑x < n)
⊢ succAbove y (castLT x hx) = x
[PROOFSTEP]
rw [succAbove_below, castSucc_castLT]
[GOAL]
case h
n m : ℕ
x y : Fin (n + 1)
h : x < y
hx : optParam (↑x < n) (_ : ↑x < n)
⊢ castSucc (castLT x hx) < y
[PROOFSTEP]
exact h
[GOAL]
n m : ℕ
x y : Fin (n + 1)
h : x < y
hy : optParam (y ≠ 0) (_ : y ≠ 0)
⊢ succAbove x (pred y hy) = y
[PROOFSTEP]
rw [succAbove_above, succ_pred]
[GOAL]
case h
n m : ℕ
x y : Fin (n + 1)
h : x < y
hy : optParam (y ≠ 0) (_ : y ≠ 0)
⊢ x ≤ castSucc (pred y hy)
[PROOFSTEP]
simpa [le_iff_val_le_val] using Nat.le_pred_of_lt h
[GOAL]
n m : ℕ
x : Fin n
y : Fin (n + 1)
h : castSucc x < y
h' : optParam (↑(succAbove y x) < n) (_ : ↑(succAbove y x) < n)
⊢ castLT (succAbove y x) h' = x
[PROOFSTEP]
simp only [succAbove_below _ _ h, castLT_castSucc]
[GOAL]
n m : ℕ
x : Fin n
y : Fin (n + 1)
h : y ≤ castSucc x
h' : optParam (succAbove y x ≠ 0) (_ : succAbove y x ≠ 0)
⊢ pred (succAbove y x) h' = x
[PROOFSTEP]
simp only [succAbove_above _ _ h, pred_succ]
[GOAL]
n m : ℕ
x y : Fin (n + 1)
h : x ≠ y
⊢ ∃ z, succAbove y z = x
[PROOFSTEP]
cases' h.lt_or_lt with hlt hlt
[GOAL]
case inl
n m : ℕ
x y : Fin (n + 1)
h : x ≠ y
hlt : x < y
⊢ ∃ z, succAbove y z = x
case inr n m : ℕ x y : Fin (n + 1) h : x ≠ y hlt : y < x ⊢ ∃ z, succAbove y z = x
[PROOFSTEP]
exacts [⟨_, succAbove_castLT hlt⟩, ⟨_, succAbove_pred hlt⟩]
[GOAL]
n m : ℕ
x y : Fin (n + 1)
⊢ (∃ z, succAbove x z = y) ↔ y ≠ x
[PROOFSTEP]
refine' ⟨_, exists_succAbove_eq⟩
[GOAL]
n m : ℕ
x y : Fin (n + 1)
⊢ (∃ z, succAbove x z = y) → y ≠ x
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case intro
n m : ℕ
x : Fin (n + 1)
y : Fin n
⊢ succAbove x y ≠ x
[PROOFSTEP]
exact succAbove_ne _ _
[GOAL]
n✝ m n : ℕ
⊢ Set.range succ = {0}ᶜ
[PROOFSTEP]
rw [← succAbove_zero]
[GOAL]
n✝ m n : ℕ
⊢ Set.range (succAbove 0) = {0}ᶜ
[PROOFSTEP]
exact range_succAbove (0 : Fin (n + 1))
[GOAL]
n m : ℕ
x : Fin (n + 1)
⊢ (∃ y, succ y = x) ↔ x ≠ 0
[PROOFSTEP]
convert @exists_succAbove_eq_iff n 0 x
[GOAL]
n m : ℕ
x✝¹ x✝ : Fin (n + 1)
h : succAbove x✝¹ = succAbove x✝
⊢ x✝¹ = x✝
[PROOFSTEP]
simpa [range_succAbove] using congr_arg (fun f : Fin n → Fin (n + 1) => (Set.range f)ᶜ) h
[GOAL]
n✝ m n : ℕ
i : Fin n
⊢ succAbove 0 i = succ i
[PROOFSTEP]
rfl
[GOAL]
n✝ m n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ castSucc 0 < succ i
[PROOFSTEP]
simp only [castSucc_zero', succ_pos]
[GOAL]
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : castSucc j < i
⊢ succAbove (succ i) (succ j) = succ (succAbove i j)
[PROOFSTEP]
have h' : castSucc j.succ < i.succ := by simpa [lt_iff_val_lt_val] using h
[GOAL]
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : castSucc j < i
⊢ castSucc (succ j) < succ i
[PROOFSTEP]
simpa [lt_iff_val_lt_val] using h
[GOAL]
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : castSucc j < i
h' : castSucc (succ j) < succ i
⊢ succAbove (succ i) (succ j) = succ (succAbove i j)
[PROOFSTEP]
ext
[GOAL]
case h
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : castSucc j < i
h' : castSucc (succ j) < succ i
⊢ ↑(succAbove (succ i) (succ j)) = ↑(succ (succAbove i j))
[PROOFSTEP]
simp [succAbove_below _ _ h, succAbove_below _ _ h']
[GOAL]
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : castSucc j ≥ i
⊢ succAbove (succ i) (succ j) = succ (succAbove i j)
[PROOFSTEP]
have h' : i.succ ≤ castSucc j.succ := by simpa [le_iff_val_le_val] using h
[GOAL]
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : castSucc j ≥ i
⊢ succ i ≤ castSucc (succ j)
[PROOFSTEP]
simpa [le_iff_val_le_val] using h
[GOAL]
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : castSucc j ≥ i
h' : succ i ≤ castSucc (succ j)
⊢ succAbove (succ i) (succ j) = succ (succAbove i j)
[PROOFSTEP]
ext
[GOAL]
case h
n✝ m n : ℕ
i : Fin (n + 1)
j : Fin n
h : castSucc j ≥ i
h' : succ i ≤ castSucc (succ j)
⊢ ↑(succAbove (succ i) (succ j)) = ↑(succ (succAbove i j))
[PROOFSTEP]
simp [succAbove_above _ _ h, succAbove_above _ _ h']
[GOAL]
n✝ m n : ℕ
⊢ succAbove 1 0 = 0
[PROOFSTEP]
rfl
[GOAL]
n✝ m n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ succAbove (succ i) 1 = succ (succAbove i 0)
[PROOFSTEP]
rw [← succ_zero_eq_one']
[GOAL]
n✝ m n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ succAbove (succ i) (succ 0) = succ (succAbove i 0)
[PROOFSTEP]
convert succ_succAbove_succ i 0
[GOAL]
n✝ m n : ℕ
j : Fin n
⊢ succAbove 1 (succ j) = succ (succ j)
[PROOFSTEP]
have := succ_succAbove_succ 0 j
[GOAL]
n✝ m n : ℕ
j : Fin n
this : succAbove (succ 0) (succ j) = succ (succAbove 0 j)
⊢ succAbove 1 (succ j) = succ (succ j)
[PROOFSTEP]
rwa [succ_zero_eq_one, zero_succAbove] at this
[GOAL]
n✝ m n : ℕ
⊢ succAbove 1 1 = 2
[PROOFSTEP]
have := succ_succAbove_succ (0 : Fin (n + 2)) (0 : Fin (n + 2))
[GOAL]
n✝ m n : ℕ
this : succAbove (succ 0) (succ ↑↑0) = succ (succAbove 0 ↑↑0)
⊢ succAbove 1 1 = 2
[PROOFSTEP]
simp only [succ_zero_eq_one, val_zero, Nat.cast_zero, zero_succAbove, succ_one_eq_two] at this
[GOAL]
n✝ m n : ℕ
this : succAbove 1 1 = 2
⊢ succAbove 1 1 = 2
[PROOFSTEP]
exact this
[GOAL]
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
⊢ predAbove p a ≤ predAbove p b
[PROOFSTEP]
dsimp [predAbove]
[GOAL]
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
⊢ (if h : castSucc p < a then pred a (_ : a ≠ 0) else castLT a (_ : ↑a < n)) ≤
    if h : castSucc p < b then pred b (_ : b ≠ 0) else castLT b (_ : ↑b < n)
[PROOFSTEP]
split_ifs with ha hb hb
[GOAL]
case pos
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : castSucc p < a
hb : castSucc p < b
⊢ pred a (_ : a ≠ 0) ≤ pred b (_ : b ≠ 0)
case neg
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : castSucc p < a
hb : ¬castSucc p < b
⊢ pred a (_ : a ≠ 0) ≤ castLT b (_ : ↑b < n)
case pos
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬castSucc p < a
hb : castSucc p < b
⊢ castLT a (_ : ↑a < n) ≤ pred b (_ : b ≠ 0)
case neg
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬castSucc p < a
hb : ¬castSucc p < b
⊢ castLT a (_ : ↑a < n) ≤ castLT b (_ : ↑b < n)
[PROOFSTEP]
all_goals simp only [le_iff_val_le_val, coe_pred]
[GOAL]
case pos
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : castSucc p < a
hb : castSucc p < b
⊢ pred a (_ : a ≠ 0) ≤ pred b (_ : b ≠ 0)
[PROOFSTEP]
simp only [le_iff_val_le_val, coe_pred]
[GOAL]
case neg
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : castSucc p < a
hb : ¬castSucc p < b
⊢ pred a (_ : a ≠ 0) ≤ castLT b (_ : ↑b < n)
[PROOFSTEP]
simp only [le_iff_val_le_val, coe_pred]
[GOAL]
case pos
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬castSucc p < a
hb : castSucc p < b
⊢ castLT a (_ : ↑a < n) ≤ pred b (_ : b ≠ 0)
[PROOFSTEP]
simp only [le_iff_val_le_val, coe_pred]
[GOAL]
case neg
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬castSucc p < a
hb : ¬castSucc p < b
⊢ castLT a (_ : ↑a < n) ≤ castLT b (_ : ↑b < n)
[PROOFSTEP]
simp only [le_iff_val_le_val, coe_pred]
[GOAL]
case pos
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : castSucc p < a
hb : castSucc p < b
⊢ ↑a - 1 ≤ ↑b - 1
[PROOFSTEP]
exact pred_le_pred H
[GOAL]
case neg
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : castSucc p < a
hb : ¬castSucc p < b
⊢ ↑a - 1 ≤ ↑(castLT b (_ : ↑b < n))
[PROOFSTEP]
calc
  _ ≤ _ := Nat.pred_le _
  _ ≤ _ := H
[GOAL]
case pos
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬castSucc p < a
hb : castSucc p < b
⊢ ↑(castLT a (_ : ↑a < n)) ≤ ↑b - 1
[PROOFSTEP]
simp at ha
[GOAL]
case pos
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha✝ : ¬castSucc p < a
hb : castSucc p < b
ha : a ≤ castSucc p
⊢ ↑(castLT a (_ : ↑a < n)) ≤ ↑b - 1
[PROOFSTEP]
exact le_pred_of_lt (lt_of_le_of_lt ha hb)
[GOAL]
case neg
n m : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬castSucc p < a
hb : ¬castSucc p < b
⊢ ↑(castLT a (_ : ↑a < n)) ≤ ↑(castLT b (_ : ↑b < n))
[PROOFSTEP]
exact H
[GOAL]
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
⊢ (fun p => predAbove p i) a ≤ (fun p => predAbove p i) b
[PROOFSTEP]
dsimp [predAbove]
[GOAL]
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
⊢ (if h : castSucc a < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n)) ≤
    if h : castSucc b < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n)
[PROOFSTEP]
split_ifs with ha hb hb
[GOAL]
case pos
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : castSucc a < i
hb : castSucc b < i
⊢ pred i (_ : i ≠ 0) ≤ pred i (_ : i ≠ 0)
[PROOFSTEP]
rfl
[GOAL]
case neg
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : castSucc a < i
hb : ¬castSucc b < i
⊢ pred i (_ : i ≠ 0) ≤ castLT i (_ : ↑i < n)
[PROOFSTEP]
exact pred_le _
[GOAL]
case pos
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬castSucc a < i
hb : castSucc b < i
⊢ castLT i (_ : ↑i < n) ≤ pred i (_ : i ≠ 0)
[PROOFSTEP]
have : b < a := castSucc_lt_castSucc_iff.mpr (hb.trans_le (le_of_not_gt ha))
[GOAL]
case pos
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬castSucc a < i
hb : castSucc b < i
this : b < a
⊢ castLT i (_ : ↑i < n) ≤ pred i (_ : i ≠ 0)
[PROOFSTEP]
exact absurd H this.not_le
[GOAL]
case neg
n m : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬castSucc a < i
hb : ¬castSucc b < i
⊢ castLT i (_ : ↑i < n) ≤ castLT i (_ : ↑i < n)
[PROOFSTEP]
rfl
[GOAL]
n m : ℕ
⊢ castPred 1 = 1
[PROOFSTEP]
cases n
[GOAL]
case zero
m : ℕ
⊢ castPred 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case succ
m n✝ : ℕ
⊢ castPred 1 = 1
[PROOFSTEP]
rfl
[GOAL]
n m : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ predAbove 0 i = pred i hi
[PROOFSTEP]
dsimp [predAbove]
[GOAL]
n m : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ (if h : 0 < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n + 1)) = pred i hi
[PROOFSTEP]
rw [dif_pos]
[GOAL]
case hc
n m : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ 0 < i
[PROOFSTEP]
exact pos_iff_ne_zero.mpr hi
[GOAL]
n m : ℕ
⊢ ↑(castPred (last (n + 1))) = ↑(last n)
[PROOFSTEP]
simp [castPred, predAbove, castSucc_lt_last]
[GOAL]
n✝ m n i : ℕ
h : i < n + 1
⊢ castPred { val := i, isLt := (_ : i < Nat.succ (n + 1)) } = { val := i, isLt := h }
[PROOFSTEP]
have : ¬castSucc (last n) < ⟨i, lt_succ_of_lt h⟩ := by simpa [lt_iff_val_lt_val] using le_of_lt_succ h
[GOAL]
n✝ m n i : ℕ
h : i < n + 1
⊢ ¬castSucc (last n) < { val := i, isLt := (_ : i < Nat.succ (n + 1)) }
[PROOFSTEP]
simpa [lt_iff_val_lt_val] using le_of_lt_succ h
[GOAL]
n✝ m n i : ℕ
h : i < n + 1
this : ¬castSucc (last n) < { val := i, isLt := (_ : i < Nat.succ (n + 1)) }
⊢ castPred { val := i, isLt := (_ : i < Nat.succ (n + 1)) } = { val := i, isLt := h }
[PROOFSTEP]
simp [castPred, predAbove, this]
[GOAL]
n✝ m n : ℕ
a : Fin (n + 2)
hx : a < last (n + 1)
⊢ ↑(castPred a) = ↑a
[PROOFSTEP]
rcases a with ⟨a, ha⟩
[GOAL]
case mk
n✝ m n a : ℕ
ha : a < n + 2
hx : { val := a, isLt := ha } < last (n + 1)
⊢ ↑(castPred { val := a, isLt := ha }) = ↑{ val := a, isLt := ha }
[PROOFSTEP]
rw [castPred_mk]
[GOAL]
case mk.h
n✝ m n a : ℕ
ha : a < n + 2
hx : { val := a, isLt := ha } < last (n + 1)
⊢ a < n + 1
[PROOFSTEP]
exact hx
[GOAL]
n m : ℕ
p : Fin (n + 1)
i : Fin (n + 2)
h : i ≤ castSucc p
⊢ predAbove p i = castPred i
[PROOFSTEP]
have : i ≤ castSucc (last n) := h.trans p.le_last
[GOAL]
n m : ℕ
p : Fin (n + 1)
i : Fin (n + 2)
h : i ≤ castSucc p
this : i ≤ castSucc (last n)
⊢ predAbove p i = castPred i
[PROOFSTEP]
simp [predAbove, castPred, h.not_lt, this.not_lt]
[GOAL]
n m : ℕ
i : Fin n
⊢ predAbove (last n) ↑↑i = castPred ↑↑i
[PROOFSTEP]
rw [predAbove_last]
[GOAL]
n m : ℕ
p : Fin n
i : Fin (n + 1)
h : castSucc p < i
⊢ predAbove p i = pred i (_ : i ≠ 0)
[PROOFSTEP]
simp [predAbove, h]
[GOAL]
n m : ℕ
p : Fin n
i : Fin (n + 1)
h : i ≠ castSucc p
⊢ succAbove (castSucc p) (predAbove p i) = i
[PROOFSTEP]
dsimp [predAbove, succAbove]
[GOAL]
n m : ℕ
p : Fin n
i : Fin (n + 1)
h : i ≠ castSucc p
⊢ (if ↑(if h : castSucc p < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n)) < ↑p then
      castSucc (if h : castSucc p < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n))
    else succ (if h : castSucc p < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n))) =
    i
[PROOFSTEP]
rcases p with ⟨p, _⟩
[GOAL]
case mk
n m : ℕ
i : Fin (n + 1)
p : ℕ
isLt✝ : p < n
h : i ≠ castSucc { val := p, isLt := isLt✝ }
⊢ (if
        ↑(if h : castSucc { val := p, isLt := isLt✝ } < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n)) <
          ↑{ val := p, isLt := isLt✝ } then
      castSucc (if h : castSucc { val := p, isLt := isLt✝ } < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n))
    else succ (if h : castSucc { val := p, isLt := isLt✝ } < i then pred i (_ : i ≠ 0) else castLT i (_ : ↑i < n))) =
    i
[PROOFSTEP]
rcases i with ⟨i, _⟩
[GOAL]
case mk.mk
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
⊢ (if
        ↑(if h : castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
              pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
            else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) <
          ↑{ val := p, isLt := isLt✝¹ } then
      castSucc
        (if h : castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
          pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
        else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))
    else
      succ
        (if h : castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
          pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
        else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))) =
    { val := i, isLt := isLt✝ }
[PROOFSTEP]
cases' lt_or_le i p with H H
[GOAL]
case mk.mk.inl
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ (if
        ↑(if h : castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
              pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
            else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) <
          ↑{ val := p, isLt := isLt✝¹ } then
      castSucc
        (if h : castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
          pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
        else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))
    else
      succ
        (if h : castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
          pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
        else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))) =
    { val := i, isLt := isLt✝ }
[PROOFSTEP]
rw [dif_neg]
[GOAL]
case mk.mk.inl
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ (if ↑(castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) < ↑{ val := p, isLt := isLt✝¹ } then
      castSucc (castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))
    else succ (castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))) =
    { val := i, isLt := isLt✝ }
case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
[PROOFSTEP]
rw [if_pos]
[GOAL]
case mk.mk.inl
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ castSucc (castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) = { val := i, isLt := isLt✝ }
case mk.mk.inl.hc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ↑(castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) < ↑{ val := p, isLt := isLt✝¹ }
case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.inl.hc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ↑(castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) < ↑{ val := p, isLt := isLt✝¹ }
case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
[PROOFSTEP]
exact H
[GOAL]
case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ ¬castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
[PROOFSTEP]
simp
[GOAL]
case mk.mk.inl.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : i < p
⊢ i ≤ p
[PROOFSTEP]
apply le_of_lt H
[GOAL]
case mk.mk.inr
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ (if
        ↑(if h : castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
              pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
            else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n)) <
          ↑{ val := p, isLt := isLt✝¹ } then
      castSucc
        (if h : castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
          pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
        else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))
    else
      succ
        (if h : castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ } then
          pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)
        else castLT { val := i, isLt := isLt✝ } (_ : ↑{ val := i, isLt := isLt✝ } < n))) =
    { val := i, isLt := isLt✝ }
[PROOFSTEP]
rw [dif_pos]
[GOAL]
case mk.mk.inr
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ (if ↑(pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)) < ↑{ val := p, isLt := isLt✝¹ } then
      castSucc (pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0))
    else succ (pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0))) =
    { val := i, isLt := isLt✝ }
case mk.mk.inr.hc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
[PROOFSTEP]
rw [if_neg]
[GOAL]
case mk.mk.inr
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ succ (pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)) = { val := i, isLt := isLt✝ }
[PROOFSTEP]
simp
[GOAL]
case mk.mk.inr.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ ¬↑(pred { val := i, isLt := isLt✝ } (_ : { val := i, isLt := isLt✝ } ≠ 0)) < ↑{ val := p, isLt := isLt✝¹ }
[PROOFSTEP]
simp only [pred, Fin.mk_lt_mk, not_lt]
[GOAL]
case mk.mk.inr.hnc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ p ≤ ↑(subNat 1 { val := i, isLt := isLt✝ } (_ : 0 < ↑{ val := i, isLt := isLt✝ }))
[PROOFSTEP]
exact Nat.le_pred_of_lt (h.symm.lt_of_le H)
[GOAL]
case mk.mk.inr.hc
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n + 1
h : { val := i, isLt := isLt✝ } ≠ castSucc { val := p, isLt := isLt✝¹ }
H : p ≤ i
⊢ castSucc { val := p, isLt := isLt✝¹ } < { val := i, isLt := isLt✝ }
[PROOFSTEP]
exact lt_of_le_of_ne H h.symm
[GOAL]
n m : ℕ
p i : Fin n
⊢ predAbove p (succAbove (castSucc p) i) = i
[PROOFSTEP]
dsimp [predAbove, succAbove]
[GOAL]
n m : ℕ
p i : Fin n
⊢ (if h : castSucc p < if ↑i < ↑p then castSucc i else succ i then
      pred (if ↑i < ↑p then castSucc i else succ i) (_ : (if ↑i < ↑p then castSucc i else succ i) ≠ 0)
    else castLT (if ↑i < ↑p then castSucc i else succ i) (_ : ↑(if ↑i < ↑p then castSucc i else succ i) < n)) =
    i
[PROOFSTEP]
rcases p with ⟨p, _⟩
[GOAL]
case mk
n m : ℕ
i : Fin n
p : ℕ
isLt✝ : p < n
⊢ (if h : castSucc { val := p, isLt := isLt✝ } < if ↑i < ↑{ val := p, isLt := isLt✝ } then castSucc i else succ i then
      pred (if ↑i < ↑{ val := p, isLt := isLt✝ } then castSucc i else succ i)
        (_ : (if ↑i < ↑{ val := p, isLt := isLt✝ } then castSucc i else succ i) ≠ 0)
    else
      castLT (if ↑i < ↑{ val := p, isLt := isLt✝ } then castSucc i else succ i)
        (_ : ↑(if ↑i < ↑{ val := p, isLt := isLt✝ } then castSucc i else succ i) < n)) =
    i
[PROOFSTEP]
rcases i with ⟨i, _⟩
[GOAL]
case mk.mk
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
⊢ (if h :
        castSucc { val := p, isLt := isLt✝¹ } <
          if ↑{ val := i, isLt := isLt✝ } < ↑{ val := p, isLt := isLt✝¹ } then castSucc { val := i, isLt := isLt✝ }
          else succ { val := i, isLt := isLt✝ } then
      pred
        (if ↑{ val := i, isLt := isLt✝ } < ↑{ val := p, isLt := isLt✝¹ } then castSucc { val := i, isLt := isLt✝ }
        else succ { val := i, isLt := isLt✝ })
        (_ :
          (if ↑{ val := i, isLt := isLt✝ } < ↑{ val := p, isLt := isLt✝¹ } then castSucc { val := i, isLt := isLt✝ }
            else succ { val := i, isLt := isLt✝ }) ≠
            0)
    else
      castLT
        (if ↑{ val := i, isLt := isLt✝ } < ↑{ val := p, isLt := isLt✝¹ } then castSucc { val := i, isLt := isLt✝ }
        else succ { val := i, isLt := isLt✝ })
        (_ :
          ↑(if ↑{ val := i, isLt := isLt✝ } < ↑{ val := p, isLt := isLt✝¹ } then castSucc { val := i, isLt := isLt✝ }
              else succ { val := i, isLt := isLt✝ }) <
            n)) =
    { val := i, isLt := isLt✝ }
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
⊢ (if h :
        { val := p, isLt := (_ : p < Nat.succ n) } <
          if i < p then { val := i, isLt := (_ : i < Nat.succ n) }
          else { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) } then
      pred
        (if i < p then { val := i, isLt := (_ : i < Nat.succ n) }
        else { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) })
        (_ :
          (if i < p then { val := i, isLt := (_ : i < Nat.succ n) }
            else { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }) ≠
            0)
    else
      castLT
        (if i < p then { val := i, isLt := (_ : i < Nat.succ n) }
        else { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) })
        (_ :
          ↑(if i < p then { val := i, isLt := (_ : i < Nat.succ n) }
              else { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }) <
            n)) =
    { val := i, isLt := isLt✝ }
[PROOFSTEP]
split_ifs with h₁ h₂ h₃
[GOAL]
case pos
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
h₁ : i < p
h₂ : { val := p, isLt := (_ : p < Nat.succ n) } < { val := i, isLt := (_ : i < Nat.succ n) }
⊢ pred { val := i, isLt := (_ : i < Nat.succ n) } (_ : { val := i, isLt := (_ : i < Nat.succ n) } ≠ 0) =
    { val := i, isLt := isLt✝ }
[PROOFSTEP]
simp only [← val_fin_lt, not_lt] at h₁ h₂
[GOAL]
case pos
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
h₁ : i < p
h₂✝ : { val := p, isLt := (_ : p < Nat.succ n) } < { val := i, isLt := (_ : i < Nat.succ n) }
h₂ : p < i
⊢ pred { val := i, isLt := (_ : i < Nat.succ n) } (_ : { val := i, isLt := (_ : i < Nat.succ n) } ≠ 0) =
    { val := i, isLt := isLt✝ }
[PROOFSTEP]
exact (lt_le_antisymm h₁ (le_of_lt h₂)).elim
[GOAL]
case neg
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
h₁ : i < p
h₂ : ¬{ val := p, isLt := (_ : p < Nat.succ n) } < { val := i, isLt := (_ : i < Nat.succ n) }
⊢ castLT { val := i, isLt := (_ : i < Nat.succ n) } (_ : ↑{ val := i, isLt := (_ : i < Nat.succ n) } < n) =
    { val := i, isLt := isLt✝ }
[PROOFSTEP]
rfl
[GOAL]
case pos
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
h₁ : ¬i < p
h₃ : { val := p, isLt := (_ : p < Nat.succ n) } < { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
⊢ pred { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
      (_ : { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) } ≠ 0) =
    { val := i, isLt := isLt✝ }
[PROOFSTEP]
rfl
[GOAL]
case neg
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
h₁ : ¬i < p
h₃ : ¬{ val := p, isLt := (_ : p < Nat.succ n) } < { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
⊢ castLT { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
      (_ : ↑{ val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) } < n) =
    { val := i, isLt := isLt✝ }
[PROOFSTEP]
simp only [← val_fin_lt, not_lt] at h₁ h₃
[GOAL]
case neg
n m p : ℕ
isLt✝¹ : p < n
i : ℕ
isLt✝ : i < n
h₁✝ : ¬i < p
h₃✝ : ¬{ val := p, isLt := (_ : p < Nat.succ n) } < { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
h₁ : p ≤ i
h₃ : i + 1 ≤ p
⊢ castLT { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
      (_ : ↑{ val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) } < n) =
    { val := i, isLt := isLt✝ }
[PROOFSTEP]
contradiction
[GOAL]
n m : ℕ
a : Fin (n + 1)
ha : a ≠ 0
ha' : optParam (castSucc a ≠ 0) (_ : castSucc a ≠ 0)
⊢ castSucc (pred a ha) = pred (castSucc a) ha'
[PROOFSTEP]
cases a
[GOAL]
case mk
n m val✝ : ℕ
isLt✝ : val✝ < n + 1
ha : { val := val✝, isLt := isLt✝ } ≠ 0
ha' : optParam (castSucc { val := val✝, isLt := isLt✝ } ≠ 0) (_ : castSucc { val := val✝, isLt := isLt✝ } ≠ 0)
⊢ castSucc (pred { val := val✝, isLt := isLt✝ } ha) = pred (castSucc { val := val✝, isLt := isLt✝ }) ha'
[PROOFSTEP]
rfl
[GOAL]
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (succAbove a b ≠ 0) (_ : succAbove a b ≠ 0)
⊢ succAbove (pred a ha) (pred b hb) = pred (succAbove a b) hk
[PROOFSTEP]
obtain hbelow | habove := lt_or_le (castSucc b) a
[GOAL]
case inl
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (succAbove a b ≠ 0) (_ : succAbove a b ≠ 0)
hbelow : castSucc b < a
⊢ succAbove (pred a ha) (pred b hb) = pred (succAbove a b) hk
[PROOFSTEP]
rw [Fin.succAbove_below]
[GOAL]
case inl
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (succAbove a b ≠ 0) (_ : succAbove a b ≠ 0)
hbelow : castSucc b < a
⊢ castSucc (pred b hb) = pred (succAbove a b) hk
[PROOFSTEP]
rwa [castSucc_pred_eq_pred_castSucc, Fin.pred_inj, Fin.succAbove_below]
[GOAL]
case inl.h
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (succAbove a b ≠ 0) (_ : succAbove a b ≠ 0)
hbelow : castSucc b < a
⊢ castSucc (pred b hb) < pred a ha
[PROOFSTEP]
rwa [castSucc_pred_eq_pred_castSucc, pred_lt_pred_iff]
[GOAL]
case inr
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (succAbove a b ≠ 0) (_ : succAbove a b ≠ 0)
habove : a ≤ castSucc b
⊢ succAbove (pred a ha) (pred b hb) = pred (succAbove a b) hk
[PROOFSTEP]
rw [Fin.succAbove_above]
[GOAL]
case inr
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (succAbove a b ≠ 0) (_ : succAbove a b ≠ 0)
habove : a ≤ castSucc b
⊢ succ (pred b hb) = pred (succAbove a b) hk
case inr.h
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (succAbove a b ≠ 0) (_ : succAbove a b ≠ 0)
habove : a ≤ castSucc b
⊢ pred a ha ≤ castSucc (pred b hb)
[PROOFSTEP]
have : (b.pred hb).succ = b.succ.pred (succ_ne_zero _) := by rw [succ_pred, pred_succ]
[GOAL]
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (succAbove a b ≠ 0) (_ : succAbove a b ≠ 0)
habove : a ≤ castSucc b
⊢ succ (pred b hb) = pred (succ b) (_ : succ b ≠ 0)
[PROOFSTEP]
rw [succ_pred, pred_succ]
[GOAL]
case inr
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (succAbove a b ≠ 0) (_ : succAbove a b ≠ 0)
habove : a ≤ castSucc b
this : succ (pred b hb) = pred (succ b) (_ : succ b ≠ 0)
⊢ succ (pred b hb) = pred (succAbove a b) hk
[PROOFSTEP]
rwa [this, Fin.pred_inj, Fin.succAbove_above]
[GOAL]
case inr.h
n m : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : optParam (succAbove a b ≠ 0) (_ : succAbove a b ≠ 0)
habove : a ≤ castSucc b
⊢ pred a ha ≤ castSucc (pred b hb)
[PROOFSTEP]
rwa [castSucc_pred_eq_pred_castSucc, Fin.pred_le_pred_iff]
[GOAL]
n✝ m n : ℕ
a : Fin n
b : Fin (n + 1)
⊢ predAbove (succ a) (succ b) = succ (predAbove a b)
[PROOFSTEP]
obtain h₁ | h₂ := lt_or_le (castSucc a) b
[GOAL]
case inl
n✝ m n : ℕ
a : Fin n
b : Fin (n + 1)
h₁ : castSucc a < b
⊢ predAbove (succ a) (succ b) = succ (predAbove a b)
[PROOFSTEP]
rw [Fin.predAbove_above _ _ h₁, Fin.succ_pred, Fin.predAbove_above, Fin.pred_succ]
[GOAL]
case inl.h
n✝ m n : ℕ
a : Fin n
b : Fin (n + 1)
h₁ : castSucc a < b
⊢ castSucc (succ a) < succ b
case inl.h n✝ m n : ℕ a : Fin n b : Fin (n + 1) h₁ : castSucc a < b ⊢ castSucc (succ a) < succ b
[PROOFSTEP]
simpa only [lt_iff_val_lt_val, coe_castSucc, val_succ, add_lt_add_iff_right] using h₁
[GOAL]
case inr
n✝ m n : ℕ
a : Fin n
b : Fin (n + 1)
h₂ : b ≤ castSucc a
⊢ predAbove (succ a) (succ b) = succ (predAbove a b)
[PROOFSTEP]
cases' n with n
[GOAL]
case inr.zero
n m : ℕ
a : Fin zero
b : Fin (zero + 1)
h₂ : b ≤ castSucc a
⊢ predAbove (succ a) (succ b) = succ (predAbove a b)
[PROOFSTEP]
exfalso
[GOAL]
case inr.zero.h
n m : ℕ
a : Fin zero
b : Fin (zero + 1)
h₂ : b ≤ castSucc a
⊢ False
[PROOFSTEP]
exact not_lt_zero' a.is_lt
[GOAL]
case inr.succ
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ castSucc a
⊢ predAbove (succ a) (succ b) = succ (predAbove a b)
[PROOFSTEP]
rw [Fin.predAbove_below a b h₂,
  Fin.predAbove_below a.succ b.succ
    (by simpa only [le_iff_val_le_val, val_succ, coe_castSucc, add_le_add_iff_right] using h₂)]
[GOAL]
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ castSucc a
⊢ succ b ≤ castSucc (succ a)
[PROOFSTEP]
simpa only [le_iff_val_le_val, val_succ, coe_castSucc, add_le_add_iff_right] using h₂
[GOAL]
case inr.succ
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ castSucc a
⊢ castPred (succ b) = succ (castPred b)
[PROOFSTEP]
ext
[GOAL]
case inr.succ.h
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ castSucc a
⊢ ↑(castPred (succ b)) = ↑(succ (castPred b))
[PROOFSTEP]
have h₀ : (b : ℕ) < n + 1 := by
  simp only [le_iff_val_le_val, coe_castSucc] at h₂
  simpa only [lt_succ_iff] using h₂.trans a.is_le
[GOAL]
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ castSucc a
⊢ ↑b < n + 1
[PROOFSTEP]
simp only [le_iff_val_le_val, coe_castSucc] at h₂
[GOAL]
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : ↑b ≤ ↑a
⊢ ↑b < n + 1
[PROOFSTEP]
simpa only [lt_succ_iff] using h₂.trans a.is_le
[GOAL]
case inr.succ.h
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ castSucc a
h₀ : ↑b < n + 1
⊢ ↑(castPred (succ b)) = ↑(succ (castPred b))
[PROOFSTEP]
have h₁ : (b.succ : ℕ) < n + 2 := by
  rw [← Nat.succ_lt_succ_iff] at h₀
  simpa only [val_succ] using h₀
[GOAL]
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ castSucc a
h₀ : ↑b < n + 1
⊢ ↑(succ b) < n + 2
[PROOFSTEP]
rw [← Nat.succ_lt_succ_iff] at h₀
[GOAL]
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ castSucc a
h₀ : Nat.succ ↑b < Nat.succ (n + 1)
⊢ ↑(succ b) < n + 2
[PROOFSTEP]
simpa only [val_succ] using h₀
[GOAL]
case inr.succ.h
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ castSucc a
h₀ : ↑b < n + 1
h₁ : ↑(succ b) < n + 2
⊢ ↑(castPred (succ b)) = ↑(succ (castPred b))
[PROOFSTEP]
simp only [coe_castPred b h₀, coe_castPred b.succ h₁, val_succ]
[GOAL]
n m : ℕ
i : Fin (n + 1)
⊢ castPred (castSucc i) = i
[PROOFSTEP]
simp [castPred, predAbove, not_lt.mpr (le_last i)]
[GOAL]
n m : ℕ
i : Fin (n + 2)
h : i < last (n + 1)
⊢ castSucc (castPred i) = i
[PROOFSTEP]
rw [castPred, predAbove, dif_neg]
[GOAL]
n m : ℕ
i : Fin (n + 2)
h : i < last (n + 1)
⊢ castSucc (castLT i (_ : ↑i < n + 1)) = i
[PROOFSTEP]
simp [Fin.eq_iff_veq]
[GOAL]
case hnc
n m : ℕ
i : Fin (n + 2)
h : i < last (n + 1)
⊢ ¬castSucc (last n) < i
[PROOFSTEP]
exact h.not_le
[GOAL]
n m : ℕ
i : Fin (n + 2)
⊢ ↑(castPred i) ≤ ↑i
[PROOFSTEP]
rcases i.le_last.eq_or_lt with (rfl | h)
[GOAL]
case inl
n m : ℕ
⊢ ↑(castPred (last (n + 1))) ≤ ↑(last (n + 1))
[PROOFSTEP]
simp
[GOAL]
case inr
n m : ℕ
i : Fin (n + 2)
h : i < last (n + 1)
⊢ ↑(castPred i) ≤ ↑i
[PROOFSTEP]
rw [castPred, predAbove, dif_neg]
[GOAL]
case inr
n m : ℕ
i : Fin (n + 2)
h : i < last (n + 1)
⊢ ↑(castLT i (_ : ↑i < n + 1)) ≤ ↑i
[PROOFSTEP]
simp
[GOAL]
case inr.hnc
n m : ℕ
i : Fin (n + 2)
h : i < last (n + 1)
⊢ ¬castSucc (last n) < i
[PROOFSTEP]
simpa [lt_iff_val_lt_val, le_iff_val_le_val, lt_succ_iff] using h
[GOAL]
n m : ℕ
i : Fin (n + 2)
⊢ ↑(castPred i) < ↑i ↔ i = last (n + 1)
[PROOFSTEP]
rcases i.le_last.eq_or_lt with (rfl | H)
[GOAL]
case inl
n m : ℕ
⊢ ↑(castPred (last (n + 1))) < ↑(last (n + 1)) ↔ last (n + 1) = last (n + 1)
[PROOFSTEP]
simp
[GOAL]
case inr
n m : ℕ
i : Fin (n + 2)
H : i < last (n + 1)
⊢ ↑(castPred i) < ↑i ↔ i = last (n + 1)
[PROOFSTEP]
simp only [_root_.ne_of_lt H]
[GOAL]
case inr
n m : ℕ
i : Fin (n + 2)
H : i < last (n + 1)
⊢ ↑(castPred i) < ↑i ↔ False
[PROOFSTEP]
rw [← castSucc_castPred H]
[GOAL]
case inr
n m : ℕ
i : Fin (n + 2)
H : i < last (n + 1)
⊢ ↑(castPred (castSucc (castPred i))) < ↑(castSucc (castPred i)) ↔ False
[PROOFSTEP]
simp
[GOAL]
n m : ℕ
i : Fin (n + 2)
⊢ i < last (n + 1) ↔ ↑(castPred i) = ↑i
[PROOFSTEP]
rcases i.le_last.eq_or_lt with (rfl | H)
[GOAL]
case inl
n m : ℕ
⊢ last (n + 1) < last (n + 1) ↔ ↑(castPred (last (n + 1))) = ↑(last (n + 1))
[PROOFSTEP]
simp
[GOAL]
case inr
n m : ℕ
i : Fin (n + 2)
H : i < last (n + 1)
⊢ i < last (n + 1) ↔ ↑(castPred i) = ↑i
[PROOFSTEP]
simp only [H]
[GOAL]
case inr
n m : ℕ
i : Fin (n + 2)
H : i < last (n + 1)
⊢ True ↔ ↑(castPred i) = ↑i
[PROOFSTEP]
rw [← castSucc_castPred H]
[GOAL]
case inr
n m : ℕ
i : Fin (n + 2)
H : i < last (n + 1)
⊢ True ↔ ↑(castPred (castSucc (castPred i))) = ↑(castSucc (castPred i))
[PROOFSTEP]
simp
[GOAL]
n m : ℕ
inst✝ : NeZero n
k : Fin n
⊢ k * 1 = k
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
m : ℕ
inst✝ : NeZero zero
k : Fin zero
⊢ k * 1 = k
[PROOFSTEP]
simp
[GOAL]
case succ
m n : ℕ
inst✝ : NeZero (Nat.succ n)
k : Fin (Nat.succ n)
⊢ k * 1 = k
[PROOFSTEP]
cases n
[GOAL]
case succ.zero
m : ℕ
inst✝ : NeZero (Nat.succ zero)
k : Fin (Nat.succ zero)
⊢ k * 1 = k
[PROOFSTEP]
simp [fin_one_eq_zero]
[GOAL]
case succ.succ
m n✝ : ℕ
inst✝ : NeZero (Nat.succ (Nat.succ n✝))
k : Fin (Nat.succ (Nat.succ n✝))
⊢ k * 1 = k
[PROOFSTEP]
simp [eq_iff_veq, mul_def, mod_eq_of_lt (is_lt k)]
[GOAL]
n m : ℕ
inst✝ : NeZero n
k : Fin n
⊢ 1 * k = k
[PROOFSTEP]
rw [Fin.mul_comm, Fin.mul_one']
[GOAL]
n m : ℕ
inst✝ : NeZero n
k : Fin n
⊢ k * 0 = 0
[PROOFSTEP]
simp [eq_iff_veq, mul_def]
[GOAL]
n m : ℕ
inst✝ : NeZero n
k : Fin n
⊢ 0 * k = 0
[PROOFSTEP]
simp [eq_iff_veq, mul_def]
[GOAL]
n✝ m n k : ℕ
i✝ : Fin (k + 1)
i : Q(ℕ)
this : «$n» =Q «$k» + 1
⊢ Q(NeZero «$n»)
[PROOFSTEP]
exact q(NeZero.succ)


[GOAL]
C : FloatCfg
e : ℤ
m : ℕ
⊢ Decidable (ValidFinite e m)
[PROOFSTEP]
unfold ValidFinite
[GOAL]
C : FloatCfg
e : ℤ
m : ℕ
⊢ Decidable (emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑(Nat.size m) - ↑prec) emin)
[PROOFSTEP]
infer_instance
[GOAL]
C : FloatCfg
⊢ emin ≤ emin + ↑prec - 1
[PROOFSTEP]
rw [add_sub_assoc]
[GOAL]
C : FloatCfg
⊢ emin ≤ emin + (↑prec - 1)
[PROOFSTEP]
apply le_add_of_nonneg_right
[GOAL]
case h
C : FloatCfg
⊢ 0 ≤ ↑prec - 1
[PROOFSTEP]
apply sub_nonneg_of_le
[GOAL]
case h.a
C : FloatCfg
⊢ 1 ≤ ↑prec
[PROOFSTEP]
apply Int.ofNat_le_ofNat_of_le
[GOAL]
case h.a.a
C : FloatCfg
⊢ 1 ≤ prec
[PROOFSTEP]
exact C.precPos
[GOAL]
C : FloatCfg
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
C : FloatCfg
this : prec ≤ 2 * emax
⊢ emin + ↑prec - 1 ≤ ↑emax
[PROOFSTEP]
rw [← Int.ofNat_le] at this
[GOAL]
C : FloatCfg
this : ↑prec ≤ ↑(2 * emax)
⊢ emin + ↑prec - 1 ≤ ↑emax
[PROOFSTEP]
rw [← sub_nonneg] at *
[GOAL]
C : FloatCfg
this✝ : ↑prec ≤ ↑(2 * emax)
this : 0 ≤ ↑(2 * emax) - ↑prec
⊢ 0 ≤ ↑emax - (emin + ↑prec - 1)
[PROOFSTEP]
simp only [emin, emax] at *
[GOAL]
C : FloatCfg
this✝ : ↑prec ≤ ↑(2 * FloatCfg.emax)
this : 0 ≤ ↑(2 * FloatCfg.emax) - ↑prec
⊢ 0 ≤ ↑FloatCfg.emax - (1 - ↑FloatCfg.emax + ↑prec - 1)
[PROOFSTEP]
ring_nf
[GOAL]
C : FloatCfg
this✝ : ↑prec ≤ ↑(2 * FloatCfg.emax)
this : 0 ≤ ↑(2 * FloatCfg.emax) - ↑prec
⊢ 0 ≤ ↑FloatCfg.emax * 2 - ↑prec
[PROOFSTEP]
rw [mul_comm]
[GOAL]
C : FloatCfg
this✝ : ↑prec ≤ ↑(2 * FloatCfg.emax)
this : 0 ≤ ↑(2 * FloatCfg.emax) - ↑prec
⊢ 0 ≤ 2 * ↑FloatCfg.emax - ↑prec
[PROOFSTEP]
assumption
[GOAL]
C : FloatCfg
⊢ emin = max (emin + ↑(Nat.size 0) - ↑prec) emin
[PROOFSTEP]
rw [max_eq_right]
[GOAL]
C : FloatCfg
⊢ emin + ↑(Nat.size 0) - ↑prec ≤ emin
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
C : FloatCfg
n d : ℕ+
⊢ Float × Bool
[PROOFSTEP]
let e₁ : ℤ := n.1.size - d.1.size - prec
[GOAL]
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(Nat.size ↑n) - ↑(Nat.size ↑d) - ↑prec
⊢ Float × Bool
[PROOFSTEP]
cases' h₁ : Int.shift2 d.1 n.1 (e₁ + prec) with d₁ n₁
[GOAL]
case mk
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(Nat.size ↑n) - ↑(Nat.size ↑d) - ↑prec
d₁ n₁ : ℕ
h₁ : Int.shift2 (↑d) (↑n) (e₁ + ↑prec) = (d₁, n₁)
⊢ Float × Bool
[PROOFSTEP]
let e₂ := if n₁ < d₁ then e₁ - 1 else e₁
[GOAL]
case mk
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(Nat.size ↑n) - ↑(Nat.size ↑d) - ↑prec
d₁ n₁ : ℕ
h₁ : Int.shift2 (↑d) (↑n) (e₁ + ↑prec) = (d₁, n₁)
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
⊢ Float × Bool
[PROOFSTEP]
let e₃ := max e₂ emin
[GOAL]
case mk
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(Nat.size ↑n) - ↑(Nat.size ↑d) - ↑prec
d₁ n₁ : ℕ
h₁ : Int.shift2 (↑d) (↑n) (e₁ + ↑prec) = (d₁, n₁)
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
⊢ Float × Bool
[PROOFSTEP]
cases' h₂ : Int.shift2 d.1 n.1 (e₃ + prec) with d₂ n₂
[GOAL]
case mk.mk
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(Nat.size ↑n) - ↑(Nat.size ↑d) - ↑prec
d₁ n₁ : ℕ
h₁ : Int.shift2 (↑d) (↑n) (e₁ + ↑prec) = (d₁, n₁)
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
d₂ n₂ : ℕ
h₂ : Int.shift2 (↑d) (↑n) (e₃ + ↑prec) = (d₂, n₂)
⊢ Float × Bool
[PROOFSTEP]
let r := mkRat n₂ d₂
[GOAL]
case mk.mk
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(Nat.size ↑n) - ↑(Nat.size ↑d) - ↑prec
d₁ n₁ : ℕ
h₁ : Int.shift2 (↑d) (↑n) (e₁ + ↑prec) = (d₁, n₁)
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
d₂ n₂ : ℕ
h₂ : Int.shift2 (↑d) (↑n) (e₃ + ↑prec) = (d₂, n₂)
r : ℚ := mkRat (↑n₂) d₂
⊢ Float × Bool
[PROOFSTEP]
let m := r.floor
[GOAL]
case mk.mk
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(Nat.size ↑n) - ↑(Nat.size ↑d) - ↑prec
d₁ n₁ : ℕ
h₁ : Int.shift2 (↑d) (↑n) (e₁ + ↑prec) = (d₁, n₁)
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
d₂ n₂ : ℕ
h₂ : Int.shift2 (↑d) (↑n) (e₃ + ↑prec) = (d₂, n₂)
r : ℚ := mkRat (↑n₂) d₂
m : ℤ := Rat.floor r
⊢ Float × Bool
[PROOFSTEP]
refine' (Float.finite Bool.false e₃ (Int.toNat m) _, r.den = 1)
[GOAL]
case mk.mk
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(Nat.size ↑n) - ↑(Nat.size ↑d) - ↑prec
d₁ n₁ : ℕ
h₁ : Int.shift2 (↑d) (↑n) (e₁ + ↑prec) = (d₁, n₁)
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
d₂ n₂ : ℕ
h₂ : Int.shift2 (↑d) (↑n) (e₃ + ↑prec) = (d₂, n₂)
r : ℚ := mkRat (↑n₂) d₂
m : ℤ := Rat.floor r
⊢ ValidFinite e₃ (Int.toNat m)
[PROOFSTEP]
exact lcProof
[GOAL]
C : FloatCfg
e : ℤ
m : ℕ
v : ValidFinite e m
m' : ℕ := Nat.succ m
ss : Nat.size m' = Nat.size m
⊢ ValidFinite e m'
[PROOFSTEP]
unfold ValidFinite at *
[GOAL]
C : FloatCfg
e : ℤ
m : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑(Nat.size m) - ↑prec) emin
m' : ℕ := Nat.succ m
ss : Nat.size m' = Nat.size m
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑(Nat.size m') - ↑prec) emin
[PROOFSTEP]
rw [ss]
[GOAL]
C : FloatCfg
e : ℤ
m : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑(Nat.size m) - ↑prec) emin
m' : ℕ := Nat.succ m
ss : Nat.size m' = Nat.size m
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑(Nat.size m) - ↑prec) emin
[PROOFSTEP]
exact v
[GOAL]
C : FloatCfg
e : ℤ
m m' : ℕ
v : ValidFinite e (Nat.succ m')
ss : Nat.size m' = Nat.size (Nat.succ m')
⊢ ValidFinite e m'
[PROOFSTEP]
unfold ValidFinite at *
[GOAL]
C : FloatCfg
e : ℤ
m m' : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑(Nat.size (Nat.succ m')) - ↑prec) emin
ss : Nat.size m' = Nat.size (Nat.succ m')
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑(Nat.size m') - ↑prec) emin
[PROOFSTEP]
rw [ss]
[GOAL]
C : FloatCfg
e : ℤ
m m' : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑(Nat.size (Nat.succ m')) - ↑prec) emin
ss : Nat.size m' = Nat.size (Nat.succ m')
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑(Nat.size (Nat.succ m')) - ↑prec) emin
[PROOFSTEP]
exact v


[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b) ≤
    comap (↑(zmultiplesHom { x // x ∈ zmultiples a }) { val := a, property := (_ : a ∈ zmultiples a) })
      (stabilizer { x // x ∈ zmultiples a } b)
[PROOFSTEP]
rw [zmultiples_le, mem_comap, mem_stabilizer_iff, zmultiplesHom_apply, coe_nat_zsmul]
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b • { val := a, property := (_ : a ∈ zmultiples a) } +ᵥ b = b
[PROOFSTEP]
simp_rw [← vadd_iterate]
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ (fun x => { val := a, property := (_ : a ∈ zmultiples a) } +ᵥ x)^[minimalPeriod (fun x => a +ᵥ x) b] b = b
[PROOFSTEP]
exact isPeriodicPt_minimalPeriod ((· +ᵥ ·) a) b
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ Injective
    ↑(QuotientAddGroup.map (zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b))
        (stabilizer { x // x ∈ zmultiples a } b)
        (↑(zmultiplesHom { x // x ∈ zmultiples a }) { val := a, property := (_ : a ∈ zmultiples a) })
        (_ :
          zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b) ≤
            comap (↑(zmultiplesHom { x // x ∈ zmultiples a }) { val := a, property := (_ : a ∈ zmultiples a) })
              (stabilizer { x // x ∈ zmultiples a } b)))
[PROOFSTEP]
rw [← ker_eq_bot_iff, eq_bot_iff]
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ ker
      (QuotientAddGroup.map (zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b))
        (stabilizer { x // x ∈ zmultiples a } b)
        (↑(zmultiplesHom { x // x ∈ zmultiples a }) { val := a, property := (_ : a ∈ zmultiples a) })
        (_ :
          zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b) ≤
            comap (↑(zmultiplesHom { x // x ∈ zmultiples a }) { val := a, property := (_ : a ∈ zmultiples a) })
              (stabilizer { x // x ∈ zmultiples a } b))) ≤
    ⊥
[PROOFSTEP]
refine' fun q => induction_on' q fun n hn => _
[GOAL]
n✝ : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
q : ℤ ⧸ zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b)
n : ℤ
hn :
  ↑n ∈
    ker
      (QuotientAddGroup.map (zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b))
        (stabilizer { x // x ∈ zmultiples a } b)
        (↑(zmultiplesHom { x // x ∈ zmultiples a }) { val := a, property := (_ : a ∈ zmultiples a) })
        (_ :
          zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b) ≤
            comap (↑(zmultiplesHom { x // x ∈ zmultiples a }) { val := a, property := (_ : a ∈ zmultiples a) })
              (stabilizer { x // x ∈ zmultiples a } b)))
⊢ ↑n ∈ ⊥
[PROOFSTEP]
rw [mem_bot, eq_zero_iff, Int.mem_zmultiples_iff, ← zsmul_vadd_eq_iff_minimalPeriod_dvd]
[GOAL]
n✝ : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
q : ℤ ⧸ zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b)
n : ℤ
hn :
  ↑n ∈
    ker
      (QuotientAddGroup.map (zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b))
        (stabilizer { x // x ∈ zmultiples a } b)
        (↑(zmultiplesHom { x // x ∈ zmultiples a }) { val := a, property := (_ : a ∈ zmultiples a) })
        (_ :
          zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b) ≤
            comap (↑(zmultiplesHom { x // x ∈ zmultiples a }) { val := a, property := (_ : a ∈ zmultiples a) })
              (stabilizer { x // x ∈ zmultiples a } b)))
⊢ n • a +ᵥ b = b
[PROOFSTEP]
exact (eq_zero_iff _).mp hn
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ ↑(orbitZpowersEquiv a b).symm ↑k =
    { val := a, property := (_ : a ∈ zpowers a) } ^ k •
      { val := b, property := (_ : b ∈ orbit { x // x ∈ zpowers a } b) }
[PROOFSTEP]
rw [orbitZpowersEquiv_symm_apply, ZMod.coe_int_cast]
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ { val := a, property := (_ : a ∈ zpowers a) } ^ (k % ↑(minimalPeriod ((fun x x_1 => x • x_1) a) b)) •
      { val := b, property := (_ : b ∈ orbit { x // x ∈ zpowers a } b) } =
    { val := a, property := (_ : a ∈ zpowers a) } ^ k •
      { val := b, property := (_ : b ∈ orbit { x // x ∈ zpowers a } b) }
[PROOFSTEP]
exact Subtype.ext (zpow_smul_mod_minimalPeriod _ _ k)
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁵ : AddGroup A
inst✝⁴ : Ring R
α✝ : Type u_3
β✝ : Type u_4
inst✝³ : Group α✝
a✝ : α✝
inst✝² : MulAction α✝ β✝
b✝ : β✝
α : Type u_5
β : Type u_6
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
k : ℤ
⊢ ↑(orbitZmultiplesEquiv a b).symm ↑k =
    k • { val := a, property := (_ : a ∈ zmultiples a) } +ᵥ
      { val := b, property := (_ : b ∈ AddAction.orbit { x // x ∈ zmultiples a } b) }
[PROOFSTEP]
rw [AddAction.orbit_zmultiples_equiv_symm_apply, ZMod.coe_int_cast]
  -- porting note: times out without `a b` explicit
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁵ : AddGroup A
inst✝⁴ : Ring R
α✝ : Type u_3
β✝ : Type u_4
inst✝³ : Group α✝
a✝ : α✝
inst✝² : MulAction α✝ β✝
b✝ : β✝
α : Type u_5
β : Type u_6
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
k : ℤ
⊢ (k % ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b)) • { val := a, property := (_ : a ∈ zmultiples a) } +ᵥ
      { val := b, property := (_ : b ∈ AddAction.orbit { x // x ∈ zmultiples a } b) } =
    k • { val := a, property := (_ : a ∈ zmultiples a) } +ᵥ
      { val := b, property := (_ : b ∈ AddAction.orbit { x // x ∈ zmultiples a } b) }
[PROOFSTEP]
exact Subtype.ext (zsmul_vadd_mod_minimalPeriod a b k)
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Ring R
α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Fintype ↑(orbit { x // x ∈ zpowers a } b)
⊢ minimalPeriod ((fun x x_1 => x • x_1) a) b = Fintype.card ↑(orbit { x // x ∈ zpowers a } b)
[PROOFSTEP]
rw [← Fintype.ofEquiv_card (orbitZpowersEquiv a b), @ZMod.card _ (_)]
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Ring R
α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Finite ↑(orbit { x // x ∈ zpowers a } b)
⊢ minimalPeriod ((fun x x_1 => x • x_1) a) b ≠ 0
[PROOFSTEP]
cases nonempty_fintype (orbit (zpowers a) b)
[GOAL]
case intro
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Ring R
α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Finite ↑(orbit { x // x ∈ zpowers a } b)
val✝ : Fintype ↑(orbit { x // x ∈ zpowers a } b)
⊢ minimalPeriod ((fun x x_1 => x • x_1) a) b ≠ 0
[PROOFSTEP]
haveI : Nonempty (orbit (zpowers a) b) := (orbit_nonempty b).to_subtype
[GOAL]
case intro
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Ring R
α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Finite ↑(orbit { x // x ∈ zpowers a } b)
val✝ : Fintype ↑(orbit { x // x ∈ zpowers a } b)
this : Nonempty ↑(orbit { x // x ∈ zpowers a } b)
⊢ minimalPeriod ((fun x x_1 => x • x_1) a) b ≠ 0
[PROOFSTEP]
rw [minimalPeriod_eq_card]
[GOAL]
case intro
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Ring R
α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Finite ↑(orbit { x // x ∈ zpowers a } b)
val✝ : Fintype ↑(orbit { x // x ∈ zpowers a } b)
this : Nonempty ↑(orbit { x // x ∈ zpowers a } b)
⊢ Fintype.card ↑(orbit { x // x ∈ zpowers a } b) ≠ 0
[PROOFSTEP]
exact Fintype.card_ne_zero
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝² : AddGroup A
inst✝¹ : Ring R
α : Type u_3
inst✝ : Group α
a : α
⊢ orderOf a = Nat.card { x // x ∈ zpowers a }
[PROOFSTEP]
have := Nat.card_congr (MulAction.orbitZpowersEquiv a (1 : α))
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝² : AddGroup A
inst✝¹ : Ring R
α : Type u_3
inst✝ : Group α
a : α
this :
  Nat.card ↑(MulAction.orbit { x // x ∈ zpowers a } 1) =
    Nat.card (ZMod (Function.minimalPeriod ((fun x x_1 => x • x_1) a) 1))
⊢ orderOf a = Nat.card { x // x ∈ zpowers a }
[PROOFSTEP]
rwa [Nat.card_zmod, orbit_subgroup_one_eq_self, eq_comm] at this
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝² : AddGroup A
inst✝¹ : Ring R
α : Type u_3
inst✝ : Group α
a : α
h : IsOfFinOrder a
⊢ Finite { x // x ∈ zpowers a }
[PROOFSTEP]
rw [← orderOf_pos_iff, order_eq_card_zpowers'] at h
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝² : AddGroup A
inst✝¹ : Ring R
α : Type u_3
inst✝ : Group α
a : α
h : 0 < Nat.card { x // x ∈ zpowers a }
⊢ Finite { x // x ∈ zpowers a }
[PROOFSTEP]
exact Nat.finite_of_card_ne_zero h.ne.symm


[GOAL]
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a✝ b a : α
s : Sym α n
⊢ ↑Multiset.card (a ::ₘ ↑s) = Nat.succ n
[PROOFSTEP]
rw [Multiset.card_cons, s.2]
[GOAL]
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a✝ b a : α
v : Vector α n
⊢ ofVector (a ::ᵥ v) = a ::ₛ ofVector v
[PROOFSTEP]
cases v
[GOAL]
case mk
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a✝ b a : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ ofVector (a ::ᵥ { val := val✝, property := property✝ }) = a ::ₛ ofVector { val := val✝, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a✝ b a : α
v : Vector α n
⊢ ↑(a ::ₛ ofVector v) = ↑(ofVector (a ::ᵥ v))
[PROOFSTEP]
cases v
[GOAL]
case mk
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a✝ b a : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ ↑(a ::ₛ ofVector { val := val✝, property := property✝ }) = ↑(ofVector (a ::ᵥ { val := val✝, property := property✝ }))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
m : Multiset α
hc : ↑Multiset.card m = n + 1
a : α
h : a ∈ m
⊢ ↑Multiset.card (Multiset.erase m a) = n
[PROOFSTEP]
rw [Multiset.card_erase_of_mem h, hc]
[GOAL]
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
m : Multiset α
hc : ↑Multiset.card m = n + 1
a : α
h : a ∈ m
⊢ Nat.pred (n + 1) = n
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
β : Type u_2
n✝ n' m : ℕ
s : Sym α✝ n✝
a b : α✝
α : Type u_3
n : ℕ
x✝ : List α
⊢ List.length x✝ = n ↔ ↑Multiset.card (Quotient.mk (List.isSetoid α) x✝) = n
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
β : Type u_2
n✝ n' m : ℕ
s : Sym α✝ n✝
a b : α✝
α : Type u_3
n : ℕ
x✝¹ x✝ : { l // List.length l = n }
⊢ Setoid.r x✝¹ x✝ ↔ ↑x✝¹ ≈ ↑x✝
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
β : Type u_2
n✝ n' m : ℕ
s✝ : Sym α✝ n✝
a✝ b : α✝
α : Type u_3
n : ℕ
a : α
s : Sym α n
⊢ (a :: ↑symEquivSym' s) = ↑symEquivSym' (a ::ₛ s)
[PROOFSTEP]
rcases s with ⟨⟨l⟩, _⟩
[GOAL]
case mk.mk
α✝ : Type u_1
β : Type u_2
n✝ n' m : ℕ
s : Sym α✝ n✝
a✝ b : α✝
α : Type u_3
n : ℕ
a : α
val✝ : Multiset α
l : List α
property✝ : ↑Multiset.card (Quot.mk Setoid.r l) = n
⊢ (a :: ↑symEquivSym' { val := Quot.mk Setoid.r l, property := property✝ }) =
    ↑symEquivSym' (a ::ₛ { val := Quot.mk Setoid.r l, property := property✝ })
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
⊢ s = replicate n a ↔ ∀ (b : α), b ∈ s → b = a
[PROOFSTEP]
erw [Subtype.ext_iff, Multiset.eq_replicate]
[GOAL]
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
⊢ (↑Multiset.card ↑s = n ∧ ∀ (b : α), b ∈ ↑s → b = a) ↔ ∀ (b : α), b ∈ s → b = a
[PROOFSTEP]
exact and_iff_right s.2
[GOAL]
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α (Nat.succ n)
⊢ ∃ a s', s = a ::ₛ s'
[PROOFSTEP]
obtain ⟨a, ha⟩ := exists_mem s
[GOAL]
case intro
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a✝ b : α
s : Sym α (Nat.succ n)
a : α
ha : a ∈ s
⊢ ∃ a s', s = a ::ₛ s'
[PROOFSTEP]
classical exact ⟨a, s.erase a ha, (cons_erase ha).symm⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a✝ b : α
s : Sym α (Nat.succ n)
a : α
ha : a ∈ s
⊢ ∃ a s', s = a ::ₛ s'
[PROOFSTEP]
exact ⟨a, s.erase a ha, (cons_erase ha).symm⟩
[GOAL]
α : Type u_1
β : Type u_2
n✝ n' m : ℕ
s : Sym α n✝
a b : α
inst✝ : Subsingleton α
n : ℕ
⊢ ∀ (a b : Sym α n), a = b
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
inst✝ : Subsingleton α
⊢ ∀ (a b : Sym α Nat.zero), a = b
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
inst✝ : Subsingleton α
n✝ : ℕ
⊢ ∀ (a b : Sym α (Nat.succ n✝)), a = b
[PROOFSTEP]
intro s s'
[GOAL]
case succ
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
inst✝ : Subsingleton α
n✝ : ℕ
s s' : Sym α (Nat.succ n✝)
⊢ s = s'
[PROOFSTEP]
obtain ⟨b, -⟩ := exists_mem s
[GOAL]
case succ.intro
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b✝ : α
inst✝ : Subsingleton α
n✝ : ℕ
s s' : Sym α (Nat.succ n✝)
b : α
⊢ s = s'
[PROOFSTEP]
rw [eq_replicate_of_subsingleton b s', eq_replicate_of_subsingleton b s]
[GOAL]
α : Type u_1
β : Type u_2
n✝ n' m : ℕ
s✝ : Sym α n✝
a b : α
n : ℕ
inst✝ : IsEmpty α
s : Sym α (Nat.succ n)
⊢ False
[PROOFSTEP]
obtain ⟨a, -⟩ := exists_mem s
[GOAL]
case intro
α : Type u_1
β : Type u_2
n✝ n' m : ℕ
s✝ : Sym α n✝
a✝ b : α
n : ℕ
inst✝ : IsEmpty α
s : Sym α (Nat.succ n)
a : α
⊢ False
[PROOFSTEP]
exact isEmptyElim a
[GOAL]
α : Type u_1
β : Type u_2
n✝ n' m : ℕ
s : Sym α n✝
a b : α
n : ℕ
f : α → β
x : Sym α n
⊢ ↑Multiset.card (Multiset.map f ↑x) = n
[PROOFSTEP]
simpa [Multiset.card_map] using x.property
[GOAL]
α✝ : Type u_1
β : Type u_2
n✝ n' m : ℕ
s✝ : Sym α✝ n✝
a b : α✝
α : Type u_3
n : ℕ
s : Sym α n
⊢ map (fun x => x) s = s
[PROOFSTEP]
ext
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
n✝ n' m : ℕ
s✝ : Sym α✝ n✝
a b : α✝
α : Type u_3
n : ℕ
s : Sym α n
⊢ ↑(map (fun x => x) s) = ↑s
[PROOFSTEP]
simp [Sym.map]
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
n✝ n' m : ℕ
s✝ : Sym α✝ n✝
a b : α✝
α : Type u_3
n : ℕ
s : Sym α n
⊢ { val := ↑s, property := (_ : (fun s => ↑Multiset.card s = n) ↑s) } = s
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
β : Type u_2
n✝ n' m : ℕ
s✝ : Sym α✝ n✝
a b : α✝
α : Type u_3
n : ℕ
s : Sym α n
⊢ map id s = s
[PROOFSTEP]
ext
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
n✝ n' m : ℕ
s✝ : Sym α✝ n✝
a b : α✝
α : Type u_3
n : ℕ
s : Sym α n
⊢ ↑(map id s) = ↑s
[PROOFSTEP]
simp [Sym.map]
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
n✝ n' m : ℕ
s✝ : Sym α✝ n✝
a b : α✝
α : Type u_3
n : ℕ
s : Sym α n
⊢ { val := ↑s, property := (_ : (fun s => ↑Multiset.card s = n) ↑s) } = s
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
n✝ n' m : ℕ
s✝ : Sym α✝ n✝
a b : α✝
α : Type u_3
β : Type u_4
γ : Type u_5
n : ℕ
g : β → γ
f : α → β
s : Sym α n
⊢ ↑(map g (map f s)) = ↑(map (g ∘ f) s)
[PROOFSTEP]
dsimp only [Sym.map]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
n✝ n' m : ℕ
s✝ : Sym α✝ n✝
a b : α✝
α : Type u_3
β : Type u_4
γ : Type u_5
n : ℕ
g : β → γ
f : α → β
s : Sym α n
⊢ Multiset.map g (Multiset.map f ↑s) = Multiset.map (g ∘ f) ↑s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a b : α
f : α → β
m : Multiset α
hc : ↑Multiset.card m = n
⊢ ↑Multiset.card (Multiset.map f m) = n
[PROOFSTEP]
simp [hc]
[GOAL]
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
e : α ≃ β
x : Sym α n
⊢ map (↑e.symm) (map (↑e) x) = x
[PROOFSTEP]
rw [map_map, Equiv.symm_comp_self, map_id]
[GOAL]
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
e : α ≃ β
x : Sym β n
⊢ map (↑e) (map (↑e.symm) x) = x
[PROOFSTEP]
rw [map_map, Equiv.self_comp_symm, map_id]
[GOAL]
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α n
⊢ ↑Multiset.card (Multiset.attach ↑s) = n
[PROOFSTEP]
conv_rhs => rw [← s.2, ← Multiset.card_attach]
[GOAL]
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α n
| n
[PROOFSTEP]
rw [← s.2, ← Multiset.card_attach]
[GOAL]
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α n
| n
[PROOFSTEP]
rw [← s.2, ← Multiset.card_attach]
[GOAL]
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α n
| n
[PROOFSTEP]
rw [← s.2, ← Multiset.card_attach]
[GOAL]
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α n
s' : Sym α n'
⊢ ↑Multiset.card (↑s + ↑s') = n + n'
[PROOFSTEP]
rw [map_add, s.2, s'.2]
[GOAL]
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s s' : Sym α n'
⊢ append s s' = ↑(Sym.cast (_ : n' + n' = n' + n')) (append s' s)
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s s' : Sym α n'
⊢ ↑(append s s') = ↑(↑(Sym.cast (_ : n' + n' = n' + n')) (append s' s))
[PROOFSTEP]
simp [append, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a✝ b✝ a b : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
⊢ a ∈ fill b i s ↔ ↑i ≠ 0 ∧ a = b ∨ a ∈ s
[PROOFSTEP]
rw [fill, mem_cast, mem_append_iff, or_comm, mem_replicate]
[GOAL]
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ↑card ↑m < n + 1
[PROOFSTEP]
rw [m.2, Nat.lt_succ_iff]
[GOAL]
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ↑card (filter ((fun x x_1 => x ≠ x_1) a) ↑m) + ↑{ val := count a ↑m, isLt := (_ : count a ↑m < n + 1) } = ↑card ↑m
[PROOFSTEP]
rw [← countp_eq_card_filter, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ↑{ val := count a ↑m, isLt := (_ : count a ↑m < n + 1) } + countp ((fun x x_1 => x ≠ x_1) a) ↑m = ↑card ↑m
[PROOFSTEP]
simp only [eq_comm, Ne.def, count]
[GOAL]
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ countp (fun x => a = x) ↑m + countp (fun x => ¬a = x) ↑m = ↑card ↑m
[PROOFSTEP]
rw [← card_eq_countp_add_countp _ _]
[GOAL]
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
m₁ m₂ : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ↑m₁.snd = ↑m₂.snd
⊢ ↑m₁.fst = ↑m₂.fst
[PROOFSTEP]
rw [← Nat.sub_sub_self (Nat.le_of_lt_succ m₁.1.is_lt), ← m₁.2.2, val_eq_coe, h, ← val_eq_coe, m₂.2.2,
  Nat.sub_sub_self (Nat.le_of_lt_succ m₂.1.is_lt)]
[GOAL]
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ↑(fill a (filterNe a m).fst (filterNe a m).snd) = ↑m
[PROOFSTEP]
rw [coe_fill, filterNe, ← val_eq_coe, Subtype.coe_mk, Fin.val_mk]
[GOAL]
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ filter ((fun x x_1 => x ≠ x_1) a) ↑m + ↑(replicate (count a ↑m) a) = ↑m
[PROOFSTEP]
ext b
[GOAL]
case a
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b✝ : α
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b (filter ((fun x x_1 => x ≠ x_1) a) ↑m + ↑(replicate (count a ↑m) a)) = count b ↑m
[PROOFSTEP]
dsimp
[GOAL]
case a
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b✝ : α
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b (filter (fun x => ¬a = x) ↑m + ↑(replicate (count a ↑m) a)) = count b ↑m
[PROOFSTEP]
rw [count_add, count_filter, Sym.coe_replicate, count_replicate]
[GOAL]
case a
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b✝ : α
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ ((if ¬a = b then count b ↑m else 0) + if b = a then count a ↑m else 0) = count b ↑m
[PROOFSTEP]
obtain rfl | h := eq_or_ne a b
[GOAL]
case a.inl
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ((if ¬a = a then count a ↑m else 0) + if a = a then count a ↑m else 0) = count a ↑m
[PROOFSTEP]
rw [if_pos rfl, if_neg (not_not.2 rfl), zero_add]
[GOAL]
case a.inr
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b✝ : α
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ ((if ¬a = b then count b ↑m else 0) + if b = a then count a ↑m else 0) = count b ↑m
[PROOFSTEP]
rw [if_pos h, if_neg h.symm, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ¬a ∈ m.snd
⊢ ↑(filterNe a (fill a m.fst m.snd)).snd = ↑m.snd
[PROOFSTEP]
rw [filterNe, ← val_eq_coe, Subtype.coe_mk, val_eq_coe, coe_fill]
[GOAL]
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ¬a ∈ m.snd
⊢ filter ((fun x x_1 => x ≠ x_1) a) (↑m.snd + ↑(replicate (↑m.fst) a)) = ↑m.snd
[PROOFSTEP]
rw [filter_add, filter_eq_self.2, add_right_eq_self, eq_zero_iff_forall_not_mem]
[GOAL]
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ¬a ∈ m.snd
⊢ ∀ (a_1 : α), ¬a_1 ∈ filter ((fun x x_1 => x ≠ x_1) a) ↑(replicate (↑m.fst) a)
[PROOFSTEP]
intro b hb
[GOAL]
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b✝ : α
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ¬a ∈ m.snd
b : α
hb : b ∈ filter ((fun x x_1 => x ≠ x_1) a) ↑(replicate (↑m.fst) a)
⊢ False
[PROOFSTEP]
rw [mem_filter, Sym.mem_coe, mem_replicate] at hb
[GOAL]
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b✝ : α
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ¬a ∈ m.snd
b : α
hb : (↑m.fst ≠ 0 ∧ b = a) ∧ (fun x x_1 => x ≠ x_1) a b
⊢ False
[PROOFSTEP]
exact hb.2 hb.1.2.symm
[GOAL]
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ¬a ∈ m.snd
⊢ ∀ (a_1 : α), a_1 ∈ ↑m.snd → (fun x x_1 => x ≠ x_1) a a_1
[PROOFSTEP]
exact fun a ha ha' => h <| ha'.symm ▸ ha
[GOAL]
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) (Nat.succ n)
⊢ decode (encode s) = s
[PROOFSTEP]
by_cases h : none ∈ s
[GOAL]
case pos
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) (Nat.succ n)
h : none ∈ s
⊢ decode (encode s) = s
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) (Nat.succ n)
h : ¬none ∈ s
⊢ decode (encode s) = s
[PROOFSTEP]
simp only [decode, h, not_false_iff, encode_of_not_none_mem, Embedding.some_apply, map_map, comp_apply, Option.some_get]
[GOAL]
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) (Nat.succ n)
h : ¬none ∈ s
⊢ map (fun x => ↑x) (attach s) = s
[PROOFSTEP]
convert s.attach_map_coe
[GOAL]
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n ⊕ Sym α (Nat.succ n)
⊢ encode (decode s) = s
[PROOFSTEP]
obtain s | s := s
[GOAL]
case inl
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n
⊢ encode (decode (Sum.inl s)) = Sum.inl s
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
⊢ encode (decode (Sum.inr s)) = Sum.inr s
[PROOFSTEP]
unfold SymOptionSuccEquiv.encode
[GOAL]
case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
⊢ (if h : none ∈ decode (Sum.inr s) then Sum.inl (erase (decode (Sum.inr s)) none h)
    else Sum.inr (map (fun o => Option.get ↑o (_ : Option.isSome ↑o = true)) (attach (decode (Sum.inr s))))) =
    Sum.inr s
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : none ∈ decode (Sum.inr s)
⊢ False
[PROOFSTEP]
obtain ⟨a, _, ha⟩ := Multiset.mem_map.mp h
[GOAL]
case pos.intro.intro
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : none ∈ decode (Sum.inr s)
a : α
left✝ : a ∈ ↑s
ha : ↑Embedding.some a = none
⊢ False
[PROOFSTEP]
exact Option.some_ne_none _ ha
[GOAL]
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : ¬none ∈ decode (Sum.inr s)
⊢ Sum.inr (map (fun o => Option.get ↑o (_ : Option.isSome ↑o = true)) (attach (decode (Sum.inr s)))) = Sum.inr s
[PROOFSTEP]
refine' congr_arg Sum.inr _
[GOAL]
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : ¬none ∈ decode (Sum.inr s)
⊢ map (fun o => Option.get ↑o (_ : Option.isSome ↑o = true)) (attach (decode (Sum.inr s))) = s
[PROOFSTEP]
refine' map_injective (Option.some_injective _) _ _
[GOAL]
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : ¬none ∈ decode (Sum.inr s)
⊢ map some (map (fun o => Option.get ↑o (_ : Option.isSome ↑o = true)) (attach (decode (Sum.inr s)))) = map some s
[PROOFSTEP]
refine' Eq.trans _ (Eq.trans (SymOptionSuccEquiv.decode (Sum.inr s)).attach_map_coe _)
[GOAL]
case neg.refine'_1
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : ¬none ∈ decode (Sum.inr s)
⊢ map some (map (fun o => Option.get ↑o (_ : Option.isSome ↑o = true)) (attach (decode (Sum.inr s)))) =
    map Subtype.val (attach (decode (Sum.inr s)))
case neg.refine'_2
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : ¬none ∈ decode (Sum.inr s)
⊢ decode (Sum.inr s) = map some s
[PROOFSTEP]
simp
[GOAL]
case neg.refine'_2
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α (Nat.succ n)
h : ¬none ∈ decode (Sum.inr s)
⊢ decode (Sum.inr s) = map some s
[PROOFSTEP]
simp