Some stuff on ites

Some lemmas about ite and coe for star and tensor_product.

@[simp]

theorem star_ite {α : Type u_1} [InvolutiveStar α] (P : Prop) [Decidable P] (a : α) (b : α) : star (if P then a else b) = if P then star a else star b

theorem coe_ite {α : Type u_1} {β : Type u_2} [CoeTC α β] (P : Prop) [Decidable P] (a : α) (b : α) : CoeTC.coe (if P then a else b) = if P then CoeTC.coe a else CoeTC.coe b

theorem ite_apply_lm {R : Type u_1} {A : Type u_2} {B : Type u_3} [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] (f : A →ₗ[R] B) (g : A →ₗ[R] B) (x : A) (P : Prop) [Decidable P] : (if P then f else g) x = if P then f x else g x

theorem TensorProduct.ite_map {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {M₄ : Type u_5} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₁ →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄) (P : Prop) [Decidable P] : TensorProduct.map (if P then f₁ else f₂) g = if P then TensorProduct.map f₁ g else TensorProduct.map f₂ g