subsingleton_short_example — Mathlib

English

A constructive proof that Short x is a subsingleton, demonstrated by induction on x.

Русский

Конструктивное доказательство, что Short x — пододинственный, демонстрируемое индукцией по x.

LaTeX

$$subsingleton_short_example : ∀ x:\mathrm{PGame}, \mathrm{Subsingleton}(\mathrm{Short}(x))$$

Lean4

theorem subsingleton_short_example : ∀ x : PGame, Subsingleton (Short x)
  | mk xl xr xL xR =>
    ⟨fun a b => by
      cases a; cases b
      congr!
      · funext x
        apply
          @Subsingleton.elim _
            (subsingleton_short_example (xL x))
              -- Decreasing goal in Lean 4 is `Subsequent (xL x) (mk α β L R)`
                      -- where `α`, `β`, `L`, and `R` are fresh hypotheses only propositionally
                      -- equal to `xl`, `xr`, `xL`, and `xR`.
                      -- (In Lean 3 it was `(mk xl xr xL xR)` instead.)

      · funext x
        apply @Subsingleton.elim _ (subsingleton_short_example (xR x))⟩
termination_by x => x
decreasing_by
  all_goals {
    subst_vars
    simp only [mk.injEq, heq_eq_eq, true_and] at *
    casesm* _ ∧ _
    subst_vars
    pgame_wf_tac
  }

Похожие утверждения