Theorem: algebra.lex_add_le_add
Proof state before:
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
h : Order.lex_impl a b
⊢ Order.lex_impl (Variables.mul a c) (Variables.mul b c)
Tactic:
match a, b, c with
 | ⟨[], _⟩, ⟨[], _⟩, ⟨[], _⟩          => rw [Order.lex_impl]
                                         split
                                         simp
                                         split
                                         repeat (rename_i prop₁ _ _ _ _ _ _ _ _ _ prop₄ _ _ _
                                                 simp at prop₁ prop₄
                                                 simp [Eq.symm prop₁] at prop₄)                                                                                  
 | ⟨x::xs, p₁⟩, ⟨y::ys, p₂⟩, ⟨z::zs, p₃⟩ => rw [Order.lex_impl]
                                            split
                                            simp
                                            split
                                            apply aux (m-1) (tail ⟨x::xs, p₁⟩) (tail ⟨y::ys, p₂⟩) (tail ⟨z::zs, p₃⟩)
                                            rw [Order.lex_impl] at h
                                            split at h
                                            rename_i prop₁ _ _ _ _ _ _ prop₂ _ _
                                            simp at prop₁ prop₂
                                            simp [Eq.symm prop₂] at prop₁
                                            split at h
                                            exact h
                                            simp at *
                                            rename_i var_mul₁ var_mul₂ _ _ _ _ _ _ _ _ eq neq heq₁ heq₂
                                            simp [map₂, Variables.mul, List.zipWith] at var_mul₁ var_mul₂
                                            have eq₁ := heq₁.left 
                                            have eq₂ := heq₂.left
                                            cases var_mul₁
                                            cases var_mul₂
                                            rename_i sum_eq _
                                            simp [eq₁, eq₂] at sum_eq
                                            contradiction
                                            rw [Order.lex_impl] at h
                                            split at h
                                            simp at *
                                            split at h
                                            rename_i var_mul₁ var_mul₂ _ _ _ _ _ _ _ _ _ heq₁ heq₂ eq
                                            simp [map₂, Variables.mul, List.zipWith] at var_mul₁ var_mul₂
                                            cases heq₁
                                            cases heq₂
                                            cases var_mul₁
                                            cases var_mul₂
                                            simp [eq]
                                            rename_i var_mul₁ var_mul₂ _ _ _ _ _ _ _ _ _ heq₁ heq₂ eq
                                            cases heq₁
                                            cases heq₂
                                            simp [map₂, Variables.mul, List.zipWith] at var_mul₁ var_mul₂
                                            cases var_mul₁ 
                                            cases var_mul₂
                                            simp at *
                                            exact h
Proof state after:
no goals