Theorem: Nat.Arith₁.le (Logic/Vorspiel/Arith.lean)

State before:
n : ℕ
i j : Fin n
⊢ ∀ (i_1 : Vector ℕ n),
    ((i_1.get i).isLtNat (i_1.get j)).or ((i_1.get i).isEqNat (i_1.get j)) = (i_1.get i).isLeNat (i_1.get j)
Tactic:
simp[Nat.or_eq, Nat.le_iff_lt_or_eq, isLeNat]
State after:
no goals