α : Type u_1
β : Type u_2
γ : Type ?u.29782
δ : Type ?u.29785
ε : Type ?u.29788
ι : Type ?u.29791
f : α →. β ⊕ α
b : β
a : α
hb : Sum.inl b ∈ f a
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
α : Type u_1
β : Type u_2
γ : Type ?u.29782
δ : Type ?u.29785
ε : Type ?u.29788
ι : Type ?u.29791
f : α →. β ⊕ α
b : β
a : α
hb : Sum.inl b ∈ f a
⊢ b ∈ fix f a
rw [PFun.mem_fix_iff]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.29782
δ : Type ?u.29785
ε : Type ?u.29788
ι : Type ?u.29791
f : α →. β ⊕ α
b : β
a : α
hb : Sum.inl b ∈ f a
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
exact Or.inl hb