ih1 — Mathlib

English

If a function ih assigns, for every a, a witness under ArgsRel a (Args.P1 x y) → P124 a, then IH1 x y holds; this is a preparatory induction step for the P1-case of multiplication.

Русский

Если ih задаёт доказательство по каждому a относительно ArgsRel и P124, то выполняется IH1 для x и y.

LaTeX

$$$\\big(\\\\forall a, \\\\mathrm{ArgsRel} \\, a \\, (\\\\mathrm{Args.P1} \\, x \\, y) \to P124 \\, a \\big) \\\\Rightarrow IH1(x,y)$$$

Lean4

theorem ih1 (ih : ∀ a, ArgsRel a (Args.P1 x y) → P124 a) : IH1 x y :=
  by
  rintro x₁ x₂ y' h₁ h₂ (rfl | hy) <;> apply ih (Args.P24 _ _ _)
  on_goal 2 => refine TransGen.tail ?_ (cutExpand_pair_right hy)
  all_goals exact TransGen.single (cutExpand_double_left h₁ h₂)

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