English
Given RelIso's e1: r1 ≃r s1 and e2: r2 ≃r s2, there is a RelIso between Sum.Lex r1 r2 and Sum.Lex s1 s2 induced by sumCongr.
Русский
Даны RelIso e1: r1 ≃r s1 и e2: r2 ≃r s2, существует RelIso между Sum.Lex r1 r2 и Sum.Lex s1 s2, индукированный через sumCongr.
LaTeX
$$$$ \text{sumLexCongr} \; e_1\; e_2 : \mathrm{Sum.Lex}\ r_1 r_2 \cong_r \mathrm{Sum.Lex}\ s_1 s_2. $$$$
Lean4
/-- Given relation isomorphisms `r₁ ≃r s₁` and `r₂ ≃r s₂`, construct a relation isomorphism for the
lexicographic orders on the sum.
-/
def sumLexCongr {α₁ α₂ β₁ β₂ r₁ r₂ s₁ s₂} (e₁ : @RelIso α₁ β₁ r₁ s₁) (e₂ : @RelIso α₂ β₂ r₂ s₂) :
Sum.Lex r₁ r₂ ≃r Sum.Lex s₁ s₂ :=
⟨Equiv.sumCongr e₁.toEquiv e₂.toEquiv,
@fun a b => by obtain ⟨f, hf⟩ := e₁; obtain ⟨g, hg⟩ := e₂; cases a <;> cases b <;> simp [hf, hg]⟩
