Theorem: algebra.lex_le_trans
Proof state before:
case h_2.inr.inr.h_2.inl
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
neq₁ : ¬x = z
neq₂ : ¬x✝¹ = y✝¹
ab : x✝¹ ≤ y✝¹
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq : x✝ = y✝
bc : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := z :: zs, property := l })
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ x ≤ z

case h_2.inr.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
neq₁ : ¬x = z
neq₂ : ¬x✝¹ = y✝¹
ab : 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✝ : ¬x✝ = y✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ x ≤ z
Tactic:
rw [x_cross_one_eq_x, y_cross_one_eq_y] at neq₂ ab
Proof state after:
case h_2.inr.inr.h_2.inl
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
neq₁ : ¬x = z
neq₂ : ¬x = y
ab : x ≤ y
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
eq : x✝ = y✝
bc : Order.lex_impl (tail { val := y :: ys, property := q }) (tail { val := z :: zs, property := l })
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ x ≤ z

case h_2.inr.inr.h_2.inr
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
l : List.length (z :: zs) = m
v₁✝¹ v₂✝¹ : Vector ℕ m
x✝¹ : ℕ
tail✝³ : List ℕ
property✝³ : List.length (x✝¹ :: tail✝³) = m
y✝¹ : ℕ
tail✝² : List ℕ
property✝² : List.length (y✝¹ :: tail✝²) = m
neq₁ : ¬x = z
neq₂ : ¬x✝¹ = y✝¹
ab : 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✝ : ¬x✝ = y✝
bc : x✝ ≤ y✝
heq₁ : x = x✝¹ ∧ xs = tail✝³
heq₂ : y = y✝¹ ∧ ys = tail✝²
heq₃ : y = x✝ ∧ ys = tail✝¹
heq₄ : z = y✝ ∧ zs = tail✝
x_cross_one_eq_x : x✝¹ = x
y_cross_one_eq_y : y✝¹ = y
x_cross_eq_x : x✝ = y
y_cross_eq_x : y✝ = z
⊢ x ≤ z