case H0
α : Type u_1
r : α → α → Prop
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ Cycle.nil
⊢ Chain r₂ Cycle.nil

case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a✝¹ : α
l✝ : List α
a✝ : Chain r₁ ↑l✝ → Chain r₂ ↑l✝
p : Chain r₁ ↑(a✝¹ :: l✝)
⊢ Chain r₂ ↑(a✝¹ :: l✝)
α : Type u_1
r : α → α → Prop
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ s
⊢ Chain r₂ s
induction s using Cycle.induction_on
no goals
case H0
α : Type u_1
r : α → α → Prop
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ Cycle.nil
⊢ Chain r₂ Cycle.nil
triv
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a✝¹ : α
l✝ : List α
a✝ : Chain r₁ ↑l✝ → Chain r₂ ↑l✝
p : List.Chain r₁ a✝¹ (l✝ ++ [a✝¹])
⊢ List.Chain r₂ a✝¹ (l✝ ++ [a✝¹])
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a✝¹ : α
l✝ : List α
a✝ : Chain r₁ ↑l✝ → Chain r₂ ↑l✝
p : Chain r₁ ↑(a✝¹ :: l✝)
⊢ Chain r₂ ↑(a✝¹ :: l✝)
rw [chain_coe_cons] at p⊢
no goals
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a✝¹ : α
l✝ : List α
a✝ : Chain r₁ ↑l✝ → Chain r₂ ↑l✝
p : List.Chain r₁ a✝¹ (l✝ ++ [a✝¹])
⊢ List.Chain r₂ a✝¹ (l✝ ++ [a✝¹])
exact p.imp H