m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y✝ : α (succ i)
z x₀ y₀ : α 0
x y : (i : Fin n) → α (succ i)
s : {i : Fin (Nat.succ n)} → α i → α i → Prop
⊢ (((0 < 0 → cons x₀ x 0 = cons y₀ y 0) ∧ ∀ (i : Fin n), succ i < 0 → cons x₀ x (succ i) = cons y₀ y (succ i)) ∧
        s x₀ y₀ ∨
      ∃ i,
        ((0 < succ i → cons x₀ x 0 = cons y₀ y 0) ∧
            ∀ (i_1 : Fin n), succ i_1 < succ i → cons x₀ x (succ i_1) = cons y₀ y (succ i_1)) ∧
          s (x i) (y i)) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ ∃ i, (∀ (j : Fin n), j < i → x j = y j) ∧ s (x i) (y i)
m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y✝ : α (succ i)
z x₀ y₀ : α 0
x y : (i : Fin n) → α (succ i)
s : {i : Fin (Nat.succ n)} → α i → α i → Prop
⊢ Pi.Lex (fun x x_1 => x < x_1) s (cons x₀ x) (cons y₀ y) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i => s) x y
simp_rw [Pi.Lex, Fin.exists_fin_succ, Fin.cons_succ, Fin.cons_zero, Fin.forall_fin_succ]
no goals
m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y✝ : α (succ i)
z x₀ y₀ : α 0
x y : (i : Fin n) → α (succ i)
s : {i : Fin (Nat.succ n)} → α i → α i → Prop
⊢ (((0 < 0 → cons x₀ x 0 = cons y₀ y 0) ∧ ∀ (i : Fin n), succ i < 0 → cons x₀ x (succ i) = cons y₀ y (succ i)) ∧
        s x₀ y₀ ∨
      ∃ i,
        ((0 < succ i → cons x₀ x 0 = cons y₀ y 0) ∧
            ∀ (i_1 : Fin n), succ i_1 < succ i → cons x₀ x (succ i_1) = cons y₀ y (succ i_1)) ∧
          s (x i) (y i)) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ ∃ i, (∀ (j : Fin n), j < i → x j = y j) ∧ s (x i) (y i)
simp [and_assoc, exists_and_left]