English
Every LTSeries can be refined to a CovBy-RelSeries in a bidirectionally well-founded order.
Русский
Каждая LTSeries может быть дополнена до CovBy-RelSeries в двунаправленно хорошо упорядоченном порядке.
LaTeX
$$$\forall {\alpha} [PartialOrder\alpha] [WellFoundedLT\alpha] [WellFoundedGT\alpha] (s : LTSeries\alpha), \exists t:\ RelSeries{(a,b)\in \alpha\times\alpha \mid a\lessdot b}, \exists i:\ Fin (s.length + 1) \hookrightarrow Fin (t.length + 1), t \circ i = s $$$
Lean4
/-- Any `LTSeries` can be refined to a `CovBy`-`RelSeries`
in a bidirectionally well-founded order. -/
theorem exists_relSeries_covBy {α} [PartialOrder α] [WellFoundedLT α] [WellFoundedGT α] (s : LTSeries α) :
∃ (t : RelSeries {(a, b) : α × α | a ⋖ b}) (i : Fin (s.length + 1) ↪ Fin (t.length + 1)),
t ∘ i = s ∧ i 0 = 0 ∧ i (.last _) = .last _ :=
by
obtain ⟨n, s, h⟩ := s
induction n with
| zero => exact ⟨⟨0, s, nofun⟩, (Equiv.refl _).toEmbedding, rfl, rfl, rfl⟩
| succ n IH =>
obtain ⟨t₁, i, ht, hi₁, hi₂⟩ := IH (s ∘ Fin.castSucc) fun _ ↦ h _
obtain ⟨t₂, h₁, m, h₂, ht₂⟩ := exists_covBy_seq_of_wellFoundedLT_wellFoundedGT_of_le (h (.last _)).le
let t₃ : RelSeries {(a, b) : α × α | a ⋖ b} := ⟨m, (t₂ ·), fun i ↦ by simpa using ht₂ i⟩
have H : t₁.last = t₂ 0 := (congr(t₁ $hi₂.symm).trans (congr_fun ht _)).trans h₁.symm
refine ⟨t₁.smash t₃ H, ⟨Fin.snoc (Fin.castLE (by simp) ∘ i) (.last _), ?_⟩, ?_, ?_, ?_⟩
· refine
Fin.lastCases (Fin.lastCases (fun _ ↦ rfl) fun j eq ↦ ?_) fun j ↦
Fin.lastCases (fun eq ↦ ?_) fun k eq ↦ Fin.ext (congr_arg Fin.val (by simpa using eq) :)
on_goal 2 => rw [eq_comm] at eq
all_goals
rw [Fin.snoc_castSucc] at eq
obtain rfl : m = 0 := by simpa [t₃] using (congr_arg Fin.val eq).trans_lt (i j).2
cases (h (.last _)).ne' (h₂.symm.trans h₁)
· refine funext (Fin.lastCases ?_ fun j ↦ ?_)
· convert h₂; simpa using RelSeries.last_smash ..
convert congr_fun ht j using 1
simp [RelSeries.smash_castLE]
all_goals simp [Fin.snoc, Fin.castPred_zero, hi₁]
