no goals
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
⊢ (i, x) ∈ enumFrom j [] → j ≤ i ∧ i < j + length [] ∧ x ∈ []
simp [enumFrom]
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
⊢ i = j ∧ x = y ∨ (i, x) ∈ enumFrom (j + 1) ys → j ≤ i ∧ i < j + (length ys + 1) ∧ (x = y ∨ x ∈ ys)
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
⊢ (i, x) ∈ enumFrom j (y :: ys) → j ≤ i ∧ i < j + length (y :: ys) ∧ x ∈ y :: ys
suffices
  i = j ∧ x = y ∨ (i, x) ∈ enumFrom (j + 1) ys →
    j ≤ i ∧ i < j + (length ys + 1) ∧ (x = y ∨ x ∈ ys)
  by simpa [enumFrom, mem_enumFrom ys]
case inl
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
h : i = j ∧ x = y
⊢ j ≤ i ∧ i < j + (length ys + 1) ∧ (x = y ∨ x ∈ ys)

case inr
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
h : (i, x) ∈ enumFrom (j + 1) ys
⊢ j ≤ i ∧ i < j + (length ys + 1) ∧ (x = y ∨ x ∈ ys)
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
⊢ i = j ∧ x = y ∨ (i, x) ∈ enumFrom (j + 1) ys → j ≤ i ∧ i < j + (length ys + 1) ∧ (x = y ∨ x ∈ ys)
rintro (h | h)
no goals
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
this : i = j ∧ x = y ∨ (i, x) ∈ enumFrom (j + 1) ys → j ≤ i ∧ i < j + (length ys + 1) ∧ (x = y ∨ x ∈ ys)
⊢ (i, x) ∈ enumFrom j (y :: ys) → j ≤ i ∧ i < j + length (y :: ys) ∧ x ∈ y :: ys
simpa [enumFrom, mem_enumFrom ys]
case inl
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
h : i = j ∧ x = y
⊢ i < i + (length ys + 1)
case inl
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
h : i = j ∧ x = y
⊢ j ≤ i ∧ i < j + (length ys + 1) ∧ (x = y ∨ x ∈ ys)
refine' ⟨le_of_eq h.1.symm, h.1 ▸ _, Or.inl h.2⟩
case inl.h
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
h : i = j ∧ x = y
⊢ 0 < length ys + 1
case inl
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
h : i = j ∧ x = y
⊢ i < i + (length ys + 1)
apply Nat.lt_add_of_pos_right
no goals
case inl.h
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
h : i = j ∧ x = y
⊢ 0 < length ys + 1
simp
case inr
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
h : (i, x) ∈ enumFrom (j + 1) ys
hji : j + 1 ≤ i
hijlen : i < j + 1 + length ys
hmem : x ∈ ys
⊢ j ≤ i ∧ i < j + (length ys + 1) ∧ (x = y ∨ x ∈ ys)
case inr
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
h : (i, x) ∈ enumFrom (j + 1) ys
⊢ j ≤ i ∧ i < j + (length ys + 1) ∧ (x = y ∨ x ∈ ys)
have ⟨hji, hijlen, hmem⟩ := mem_enumFrom _ h
case inr.refine'_1
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
h : (i, x) ∈ enumFrom (j + 1) ys
hji : j + 1 ≤ i
hijlen : i < j + 1 + length ys
hmem : x ∈ ys
⊢ j ≤ i

case inr.refine'_2
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
h : (i, x) ∈ enumFrom (j + 1) ys
hji : j + 1 ≤ i
hijlen : i < j + 1 + length ys
hmem : x ∈ ys
⊢ i < j + (length ys + 1)

case inr.refine'_3
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
h : (i, x) ∈ enumFrom (j + 1) ys
hji : j + 1 ≤ i
hijlen : i < j + 1 + length ys
hmem : x ∈ ys
⊢ x = y ∨ x ∈ ys
case inr
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
h : (i, x) ∈ enumFrom (j + 1) ys
hji : j + 1 ≤ i
hijlen : i < j + 1 + length ys
hmem : x ∈ ys
⊢ j ≤ i ∧ i < j + (length ys + 1) ∧ (x = y ∨ x ∈ ys)
refine' ⟨_, _, _⟩
no goals
case inr.refine'_1
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
h : (i, x) ∈ enumFrom (j + 1) ys
hji : j + 1 ≤ i
hijlen : i < j + 1 + length ys
hmem : x ∈ ys
⊢ j ≤ i
exact le_trans (Nat.le_succ _) hji
case h.e'_4
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
h : (i, x) ∈ enumFrom (j + 1) ys
hji : j + 1 ≤ i
hijlen : i < j + 1 + length ys
hmem : x ∈ ys
⊢ j + (length ys + 1) = j + 1 + length ys
case inr.refine'_2
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
h : (i, x) ∈ enumFrom (j + 1) ys
hji : j + 1 ≤ i
hijlen : i < j + 1 + length ys
hmem : x ∈ ys
⊢ i < j + (length ys + 1)
convert hijlen using 1
no goals
case h.e'_4
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
h : (i, x) ∈ enumFrom (j + 1) ys
hji : j + 1 ≤ i
hijlen : i < j + 1 + length ys
hmem : x ∈ ys
⊢ j + (length ys + 1) = j + 1 + length ys
ac_rfl
no goals
case inr.refine'_3
ι : Type ?u.432423
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
i j : ℕ
y : α
ys : List α
h : (i, x) ∈ enumFrom (j + 1) ys
hji : j + 1 ≤ i
hijlen : i < j + 1 + length ys
hmem : x ∈ ys
⊢ x = y ∨ x ∈ ys
simp [hmem]