Porting note: `apply` → `induction`

[pitmonticone]

Classifies porting notes claiming:

apply → induction

Examples

mathlib4/Mathlib/Data/Polynomial/Eval.lean

Lines 419 to 427 in f0f609c

	@[simp]
	theorem eval_C_mul : (C a * p).eval x = a * p.eval x := by
	-- Porting note: `apply` → `induction`
	induction p using Polynomial.induction_on' with
	| h_add p q ph qh =>
	simp only [mul_add, eval_add, ph, qh]
	| h_monomial n b =>
	simp only [mul_assoc, C_mul_monomial, eval_monomial]
	#align polynomial.eval_C_mul Polynomial.eval_C_mul

mathlib4/Mathlib/Data/Polynomial/Eval.lean

Lines 467 to 476 in f0f609c

	@[simp]
	theorem eval_mul_X : (p * X).eval x = p.eval x * x := by
	-- Porting note: `apply` → `induction`
	induction p using Polynomial.induction_on' with
	| h_add p q ph qh =>
	simp only [add_mul, eval_add, ph, qh]
	| h_monomial n a =>
	simp only [← monomial_one_one_eq_X, monomial_mul_monomial, eval_monomial, mul_one, pow_succ',
	mul_assoc]
	#align polynomial.eval_mul_X Polynomial.eval_mul_X

mathlib4/Mathlib/Data/Polynomial/Eval.lean

Lines 604 to 612 in f0f609c

	@[simp]
	theorem mul_X_comp : (p * X).comp r = p.comp r * r := by
	-- Porting note: `apply` → `induction`
	induction p using Polynomial.induction_on' with
	| h_add p q hp hq =>
	simp only [hp, hq, add_mul, add_comp]
	| h_monomial n b =>
	simp only [pow_succ', mul_assoc, monomial_mul_X, monomial_comp]
	#align polynomial.mul_X_comp Polynomial.mul_X_comp

mathlib4/Mathlib/Data/Polynomial/Eval.lean

Lines 628 to 636 in f0f609c

	@[simp]
	theorem C_mul_comp : (C a * p).comp r = C a * p.comp r := by
	-- Porting note: `apply` → `induction`
	induction p using Polynomial.induction_on' with
	| h_add p q hp hq =>
	simp [hp, hq, mul_add]
	| h_monomial n b =>
	simp [mul_assoc]
	#align polynomial.C_mul_comp Polynomial.C_mul_comp

mathlib4/Mathlib/Data/Polynomial/Eval.lean

Lines 628 to 636 in f0f609c

	@[simp]
	theorem C_mul_comp : (C a * p).comp r = C a * p.comp r := by
	-- Porting note: `apply` → `induction`
	induction p using Polynomial.induction_on' with
	| h_add p q hp hq =>
	simp [hp, hq, mul_add]
	| h_monomial n b =>
	simp [mul_assoc]
	#align polynomial.C_mul_comp Polynomial.C_mul_comp

[pitmonticone]

Resolved by #11444.