simp not resolving an "and.intro rfl rfl"

Stream: new members

[Yakov Pechersky]

I have a tactic state after a simp that looks like:

case list.cons, list.cons, nat.succ
α : Type u_1,
β : Type u_2,
hd : α,
tl : list α,
IH :
  ∀ {l' : list β} {i : ℕ} (h : i < (tl.zip l').length),
    tl.length = l'.length → (tl.zip l').nth_le i h = (tl.nth_le i _, l'.nth_le i _),
hd' : β,
tl' : list β,
i : ℕ,
h : i.succ < ((hd :: tl).zip (hd' :: tl')).length,
hl : tl.length = tl'.length
⊢ tl.nth_le i _ = tl.nth_le i _ ∧ tl'.nth_le i _ = tl'.nth_le i _

[Yakov Pechersky]

Why doesn't simp resolve the last statement? mwe:

import data.list.basic

open list

namespace list

section list

variables {α β : Type*} (l : list α) (l' : list β) (x : α) (x' : β)

@[simp] lemma zip_nil_left : (@nil α).zip l' = nil := rfl

@[simp] lemma zip_nil_right : l.zip (@nil β) = nil :=
by { induction l; simp only [zip, zip_with] }

@[simp] lemma zip_cons : (x :: l).zip (x' :: l') = (x, x') :: l.zip l' := rfl

@[simp] lemma length_zip : (l.zip l').length = min l.length l'.length :=
begin
  induction l with hd tl IH generalizing l',
  { simp only [zip_nil_left, min_eq_left, length, zero_le], },
  { cases l',
    { simp only [zip_nil_right, length, zero_le, min_eq_right] },
    { simp only [IH, min_add_add_right, zip_cons, length] } }
end

variables {l l'}

lemma nth_le_zip {i : ℕ} (h : i < (l.zip l').length) (hl : l.length = l'.length) :
  (l.zip l').nth_le i h =
    (l.nth_le i ((@lt_min_iff _ _ i l.length l'.length).mp (list.length_zip l l' ▸ h)).left,
    l'.nth_le i ((@lt_min_iff _ _ i l.length l'.length).mp (list.length_zip l l' ▸ h)).right) :=
begin
  induction l with hd tl IH generalizing l' i,
  { simp only [zip_nil_left, length] at h,
    exact absurd h (nat.not_lt_zero i) },
  { cases l' with hd' tl',
    { simpa only using h },
    { cases i,
      { simp only [zip_cons, nth_le] },
      { simp only [add_left_inj, length] at hl,
        simp [IH, hl],
      /-
case list.cons, list.cons, nat.succ
α : Type u_1,
β : Type u_2,
hd : α,
tl : list α,
IH :
  ∀ {l' : list β} {i : ℕ} (h : i < (tl.zip l').length),
    tl.length = l'.length → (tl.zip l').nth_le i h = (tl.nth_le i _, l'.nth_le i _),
hd' : β,
tl' : list β,
i : ℕ,
h : i.succ < ((hd :: tl).zip (hd' :: tl')).length,
hl : tl.length = tl'.length
⊢ tl.nth_le i _ = tl.nth_le i _ ∧ tl'.nth_le i _ = tl'.nth_le i _
-/

        exact and.intro rfl rfl,
      },
    } }
end


end list

end list