case a
α : Type ?u.7053
β : Type ?u.7056
n : ℕ
i✝ : Fin n
i : Fin (Nat.succ n)
⊢ i ∈ Ioi (succ i✝) ↔ i ∈ map (succEmbedding n).toEmbedding (Ioi i✝)
α : Type ?u.7053
β : Type ?u.7056
n : ℕ
i : Fin n
⊢ Ioi (succ i) = map (succEmbedding n).toEmbedding (Ioi i)
ext i
case a
α : Type ?u.7053
β : Type ?u.7056
n : ℕ
i✝ : Fin n
i : Fin (Nat.succ n)
⊢ succ i✝ < i ↔ ∃ a, i✝ < a ∧ ↑(succEmbedding n).toEmbedding a = i
case a
α : Type ?u.7053
β : Type ?u.7056
n : ℕ
i✝ : Fin n
i : Fin (Nat.succ n)
⊢ i ∈ Ioi (succ i✝) ↔ i ∈ map (succEmbedding n).toEmbedding (Ioi i✝)
simp only [mem_filter, mem_Ioi, mem_map, mem_univ, true_and_iff, Function.Embedding.coeFn_mk,
  exists_true_left]
case a.mp
α : Type ?u.7053
β : Type ?u.7056
n : ℕ
i✝ : Fin n
i : Fin (Nat.succ n)
⊢ succ i✝ < i → ∃ a, i✝ < a ∧ ↑(succEmbedding n).toEmbedding a = i

case a.mpr
α : Type ?u.7053
β : Type ?u.7056
n : ℕ
i✝ : Fin n
i : Fin (Nat.succ n)
⊢ (∃ a, i✝ < a ∧ ↑(succEmbedding n).toEmbedding a = i) → succ i✝ < i
case a
α : Type ?u.7053
β : Type ?u.7056
n : ℕ
i✝ : Fin n
i : Fin (Nat.succ n)
⊢ succ i✝ < i ↔ ∃ a, i✝ < a ∧ ↑(succEmbedding n).toEmbedding a = i
constructor
case a.mp.refine'_1
α : Type ?u.7053
β : Type ?u.7056
n : ℕ
i✝ : Fin n
i : Fin (Nat.succ n)
⊢ succ i✝ < 0 → ∃ a, i✝ < a ∧ ↑(succEmbedding n).toEmbedding a = 0

case a.mp.refine'_2
α : Type ?u.7053
β : Type ?u.7056
n : ℕ
i✝ : Fin n
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), succ i✝ < succ i → ∃ a, i✝ < a ∧ ↑(succEmbedding n).toEmbedding a = succ i
case a.mp
α : Type ?u.7053
β : Type ?u.7056
n : ℕ
i✝ : Fin n
i : Fin (Nat.succ n)
⊢ succ i✝ < i → ∃ a, i✝ < a ∧ ↑(succEmbedding n).toEmbedding a = i
refine' cases _ _ i
no goals
case a.mp.refine'_1
α : Type ?u.7053
β : Type ?u.7056
n : ℕ
i✝ : Fin n
i : Fin (Nat.succ n)
⊢ succ i✝ < 0 → ∃ a, i✝ < a ∧ ↑(succEmbedding n).toEmbedding a = 0
rintro ⟨⟨⟩⟩
case a.mp.refine'_2
α : Type ?u.7053
β : Type ?u.7056
n : ℕ
i✝¹ : Fin n
i✝ : Fin (Nat.succ n)
i : Fin n
hi : succ i✝¹ < succ i
⊢ ∃ a, i✝¹ < a ∧ ↑(succEmbedding n).toEmbedding a = succ i
case a.mp.refine'_2
α : Type ?u.7053
β : Type ?u.7056
n : ℕ
i✝ : Fin n
i : Fin (Nat.succ n)
⊢ ∀ (i : Fin n), succ i✝ < succ i → ∃ a, i✝ < a ∧ ↑(succEmbedding n).toEmbedding a = succ i
intro i hi
no goals
case a.mp.refine'_2
α : Type ?u.7053
β : Type ?u.7056
n : ℕ
i✝¹ : Fin n
i✝ : Fin (Nat.succ n)
i : Fin n
hi : succ i✝¹ < succ i
⊢ ∃ a, i✝¹ < a ∧ ↑(succEmbedding n).toEmbedding a = succ i
refine' ⟨i, succ_lt_succ_iff.mp hi, rfl⟩
case a.mpr.intro.intro
α : Type ?u.7053
β : Type ?u.7056
n : ℕ
i✝ i : Fin n
hi : i✝ < i
⊢ succ i✝ < ↑(succEmbedding n).toEmbedding i
case a.mpr
α : Type ?u.7053
β : Type ?u.7056
n : ℕ
i✝ : Fin n
i : Fin (Nat.succ n)
⊢ (∃ a, i✝ < a ∧ ↑(succEmbedding n).toEmbedding a = i) → succ i✝ < i
rintro ⟨i, hi, rfl⟩
no goals
case a.mpr.intro.intro
α : Type ?u.7053
β : Type ?u.7056
n : ℕ
i✝ i : Fin n
hi : i✝ < i
⊢ succ i✝ < ↑(succEmbedding n).toEmbedding i
simpa