theorem
proved
tactic proof
PApply_FApply
show as:
view Lean formalization →
formal statement (Lean)
165theorem PApply_FApply {n : ℕ}
166 (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
167 (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
168 PApply lam hInv β (FApply lam hInv β v) = PApply lam hInv β v := by
proof body
Tactic-mode proof.
169 ext i
170 have hsubi :
171 PApply lam hInv β (FApply lam hInv β v) i
172 = PApply lam hInv β (2 • PApply lam hInv β v) i - PApply lam hInv β v i := by
173 unfold FApply
174 rw [PApply_sub]
175 rfl
176 have hsmuli :
177 PApply lam hInv β (2 • PApply lam hInv β v) i
178 = (2 • PApply lam hInv β (PApply lam hInv β v)) i := by
179 simpa using congrFun (PApply_smul lam hInv β 2 (PApply lam hInv β v)) i
180 have hidi : PApply lam hInv β (PApply lam hInv β v) i = PApply lam hInv β v i := by
181 simpa using congrFun (PApply_idempotent lam hInv β hμ v) i
182 rw [hsubi, hsmuli]
183 simp [hidi]
184 ring
185