case zero
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n : ℕ
hin✝ : ¬IsMax ((succ^[n - 1]) i)
hin : ¬IsMax ((succ^[Nat.zero - 1]) i)
⊢ (pred^[Nat.zero]) ((succ^[Nat.zero]) i) = i

case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n - 1]) i) → (pred^[n]) ((succ^[n]) i) = i
hin : ¬IsMax ((succ^[Nat.succ n - 1]) i)
⊢ (pred^[Nat.succ n]) ((succ^[Nat.succ n]) i) = i
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n : ℕ
hin : ¬IsMax ((succ^[n - 1]) i)
⊢ (pred^[n]) ((succ^[n]) i) = i
induction' n with n hn
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n - 1]) i) → (pred^[n]) ((succ^[n]) i) = i
hin : ¬IsMax ((succ^[n]) i)
⊢ (pred^[Nat.succ n]) ((succ^[Nat.succ n]) i) = i
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n - 1]) i) → (pred^[n]) ((succ^[n]) i) = i
hin : ¬IsMax ((succ^[Nat.succ n - 1]) i)
⊢ (pred^[Nat.succ n]) ((succ^[Nat.succ n]) i) = i
rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hin
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n - 1]) i) → (pred^[n]) ((succ^[n]) i) = i
hin : ¬IsMax ((succ^[n]) i)
h_not_max : ¬IsMax ((succ^[n - 1]) i)
⊢ (pred^[n] ∘ pred) ((succ ∘ succ^[n]) i) = i
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n - 1]) i) → (pred^[n]) ((succ^[n]) i) = i
hin : ¬IsMax ((succ^[n]) i)
h_not_max : ¬IsMax ((succ^[n - 1]) i)
⊢ (pred^[Nat.succ n]) ((succ^[Nat.succ n]) i) = i
rw [Function.iterate_succ, Function.iterate_succ']
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n - 1]) i) → (pred^[n]) ((succ^[n]) i) = i
hin : ¬IsMax ((succ^[n]) i)
h_not_max : ¬IsMax ((succ^[n - 1]) i)
⊢ (pred^[n]) (pred (succ ((succ^[n]) i))) = i
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n - 1]) i) → (pred^[n]) ((succ^[n]) i) = i
hin : ¬IsMax ((succ^[n]) i)
h_not_max : ¬IsMax ((succ^[n - 1]) i)
⊢ (pred^[n] ∘ pred) ((succ ∘ succ^[n]) i) = i
simp only [Function.comp_apply]
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n - 1]) i) → (pred^[n]) ((succ^[n]) i) = i
hin : ¬IsMax ((succ^[n]) i)
h_not_max : ¬IsMax ((succ^[n - 1]) i)
⊢ (pred^[n]) ((succ^[n]) i) = i
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n - 1]) i) → (pred^[n]) ((succ^[n]) i) = i
hin : ¬IsMax ((succ^[n]) i)
h_not_max : ¬IsMax ((succ^[n - 1]) i)
⊢ (pred^[n]) (pred (succ ((succ^[n]) i))) = i
rw [pred_succ_of_not_isMax hin]
no goals
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n - 1]) i) → (pred^[n]) ((succ^[n]) i) = i
hin : ¬IsMax ((succ^[n]) i)
h_not_max : ¬IsMax ((succ^[n - 1]) i)
⊢ (pred^[n]) ((succ^[n]) i) = i
exact hn h_not_max
no goals
case zero
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n : ℕ
hin✝ : ¬IsMax ((succ^[n - 1]) i)
hin : ¬IsMax ((succ^[Nat.zero - 1]) i)
⊢ (pred^[Nat.zero]) ((succ^[Nat.zero]) i) = i
simp only [Nat.zero_eq, Function.iterate_zero, id.def]
case zero
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n : ℕ
hin✝ : ¬IsMax ((succ^[n - 1]) i)
hn : ¬IsMax ((succ^[Nat.zero - 1]) i) → (pred^[Nat.zero]) ((succ^[Nat.zero]) i) = i
hin : ¬IsMax ((succ^[Nat.zero]) i)
⊢ ¬IsMax ((succ^[Nat.zero - 1]) i)

case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[Nat.succ n - 1]) i) → (pred^[Nat.succ n]) ((succ^[Nat.succ n]) i) = i
hin : ¬IsMax ((succ^[Nat.succ n]) i)
⊢ ¬IsMax ((succ^[Nat.succ n - 1]) i)
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n - 1]) i) → (pred^[n]) ((succ^[n]) i) = i
hin : ¬IsMax ((succ^[n]) i)
⊢ ¬IsMax ((succ^[n - 1]) i)
cases' n with n
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n]) i) → (pred^[Nat.succ n]) ((succ^[Nat.succ n]) i) = i
hin : ¬IsMax ((succ^[Nat.succ n]) i)
⊢ ¬IsMax ((succ^[n]) i)
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[Nat.succ n - 1]) i) → (pred^[Nat.succ n]) ((succ^[Nat.succ n]) i) = i
hin : ¬IsMax ((succ^[Nat.succ n]) i)
⊢ ¬IsMax ((succ^[Nat.succ n - 1]) i)
rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hn⊢
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n]) i) → (pred^[Nat.succ n]) ((succ^[Nat.succ n]) i) = i
hin : ¬IsMax ((succ^[Nat.succ n]) i)
h_sub_le : (succ^[n]) i ≤ (succ^[Nat.succ n]) i
⊢ ¬IsMax ((succ^[n]) i)
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n]) i) → (pred^[Nat.succ n]) ((succ^[Nat.succ n]) i) = i
hin : ¬IsMax ((succ^[Nat.succ n]) i)
⊢ ¬IsMax ((succ^[n]) i)
have h_sub_le : (succ^[n]) i ≤ (succ^[n.succ]) i := by
  rw [Function.iterate_succ']
  exact le_succ _
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n]) i) → (pred^[Nat.succ n]) ((succ^[Nat.succ n]) i) = i
hin : ¬IsMax ((succ^[Nat.succ n]) i)
h_sub_le : (succ^[n]) i ≤ (succ^[Nat.succ n]) i
h_max : IsMax ((succ^[n]) i)
j : α
hj : (succ^[Nat.succ n]) i ≤ j
⊢ j ≤ (succ^[Nat.succ n]) i
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n]) i) → (pred^[Nat.succ n]) ((succ^[Nat.succ n]) i) = i
hin : ¬IsMax ((succ^[Nat.succ n]) i)
h_sub_le : (succ^[n]) i ≤ (succ^[Nat.succ n]) i
⊢ ¬IsMax ((succ^[n]) i)
refine' fun h_max => hin fun j hj => _
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n]) i) → (pred^[Nat.succ n]) ((succ^[Nat.succ n]) i) = i
hin : ¬IsMax ((succ^[Nat.succ n]) i)
h_sub_le : (succ^[n]) i ≤ (succ^[Nat.succ n]) i
h_max : IsMax ((succ^[n]) i)
j : α
hj : (succ^[Nat.succ n]) i ≤ j
hj_le : j ≤ (succ^[n]) i
⊢ j ≤ (succ^[Nat.succ n]) i
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n]) i) → (pred^[Nat.succ n]) ((succ^[Nat.succ n]) i) = i
hin : ¬IsMax ((succ^[Nat.succ n]) i)
h_sub_le : (succ^[n]) i ≤ (succ^[Nat.succ n]) i
h_max : IsMax ((succ^[n]) i)
j : α
hj : (succ^[Nat.succ n]) i ≤ j
⊢ j ≤ (succ^[Nat.succ n]) i
have hj_le : j ≤ (succ^[n]) i := h_max (h_sub_le.trans hj)
no goals
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n]) i) → (pred^[Nat.succ n]) ((succ^[Nat.succ n]) i) = i
hin : ¬IsMax ((succ^[Nat.succ n]) i)
h_sub_le : (succ^[n]) i ≤ (succ^[Nat.succ n]) i
h_max : IsMax ((succ^[n]) i)
j : α
hj : (succ^[Nat.succ n]) i ≤ j
hj_le : j ≤ (succ^[n]) i
⊢ j ≤ (succ^[Nat.succ n]) i
exact hj_le.trans h_sub_le
no goals
case zero
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n : ℕ
hin✝ : ¬IsMax ((succ^[n - 1]) i)
hn : ¬IsMax ((succ^[Nat.zero - 1]) i) → (pred^[Nat.zero]) ((succ^[Nat.zero]) i) = i
hin : ¬IsMax ((succ^[Nat.zero]) i)
⊢ ¬IsMax ((succ^[Nat.zero - 1]) i)
simpa using hin
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n]) i) → (pred^[Nat.succ n]) ((succ^[Nat.succ n]) i) = i
hin : ¬IsMax ((succ^[Nat.succ n]) i)
⊢ (succ^[n]) i ≤ (succ ∘ succ^[n]) i
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n]) i) → (pred^[Nat.succ n]) ((succ^[Nat.succ n]) i) = i
hin : ¬IsMax ((succ^[Nat.succ n]) i)
⊢ (succ^[n]) i ≤ (succ^[Nat.succ n]) i
rw [Function.iterate_succ']
no goals
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
a b i : α
n✝ : ℕ
hin✝ : ¬IsMax ((succ^[n✝ - 1]) i)
n : ℕ
hn : ¬IsMax ((succ^[n]) i) → (pred^[Nat.succ n]) ((succ^[Nat.succ n]) i) = i
hin : ¬IsMax ((succ^[Nat.succ n]) i)
⊢ (succ^[n]) i ≤ (succ ∘ succ^[n]) i
exact le_succ _