Theorem: Smt.Reconstruct.Prop.drop_append (Smt/Reconstruct/Prop/Lemmas.lean)

State before:
α : Type u_1
a b : List α
⊢ drop a.length (a ++ b) = b
Tactic:
have H3:= take_append_drop a.length (a ++ b)
State after:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ drop a.length (a ++ b) = b

State before:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ drop a.length (a ++ b) = b
Tactic:
apply (append_inj H3 _).2
State after:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ (take a.length (a ++ b)).length = a.length

State before:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ (take a.length (a ++ b)).length = a.length
Tactic:
rw [length_take]
State after:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ a.length ≤ (a ++ b).length

State before:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ a.length ≤ (a ++ b).length
Tactic:
rw [length_append]
State after:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ a.length ≤ a.length + b.length

State before:
α : Type u_1
a b : List α
H3 : take a.length (a ++ b) ++ drop a.length (a ++ b) = a ++ b
⊢ a.length ≤ a.length + b.length
Tactic:
apply le_add_right
State after:
no goals