case refine'_1
α : Type u_1
β : Type ?u.24500
γ : Type ?u.24503
δ : Type ?u.24506
r : α → α → Prop
a b c d : α
h : ReflTransGen r a b
⊢ b = a ∨ TransGen r a b

case refine'_2
α : Type u_1
β : Type ?u.24500
γ : Type ?u.24503
δ : Type ?u.24506
r : α → α → Prop
a b c d : α
h : b = a ∨ TransGen r a b
⊢ ReflTransGen r a b
α : Type u_1
β : Type ?u.24500
γ : Type ?u.24503
δ : Type ?u.24506
r : α → α → Prop
a b c d : α
⊢ ReflTransGen r a b ↔ b = a ∨ TransGen r a b
refine' ⟨fun h ↦ _, fun h ↦ _⟩
case refine'_1.refl
α : Type u_1
β : Type ?u.24500
γ : Type ?u.24503
δ : Type ?u.24506
r : α → α → Prop
a c d : α
⊢ a = a ∨ TransGen r a a

case refine'_1.tail
α : Type u_1
β : Type ?u.24500
γ : Type ?u.24503
δ : Type ?u.24506
r : α → α → Prop
a b c✝ d c : α
hac : ReflTransGen r a c
hcb : r c b
⊢ b = a ∨ TransGen r a b
case refine'_1
α : Type u_1
β : Type ?u.24500
γ : Type ?u.24503
δ : Type ?u.24506
r : α → α → Prop
a b c d : α
h : ReflTransGen r a b
⊢ b = a ∨ TransGen r a b
cases' h with c _ hac hcb
no goals
case refine'_1.refl
α : Type u_1
β : Type ?u.24500
γ : Type ?u.24503
δ : Type ?u.24506
r : α → α → Prop
a c d : α
⊢ a = a ∨ TransGen r a a
exact Or.inl rfl
no goals
case refine'_1.tail
α : Type u_1
β : Type ?u.24500
γ : Type ?u.24503
δ : Type ?u.24506
r : α → α → Prop
a b c✝ d c : α
hac : ReflTransGen r a c
hcb : r c b
⊢ b = a ∨ TransGen r a b
exact Or.inr (TransGen.tail' hac hcb)
case refine'_2.inl
α : Type u_1
β : Type ?u.24500
γ : Type ?u.24503
δ : Type ?u.24506
r : α → α → Prop
b c d : α
⊢ ReflTransGen r b b

case refine'_2.inr
α : Type u_1
β : Type ?u.24500
γ : Type ?u.24503
δ : Type ?u.24506
r : α → α → Prop
a b c d : α
h : TransGen r a b
⊢ ReflTransGen r a b
case refine'_2
α : Type u_1
β : Type ?u.24500
γ : Type ?u.24503
δ : Type ?u.24506
r : α → α → Prop
a b c d : α
h : b = a ∨ TransGen r a b
⊢ ReflTransGen r a b
rcases h with (rfl | h)
no goals
case refine'_2.inl
α : Type u_1
β : Type ?u.24500
γ : Type ?u.24503
δ : Type ?u.24506
r : α → α → Prop
b c d : α
⊢ ReflTransGen r b b
rfl
no goals
case refine'_2.inr
α : Type u_1
β : Type ?u.24500
γ : Type ?u.24503
δ : Type ?u.24506
r : α → α → Prop
a b c d : α
h : TransGen r a b
⊢ ReflTransGen r a b
exact h.to_reflTransGen