English
Induction on height via reflections of roots.
Русский
Индукция по высоте через отражения корней.
LaTeX
$$RootPairing.Base.IsPos.induction_on_reflect$$
Lean4
theorem induction_on_reflect {i : ι} (h₀ : b.IsPos i) {p : ι → Prop} (h₁ : ∀ i ∈ b.support, p i)
(h₂ : ∀ i j, p i → j ∈ b.support → p (P.reflectionPerm j i)) : p i :=
by
generalize hN : (b.height i).natAbs = N
induction N using Nat.strongRecOn generalizing i with
| ind n ih =>
obtain ⟨j, hj, hj'⟩ := h₀.exists_mem_support_pos_pairingIn
rw [P.zero_lt_pairingIn_iff'] at hj'
rcases eq_or_ne i j with rfl | hij; · exact h₁ i hj
have hk := h₀.reflectionPerm hj hij
have : (b.height (P.reflectionPerm j i)).natAbs < n :=
by
suffices b.height (P.reflectionPerm j i) < b.height i
by
have : (b.height (P.reflectionPerm j i)).natAbs = b.height (P.reflectionPerm j i) :=
Int.natAbs_of_nonneg <| (isPos_iff' _).mp hk
cutsat
have := P.reflection_apply_root' ℤ (i := j) (j := i)
rw [← root_reflectionPerm, sub_eq_add_neg, ← neg_smul] at this
rw [b.height_add_zsmul this]
replace hj : 0 < b.height j := (isPos_iff _).mp <| isPos_of_mem_support hj
aesop
simpa using h₂ (P.reflectionPerm j i) j (ih (m := (b.height (P.reflectionPerm j i)).natAbs) this hk rfl) hj
