case refl
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∃ n, List.length L₁ = List.length L₁ + 2 * n

case tail
α : Type u
L L₁ L₂✝ L₃✝ L₄ L₂ L₃ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ L₂
h₂₃ : Step L₂ L₃
ih : ∃ n, List.length L₁ = List.length L₂ + 2 * n
⊢ ∃ n, List.length L₁ = List.length L₃ + 2 * n
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
h : Red L₁ L₂
⊢ ∃ n, List.length L₁ = List.length L₂ + 2 * n
induction' h with L₂ L₃ _h₁₂ h₂₃ ih
no goals
case refl
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∃ n, List.length L₁ = List.length L₁ + 2 * n
exact ⟨0, rfl⟩
case tail.intro
α : Type u
L L₁ L₂✝ L₃✝ L₄ L₂ L₃ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ L₂
h₂₃ : Step L₂ L₃
n : ℕ
eq : List.length L₁ = List.length L₂ + 2 * n
⊢ ∃ n, List.length L₁ = List.length L₃ + 2 * n
case tail
α : Type u
L L₁ L₂✝ L₃✝ L₄ L₂ L₃ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ L₂
h₂₃ : Step L₂ L₃
ih : ∃ n, List.length L₁ = List.length L₂ + 2 * n
⊢ ∃ n, List.length L₁ = List.length L₃ + 2 * n
rcases ih with ⟨n, eq⟩
case tail.intro
α : Type u
L L₁ L₂✝ L₃✝ L₄ L₂ L₃ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ L₂
h₂₃ : Step L₂ L₃
n : ℕ
eq : List.length L₁ = List.length L₂ + 2 * n
⊢ List.length L₁ = List.length L₃ + 2 * (1 + n)
case tail.intro
α : Type u
L L₁ L₂✝ L₃✝ L₄ L₂ L₃ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ L₂
h₂₃ : Step L₂ L₃
n : ℕ
eq : List.length L₁ = List.length L₂ + 2 * n
⊢ ∃ n, List.length L₁ = List.length L₃ + 2 * n
exists 1 + n
no goals
case tail.intro
α : Type u
L L₁ L₂✝ L₃✝ L₄ L₂ L₃ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ L₂
h₂₃ : Step L₂ L₃
n : ℕ
eq : List.length L₁ = List.length L₂ + 2 * n
⊢ List.length L₁ = List.length L₃ + 2 * (1 + n)
simp [mul_add, eq, (Step.length h₂₃).symm, add_assoc]