Theorem: List.eq_of_isInfix_len_ge (One.lean)

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
⊢ l₁ = l₂
Tactic:
have ⟨s, t, heq⟩ := h
State after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
⊢ l₁ = l₂

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
⊢ l₁ = l₂
Tactic:
have len_sum_eq := congr_arg length heq
State after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length (s ++ l₁ ++ t) = length l₂
⊢ l₁ = l₂

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length (s ++ l₁ ++ t) = length l₂
⊢ l₁ = l₂
Tactic:
simp only [append_assoc, length_append] at len_sum_eq
State after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length s + (length l₁ + length t) = length l₂
⊢ l₁ = l₂

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length s + (length l₁ + length t) = length l₂
⊢ l₁ = l₂
Tactic:
rw [add_comm (length l₁), add_comm, add_comm (length t), add_assoc] at len_sum_eq
State after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₁ + (length t + length s) = length l₂
⊢ l₁ = l₂

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₁ + (length t + length s) = length l₂
⊢ l₁ = l₂
Tactic:
have len_eq : length l₁ = length l₂ := by
  apply ge_antisymm len_ge
  rw [← len_sum_eq]
  apply Nat.le_add_right
State after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₁ + (length t + length s) = length l₂
len_eq : length l₁ = length l₂
⊢ l₁ = l₂

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₁ + (length t + length s) = length l₂
len_eq : length l₁ = length l₂
⊢ l₁ = l₂
Tactic:
rw [len_eq] at len_sum_eq
State after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₂ + (length t + length s) = length l₂
len_eq : length l₁ = length l₂
⊢ l₁ = l₂

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₂ + (length t + length s) = length l₂
len_eq : length l₁ = length l₂
⊢ l₁ = l₂
Tactic:
simp only [add_right_eq_self, zero_le, ge_iff_le, nonpos_iff_eq_zero, add_eq_zero_iff] at len_sum_eq
State after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_eq : length l₁ = length l₂
len_sum_eq : length t = 0 ∧ length s = 0
⊢ l₁ = l₂

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_eq : length l₁ = length l₂
len_sum_eq : length t = 0 ∧ length s = 0
⊢ l₁ = l₂
Tactic:
have ⟨teq, seq⟩ := len_sum_eq
State after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_eq : length l₁ = length l₂
len_sum_eq : length t = 0 ∧ length s = 0
teq : length t = 0
seq : length s = 0
⊢ l₁ = l₂

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_eq : length l₁ = length l₂
len_sum_eq : length t = 0 ∧ length s = 0
teq : length t = 0
seq : length s = 0
⊢ l₁ = l₂
Tactic:
rw [List.length_eq_zero] at seq
State after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_eq : length l₁ = length l₂
len_sum_eq : length t = 0 ∧ length s = 0
teq : length t = 0
seq : s = []
⊢ l₁ = l₂

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_eq : length l₁ = length l₂
len_sum_eq : length t = 0 ∧ length s = 0
teq : length t = 0
seq : s = []
⊢ l₁ = l₂
Tactic:
rw [List.length_eq_zero] at teq
State after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_eq : length l₁ = length l₂
len_sum_eq : length t = 0 ∧ length s = 0
teq : t = []
seq : s = []
⊢ l₁ = l₂

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_eq : length l₁ = length l₂
len_sum_eq : length t = 0 ∧ length s = 0
teq : t = []
seq : s = []
⊢ l₁ = l₂
Tactic:
subst_vars
State after:
α : Type u_1
l₁ : List α
len_sum_eq : length [] = 0 ∧ length [] = 0
h : l₁ <:+: [] ++ l₁ ++ []
len_ge : length l₁ ≥ length ([] ++ l₁ ++ [])
len_eq : length l₁ = length ([] ++ l₁ ++ [])
⊢ l₁ = [] ++ l₁ ++ []

State before:
α : Type u_1
l₁ : List α
len_sum_eq : length [] = 0 ∧ length [] = 0
h : l₁ <:+: [] ++ l₁ ++ []
len_ge : length l₁ ≥ length ([] ++ l₁ ++ [])
len_eq : length l₁ = length ([] ++ l₁ ++ [])
⊢ l₁ = [] ++ l₁ ++ []
Tactic:
simp only [append_nil, nil_append]
State after:
no goals

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₁ + (length t + length s) = length l₂
⊢ length l₁ = length l₂
Tactic:
apply ge_antisymm len_ge
State after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₁ + (length t + length s) = length l₂
⊢ length l₁ ≤ length l₂

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₁ + (length t + length s) = length l₂
⊢ length l₁ ≤ length l₂
Tactic:
rw [← len_sum_eq]
State after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₁ + (length t + length s) = length l₂
⊢ length l₁ ≤ length l₁ + (length t + length s)

State before:
α : Type u_1
l₁ l₂ : List α
h : l₁ <:+: l₂
len_ge : length l₁ ≥ length l₂
s t : List α
heq : s ++ l₁ ++ t = l₂
len_sum_eq : length l₁ + (length t + length s) = length l₂
⊢ length l₁ ≤ length l₁ + (length t + length s)
Tactic:
apply Nat.le_add_right
State after:
no goals