refactor(linear_algebra/tensor_product): make lift f (x ⊗ₜ y) = f x y true by rfl (#18121)

Since this is essentially the "primitive" recursor, it is very convenient for it to expand definitionally.

With this change, the following lemmas are now rfl:

* `algebra.mul'_apply`
* `free_monoid.lift_comp_of`
* `free_monoid.lift_eval_of`
* `tensor_product.lie_module.lift_apply`
* `alternating_map.dom_coprod'_apply`
* `contract_left_apply`
* `contract_right_apply`
* `dual_tensor_hom_apply`
* `derivation.tensor_product_to_tmul`
* `poly_equiv_tensor.to_fun_linear_tmul_apply`
* `tensor_product.lift.tmul`
* `tensor_product.lift.tmul'`
* `algebra.tensor_product.lift_tmul`
* `algebra.tensor_product.lmul'_apply_tmul`
* `tensor_product.algebra.smul_def`

And one lemma is no longer rfl

* `free_monoid.lift_apply`

Author: eric-wieser

src/algebra/algebra/bilinear.lean

@@ -59,8 +59,7 @@ variables {R}
 @[simp] lemma mul_right_apply (a b : A) : mul_right R a b = b * a := rfl
 @[simp] lemma mul_left_right_apply (a b x : A) : mul_left_right R (a, b) x = a * x * b := rfl
 
-@[simp] lemma mul'_apply {a b : A} : mul' R A (a ⊗ₜ b) = a * b :=
-by simp only [linear_map.mul', tensor_product.lift.tmul, mul_apply']
+@[simp] lemma mul'_apply {a b : A} : mul' R A (a ⊗ₜ b) = a * b := rfl
 
 @[simp] lemma mul_left_zero_eq_zero :
   mul_left R (0 : A) = 0 :=

src/algebra/free_monoid/basic.lean

@@ -136,27 +136,41 @@ lemma hom_eq ⦃f g : free_monoid α →* M⦄ (h : ∀ x, f (of x) = g (of x))
 monoid_hom.ext $ λ l, rec_on l (f.map_one.trans g.map_one.symm) $
   λ x xs hxs, by simp only [h, hxs, monoid_hom.map_mul]
 
+/-- A variant of `list.prod` that has `[x].prod = x` true definitionally.
+
+The purpose is to make `free_monoid.lift_eval_of` true by `rfl`. -/
+@[to_additive "A variant of `list.sum` that has `[x].sum = x` true definitionally.
+
+The purpose is to make `free_add_monoid.lift_eval_of` true by `rfl`."]
+def prod_aux {M} [monoid M] (l : list M) : M :=
+l.rec_on 1 (λ x xs (_ : M), list.foldl (*) x xs)
+
+@[to_additive]
+lemma prod_aux_eq : ∀ l : list M, free_monoid.prod_aux l = l.prod
+| [] := rfl
+| (x :: xs) := congr_arg (λ x, list.foldl (*) x xs) (one_mul _).symm
+
 /-- Equivalence between maps `α → M` and monoid homomorphisms `free_monoid α →* M`. -/
 @[to_additive "Equivalence between maps `α → A` and additive monoid homomorphisms
 `free_add_monoid α →+ A`."]
 def lift : (α → M) ≃ (free_monoid α →* M) :=
-{ to_fun := λ f, ⟨λ l, (l.to_list.map f).prod, rfl,
-    λ l₁ l₂, by simp only [to_list_mul, list.map_append, list.prod_append]⟩,
+{ to_fun := λ f, ⟨λ l, free_monoid.prod_aux (l.to_list.map f), rfl,
+    λ l₁ l₂, by simp only [prod_aux_eq, to_list_mul, list.map_append, list.prod_append]⟩,
   inv_fun := λ f x, f (of x),
-  left_inv := λ f, funext $ λ x, one_mul (f x),
-  right_inv := λ f, hom_eq $ λ x, one_mul (f (of x)) }
+  left_inv := λ f, rfl,
+  right_inv := λ f, hom_eq $ λ x, rfl }
 
 @[simp, to_additive]
 lemma lift_symm_apply (f : free_monoid α →* M) : lift.symm f = f ∘ of := rfl
 
 @[to_additive]
-lemma lift_apply (f : α → M) (l : free_monoid α) : lift f l = (l.to_list.map f).prod := rfl
+lemma lift_apply (f : α → M) (l : free_monoid α) : lift f l = (l.to_list.map f).prod :=
+prod_aux_eq _
 
-@[to_additive] lemma lift_comp_of (f : α → M) : lift f ∘ of = f := lift.symm_apply_apply f
+@[to_additive] lemma lift_comp_of (f : α → M) : lift f ∘ of = f := rfl
 
 @[simp, to_additive]
-lemma lift_eval_of (f : α → M) (x : α) : lift f (of x) = f x :=
-congr_fun (lift_comp_of f) x
+lemma lift_eval_of (f : α → M) (x : α) : lift f (of x) = f x := rfl
 
 @[simp, to_additive]
 lemma lift_restrict (f : free_monoid α →* M) : lift (f ∘ of) = f :=

src/algebra/lie/tensor_product.lean

@@ -87,7 +87,7 @@ def lift : (M →ₗ[R] N →ₗ[R] P) ≃ₗ⁅R,L⁆ (M ⊗[R] N →ₗ[R] P)
 
 @[simp] lemma lift_apply (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :
   lift R L M N P f (m ⊗ₜ n) = f m n :=
-lift.equiv_apply R M N P f m n
+rfl
 
 /-- A weaker form of the universal property for tensor product of modules of a Lie algebra.
 

src/category_theory/monoidal/internal/Module.lean

@@ -66,7 +66,7 @@ instance (A : Mon_ (Module.{u} R)) : algebra R A.X :=
     have h₂ := linear_map.congr_fun A.mul_one (a ⊗ₜ r),
     exact h₁.trans h₂.symm,
   end,
-  smul_def' := λ r a, by { convert (linear_map.congr_fun A.one_mul (r ⊗ₜ a)).symm, simp, },
+  smul_def' := λ r a, (linear_map.congr_fun A.one_mul (r ⊗ₜ a)).symm,
   ..A.one }
 
 @[simp] lemma algebra_map (A : Mon_ (Module.{u} R)) (r : R) : algebra_map R A.X r = A.one r := rfl
@@ -127,10 +127,8 @@ def inverse : Algebra.{u} R ⥤ Mon_ (Module.{u} R) :=
 { obj := inverse_obj,
   map := λ A B f,
   { hom := f.to_linear_map,
-    one_hom' :=
-      by { ext, dsimp, simp only [ring_hom.map_one, alg_hom.map_one] },
-    mul_hom' :=
-      by { ext, dsimp, simp only [linear_map.mul'_apply, ring_hom.map_mul, alg_hom.map_mul] } } }.
+    one_hom' := linear_map.ext f.commutes,
+    mul_hom' := tensor_product.ext $ linear_map.ext₂ $ map_mul f, } }
 
 end Mon_Module_equivalence_Algebra
 
@@ -146,19 +144,17 @@ def Mon_Module_equivalence_Algebra : Mon_ (Module.{u} R) ≌ Algebra R :=
   unit_iso := nat_iso.of_components
     (λ A,
     { hom := { hom := { to_fun := id, map_add' := λ x y, rfl, map_smul' := λ r a, rfl, },
-               mul_hom' := by { ext, dsimp at *,
-                                simp only [linear_map.mul'_apply, Mon_.X.ring_mul] } },
+               mul_hom' := by { ext, dsimp at *, refl } },
       inv := { hom := { to_fun := id, map_add' := λ x y, rfl, map_smul' := λ r a, rfl, },
-               mul_hom' := by { ext, dsimp at *,
-                                simp only [linear_map.mul'_apply, Mon_.X.ring_mul]} } })
+               mul_hom' := by { ext, dsimp at *, refl } } })
     (by tidy),
   counit_iso := nat_iso.of_components (λ A,
   { hom :=
     { to_fun := id,
       map_zero' := rfl,
       map_add' := λ x y, rfl,
       map_one' := (algebra_map R A).map_one,
-      map_mul' := λ x y, linear_map.mul'_apply,
+      map_mul' := λ x y, (@linear_map.mul'_apply R _ _ _ _ _ _ x y),
       commutes' := λ r, rfl, },
     inv :=
     { to_fun := id,

src/group_theory/submonoid/membership.lean

@@ -291,8 +291,8 @@ by rw [free_monoid.mrange_lift, subtype.range_coe]
 @[to_additive] lemma closure_eq_image_prod (s : set M) :
   (closure s : set M) = list.prod '' {l : list M | ∀ x ∈ l, x ∈ s} :=
 begin
-  rw [closure_eq_mrange, coe_mrange, ← list.range_map_coe, ← set.range_comp],
-  refl
+  rw [closure_eq_mrange, coe_mrange, ← list.range_map_coe, ← set.range_comp, function.comp],
+  exact congr_arg _ (funext $ free_monoid.lift_apply _),
 end
 
 @[to_additive]

src/linear_algebra/alternating.lean

@@ -862,7 +862,7 @@ tensor_product.lift $ by
 lemma dom_coprod'_apply
   (a : alternating_map R' Mᵢ N₁ ιa) (b : alternating_map R' Mᵢ N₂ ιb) :
   dom_coprod' (a ⊗ₜ[R'] b) = dom_coprod a b :=
-by simp only [dom_coprod', tensor_product.lift.tmul, linear_map.mk₂_apply]
+rfl
 
 end alternating_map
 

src/linear_algebra/contraction.lean

@@ -48,14 +48,14 @@ def dual_tensor_hom : (module.dual R M) ⊗ N →ₗ[R] M →ₗ[R] N :=
 variables {R M N P Q}
 
 @[simp] lemma contract_left_apply (f : module.dual R M) (m : M) :
-  contract_left R M (f ⊗ₜ m) = f m := by apply uncurry_apply
+  contract_left R M (f ⊗ₜ m) = f m := rfl
 
 @[simp] lemma contract_right_apply (f : module.dual R M) (m : M) :
-  contract_right R M (m ⊗ₜ f) = f m := by apply uncurry_apply
+  contract_right R M (m ⊗ₜ f) = f m := rfl
 
 @[simp] lemma dual_tensor_hom_apply (f : module.dual R M) (m : M) (n : N) :
   dual_tensor_hom R M N (f ⊗ₜ n) m = (f m) • n :=
-by { dunfold dual_tensor_hom, rw uncurry_apply, refl, }
+rfl
 
 @[simp] lemma transpose_dual_tensor_hom (f : module.dual R M) (m : M) :
   dual.transpose (dual_tensor_hom R M M (f ⊗ₜ m)) = dual_tensor_hom R _ _ (dual.eval R M m ⊗ₜ f) :=
@@ -199,6 +199,7 @@ begin
   have h : function.surjective e.to_linear_map := e.surjective,
   refine (cancel_right h).1 _,
   ext p f q m,
+  dsimp [ltensor_hom_equiv_hom_ltensor],
   simp only [ltensor_hom_equiv_hom_ltensor, dual_tensor_hom_equiv, compr₂_apply, mk_apply, coe_comp,
   linear_equiv.coe_to_linear_map, function.comp_app, map_tmul, linear_equiv.coe_coe,
   dual_tensor_hom_equiv_of_basis_apply, linear_equiv.trans_apply, congr_tmul,

src/linear_algebra/tensor_product.lean

@@ -403,8 +403,7 @@ add_con.add_con_gen_le $ λ x y hxy, match x, y, hxy with
     by simp_rw [add_monoid_hom.map_add, add_comm]
 end
 
-lemma lift_aux_tmul (m n) : lift_aux f (m ⊗ₜ n) = f m n :=
-zero_add _
+lemma lift_aux_tmul (m n) : lift_aux f (m ⊗ₜ n) = f m n := rfl
 
 variable {f}
 
@@ -422,11 +421,8 @@ def lift : M ⊗ N →ₗ[R] P :=
   .. lift_aux f }
 variable {f}
 
-@[simp] lemma lift.tmul (x y) : lift f (x ⊗ₜ y) = f x y :=
-zero_add _
-
-@[simp] lemma lift.tmul' (x y) : (lift f).1 (x ⊗ₜ y) = f x y :=
-lift.tmul _ _
+@[simp] lemma lift.tmul (x y) : lift f (x ⊗ₜ y) = f x y := rfl
+@[simp] lemma lift.tmul' (x y) : (lift f).1 (x ⊗ₜ y) = f x y := rfl
 
 theorem ext' {g h : (M ⊗[R] N) →ₗ[R] P}
   (H : ∀ x y, g (x ⊗ₜ y) = h (x ⊗ₜ y)) : g = h :=
@@ -653,11 +649,11 @@ variables [add_comm_monoid Q'] [module R Q']
 
 lemma map_comp (f₂ : P →ₗ[R] P') (f₁ : M →ₗ[R] P) (g₂ : Q →ₗ[R] Q') (g₁ : N →ₗ[R] Q) :
   map (f₂.comp f₁) (g₂.comp g₁) = (map f₂ g₂).comp (map f₁ g₁) :=
-ext' $ λ _ _, by simp only [linear_map.comp_apply, map_tmul]
+ext' $ λ _ _, rfl
 
 lemma lift_comp_map (i : P →ₗ[R] Q →ₗ[R] Q') (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
   (lift i).comp (map f g) = lift ((i.comp f).compl₂ g) :=
-ext' $ λ _ _, by simp only [lift.tmul, map_tmul, linear_map.compl₂_apply, linear_map.comp_apply]
+ext' $ λ _ _, rfl
 
 local attribute [ext] ext
 

src/ring_theory/derivation.lean

@@ -520,7 +520,7 @@ tensor_product.algebra_tensor_module.lift ((linear_map.lsmul S (S →ₗ[R] M)).
 
 lemma derivation.tensor_product_to_tmul (D : derivation R S M) (s t : S) :
   D.tensor_product_to (s ⊗ₜ t) = s • D t :=
-tensor_product.lift.tmul s t
+rfl
 
 lemma derivation.tensor_product_to_mul (D : derivation R S M) (x y : S ⊗[R] S) :
   D.tensor_product_to (x * y) = tensor_product.lmul' R x • D.tensor_product_to y +
@@ -815,7 +815,7 @@ begin
   { generalize : f x = y, obtain ⟨y, rfl⟩ := ideal.quotient.mk_surjective y, refl },
   have e₂ : x = kaehler_differential.quotient_cotangent_ideal_ring_equiv
     R S (is_scalar_tower.to_alg_hom R S _ x),
-  { exact ((tensor_product.lmul'_apply_tmul x 1).trans (mul_one x)).symm },
+  { exact (mul_one x).symm },
   split,
   { intro e,
     exact (e₁.trans (@ring_equiv.congr_arg _ _ _ _ _ _

src/ring_theory/polynomial_algebra.lean

@@ -72,7 +72,7 @@ tensor_product.lift (to_fun_bilinear R A)
 
 @[simp]
 lemma to_fun_linear_tmul_apply (a : A) (p : R[X]) :
-  to_fun_linear R A (a ⊗ₜ[R] p) = to_fun_bilinear R A a p := lift.tmul _ _
+  to_fun_linear R A (a ⊗ₜ[R] p) = to_fun_bilinear R A a p := rfl
 
 -- We apparently need to provide the decidable instance here
 -- in order to successfully rewrite by this lemma.
@@ -125,10 +125,7 @@ alg_hom_of_linear_map_tensor_product
 
 @[simp] lemma to_fun_alg_hom_apply_tmul (a : A) (p : R[X]) :
   to_fun_alg_hom R A (a ⊗ₜ[R] p) = p.sum (λ n r, monomial n (a * (algebra_map R A) r)) :=
-begin
-  dsimp [to_fun_alg_hom],
-  rw [to_fun_linear_tmul_apply, to_fun_bilinear_apply_eq_sum],
-end
+to_fun_bilinear_apply_eq_sum R A _ _
 
 /--
 (Implementation detail.)