bump to nightly-2023-08-15-09

mathlib commit leanprover-community/mathlib@32a7e53

Mathbin/Algebra/Hom/Iterate.lean

@@ -56,13 +56,11 @@ theorem iterate_map_one (f : M →* M) (n : ℕ) : (f^[n]) 1 = 1 :=
 #align add_monoid_hom.iterate_map_zero AddMonoidHom.iterate_map_zero
 -/
 
-#print MonoidHom.iterate_map_mul /-
 @[simp, to_additive]
 theorem iterate_map_mul (f : M →* M) (n : ℕ) (x y) : (f^[n]) (x * y) = (f^[n]) x * (f^[n]) y :=
   Semiconj₂.iterate f.map_mul n x y
 #align monoid_hom.iterate_map_mul MonoidHom.iterate_map_mul
 #align add_monoid_hom.iterate_map_add AddMonoidHom.iterate_map_add
--/
 
 end
 
@@ -163,17 +161,13 @@ theorem iterate_map_zero : (f^[n]) 0 = 0 :=
 #align ring_hom.iterate_map_zero RingHom.iterate_map_zero
 -/
 
-#print RingHom.iterate_map_add /-
 theorem iterate_map_add : (f^[n]) (x + y) = (f^[n]) x + (f^[n]) y :=
   f.toAddMonoidHom.iterate_map_add n x y
 #align ring_hom.iterate_map_add RingHom.iterate_map_add
--/
 
-#print RingHom.iterate_map_mul /-
 theorem iterate_map_mul : (f^[n]) (x * y) = (f^[n]) x * (f^[n]) y :=
   f.toMonoidHom.iterate_map_mul n x y
 #align ring_hom.iterate_map_mul RingHom.iterate_map_mul
--/
 
 #print RingHom.iterate_map_pow /-
 theorem iterate_map_pow (a) (n m : ℕ) : (f^[n]) (a ^ m) = (f^[n]) a ^ m :=

Mathbin/Algebra/Lie/Nilpotent.lean

@@ -250,16 +250,16 @@ instance (priority := 100) trivialIsNilpotent [IsTrivial L M] : IsNilpotent R L
 #align lie_module.trivial_is_nilpotent LieModule.trivialIsNilpotent
 -/
 
-#print LieModule.nilpotent_endo_of_nilpotent_module /-
-theorem nilpotent_endo_of_nilpotent_module [hM : IsNilpotent R L M] :
+#print LieModule.exists_forall_pow_toEndomorphism_eq_zero /-
+theorem exists_forall_pow_toEndomorphism_eq_zero [hM : IsNilpotent R L M] :
     ∃ k : ℕ, ∀ x : L, toEndomorphism R L M x ^ k = 0 :=
   by
   obtain ⟨k, hM⟩ := hM
   use k
   intro x; ext m
   rw [LinearMap.pow_apply, LinearMap.zero_apply, ← @LieSubmodule.mem_bot R L M, ← hM]
   exact iterate_to_endomorphism_mem_lower_central_series R L M x m k
-#align lie_module.nilpotent_endo_of_nilpotent_module LieModule.nilpotent_endo_of_nilpotent_module
+#align lie_module.nilpotent_endo_of_nilpotent_module LieModule.exists_forall_pow_toEndomorphism_eq_zero
 -/
 
 #print LieModule.iInf_max_gen_zero_eigenspace_eq_top_of_nilpotent /-
@@ -641,7 +641,7 @@ open LieAlgebra
 #print LieAlgebra.nilpotent_ad_of_nilpotent_algebra /-
 theorem LieAlgebra.nilpotent_ad_of_nilpotent_algebra [IsNilpotent R L] :
     ∃ k : ℕ, ∀ x : L, ad R L x ^ k = 0 :=
-  LieModule.nilpotent_endo_of_nilpotent_module R L L
+  LieModule.exists_forall_pow_toEndomorphism_eq_zero R L L
 #align lie_algebra.nilpotent_ad_of_nilpotent_algebra LieAlgebra.nilpotent_ad_of_nilpotent_algebra
 -/
 

Mathbin/Combinatorics/SimpleGraph/Basic.lean

@@ -2262,33 +2262,33 @@ section InduceHom
 variable {G G'} {G'' : SimpleGraph X} {s : Set V} {t : Set W} {r : Set X} (φ : G →g G')
   (φst : Set.MapsTo φ s t) (ψ : G' →g G'') (ψtr : Set.MapsTo ψ t r)
 
-#print SimpleGraph.InduceHom /-
+#print SimpleGraph.induceHom /-
 /-- The restriction of a morphism of graphs to induced subgraphs. -/
-def InduceHom : G.induce s →g G'.induce t
+def induceHom : G.induce s →g G'.induce t
     where
   toFun := Set.MapsTo.restrict φ s t φst
   map_rel' _ _ := φ.map_rel'
-#align simple_graph.induce_hom SimpleGraph.InduceHom
+#align simple_graph.induce_hom SimpleGraph.induceHom
 -/
 
 #print SimpleGraph.coe_induceHom /-
 @[simp, norm_cast]
-theorem coe_induceHom : ⇑(InduceHom φ φst) = Set.MapsTo.restrict φ s t φst :=
+theorem coe_induceHom : ⇑(induceHom φ φst) = Set.MapsTo.restrict φ s t φst :=
   rfl
 #align simple_graph.coe_induce_hom SimpleGraph.coe_induceHom
 -/
 
 #print SimpleGraph.induceHom_id /-
 @[simp]
 theorem induceHom_id (G : SimpleGraph V) (s) :
-    InduceHom (Hom.id : G →g G) (Set.mapsTo_id s) = Hom.id := by ext x; rfl
+    induceHom (Hom.id : G →g G) (Set.mapsTo_id s) = Hom.id := by ext x; rfl
 #align simple_graph.induce_hom_id SimpleGraph.induceHom_id
 -/
 
 #print SimpleGraph.induceHom_comp /-
 @[simp]
 theorem induceHom_comp :
-    (InduceHom ψ ψtr).comp (InduceHom φ φst) = InduceHom (ψ.comp φ) (ψtr.comp φst) := by ext x; rfl
+    (induceHom ψ ψtr).comp (induceHom φ φst) = induceHom (ψ.comp φ) (ψtr.comp φst) := by ext x; rfl
 #align simple_graph.induce_hom_comp SimpleGraph.induceHom_comp
 -/
 

Mathbin/Combinatorics/SimpleGraph/Connectivity.lean

@@ -2747,28 +2747,28 @@ abbrev Subgraph.Connected (H : G.Subgraph) : Prop :=
 #align simple_graph.subgraph.connected SimpleGraph.Subgraph.Connected
 -/
 
-#print SimpleGraph.singletonSubgraph_connected /-
-theorem singletonSubgraph_connected {v : V} : (G.singletonSubgraph v).Connected :=
-  by
+#print SimpleGraph.Subgraph.singletonSubgraph_connected /-
+theorem SimpleGraph.Subgraph.singletonSubgraph_connected {v : V} :
+    (G.singletonSubgraph v).Connected := by
   constructor
   rintro ⟨a, ha⟩ ⟨b, hb⟩
   simp only [singleton_subgraph_verts, Set.mem_singleton_iff] at ha hb 
   subst_vars
-#align simple_graph.singleton_subgraph_connected SimpleGraph.singletonSubgraph_connected
+#align simple_graph.singleton_subgraph_connected SimpleGraph.Subgraph.singletonSubgraph_connected
 -/
 
-#print SimpleGraph.subgraphOfAdj_connected /-
+#print SimpleGraph.Subgraph.subgraphOfAdj_connected /-
 @[simp]
-theorem subgraphOfAdj_connected {v w : V} (hvw : G.Adj v w) : (G.subgraphOfAdj hvw).Connected :=
-  by
+theorem SimpleGraph.Subgraph.subgraphOfAdj_connected {v w : V} (hvw : G.Adj v w) :
+    (G.subgraphOfAdj hvw).Connected := by
   constructor
   rintro ⟨a, ha⟩ ⟨b, hb⟩
   simp only [subgraph_of_adj_verts, Set.mem_insert_iff, Set.mem_singleton_iff] at ha hb 
   obtain rfl | rfl := ha <;> obtain rfl | rfl := hb <;>
     first
     | rfl
     | · apply adj.reachable; simp
-#align simple_graph.subgraph_of_adj_connected SimpleGraph.subgraphOfAdj_connected
+#align simple_graph.subgraph_of_adj_connected SimpleGraph.Subgraph.subgraphOfAdj_connected
 -/
 
 #print SimpleGraph.Preconnected.set_univ_walk_nonempty /-

Mathbin/Combinatorics/SimpleGraph/Ends/Defs.lean

@@ -212,7 +212,7 @@ If `K ⊆ L`, the components outside of `L` are all contained in a single compon
 -/
 @[reducible]
 def hom (h : K ⊆ L) (C : G.ComponentCompl L) : G.ComponentCompl K :=
-  C.map <| InduceHom Hom.id <| Set.compl_subset_compl.2 h
+  C.map <| induceHom Hom.id <| Set.compl_subset_compl.2 h
 #align simple_graph.component_compl.hom SimpleGraph.ComponentCompl.hom
 -/
 

Mathbin/Data/Polynomial/Derivative.lean

@@ -187,13 +187,11 @@ theorem derivative_X_add_C (c : R) : (X + C c).derivative = 1 := by
 #align polynomial.derivative_X_add_C Polynomial.derivative_X_add_C
 -/
 
-#print Polynomial.iterate_derivative_add /-
 @[simp]
 theorem iterate_derivative_add {f g : R[X]} {k : ℕ} :
     (derivative^[k]) (f + g) = (derivative^[k]) f + (derivative^[k]) g :=
   derivative.toAddMonoidHom.iterate_map_add _ _ _
 #align polynomial.iterate_derivative_add Polynomial.iterate_derivative_add
--/
 
 #print Polynomial.derivative_sum /-
 @[simp]

Mathbin/FieldTheory/PerfectClosure.lean

@@ -44,12 +44,10 @@ def frobeniusEquiv [PerfectRing R p] : R ≃+* R :=
 #align frobenius_equiv frobeniusEquiv
 -/
 
-#print pthRoot /-
 /-- `p`-th root of an element in a `perfect_ring` as a `ring_hom`. -/
 def pthRoot [PerfectRing R p] : R →+* R :=
   (frobeniusEquiv R p).symm
 #align pth_root pthRoot
--/
 
 end Defs
 
@@ -65,96 +63,68 @@ theorem coe_frobeniusEquiv : ⇑(frobeniusEquiv R p) = frobenius R p :=
 #align coe_frobenius_equiv coe_frobeniusEquiv
 -/
 
-#print coe_frobeniusEquiv_symm /-
 @[simp]
 theorem coe_frobeniusEquiv_symm : ⇑(frobeniusEquiv R p).symm = pthRoot R p :=
   rfl
 #align coe_frobenius_equiv_symm coe_frobeniusEquiv_symm
--/
 
-#print frobenius_pthRoot /-
 @[simp]
 theorem frobenius_pthRoot (x : R) : frobenius R p (pthRoot R p x) = x :=
   (frobeniusEquiv R p).apply_symm_apply x
 #align frobenius_pth_root frobenius_pthRoot
--/
 
-#print pthRoot_pow_p /-
 @[simp]
 theorem pthRoot_pow_p (x : R) : pthRoot R p x ^ p = x :=
   frobenius_pthRoot x
 #align pth_root_pow_p pthRoot_pow_p
--/
 
-#print pthRoot_frobenius /-
 @[simp]
 theorem pthRoot_frobenius (x : R) : pthRoot R p (frobenius R p x) = x :=
   (frobeniusEquiv R p).symm_apply_apply x
 #align pth_root_frobenius pthRoot_frobenius
--/
 
-#print pthRoot_pow_p' /-
 @[simp]
 theorem pthRoot_pow_p' (x : R) : pthRoot R p (x ^ p) = x :=
   pthRoot_frobenius x
 #align pth_root_pow_p' pthRoot_pow_p'
--/
 
-#print leftInverse_pthRoot_frobenius /-
 theorem leftInverse_pthRoot_frobenius : LeftInverse (pthRoot R p) (frobenius R p) :=
   pthRoot_frobenius
 #align left_inverse_pth_root_frobenius leftInverse_pthRoot_frobenius
--/
 
-#print rightInverse_pthRoot_frobenius /-
 theorem rightInverse_pthRoot_frobenius : Function.RightInverse (pthRoot R p) (frobenius R p) :=
   frobenius_pthRoot
 #align right_inverse_pth_root_frobenius rightInverse_pthRoot_frobenius
--/
 
-#print commute_frobenius_pthRoot /-
 theorem commute_frobenius_pthRoot : Function.Commute (frobenius R p) (pthRoot R p) := fun x =>
   (frobenius_pthRoot x).trans (pthRoot_frobenius x).symm
 #align commute_frobenius_pth_root commute_frobenius_pthRoot
--/
 
-#print eq_pthRoot_iff /-
 theorem eq_pthRoot_iff {x y : R} : x = pthRoot R p y ↔ frobenius R p x = y :=
   (frobeniusEquiv R p).toEquiv.eq_symm_apply
 #align eq_pth_root_iff eq_pthRoot_iff
--/
 
-#print pthRoot_eq_iff /-
 theorem pthRoot_eq_iff {x y : R} : pthRoot R p x = y ↔ x = frobenius R p y :=
   (frobeniusEquiv R p).toEquiv.symm_apply_eq
 #align pth_root_eq_iff pthRoot_eq_iff
--/
 
-#print MonoidHom.map_pthRoot /-
 theorem MonoidHom.map_pthRoot (x : R) : f (pthRoot R p x) = pthRoot S p (f x) :=
   eq_pthRoot_iff.2 <| by rw [← f.map_frobenius, frobenius_pthRoot]
 #align monoid_hom.map_pth_root MonoidHom.map_pthRoot
--/
 
-#print MonoidHom.map_iterate_pthRoot /-
 theorem MonoidHom.map_iterate_pthRoot (x : R) (n : ℕ) :
     f ((pthRoot R p^[n]) x) = (pthRoot S p^[n]) (f x) :=
   Semiconj.iterate_right f.map_pthRoot n x
 #align monoid_hom.map_iterate_pth_root MonoidHom.map_iterate_pthRoot
--/
 
-#print RingHom.map_pthRoot /-
 theorem RingHom.map_pthRoot (x : R) : g (pthRoot R p x) = pthRoot S p (g x) :=
   g.toMonoidHom.map_pthRoot x
 #align ring_hom.map_pth_root RingHom.map_pthRoot
--/
 
-#print RingHom.map_iterate_pthRoot /-
 theorem RingHom.map_iterate_pthRoot (x : R) (n : ℕ) :
     g ((pthRoot R p^[n]) x) = (pthRoot S p^[n]) (g x) :=
   g.toMonoidHom.map_iterate_pthRoot x n
 #align ring_hom.map_iterate_pth_root RingHom.map_iterate_pthRoot
--/
 
 variable (p)
 
@@ -594,14 +564,12 @@ instance : PerfectRing (PerfectClosure K p) p
     induction_on e fun ⟨n, x⟩ => by simp only [lift_on_mk, frobenius_mk];
       exact (Quot.sound <| r.intro _ _).symm
 
-#print PerfectClosure.eq_pthRoot /-
 theorem eq_pthRoot (x : ℕ × K) : mk K p x = (pthRoot (PerfectClosure K p) p^[x.1]) (of K p x.2) :=
   by
   rcases x with ⟨m, x⟩
   induction' m with m ih; · rfl
   rw [iterate_succ_apply', ← ih] <;> rfl
 #align perfect_closure.eq_pth_root PerfectClosure.eq_pthRoot
--/
 
 #print PerfectClosure.lift /-
 /-- Given a field `K` of characteristic `p` and a perfect ring `L` of the same characteristic,

Mathbin/LinearAlgebra/BilinearForm.lean

@@ -1144,8 +1144,8 @@ theorem isSymm_neg {B : BilinForm R₁ M₁} : (-B).IsSymm ↔ B.IsSymm :=
 #align bilin_form.is_symm_neg BilinForm.isSymm_neg
 -/
 
-#print BilinForm.isSymm_iff_flip' /-
-theorem isSymm_iff_flip' [Algebra R₂ R] : B.IsSymm ↔ flipHom R₂ B = B :=
+#print BilinForm.isSymm_iff_flip /-
+theorem isSymm_iff_flip [Algebra R₂ R] : B.IsSymm ↔ flipHom R₂ B = B :=
   by
   constructor
   · intro h
@@ -1154,7 +1154,7 @@ theorem isSymm_iff_flip' [Algebra R₂ R] : B.IsSymm ↔ flipHom R₂ B = B :=
   · intro h x y
     conv_lhs => rw [← h]
     simp
-#align bilin_form.is_symm_iff_flip' BilinForm.isSymm_iff_flip'
+#align bilin_form.is_symm_iff_flip' BilinForm.isSymm_iff_flip
 -/
 
 #print BilinForm.IsAlt /-