-- Mathlib/Data/Stream/Init.lean
theorem cycle_eq : ∀ (l : List α) (h : l ≠ []), cycle l h = l ++ₛ cycle l h
  | [], h => absurd rfl h
  | List.cons a l, _ =>
    have gen : ∀ l' a', corec Stream'.cycleF Stream'.cycleG (a', l', a, l) =
        (a'::l') ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Proof state:
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
l' : List α
⊢ ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l', a, l) = a' :: l' ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
induction' l' with a₁ l₁ ih

Result:
case nil
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
⊢ ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', [], a, l) = [a'] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

case cons
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
⊢ ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', a₁ :: l₁, a, l) =
      a' :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Proof state:
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
⊢ ∀ (l' : List α) (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l', a, l) = a' :: l' ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
intro l'

Result:
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
l' : List α
⊢ ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l', a, l) = a' :: l' ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Proof state:
case nil
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
⊢ ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', [], a, l) = [a'] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
intros

Result:
case nil
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a'✝ : α
⊢ corec Stream'.cycleF Stream'.cycleG (a'✝, [], a, l) = [a'✝] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Proof state:
case cons
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
a'✝ : α
⊢ corec Stream'.cycleF Stream'.cycleG (a'✝, a₁ :: l₁, a, l) =
    a'✝ :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
rw [corec_eq, Stream'.cycle_g_cons, ih a₁]

Result:
case cons
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
a'✝ : α
⊢ Stream'.cycleF (a'✝, a₁ :: l₁, a, l) :: (a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)) =
    a'✝ :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Proof state:
case cons
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
⊢ ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', a₁ :: l₁, a, l) =
      a' :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
intros

Result:
case cons
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
a'✝ : α
⊢ corec Stream'.cycleF Stream'.cycleG (a'✝, a₁ :: l₁, a, l) =
    a'✝ :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Proof state:
case nil
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a'✝ : α
⊢ corec Stream'.cycleF Stream'.cycleG (a'✝, [], a, l) = [a'✝] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
rw [corec_eq]

Result:
case nil
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a'✝ : α
⊢ Stream'.cycleF (a'✝, [], a, l) :: corec Stream'.cycleF Stream'.cycleG (Stream'.cycleG (a'✝, [], a, l)) =
    [a'✝] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Proof state:
case nil
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a'✝ : α
⊢ Stream'.cycleF (a'✝, [], a, l) :: corec Stream'.cycleF Stream'.cycleG (Stream'.cycleG (a'✝, [], a, l)) =
    [a'✝] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
a'✝ : α
⊢ Stream'.cycleF (a'✝, a₁ :: l₁, a, l) :: (a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)) =
    a'✝ :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
rfl

Result:
no goals