Merge remote-tracking branch 'origin/master' into adomani/lint_multip…

…le_goals

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -235,7 +235,7 @@ theorem first_vote_neg (p q : ℕ) (h : 0 < p + q) :
   have := condCount_compl
     {l : List ℤ | l.headI = 1}ᶜ (countedSequence_finite p q) (countedSequence_nonempty p q)
   rw [compl_compl, first_vote_pos _ _ h] at this
-  rw [← ENNReal.sub_eq_of_add_eq _ this, ENNReal.eq_div_iff, ENNReal.mul_sub, mul_one,
+  rw [ENNReal.eq_sub_of_add_eq _ this, ENNReal.eq_div_iff, ENNReal.mul_sub, mul_one,
     ENNReal.mul_div_cancel', ENNReal.add_sub_cancel_left]
   all_goals simp_all [ENNReal.div_eq_top]
 

Mathlib.lean

@@ -1097,6 +1097,7 @@ import Mathlib.Analysis.Convex.Cone.Extension
 import Mathlib.Analysis.Convex.Cone.InnerDual
 import Mathlib.Analysis.Convex.Cone.Pointed
 import Mathlib.Analysis.Convex.Cone.Proper
+import Mathlib.Analysis.Convex.Continuous
 import Mathlib.Analysis.Convex.Contractible
 import Mathlib.Analysis.Convex.Deriv
 import Mathlib.Analysis.Convex.EGauge
@@ -2518,6 +2519,7 @@ import Mathlib.Data.Real.GoldenRatio
 import Mathlib.Data.Real.Hyperreal
 import Mathlib.Data.Real.Irrational
 import Mathlib.Data.Real.Pi.Bounds
+import Mathlib.Data.Real.Pi.Irrational
 import Mathlib.Data.Real.Pi.Leibniz
 import Mathlib.Data.Real.Pi.Wallis
 import Mathlib.Data.Real.Pointwise
@@ -4067,8 +4069,10 @@ import Mathlib.RingTheory.TensorProduct.MvPolynomial
 import Mathlib.RingTheory.Trace.Basic
 import Mathlib.RingTheory.Trace.Defs
 import Mathlib.RingTheory.TwoSidedIdeal.Basic
+import Mathlib.RingTheory.TwoSidedIdeal.BigOperators
 import Mathlib.RingTheory.TwoSidedIdeal.Instances
 import Mathlib.RingTheory.TwoSidedIdeal.Lattice
+import Mathlib.RingTheory.TwoSidedIdeal.Operations
 import Mathlib.RingTheory.UniqueFactorizationDomain
 import Mathlib.RingTheory.Unramified.Basic
 import Mathlib.RingTheory.Unramified.Derivations

Mathlib/Algebra/Algebra/Basic.lean

@@ -185,8 +185,7 @@ theorem End_algebraMap_isUnit_inv_apply_eq_iff {x : R}
     mpr := fun H =>
       H.symm ▸ by
         apply_fun ⇑h.unit.val using ((Module.End_isUnit_iff _).mp h).injective
-        erw [End_isUnit_apply_inv_apply_of_isUnit]
-        rfl }
+        simpa using End_isUnit_apply_inv_apply_of_isUnit h (x • m') }
 
 theorem End_algebraMap_isUnit_inv_apply_eq_iff' {x : R}
     (h : IsUnit (algebraMap R (Module.End S M) x)) (m m' : M) :
@@ -195,8 +194,7 @@ theorem End_algebraMap_isUnit_inv_apply_eq_iff' {x : R}
     mpr := fun H =>
       H.symm ▸ by
         apply_fun (↑h.unit : M → M) using ((Module.End_isUnit_iff _).mp h).injective
-        erw [End_isUnit_apply_inv_apply_of_isUnit]
-        rfl }
+        simpa using End_isUnit_apply_inv_apply_of_isUnit h (x • m') |>.symm }
 
 end
 

Mathlib/Algebra/CharP/Defs.lean

@@ -11,6 +11,7 @@ import Mathlib.Data.Nat.Cast.Prod
 import Mathlib.Data.Nat.Find
 import Mathlib.Data.Nat.Prime.Defs
 import Mathlib.Data.ULift
+import Mathlib.Tactic.NormNum.Basic
 
 /-!
 # Characteristic of semirings
@@ -102,10 +103,10 @@ lemma intCast_injOn_Ico [IsRightCancelAdd R] : InjOn (Int.cast : ℤ → R) (Ico
 
 lemma intCast_eq_zero_iff (a : ℤ) : (a : R) = 0 ↔ (p : ℤ) ∣ a := by
   rcases lt_trichotomy a 0 with (h | rfl | h)
-  · rw [← neg_eq_zero, ← Int.cast_neg, ← dvd_neg]
+  · rw [← neg_eq_zero, ← Int.cast_neg, ← Int.dvd_neg]
     lift -a to ℕ using neg_nonneg.mpr (le_of_lt h) with b
     rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]
-  · simp only [Int.cast_zero, eq_self_iff_true, dvd_zero]
+  · simp only [Int.cast_zero, eq_self_iff_true, Int.dvd_zero]
   · lift a to ℕ using le_of_lt h with b
     rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]
 

Mathlib/Algebra/Group/Hom/Defs.lean

@@ -452,7 +452,7 @@ theorem map_pow [Monoid G] [Monoid H] [MonoidHomClass F G H] (f : F) (a : G) :
   | n + 1 => by rw [pow_succ, pow_succ, map_mul, map_pow f a n]
 
 @[to_additive (attr := simp)]
-lemma map_comp_pow [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : ι → G) (n : ℕ) :
+lemma map_comp_pow [Monoid G] [Monoid H] [MonoidHomClass F G H] (f : F) (g : ι → G) (n : ℕ) :
     f ∘ (g ^ n) = f ∘ g ^ n := by ext; simp
 
 @[to_additive]

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -69,7 +69,7 @@ Definitions in the file:
 * `MonoidHom.ker f` : the kernel of a group homomorphism `f` is the subgroup of elements `x : G`
   such that `f x = 1`
 
-* `MonoidHom.eq_locus f g` : given group homomorphisms `f`, `g`, the elements of `G` such that
+* `MonoidHom.eqLocus f g` : given group homomorphisms `f`, `g`, the elements of `G` such that
   `f x = g x` form a subgroup of `G`
 
 ## Implementation notes

Mathlib/Algebra/Lie/Subalgebra.lean

@@ -224,7 +224,7 @@ variable [Module R M]
 `L`, we may regard `M` as a Lie module of `L'` by restriction. -/
 instance lieModule [LieModule R L M] : LieModule R L' M where
   smul_lie t x m := by
-    rw [coe_bracket_of_module]; erw [smul_lie]; simp only [coe_bracket_of_module]
+    rw [coe_bracket_of_module, Submodule.coe_smul_of_tower, smul_lie, coe_bracket_of_module]
   lie_smul t x m := by simp only [coe_bracket_of_module, lie_smul]
 
 /-- An `L`-equivariant map of Lie modules `M → N` is `L'`-equivariant for any Lie subalgebra

Mathlib/Algebra/ModEq.lean

@@ -5,6 +5,7 @@ Authors: Yaël Dillies
 -/
 import Mathlib.Data.Int.ModEq
 import Mathlib.Algebra.Field.Basic
+import Mathlib.Algebra.Order.Ring.Int
 import Mathlib.GroupTheory.QuotientGroup.Basic
 
 /-!

Mathlib/Algebra/Module/Equiv/Basic.lean

@@ -122,7 +122,7 @@ protected theorem smul_def (f : M ≃ₗ[R] M) (a : M) : f • a = f a :=
 
 /-- `LinearEquiv.applyDistribMulAction` is faithful. -/
 instance apply_faithfulSMul : FaithfulSMul (M ≃ₗ[R] M) M :=
-  ⟨@fun _ _ ↦ LinearEquiv.ext⟩
+  ⟨LinearEquiv.ext⟩
 
 instance apply_smulCommClass [SMul S R] [SMul S M] [IsScalarTower S R M] :
     SMulCommClass S (M ≃ₗ[R] M) M where

Mathlib/Algebra/Module/LinearMap/Defs.lean

@@ -933,9 +933,8 @@ end Actions
 
 section RestrictScalarsAsLinearMap
 
-variable {R S M N : Type*} [Semiring R] [Semiring S] [AddCommGroup M] [AddCommGroup N] [Module R M]
-   [Module R N] [Module S M] [Module S N]
-  [LinearMap.CompatibleSMul M N R S]
+variable {R S M N P : Type*} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N]
+  [Module R M] [Module R N] [Module S M] [Module S N] [CompatibleSMul M N R S]
 
 variable (R S M N) in
 @[simp]
@@ -948,7 +947,9 @@ theorem restrictScalars_add (f g : M →ₗ[S] N) :
   rfl
 
 @[simp]
-theorem restrictScalars_neg (f : M →ₗ[S] N) : (-f).restrictScalars R = -f.restrictScalars R :=
+theorem restrictScalars_neg {M N : Type*} [AddCommGroup M] [AddCommGroup N]
+    [Module R M] [Module R N] [Module S M] [Module S N] [CompatibleSMul M N R S]
+    (f : M →ₗ[S] N) : (-f).restrictScalars R = -f.restrictScalars R :=
   rfl
 
 variable {R₁ : Type*} [Semiring R₁] [Module R₁ N] [SMulCommClass S R₁ N] [SMulCommClass R R₁ N]
@@ -958,6 +959,18 @@ theorem restrictScalars_smul (c : R₁) (f : M →ₗ[S] N) :
     (c • f).restrictScalars R = c • f.restrictScalars R :=
   rfl
 
+@[simp]
+lemma restrictScalars_comp [AddCommMonoid P] [Module S P] [Module R P]
+    [CompatibleSMul N P R S] [CompatibleSMul M P R S] (f : N →ₗ[S] P) (g : M →ₗ[S] N) :
+    (f ∘ₗ g).restrictScalars R = f.restrictScalars R ∘ₗ g.restrictScalars R := by
+  rfl
+
+@[simp]
+lemma restrictScalars_trans {T : Type*} [CommSemiring T] [Module T M] [Module T N]
+    [CompatibleSMul M N S T] [CompatibleSMul M N R T] (f : M →ₗ[T] N) :
+    (f.restrictScalars S).restrictScalars R = f.restrictScalars R :=
+  rfl
+
 variable (S M N R R₁)
 
 /-- `LinearMap.restrictScalars` as a `LinearMap`. -/

Mathlib/Algebra/MvPolynomial/Basic.lean

@@ -1357,6 +1357,11 @@ theorem comp_aeval {B : Type*} [CommSemiring B] [Algebra R B] (φ : S₁ →ₐ[
   ext i
   simp
 
+lemma comp_aeval_apply {B : Type*} [CommSemiring B] [Algebra R B] (φ : S₁ →ₐ[R] B)
+    (p : MvPolynomial σ R) :
+    φ (aeval f p) = aeval (fun i ↦ φ (f i)) p := by
+  rw [← comp_aeval, AlgHom.coe_comp, comp_apply]
+
 @[simp]
 theorem map_aeval {B : Type*} [CommSemiring B] (g : σ → S₁) (φ : S₁ →+* B) (p : MvPolynomial σ R) :
     φ (aeval g p) = eval₂Hom (φ.comp (algebraMap R S₁)) (fun i => φ (g i)) p := by
@@ -1537,6 +1542,17 @@ theorem eval_mem {p : MvPolynomial σ S} {s : subS} (hs : ∀ i ∈ p.support, p
 
 end EvalMem
 
+variable {S T : Type*} [CommSemiring S] [Algebra R S] [CommSemiring T] [Algebra R T] [Algebra S T]
+  [IsScalarTower R S T]
+
+lemma aeval_sum_elim {σ τ : Type*} (p : MvPolynomial (σ ⊕ τ) R) (f : τ → S) (g : σ → T) :
+    (aeval (Sum.elim g (algebraMap S T ∘ f))) p =
+      (aeval g) ((aeval (Sum.elim X (C ∘ f))) p) := by
+  induction' p using MvPolynomial.induction_on with r p q hp hq p i h
+  · simp [← IsScalarTower.algebraMap_apply]
+  · simp [hp, hq]
+  · cases i <;> simp [h]
+
 end CommSemiring
 
 end MvPolynomial

Mathlib/Algebra/MvPolynomial/PDeriv.lean

@@ -115,6 +115,27 @@ theorem pderiv_map {S} [CommSemiring S] {φ : R →+* S} {f : MvPolynomial σ R}
   · simp [eq]
   · simp [eq, h]
 
+lemma pderiv_rename {τ : Type*} [DecidableEq τ] [DecidableEq σ] {f : σ → τ}
+    (hf : Function.Injective f) (x : σ) (p : MvPolynomial σ R) :
+    pderiv (f x) (rename f p) = rename f (pderiv x p) := by
+  induction' p using MvPolynomial.induction_on with a p q hp hq p a h
+  · simp
+  · simp [hp, hq]
+  · simp only [map_mul, MvPolynomial.rename_X, Derivation.leibniz, MvPolynomial.pderiv_X,
+      Pi.single_apply, hf.eq_iff, smul_eq_mul, mul_ite, mul_one, mul_zero, h, map_add, add_left_inj]
+    split_ifs <;> simp
+
+lemma aeval_sum_elim_pderiv_inl {S τ : Type*} [CommRing S] [Algebra R S]
+    (p : MvPolynomial (σ ⊕ τ) R) (f : τ → S) (j : σ) :
+    aeval (Sum.elim X (C ∘ f)) ((pderiv (Sum.inl j)) p) =
+      (pderiv j) ((aeval (Sum.elim X (C ∘ f))) p) := by
+  classical
+  induction' p using MvPolynomial.induction_on with a p q hp hq p q h
+  · simp
+  · simp [hp, hq]
+  · simp only [Derivation.leibniz, pderiv_X, smul_eq_mul, map_add, map_mul, aeval_X, h]
+    cases q <;> simp [Pi.single_apply]
+
 end PDeriv
 
 end MvPolynomial

Mathlib/Algebra/Order/BigOperators/Expect.lean

@@ -130,8 +130,7 @@ end LinearOrderedAddCommMonoid
 section LinearOrderedAddCommGroup
 variable [LinearOrderedAddCommGroup α] [Module ℚ≥0 α] [PosSMulMono ℚ≥0 α]
 
--- TODO: Norm version
-lemma abs_expect_le_expect_abs (s : Finset ι) (f : ι → α) : |𝔼 i ∈ s, f i| ≤ 𝔼 i ∈ s, |f i| :=
+lemma abs_expect_le (s : Finset ι) (f : ι → α) : |𝔼 i ∈ s, f i| ≤ 𝔼 i ∈ s, |f i| :=
   le_expect_of_subadditive abs_zero abs_add (fun _ ↦ abs_nnqsmul _)
 
 end LinearOrderedAddCommGroup

Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

@@ -221,6 +221,16 @@ theorem abs_sum_of_nonneg' {G : Type*} [LinearOrderedAddCommGroup G] {f : ι →
     (hf : ∀ i, 0 ≤ f i) : |∑ i ∈ s, f i| = ∑ i ∈ s, f i := by
   rw [abs_of_nonneg (Finset.sum_nonneg' hf)]
 
+section CommMonoid
+variable [CommMonoid α] [LE α] [CovariantClass α α (· * ·) (· ≤ ·)] {s : Finset ι} {f : ι → α}
+
+@[to_additive (attr := simp)]
+lemma mulLECancellable_prod :
+    MulLECancellable (∏ i ∈ s, f i) ↔ ∀ ⦃i⦄, i ∈ s → MulLECancellable (f i) := by
+  induction' s using Finset.cons_induction with i s hi ih <;> simp [*]
+
+end CommMonoid
+
 section Pigeonhole
 
 variable [DecidableEq β]