English
A membership condition for f.fix a: either b ∈ f a, or there exists a' with Sum.inr a' ∈ f a and b ∈ f.fix a'.
Русский
Условия принадлежности для f.fix a: либо b ∈ f(a), либо существует a' с Sum.inr a' ∈ f(a) и b ∈ f.fix a'.
LaTeX
$$$b \\in f.fix(a) \\iff \\mathrm{Sum.inl}\\, b \\in f(a) \\lor \\exists a', \\mathrm{Sum.inr}\\, a' \\in f(a) \\land b \\in f.fix(a')$$$
Lean4
theorem mem_fix_iff {f : α →. β ⊕ α} {a : α} {b : β} :
b ∈ f.fix a ↔ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a' :=
⟨fun h => by
let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h
rw [WellFounded.fixF_eq] at h₂
simp only [Part.mem_assert_iff] at h₂
obtain ⟨h₂, h₃⟩ := h₂
split at h₃
next e => simp only [Part.mem_some_iff] at h₃; subst b; exact Or.inl ⟨h₂, e⟩
next e => exact Or.inr ⟨_, ⟨_, e⟩, Part.mem_assert _ h₃⟩, fun h =>
by
simp only [fix, Part.mem_assert_iff]
rcases h with (⟨h₁, h₂⟩ | ⟨a', h, h₃⟩)
· refine ⟨⟨_, fun y h' => ?_⟩, ?_⟩
· injection Part.mem_unique ⟨h₁, h₂⟩ h'
· rw [WellFounded.fixF_eq]
-- Porting note: used to be simp [h₁, h₂]
apply Part.mem_assert h₁
split
next e => injection h₂.symm.trans e with h; simp [h]
next e => injection h₂.symm.trans e
· simp only [fix, Part.mem_assert_iff] at h₃
obtain ⟨h₃, h₄⟩ := h₃
refine ⟨⟨_, fun y h' => ?_⟩, ?_⟩
· injection Part.mem_unique h h' with e
exact e ▸ h₃
· obtain ⟨h₁, h₂⟩ := h
rw [WellFounded.fixF_eq]
-- Porting note: used to be simp [h₁, h₂, h₄]
apply Part.mem_assert h₁
split
next e => injection h₂.symm.trans e
next e => injection h₂.symm.trans e; subst a'; exact h₄⟩
