case refine'_1
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ l, Chain r b l ∧ getLast (b :: l) (_ : b :: l ≠ []) = b

case refine'_2
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
h : Relation.ReflTransGen r a b
⊢ ∀ {a c : α},
    r a c →
      Relation.ReflTransGen r c b →
        (∃ l, Chain r c l ∧ getLast (c :: l) (_ : c :: l ≠ []) = b) →
          ∃ l, Chain r a l ∧ getLast (a :: l) (_ : a :: l ≠ []) = b
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ l, Chain r a l ∧ getLast (a :: l) (_ : a :: l ≠ []) = b
refine' Relation.ReflTransGen.head_induction_on h _ _
no goals
case refine'_1
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ l, Chain r b l ∧ getLast (b :: l) (_ : b :: l ≠ []) = b
exact ⟨[], Chain.nil, rfl⟩
case refine'_2
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
ih : ∃ l, Chain r d l ∧ getLast (d :: l) (_ : d :: l ≠ []) = b
⊢ ∃ l, Chain r c l ∧ getLast (c :: l) (_ : c :: l ≠ []) = b
case refine'_2
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
h : Relation.ReflTransGen r a b
⊢ ∀ {a c : α},
    r a c →
      Relation.ReflTransGen r c b →
        (∃ l, Chain r c l ∧ getLast (c :: l) (_ : c :: l ≠ []) = b) →
          ∃ l, Chain r a l ∧ getLast (a :: l) (_ : a :: l ≠ []) = b
intro c d e _ ih
case refine'_2.intro.intro
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
l : List α
hl₁ : Chain r d l
hl₂ : getLast (d :: l) (_ : d :: l ≠ []) = b
⊢ ∃ l, Chain r c l ∧ getLast (c :: l) (_ : c :: l ≠ []) = b
case refine'_2
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
ih : ∃ l, Chain r d l ∧ getLast (d :: l) (_ : d :: l ≠ []) = b
⊢ ∃ l, Chain r c l ∧ getLast (c :: l) (_ : c :: l ≠ []) = b
obtain ⟨l, hl₁, hl₂⟩ := ih
case refine'_2.intro.intro
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
l : List α
hl₁ : Chain r d l
hl₂ : getLast (d :: l) (_ : d :: l ≠ []) = b
⊢ getLast (c :: d :: l) (_ : c :: d :: l ≠ []) = b
case refine'_2.intro.intro
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
l : List α
hl₁ : Chain r d l
hl₂ : getLast (d :: l) (_ : d :: l ≠ []) = b
⊢ ∃ l, Chain r c l ∧ getLast (c :: l) (_ : c :: l ≠ []) = b
refine' ⟨d :: l, Chain.cons e hl₁, _⟩
no goals
case refine'_2.intro.intro
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
l : List α
hl₁ : Chain r d l
hl₂ : getLast (d :: l) (_ : d :: l ≠ []) = b
⊢ getLast (c :: d :: l) (_ : c :: d :: l ≠ []) = b
rwa [getLast_cons_cons]