-- Mathlib/Data/Seq/Seq.lean
theorem mem_rec_on {C : Seq α → Prop} {a s} (M : a ∈ s)
    (h1 : ∀ b s', a = b ∨ C s' → C (cons b s')) : C s

Proof state:
case intro.succ
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
e : some a = ↑s (k + 1)
⊢ C s

Tactic:
cases s with
| nil => injection e
| cons b s' =>
  have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl
  rw [h_eq] at e
  apply h1 _ _ (Or.inr (IH e))

Result:
no goals

Proof state:
case intro.zero
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
TH : s = cons a s.tail
⊢ C (cons a s.tail)

Tactic:
apply h1 _ _ (Or.inl rfl)

Result:
no goals

Proof state:
case intro.succ.nil
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
e : some a = ↑nil (k + 1)
⊢ C nil

Tactic:
injection e

Result:
no goals

Proof state:
case intro.succ.cons
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
s' : Seq α
e : some a = ↑(cons b s') (k + 1)
⊢ C (cons b s')

Tactic:
have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl

Result:
case intro.succ.cons
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
s' : Seq α
e : some a = ↑(cons b s') (k + 1)
h_eq : ↑(cons b s') k.succ = ↑s' k
⊢ C (cons b s')

Proof state:
case a
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
⊢ instFunctorOption.1 (fun a' => (a', s.tail)) (↑s 0) = some (a, s.tail)

Tactic:
rw [← e]

Result:
case a
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
⊢ instFunctorOption.1 (fun a' => (a', s.tail)) (some a) = some (a, s.tail)

Proof state:
case mk
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
val✝ : Stream' (Option α)
property✝ : val✝.IsSeq
e : some a = ↑(cons b ⟨val✝, property✝⟩) (k + 1)
⊢ ↑(cons b ⟨val✝, property✝⟩) k.succ = ↑⟨val✝, property✝⟩ k

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
C : Seq α → Prop
a : α
s : Seq α
M : a ∈ s
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
⊢ C s

Tactic:
obtain ⟨k, e⟩ := M

Result:
case intro
α : Type u
C : Seq α → Prop
a : α
s : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e : some a = (↑s).get k
⊢ C s

Proof state:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
s' : Seq α
e : some a = ↑(cons b s') (k + 1)
⊢ ↑(cons b s') k.succ = ↑s' k

Tactic:
cases s' using Subtype.recOn

Result:
case mk
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
val✝ : Stream' (Option α)
property✝ : val✝.IsSeq
e : some a = ↑(cons b ⟨val✝, property✝⟩) (k + 1)
⊢ ↑(cons b ⟨val✝, property✝⟩) k.succ = ↑⟨val✝, property✝⟩ k

Proof state:
case intro.succ.cons
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
s' : Seq α
e : some a = ↑(cons b s') (k + 1)
h_eq : ↑(cons b s') k.succ = ↑s' k
⊢ C (cons b s')

Tactic:
rw [h_eq] at e

Result:
case intro.succ.cons
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
s' : Seq α
e : some a = ↑s' k
h_eq : ↑(cons b s') k.succ = ↑s' k
⊢ C (cons b s')

Proof state:
case intro
α : Type u
C : Seq α → Prop
a : α
s : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e : some a = (↑s).get k
⊢ C s

Tactic:
unfold Stream'.get at e

Result:
case intro
α : Type u
C : Seq α → Prop
a : α
s : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e : some a = ↑s k
⊢ C s

Proof state:
case intro.zero
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
TH : s = cons a s.tail
⊢ C s

Tactic:
rw [TH]

Result:
case intro.zero
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
TH : s = cons a s.tail
⊢ C (cons a s.tail)

Proof state:
case a
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
⊢ instFunctorOption.1 (fun a' => (a', s.tail)) (some a) = some (a, s.tail)

Tactic:
rfl

Result:
no goals

Proof state:
case a
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
⊢ s.destruct = some (a, s.tail)

Tactic:
unfold destruct get? Functor.map

Result:
case a
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
⊢ instFunctorOption.1 (fun a' => (a', s.tail)) (↑s 0) = some (a, s.tail)

Proof state:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
⊢ s = cons a s.tail

Tactic:
apply destruct_eq_cons

Result:
case a
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
⊢ s.destruct = some (a, s.tail)

Proof state:
case intro
α : Type u
C : Seq α → Prop
a : α
s : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e : some a = ↑s k
⊢ C s

Tactic:
induction' k with k IH generalizing s

Result:
case intro.zero
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
⊢ C s

case intro.succ
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
e : some a = ↑s (k + 1)
⊢ C s

Proof state:
case intro.zero
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
⊢ C s

Tactic:
have TH : s = cons a (tail s) := by
  apply destruct_eq_cons
  unfold destruct get? Functor.map
  rw [← e]
  rfl

Result:
case intro.zero
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
TH : s = cons a s.tail
⊢ C s

Proof state:
case intro.succ.cons
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
s' : Seq α
e : some a = ↑s' k
h_eq : ↑(cons b s') k.succ = ↑s' k
⊢ C (cons b s')

Tactic:
apply h1 _ _ (Or.inr (IH e))

Result:
no goals