case H
α : Type u_1
β : Type u_2
γ : Type ?u.29936
δ : Type ?u.29939
ε : Type ?u.29942
ι : Type ?u.29945
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ fix f a ↔ b ∈ fix f a'
α : Type u_1
β : Type u_2
γ : Type ?u.29936
δ : Type ?u.29939
ε : Type ?u.29942
ι : Type ?u.29945
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
⊢ fix f a = fix f a'
ext b
case H.mp
α : Type u_1
β : Type u_2
γ : Type ?u.29936
δ : Type ?u.29939
ε : Type ?u.29942
ι : Type ?u.29945
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ fix f a → b ∈ fix f a'

case H.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.29936
δ : Type ?u.29939
ε : Type ?u.29942
ι : Type ?u.29945
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ fix f a' → b ∈ fix f a
case H
α : Type u_1
β : Type u_2
γ : Type ?u.29936
δ : Type ?u.29939
ε : Type ?u.29942
ι : Type ?u.29945
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ fix f a ↔ b ∈ fix f a'
constructor
case H.mp
α : Type u_1
β : Type u_2
γ : Type ?u.29936
δ : Type ?u.29939
ε : Type ?u.29942
ι : Type ?u.29945
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ fix f a
⊢ b ∈ fix f a'
case H.mp
α : Type u_1
β : Type u_2
γ : Type ?u.29936
δ : Type ?u.29939
ε : Type ?u.29942
ι : Type ?u.29945
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ fix f a → b ∈ fix f a'
intro h
case H.mp.inr.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type ?u.29936
δ : Type ?u.29939
ε : Type ?u.29942
ι : Type ?u.29945
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ fix f a
h' : Sum.inr a' ∈ f a
e' : b ∈ fix f a'
⊢ b ∈ fix f a'
case H.mp
α : Type u_1
β : Type u_2
γ : Type ?u.29936
δ : Type ?u.29939
ε : Type ?u.29942
ι : Type ?u.29945
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ fix f a
⊢ b ∈ fix f a'
obtain h' | ⟨a, h', e'⟩ := mem_fix_iff.1 h <;> cases Part.mem_unique ha' h'
no goals
case H.mp.inr.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type ?u.29936
δ : Type ?u.29939
ε : Type ?u.29942
ι : Type ?u.29945
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ fix f a
h' : Sum.inr a' ∈ f a
e' : b ∈ fix f a'
⊢ b ∈ fix f a'
exact e'
case H.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.29936
δ : Type ?u.29939
ε : Type ?u.29942
ι : Type ?u.29945
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ fix f a'
⊢ b ∈ fix f a
case H.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.29936
δ : Type ?u.29939
ε : Type ?u.29942
ι : Type ?u.29945
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ fix f a' → b ∈ fix f a
intro h
case H.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.29936
δ : Type ?u.29939
ε : Type ?u.29942
ι : Type ?u.29945
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ fix f a'
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
case H.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.29936
δ : Type ?u.29939
ε : Type ?u.29942
ι : Type ?u.29945
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ fix f a'
⊢ b ∈ fix f a
rw [PFun.mem_fix_iff]
no goals
case H.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.29936
δ : Type ?u.29939
ε : Type ?u.29942
ι : Type ?u.29945
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ fix f a'
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
exact Or.inr ⟨a', ha', h⟩