case single
α : Type u_1
β : Type u_2
γ : Type ?u.23090
δ : Type ?u.23093
r : α → α → Prop
a✝¹ b✝¹ c d : α
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
b✝ : α
a✝ : r a b✝
⊢ TransGen p (f a) (f b✝)

case tail
α : Type u_1
β : Type u_2
γ : Type ?u.23090
δ : Type ?u.23093
r : α → α → Prop
a✝² b✝¹ c d : α
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : TransGen p (f a) (f b✝)
⊢ TransGen p (f a) (f c✝)
α : Type u_1
β : Type u_2
γ : Type ?u.23090
δ : Type ?u.23093
r : α → α → Prop
a✝ b✝ c d : α
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
hab : TransGen r a b
⊢ TransGen p (f a) (f b)
induction hab
case tail
α : Type u_1
β : Type u_2
γ : Type ?u.23090
δ : Type ?u.23093
r : α → α → Prop
a✝² b✝¹ c d : α
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : TransGen p (f a) (f b✝)
⊢ TransGen p (f a) (f c✝)
case single
α : Type u_1
β : Type u_2
γ : Type ?u.23090
δ : Type ?u.23093
r : α → α → Prop
a✝¹ b✝¹ c d : α
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
b✝ : α
a✝ : r a b✝
⊢ TransGen p (f a) (f b✝)

case tail
α : Type u_1
β : Type u_2
γ : Type ?u.23090
δ : Type ?u.23093
r : α → α → Prop
a✝² b✝¹ c d : α
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : TransGen p (f a) (f b✝)
⊢ TransGen p (f a) (f c✝)
case single c hac => exact TransGen.single (h a c hac)
no goals
case tail
α : Type u_1
β : Type u_2
γ : Type ?u.23090
δ : Type ?u.23093
r : α → α → Prop
a✝² b✝¹ c d : α
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : TransGen p (f a) (f b✝)
⊢ TransGen p (f a) (f c✝)
case tail c d _ hcd hac => exact TransGen.tail hac (h c d hcd)
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.23090
δ : Type ?u.23093
r : α → α → Prop
a✝ b✝ c✝ d : α
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
c : α
hac : r a c
⊢ TransGen p (f a) (f c)
exact TransGen.single (h a c hac)
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.23090
δ : Type ?u.23093
r : α → α → Prop
a✝¹ b✝ c✝ d✝ : α
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
c d : α
a✝ : TransGen r a c
hcd : r c d
hac : TransGen p (f a) (f c)
⊢ TransGen p (f a) (f d)
exact TransGen.tail hac (h c d hcd)