-- Mathlib/Data/Vector3.lean
theorem vectorAllP_iff_forall (p : α → Prop) (v : Vector3 α n) :
    VectorAllP p v ↔ ∀ i, p (v i)

Proof state:
case refine_1
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ VectorAllP p [] ↔ ∀ (i : Fin2 0), p []

Tactic:
exact ⟨fun _ => Fin2.elim0, fun _ => trivial⟩

Result:
no goals

Proof state:
case refine_2.refine_2
α : Type u_1
n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
h : ∀ (i : Fin2 (n + 1)), p ((a :: v) i)
i : Fin2 n
⊢ p (v i)

Tactic:
simpa using h (fs i)

Result:
no goals

Proof state:
case refine_2.refine_1
α : Type u_1
n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
h : ∀ (i : Fin2 (n + 1)), p ((a :: v) i)
⊢ p a

Tactic:
simpa using h fz

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)

Tactic:
refine v.recOn ?_ ?_

Result:
case refine_1
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ VectorAllP p [] ↔ ∀ (i : Fin2 0), p []

case refine_2
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ ∀ {n : ℕ} (a : α) (w : Vector3 α n),
    (VectorAllP p w ↔ ∀ (i : Fin2 n), p (w i)) → (VectorAllP p (a :: w) ↔ ∀ (i : Fin2 (n + 1)), p ((a :: w) i))

Proof state:
case refine_2
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ ∀ {n : ℕ} (a : α) (w : Vector3 α n),
    (VectorAllP p w ↔ ∀ (i : Fin2 n), p (w i)) → (p a ∧ VectorAllP p w ↔ ∀ (i : Fin2 (n + 1)), p ((a :: w) i))

Tactic:
refine fun {n} a v IH =>
  (and_congr_right fun _ => IH).trans
    ⟨fun ⟨pa, h⟩ i => by
      refine i.cases' ?_ ?_
      exacts [pa, h], fun h => ⟨?_, fun i => ?_⟩⟩

Result:
case refine_2.refine_1
α : Type u_1
n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
h : ∀ (i : Fin2 (n + 1)), p ((a :: v) i)
⊢ p a

case refine_2.refine_2
α : Type u_1
n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
h : ∀ (i : Fin2 (n + 1)), p ((a :: v) i)
i : Fin2 n
⊢ p (v i)

Proof state:
case refine_2
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ ∀ {n : ℕ} (a : α) (w : Vector3 α n),
    (VectorAllP p w ↔ ∀ (i : Fin2 n), p (w i)) → (VectorAllP p (a :: w) ↔ ∀ (i : Fin2 (n + 1)), p ((a :: w) i))

Tactic:
simp only [vectorAllP_cons]

Result:
case refine_2
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ ∀ {n : ℕ} (a : α) (w : Vector3 α n),
    (VectorAllP p w ↔ ∀ (i : Fin2 n), p (w i)) → (p a ∧ VectorAllP p w ↔ ∀ (i : Fin2 (n + 1)), p ((a :: w) i))

Proof state:
case refine_1
α : Type u_1
n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
x✝ : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (n + 1)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ p ((a :: v) fz)

case refine_2
α : Type u_1
n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
x✝ : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (n + 1)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ ∀ (n_1 : Fin2 n), p ((a :: v) n_1.fs)

Tactic:
exacts [pa, h]

Result:
no goals

Proof state:
α : Type u_1
n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
x✝ : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (n + 1)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ p ((a :: v) i)

Tactic:
refine i.cases' ?_ ?_

Result:
case refine_1
α : Type u_1
n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
x✝ : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (n + 1)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ p ((a :: v) fz)

case refine_2
α : Type u_1
n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
x✝ : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (n + 1)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ ∀ (n_1 : Fin2 n), p ((a :: v) n_1.fs)