mulOneRelabelling — Mathlib

Lean4
/-- `x * 1` has the same moves as `x`. -/
def mulOneRelabelling : ∀ x : PGame.{u}, x * 1 ≡r x
  | ⟨xl, xr, xL, xR⟩ => by
    -- Porting note: the next four lines were just `unfold has_one.one,`

    change _ * One.one ≡r _
    unfold One.one
    unfold instOnePGame
    change mk _ _ _ _ * mk _ _ _ _ ≡r _
    refine ⟨(Equiv.sumEmpty _ _).trans (Equiv.prodPUnit _), (Equiv.emptySum _ _).trans (Equiv.prodPUnit _), ?_, ?_⟩ <;>
        (try rintro (⟨i, ⟨⟩⟩ | ⟨i, ⟨⟩⟩)) <;>
      { dsimp
        apply (Relabelling.subCongr (Relabelling.refl _) (mulZeroRelabelling _)).trans
        rw [sub_zero_eq_add_zero]
        exact
          (addZeroRelabelling _).trans <|
            (((mulOneRelabelling _).addCongr (mulZeroRelabelling _)).trans <| addZeroRelabelling _)
      }
Похожие утверждения