bump to nightly-2023-08-26-09

mathlib commit leanprover-community/mathlib@32a7e53

Mathbin/Algebra/BigOperators/Finsupp.lean

@@ -681,28 +681,29 @@ theorem prod_dvd_prod_of_subset_of_dvd [AddCommMonoid M] [CommMonoid N] {f1 f2 :
 #align finsupp.prod_dvd_prod_of_subset_of_dvd Finsupp.prod_dvd_prod_of_subset_of_dvd
 -/
 
-#print Finsupp.indicator_eq_sum_single /-
-theorem indicator_eq_sum_single [AddCommMonoid M] (s : Finset α) (f : ∀ a ∈ s, M) :
+#print Finsupp.indicator_eq_sum_attach_single /-
+theorem indicator_eq_sum_attach_single [AddCommMonoid M] (s : Finset α) (f : ∀ a ∈ s, M) :
     indicator s f = ∑ x in s.attach, single x (f x x.2) :=
   by
   rw [← sum_single (indicator s f), Sum, sum_subset (support_indicator_subset _ _), ← sum_attach]
   · refine' Finset.sum_congr rfl fun x hx => _
     rw [indicator_of_mem]
   intro i _ hi
   rw [not_mem_support_iff.mp hi, single_zero]
-#align finsupp.indicator_eq_sum_single Finsupp.indicator_eq_sum_single
+#align finsupp.indicator_eq_sum_single Finsupp.indicator_eq_sum_attach_single
 -/
 
-#print Finsupp.prod_indicator_index /-
+#print Finsupp.prod_indicator_index_eq_prod_attach /-
 @[simp, to_additive]
-theorem prod_indicator_index [Zero M] [CommMonoid N] {s : Finset α} (f : ∀ a ∈ s, M) {h : α → M → N}
-    (h_zero : ∀ a ∈ s, h a 0 = 1) : (indicator s f).Prod h = ∏ x in s.attach, h x (f x x.2) :=
+theorem prod_indicator_index_eq_prod_attach [Zero M] [CommMonoid N] {s : Finset α} (f : ∀ a ∈ s, M)
+    {h : α → M → N} (h_zero : ∀ a ∈ s, h a 0 = 1) :
+    (indicator s f).Prod h = ∏ x in s.attach, h x (f x x.2) :=
   by
   rw [prod_of_support_subset _ (support_indicator_subset _ _) h h_zero, ← prod_attach]
   refine' Finset.prod_congr rfl fun x hx => _
   rw [indicator_of_mem]
-#align finsupp.prod_indicator_index Finsupp.prod_indicator_index
-#align finsupp.sum_indicator_index Finsupp.sum_indicator_index
+#align finsupp.prod_indicator_index Finsupp.prod_indicator_index_eq_prod_attach
+#align finsupp.sum_indicator_index Finsupp.sum_indicator_index_eq_sum_attach
 -/
 
 end Finsupp

Mathbin/Analysis/Calculus/Deriv/Basic.lean

@@ -513,11 +513,13 @@ theorem HasDerivWithinAt.union (hs : HasDerivWithinAt f f' s x) (ht : HasDerivWi
 #align has_deriv_within_at.union HasDerivWithinAt.union
 -/
 
-#print HasDerivWithinAt.nhdsWithin /-
-theorem HasDerivWithinAt.nhdsWithin (h : HasDerivWithinAt f f' s x) (ht : s ∈ 𝓝[t] x) :
+/- warning: has_deriv_within_at.nhds_within clashes with has_deriv_within_at.mono_of_mem -> HasDerivWithinAt.mono_of_mem
+Case conversion may be inaccurate. Consider using '#align has_deriv_within_at.nhds_within HasDerivWithinAt.mono_of_memₓ'. -/
+#print HasDerivWithinAt.mono_of_mem /-
+theorem HasDerivWithinAt.mono_of_mem (h : HasDerivWithinAt f f' s x) (ht : s ∈ 𝓝[t] x) :
     HasDerivWithinAt f f' t x :=
   (hasDerivWithinAt_inter' ht).1 (h.mono (inter_subset_right _ _))
-#align has_deriv_within_at.nhds_within HasDerivWithinAt.nhdsWithin
+#align has_deriv_within_at.nhds_within HasDerivWithinAt.mono_of_mem
 -/
 
 #print HasDerivWithinAt.hasDerivAt /-

Mathbin/Analysis/Calculus/Fderiv/Basic.lean

@@ -586,11 +586,13 @@ theorem HasFDerivWithinAt.union (hs : HasFDerivWithinAt f f' s x)
 #align has_fderiv_within_at.union HasFDerivWithinAt.union
 -/
 
-#print HasFDerivWithinAt.nhdsWithin /-
-theorem HasFDerivWithinAt.nhdsWithin (h : HasFDerivWithinAt f f' s x) (ht : s ∈ 𝓝[t] x) :
+/- warning: has_fderiv_within_at.nhds_within clashes with has_fderiv_within_at.mono_of_mem -> HasFDerivWithinAt.mono_of_mem
+Case conversion may be inaccurate. Consider using '#align has_fderiv_within_at.nhds_within HasFDerivWithinAt.mono_of_memₓ'. -/
+#print HasFDerivWithinAt.mono_of_mem /-
+theorem HasFDerivWithinAt.mono_of_mem (h : HasFDerivWithinAt f f' s x) (ht : s ∈ 𝓝[t] x) :
     HasFDerivWithinAt f f' t x :=
   (hasFDerivWithinAt_inter' ht).1 (h.mono (inter_subset_right _ _))
-#align has_fderiv_within_at.nhds_within HasFDerivWithinAt.nhdsWithin
+#align has_fderiv_within_at.nhds_within HasFDerivWithinAt.mono_of_mem
 -/
 
 #print HasFDerivWithinAt.hasFDerivAt /-

Mathbin/Data/Int/Bitwise.lean

@@ -453,30 +453,31 @@ theorem shiftl_sub (m : ℤ) (n : ℕ) (k : ℤ) : shiftl m (n - k) = shiftr (sh
 
 #print Int.shiftl_eq_mul_pow /-
 theorem shiftl_eq_mul_pow : ∀ (m : ℤ) (n : ℕ), shiftl m n = m * ↑(2 ^ n)
-  | (m : ℕ), n => congr_arg coe (Nat.shiftl_eq_mul_pow _ _)
+  | (m : ℕ), n => congr_arg coe (Nat.shiftLeft_eq_mul_pow _ _)
   | -[m+1], n => @congr_arg ℕ ℤ _ _ (fun i => -i) (Nat.shiftl'_tt_eq_mul_pow _ _)
 #align int.shiftl_eq_mul_pow Int.shiftl_eq_mul_pow
 -/
 
 #print Int.shiftr_eq_div_pow /-
 theorem shiftr_eq_div_pow : ∀ (m : ℤ) (n : ℕ), shiftr m n = m / ↑(2 ^ n)
-  | (m : ℕ), n => by rw [shiftr_coe_nat] <;> exact congr_arg coe (Nat.shiftr_eq_div_pow _ _)
-  | -[m+1], n => by
-    rw [shiftr_neg_succ, neg_succ_of_nat_div, Nat.shiftr_eq_div_pow]; rfl
+  | (m : ℕ), n => by rw [shiftr_coe_nat] <;> exact congr_arg coe (Nat.shiftRight_eq_div_pow _ _)
+  | -[m+1], n =>
+    by
+    rw [shiftr_neg_succ, neg_succ_of_nat_div, Nat.shiftRight_eq_div_pow]; rfl
     exact coe_nat_lt_coe_nat_of_lt (pow_pos (by decide) _)
 #align int.shiftr_eq_div_pow Int.shiftr_eq_div_pow
 -/
 
 #print Int.one_shiftl /-
 theorem one_shiftl (n : ℕ) : shiftl 1 n = (2 ^ n : ℕ) :=
-  congr_arg coe (Nat.one_shiftl _)
+  congr_arg coe (Nat.one_shiftLeft _)
 #align int.one_shiftl Int.one_shiftl
 -/
 
 #print Int.zero_shiftl /-
 @[simp]
 theorem zero_shiftl : ∀ n : ℤ, shiftl 0 n = 0
-  | (n : ℕ) => congr_arg coe (Nat.zero_shiftl _)
+  | (n : ℕ) => congr_arg coe (Nat.zero_shiftLeft _)
   | -[n+1] => congr_arg coe (Nat.zero_shiftr _)
 #align int.zero_shiftl Int.zero_shiftl
 -/

Mathbin/Data/Nat/Size.lean

@@ -19,13 +19,13 @@ namespace Nat
 /-! ### `shiftl` and `shiftr` -/
 
 
-#print Nat.shiftl_eq_mul_pow /-
-theorem shiftl_eq_mul_pow (m) : ∀ n, shiftl m n = m * 2 ^ n
+#print Nat.shiftLeft_eq_mul_pow /-
+theorem shiftLeft_eq_mul_pow (m) : ∀ n, shiftl m n = m * 2 ^ n
   | 0 => (Nat.mul_one _).symm
   | k + 1 =>
     show bit0 (shiftl m k) = m * (2 * 2 ^ k) by
       rw [bit0_val, shiftl_eq_mul_pow, mul_left_comm, mul_comm 2]
-#align nat.shiftl_eq_mul_pow Nat.shiftl_eq_mul_pow
+#align nat.shiftl_eq_mul_pow Nat.shiftLeft_eq_mul_pow
 -/
 
 #print Nat.shiftl'_tt_eq_mul_pow /-
@@ -39,34 +39,32 @@ theorem shiftl'_tt_eq_mul_pow (m) : ∀ n, shiftl' true m n + 1 = (m + 1) * 2 ^
 #align nat.shiftl'_tt_eq_mul_pow Nat.shiftl'_tt_eq_mul_pow
 -/
 
-#print Nat.one_shiftl /-
-theorem one_shiftl (n) : shiftl 1 n = 2 ^ n :=
-  (shiftl_eq_mul_pow _ _).trans (Nat.one_mul _)
-#align nat.one_shiftl Nat.one_shiftl
+#print Nat.one_shiftLeft /-
+theorem one_shiftLeft (n) : shiftl 1 n = 2 ^ n :=
+  (shiftLeft_eq_mul_pow _ _).trans (Nat.one_mul _)
+#align nat.one_shiftl Nat.one_shiftLeft
 -/
 
-#print Nat.zero_shiftl /-
+#print Nat.zero_shiftLeft /-
 @[simp]
-theorem zero_shiftl (n) : shiftl 0 n = 0 :=
-  (shiftl_eq_mul_pow _ _).trans (Nat.zero_mul _)
-#align nat.zero_shiftl Nat.zero_shiftl
+theorem zero_shiftLeft (n) : shiftl 0 n = 0 :=
+  (shiftLeft_eq_mul_pow _ _).trans (Nat.zero_mul _)
+#align nat.zero_shiftl Nat.zero_shiftLeft
 -/
 
-#print Nat.shiftr_eq_div_pow /-
-theorem shiftr_eq_div_pow (m) : ∀ n, shiftr m n = m / 2 ^ n
+#print Nat.shiftRight_eq_div_pow /-
+theorem shiftRight_eq_div_pow (m) : ∀ n, shiftr m n = m / 2 ^ n
   | 0 => (Nat.div_one _).symm
   | k + 1 =>
     (congr_arg div2 (shiftr_eq_div_pow k)).trans <| by
       rw [div2_val, Nat.div_div_eq_div_mul, mul_comm] <;> rfl
-#align nat.shiftr_eq_div_pow Nat.shiftr_eq_div_pow
+#align nat.shiftr_eq_div_pow Nat.shiftRight_eq_div_pow
 -/
 
-#print Nat.zero_shiftr /-
 @[simp]
 theorem zero_shiftr (n) : shiftr 0 n = 0 :=
-  (shiftr_eq_div_pow _ _).trans (Nat.zero_div _)
+  (shiftRight_eq_div_pow _ _).trans (Nat.zero_div _)
 #align nat.zero_shiftr Nat.zero_shiftr
--/
 
 #print Nat.shiftl'_ne_zero_left /-
 theorem shiftl'_ne_zero_left (b) {m} (h : m ≠ 0) (n) : shiftl' b m n ≠ 0 := by
@@ -144,11 +142,11 @@ theorem size_shiftl' {b m n} (h : shiftl' b m n ≠ 0) : size (shiftl' b m n) =
 #align nat.size_shiftl' Nat.size_shiftl'
 -/
 
-#print Nat.size_shiftl /-
+#print Nat.size_shiftLeft /-
 @[simp]
-theorem size_shiftl {m} (h : m ≠ 0) (n) : size (shiftl m n) = size m + n :=
+theorem size_shiftLeft {m} (h : m ≠ 0) (n) : size (shiftl m n) = size m + n :=
   size_shiftl' (shiftl'_ne_zero_left _ h _)
-#align nat.size_shiftl Nat.size_shiftl
+#align nat.size_shiftl Nat.size_shiftLeft
 -/
 
 #print Nat.lt_size_self /-

Mathbin/Data/Num/Lemmas.lean

@@ -1197,7 +1197,7 @@ theorem lxor'_to_nat : ∀ m n, (lxor m n : ℕ) = Nat.lxor' m n := by
 @[simp, norm_cast]
 theorem shiftl_to_nat (m n) : (shiftl m n : ℕ) = Nat.shiftl m n :=
   by
-  cases m <;> dsimp only [shiftl]; · symm; apply Nat.zero_shiftl
+  cases m <;> dsimp only [shiftl]; · symm; apply Nat.zero_shiftLeft
   simp; induction' n with n IH; · rfl
   simp [PosNum.shiftl, Nat.shiftl_succ]; rw [← IH]
 #align num.shiftl_to_nat Num.shiftl_to_nat
@@ -1210,7 +1210,7 @@ theorem shiftr_to_nat (m n) : (shiftr m n : ℕ) = Nat.shiftr m n :=
   cases' m with m <;> dsimp only [shiftr]; · symm; apply Nat.zero_shiftr
   induction' n with n IH generalizing m; · cases m <;> rfl
   cases' m with m m <;> dsimp only [PosNum.shiftr]
-  · rw [Nat.shiftr_eq_div_pow]; symm; apply Nat.div_eq_of_lt
+  · rw [Nat.shiftRight_eq_div_pow]; symm; apply Nat.div_eq_of_lt
     exact @Nat.pow_lt_pow_of_lt_right 2 (by decide) 0 (n + 1) (Nat.succ_pos _)
   · trans; apply IH
     change Nat.shiftr m n = Nat.shiftr (bit1 m) (n + 1)

Mathbin/FieldTheory/IsAlgClosed/Basic.lean

@@ -251,41 +251,42 @@ variable (K L M)
 
 open Subalgebra AlgHom Function
 
-#print lift.SubfieldWithHom /-
+#print IsAlgClosed.lift.SubfieldWithHom /-
 /-- This structure is used to prove the existence of a homomorphism from any algebraic extension
 into an algebraic closure -/
-structure SubfieldWithHom where
+structure IsAlgClosed.lift.SubfieldWithHom where
   carrier : Subalgebra K L
   emb : carrier →ₐ[K] M
-#align lift.subfield_with_hom lift.SubfieldWithHom
+#align lift.subfield_with_hom IsAlgClosed.lift.SubfieldWithHom
 -/
 
 variable {K L M hL}
 
 namespace SubfieldWithHom
 
-variable {E₁ E₂ E₃ : SubfieldWithHom K L M hL}
+variable {E₁ E₂ E₃ : IsAlgClosed.lift.SubfieldWithHom K L M hL}
 
-instance : LE (SubfieldWithHom K L M hL)
+instance : LE (IsAlgClosed.lift.SubfieldWithHom K L M hL)
     where le E₁ E₂ := ∃ h : E₁.carrier ≤ E₂.carrier, ∀ x, E₂.emb (inclusion h x) = E₁.emb x
 
-noncomputable instance : Inhabited (SubfieldWithHom K L M hL) :=
+noncomputable instance : Inhabited (IsAlgClosed.lift.SubfieldWithHom K L M hL) :=
   ⟨{  carrier := ⊥
       emb := (Algebra.ofId K M).comp (Algebra.botEquiv K L).toAlgHom }⟩
 
-#print lift.SubfieldWithHom.le_def /-
-theorem le_def : E₁ ≤ E₂ ↔ ∃ h : E₁.carrier ≤ E₂.carrier, ∀ x, E₂.emb (inclusion h x) = E₁.emb x :=
+#print IsAlgClosed.lift.SubfieldWithHom.le_def /-
+theorem IsAlgClosed.lift.SubfieldWithHom.le_def :
+    E₁ ≤ E₂ ↔ ∃ h : E₁.carrier ≤ E₂.carrier, ∀ x, E₂.emb (inclusion h x) = E₁.emb x :=
   Iff.rfl
-#align lift.subfield_with_hom.le_def lift.SubfieldWithHom.le_def
+#align lift.subfield_with_hom.le_def IsAlgClosed.lift.SubfieldWithHom.le_def
 -/
 
-#print lift.SubfieldWithHom.compat /-
-theorem compat (h : E₁ ≤ E₂) : ∀ x, E₂.emb (inclusion h.fst x) = E₁.emb x := by rw [le_def] at h ;
-  cases h; assumption
-#align lift.subfield_with_hom.compat lift.SubfieldWithHom.compat
+#print IsAlgClosed.lift.SubfieldWithHom.compat /-
+theorem IsAlgClosed.lift.SubfieldWithHom.compat (h : E₁ ≤ E₂) :
+    ∀ x, E₂.emb (inclusion h.fst x) = E₁.emb x := by rw [le_def] at h ; cases h; assumption
+#align lift.subfield_with_hom.compat IsAlgClosed.lift.SubfieldWithHom.compat
 -/
 
-instance : Preorder (SubfieldWithHom K L M hL)
+instance : Preorder (IsAlgClosed.lift.SubfieldWithHom K L M hL)
     where
   le := (· ≤ ·)
   le_refl E := ⟨le_rfl, by simp⟩
@@ -295,11 +296,12 @@ instance : Preorder (SubfieldWithHom K L M hL)
 
 open Lattice
 
-#print lift.SubfieldWithHom.maximal_subfieldWithHom_chain_bounded /-
-theorem maximal_subfieldWithHom_chain_bounded (c : Set (SubfieldWithHom K L M hL))
-    (hc : IsChain (· ≤ ·) c) : ∃ ub : SubfieldWithHom K L M hL, ∀ N, N ∈ c → N ≤ ub :=
+#print IsAlgClosed.lift.SubfieldWithHom.maximal_subfieldWithHom_chain_bounded /-
+theorem IsAlgClosed.lift.SubfieldWithHom.maximal_subfieldWithHom_chain_bounded
+    (c : Set (IsAlgClosed.lift.SubfieldWithHom K L M hL)) (hc : IsChain (· ≤ ·) c) :
+    ∃ ub : IsAlgClosed.lift.SubfieldWithHom K L M hL, ∀ N, N ∈ c → N ≤ ub :=
   if hcn : c.Nonempty then
-    let ub : SubfieldWithHom K L M hL :=
+    let ub : IsAlgClosed.lift.SubfieldWithHom K L M hL :=
       haveI : Nonempty c := Set.Nonempty.to_subtype hcn
       { carrier := ⨆ i : c, (i : subfield_with_hom K L M hL).carrier
         emb :=
@@ -318,40 +320,45 @@ theorem maximal_subfieldWithHom_chain_bounded (c : Set (SubfieldWithHom K L M hL
                   inclusion_self, AlgHom.id_apply x])
             _ rfl }
     ⟨ub, fun N hN =>
-      ⟨(le_iSup (fun i : c => (i : SubfieldWithHom K L M hL).carrier) ⟨N, hN⟩ : _),
+      ⟨(le_iSup (fun i : c => (i : IsAlgClosed.lift.SubfieldWithHom K L M hL).carrier) ⟨N, hN⟩ : _),
         by
         intro x
         simp [ub]
         rfl⟩⟩
   else by rw [Set.not_nonempty_iff_eq_empty] at hcn ; simp [hcn]
-#align lift.subfield_with_hom.maximal_subfield_with_hom_chain_bounded lift.SubfieldWithHom.maximal_subfieldWithHom_chain_bounded
+#align lift.subfield_with_hom.maximal_subfield_with_hom_chain_bounded IsAlgClosed.lift.SubfieldWithHom.maximal_subfieldWithHom_chain_bounded
 -/
 
 variable (hL M)
 
-#print lift.SubfieldWithHom.exists_maximal_subfieldWithHom /-
-theorem exists_maximal_subfieldWithHom : ∃ E : SubfieldWithHom K L M hL, ∀ N, E ≤ N → N ≤ E :=
-  exists_maximal_of_chains_bounded maximal_subfieldWithHom_chain_bounded fun _ _ _ => le_trans
-#align lift.subfield_with_hom.exists_maximal_subfield_with_hom lift.SubfieldWithHom.exists_maximal_subfieldWithHom
+#print IsAlgClosed.lift.SubfieldWithHom.exists_maximal_subfieldWithHom /-
+theorem IsAlgClosed.lift.SubfieldWithHom.exists_maximal_subfieldWithHom :
+    ∃ E : IsAlgClosed.lift.SubfieldWithHom K L M hL, ∀ N, E ≤ N → N ≤ E :=
+  exists_maximal_of_chains_bounded
+    IsAlgClosed.lift.SubfieldWithHom.maximal_subfieldWithHom_chain_bounded fun _ _ _ => le_trans
+#align lift.subfield_with_hom.exists_maximal_subfield_with_hom IsAlgClosed.lift.SubfieldWithHom.exists_maximal_subfieldWithHom
 -/
 
-#print lift.SubfieldWithHom.maximalSubfieldWithHom /-
+#print IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom /-
 /-- The maximal `subfield_with_hom`. We later prove that this is equal to `⊤`. -/
-noncomputable def maximalSubfieldWithHom : SubfieldWithHom K L M hL :=
-  Classical.choose (exists_maximal_subfieldWithHom M hL)
-#align lift.subfield_with_hom.maximal_subfield_with_hom lift.SubfieldWithHom.maximalSubfieldWithHom
+noncomputable def IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom :
+    IsAlgClosed.lift.SubfieldWithHom K L M hL :=
+  Classical.choose (IsAlgClosed.lift.SubfieldWithHom.exists_maximal_subfieldWithHom M hL)
+#align lift.subfield_with_hom.maximal_subfield_with_hom IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom
 -/
 
-#print lift.SubfieldWithHom.maximalSubfieldWithHom_is_maximal /-
-theorem maximalSubfieldWithHom_is_maximal :
-    ∀ N : SubfieldWithHom K L M hL,
-      maximalSubfieldWithHom M hL ≤ N → N ≤ maximalSubfieldWithHom M hL :=
-  Classical.choose_spec (exists_maximal_subfieldWithHom M hL)
-#align lift.subfield_with_hom.maximal_subfield_with_hom_is_maximal lift.SubfieldWithHom.maximalSubfieldWithHom_is_maximal
+#print IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom_is_maximal /-
+theorem IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom_is_maximal :
+    ∀ N : IsAlgClosed.lift.SubfieldWithHom K L M hL,
+      IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom M hL ≤ N →
+        N ≤ IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom M hL :=
+  Classical.choose_spec (IsAlgClosed.lift.SubfieldWithHom.exists_maximal_subfieldWithHom M hL)
+#align lift.subfield_with_hom.maximal_subfield_with_hom_is_maximal IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom_is_maximal
 -/
 
-#print lift.SubfieldWithHom.maximalSubfieldWithHom_eq_top /-
-theorem maximalSubfieldWithHom_eq_top : (maximalSubfieldWithHom M hL).carrier = ⊤ :=
+#print IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom_eq_top /-
+theorem IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom_eq_top :
+    (IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom M hL).carrier = ⊤ :=
   by
   rw [eq_top_iff]
   intro x _
@@ -384,7 +391,7 @@ theorem maximalSubfieldWithHom_eq_top : (maximalSubfieldWithHom M hL).carrier =
     simp only [O', restrict_scalars_apply, AlgHom.commutes]
   refine' (maximal_subfield_with_hom_is_maximal M hL O' hO').fst _
   exact Algebra.subset_adjoin (Set.mem_singleton x)
-#align lift.subfield_with_hom.maximal_subfield_with_hom_eq_top lift.SubfieldWithHom.maximalSubfieldWithHom_eq_top
+#align lift.subfield_with_hom.maximal_subfield_with_hom_eq_top IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom_eq_top
 -/
 
 end SubfieldWithHom
@@ -400,8 +407,9 @@ variable (K L M)
 
 /-- Less general version of `lift`. -/
 private noncomputable irreducible_def lift_aux : L →ₐ[K] M :=
-  (lift.SubfieldWithHom.maximalSubfieldWithHom M hL).emb.comp <|
-    Eq.recOn (lift.SubfieldWithHom.maximalSubfieldWithHom_eq_top M hL).symm Algebra.toTop
+  (IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom M hL).emb.comp <|
+    Eq.recOn (IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom_eq_top M hL).symm
+      Algebra.toTop
 
 variable {R : Type u} [CommRing R]
 

Mathbin/Geometry/Manifold/Mfderiv.lean

@@ -585,11 +585,11 @@ theorem HasMFDerivWithinAt.union (hs : HasMFDerivWithinAt I I' f s x f')
 #align has_mfderiv_within_at.union HasMFDerivWithinAt.union
 -/
 
-#print HasMFDerivWithinAt.nhdsWithin /-
-theorem HasMFDerivWithinAt.nhdsWithin (h : HasMFDerivWithinAt I I' f s x f') (ht : s ∈ 𝓝[t] x) :
+#print HasMFDerivWithinAt.mono_of_mem /-
+theorem HasMFDerivWithinAt.mono_of_mem (h : HasMFDerivWithinAt I I' f s x f') (ht : s ∈ 𝓝[t] x) :
     HasMFDerivWithinAt I I' f t x f' :=
   (hasMFDerivWithinAt_inter' ht).1 (h.mono (inter_subset_right _ _))
-#align has_mfderiv_within_at.nhds_within HasMFDerivWithinAt.nhdsWithin
+#align has_mfderiv_within_at.nhds_within HasMFDerivWithinAt.mono_of_mem
 -/
 
 #print HasMFDerivWithinAt.hasMFDerivAt /-

Mathbin/Logic/Relation.lean

@@ -690,10 +690,10 @@ instance : IsRefl α (ReflTransGen r) :=
 instance : IsTrans α (ReflTransGen r) :=
   ⟨@ReflTransGen.trans α r⟩
 
-#print Relation.refl_trans_gen_idem /-
-theorem refl_trans_gen_idem : ReflTransGen (ReflTransGen r) = ReflTransGen r :=
+#print Relation.reflTransGen_idem /-
+theorem reflTransGen_idem : ReflTransGen (ReflTransGen r) = ReflTransGen r :=
   reflTransGen_eq_self reflexive_reflTransGen transitive_reflTransGen
-#align relation.refl_trans_gen_idem Relation.refl_trans_gen_idem
+#align relation.refl_trans_gen_idem Relation.reflTransGen_idem
 -/
 
 #print Relation.ReflTransGen.lift' /-