Theorem: algebra.Order.lex_true_of_ble_lex_true
Proof state before:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
hneq₂ : x✝ = y✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x = x✝
eq₄ : y = y✝
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹
Tactic:
rw [eq₁] at eq₃
Proof state after:
case h_2.inr.h_2.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝⁵ })
      (tail { val := y :: ys, property := property✝⁴ }) =
    true
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : x = x✝ ∧ xs = tail✝¹
heq₄ : y = y✝ ∧ ys = tail✝
hneq₂ : x✝ = y✝
eq₁ : x = x✝¹
eq₂ : y = y✝¹
eq₃ : x✝¹ = x✝
eq₄ : y = y✝
⊢ x✝¹ ≤ y✝¹

case h_2.inr.h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝⁵ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝⁴ : List.length (y :: ys) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
heq₁ : { val := x :: xs, property := property✝⁵ } = { val := x✝¹ :: tail✝³, property := property✝³ }
heq₂ : { val := y :: ys, property := property✝⁴ } = { val := y✝¹ :: tail✝², property := property✝² }
hneq₁ : ¬x✝¹ = y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝⁵ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝⁴ } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬(x✝ == y✝) = true
h : decide (x✝ ≤ y✝) = true
⊢ x✝¹ ≤ y✝¹