ι : Type ?u.314687
I✝ J : Box ι
x✝ y✝ : ι → ℝ
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (lower I i) (upper I i)
y : Fin n → ℝ
hy : y ∈ ↑(face I i)
⊢ Fin.insertNth i x y ∈ ↑I
ι : Type ?u.314687
I✝ J : Box ι
x✝ y : ι → ℝ
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (lower I i) (upper I i)
⊢ MapsTo (Fin.insertNth i x) ↑(face I i) ↑I
intro y hy
ι : Type ?u.314687
I✝ J : Box ι
x✝ y✝ : ι → ℝ
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (lower I i) (upper I i)
y : Fin n → ℝ
hy : y ∈ ↑(face I i)
⊢ x ∈ Ioc (lower I i) (upper I i) ∧
    ∀ (j : Fin n), y j ∈ Ioc (lower I (↑(Fin.succAbove i) j)) (upper I (↑(Fin.succAbove i) j))
ι : Type ?u.314687
I✝ J : Box ι
x✝ y✝ : ι → ℝ
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (lower I i) (upper I i)
y : Fin n → ℝ
hy : y ∈ ↑(face I i)
⊢ Fin.insertNth i x y ∈ ↑I
simp_rw [mem_coe, mem_def, i.forall_iff_succAbove, Fin.insertNth_apply_same,
  Fin.insertNth_apply_succAbove]
no goals
ι : Type ?u.314687
I✝ J : Box ι
x✝ y✝ : ι → ℝ
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (lower I i) (upper I i)
y : Fin n → ℝ
hy : y ∈ ↑(face I i)
⊢ x ∈ Ioc (lower I i) (upper I i) ∧
    ∀ (j : Fin n), y j ∈ Ioc (lower I (↑(Fin.succAbove i) j)) (upper I (↑(Fin.succAbove i) j))
exact ⟨hx, hy⟩