Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit c8ab806

Browse files
digama0digama0
committed
feat(tactic/alias.lean): use current namespace in alias (#14961)
This makes `alias foo <- bar` use the current namespace to resolve the new alias name `bar`, for consistency with `def bar := foo` and leanprover-community/mathlib4#293.
1 parent 5de765c commit c8ab806

75 files changed

Lines changed: 241 additions & 239 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎scripts/nolints.txt‎

Lines changed: 1 addition & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -533,15 +533,6 @@ apply_nolint tactic.abel.term doc_blame
533533
apply_nolint tactic.abel.termg doc_blame
534534
apply_nolint tactic.interactive.abel.mode doc_blame
535535

536-
-- tactic/alias.lean
537-
apply_nolint tactic.alias.alias_attr doc_blame
538-
apply_nolint tactic.alias.alias_direct doc_blame
539-
apply_nolint tactic.alias.alias_iff doc_blame
540-
apply_nolint tactic.alias.get_alias_target doc_blame
541-
apply_nolint tactic.alias.get_lambda_body doc_blame
542-
apply_nolint tactic.alias.make_left_right doc_blame
543-
apply_nolint tactic.alias.mk_iff_mp_app doc_blame
544-
545536
-- tactic/chain.lean
546537
apply_nolint tactic.abstract_if_success doc_blame
547538
apply_nolint tactic.chain doc_blame
@@ -1036,4 +1027,4 @@ apply_nolint Cauchy.gen doc_blame
10361027
apply_nolint uniform_space.completion.completion_separation_quotient_equiv doc_blame
10371028
apply_nolint uniform_space.completion.cpkg doc_blame
10381029
apply_nolint uniform_space.completion.extension₂ doc_blame
1039-
apply_nolint uniform_space.completion.map₂ doc_blame
1030+
apply_nolint uniform_space.completion.map₂ doc_blame

‎src/algebra/group_power/lemmas.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -520,24 +520,24 @@ end linear_ordered_ring
520520

521521
namespace int
522522

523-
alias int.units_sq ← int.units_pow_two
523+
alias units_sq ← units_pow_two
524524

525525
lemma units_pow_eq_pow_mod_two (u : ℤˣ) (n : ℕ) : u ^ n = u ^ (n % 2) :=
526526
by conv {to_lhs, rw ← nat.mod_add_div n 2}; rw [pow_add, pow_mul, units_sq, one_pow, mul_one]
527527

528528
@[simp] lemma nat_abs_sq (x : ℤ) : (x.nat_abs ^ 2 : ℤ) = x ^ 2 :=
529529
by rw [sq, int.nat_abs_mul_self', sq]
530530

531-
alias int.nat_abs_sq ← int.nat_abs_pow_two
531+
alias nat_abs_sq ← nat_abs_pow_two
532532

533533
lemma abs_le_self_sq (a : ℤ) : (int.nat_abs a : ℤ) ≤ a ^ 2 :=
534534
by { rw [← int.nat_abs_sq a, sq], norm_cast, apply nat.le_mul_self }
535535

536-
alias int.abs_le_self_sq ← int.abs_le_self_pow_two
536+
alias abs_le_self_sq ← abs_le_self_pow_two
537537

538538
lemma le_self_sq (b : ℤ) : b ≤ b ^ 2 := le_trans (le_nat_abs) (abs_le_self_sq _)
539539

540-
alias int.le_self_sq ← int.le_self_pow_two
540+
alias le_self_sq ← le_self_pow_two
541541

542542
lemma pow_right_injective {x : ℤ} (h : 1 < x.nat_abs) : function.injective ((^) x : ℕ → ℤ) :=
543543
begin

‎src/analysis/asymptotics/asymptotics.lean‎

Lines changed: 22 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ def is_O_with (c : ℝ) (l : filter α) (f : α → E) (g : α → F) : Prop :=
7878
/-- Definition of `is_O_with`. We record it in a lemma as `is_O_with` is irreducible. -/
7979
lemma is_O_with_iff : is_O_with c l f g ↔ ∀ᶠ x in l, ∥f x∥ ≤ c * ∥g x∥ := by rw is_O_with
8080

81-
alias is_O_with_iff ↔ asymptotics.is_O_with.bound asymptotics.is_O_with.of_bound
81+
alias is_O_with_iff ↔ is_O_with.bound is_O_with.of_bound
8282

8383
/-- The Landau notation `f =O[l] g` where `f` and `g` are two functions on a type `α` and `l` is
8484
a filter on `α`, means that eventually for `l`, `∥f∥` is bounded by a constant multiple of `∥g∥`.
@@ -116,14 +116,14 @@ notation f ` =o[`:100 l `] ` g:100 := is_o l f g
116116
`is_o` to be irreducible at the end of this file. -/
117117
lemma is_o_iff_forall_is_O_with : f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → is_O_with c l f g := by rw is_o
118118

119-
alias is_o_iff_forall_is_O_with ↔ asymptotics.is_o.forall_is_O_with asymptotics.is_o.of_is_O_with
119+
alias is_o_iff_forall_is_O_with ↔ is_o.forall_is_O_with is_o.of_is_O_with
120120

121121
/-- Definition of `is_o` in terms of filters. We record it in a lemma as we will set
122122
`is_o` to be irreducible at the end of this file. -/
123123
lemma is_o_iff : f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ x in l, ∥f x∥ ≤ c * ∥g x∥ :=
124124
by simp only [is_o, is_O_with]
125125

126-
alias is_o_iff ↔ asymptotics.is_o.bound asymptotics.is_o.of_bound
126+
alias is_o_iff ↔ is_o.bound is_o.of_bound
127127

128128
lemma is_o.def (h : f =o[l] g) (hc : 0 < c) : ∀ᶠ x in l, ∥f x∥ ≤ c * ∥g x∥ :=
129129
is_o_iff.1 h hc
@@ -425,79 +425,79 @@ is_o.of_is_O_with $ λ c cpos, (h.forall_is_O_with cpos).sup (h'.forall_is_O_wit
425425
@[simp] theorem is_O_with_norm_right : is_O_with c l f (λ x, ∥g' x∥) ↔ is_O_with c l f g' :=
426426
by simp only [is_O_with, norm_norm]
427427

428-
alias is_O_with_norm_right ↔ asymptotics.is_O_with.of_norm_right asymptotics.is_O_with.norm_right
428+
alias is_O_with_norm_right ↔ is_O_with.of_norm_right is_O_with.norm_right
429429

430430
@[simp] theorem is_O_norm_right : f =O[l] (λ x, ∥g' x∥) ↔ f =O[l] g' :=
431431
by { unfold is_O, exact exists_congr (λ _, is_O_with_norm_right) }
432432

433-
alias is_O_norm_right ↔ asymptotics.is_O.of_norm_right asymptotics.is_O.norm_right
433+
alias is_O_norm_right ↔ is_O.of_norm_right is_O.norm_right
434434

435435
@[simp] theorem is_o_norm_right : f =o[l] (λ x, ∥g' x∥) ↔ f =o[l] g' :=
436436
by { unfold is_o, exact forall₂_congr (λ _ _, is_O_with_norm_right) }
437437

438-
alias is_o_norm_right ↔ asymptotics.is_o.of_norm_right asymptotics.is_o.norm_right
438+
alias is_o_norm_right ↔ is_o.of_norm_right is_o.norm_right
439439

440440
@[simp] theorem is_O_with_norm_left : is_O_with c l (λ x, ∥f' x∥) g ↔ is_O_with c l f' g :=
441441
by simp only [is_O_with, norm_norm]
442442

443-
alias is_O_with_norm_left ↔ asymptotics.is_O_with.of_norm_left asymptotics.is_O_with.norm_left
443+
alias is_O_with_norm_left ↔ is_O_with.of_norm_left is_O_with.norm_left
444444

445445
@[simp] theorem is_O_norm_left : (λ x, ∥f' x∥) =O[l] g ↔ f' =O[l] g :=
446446
by { unfold is_O, exact exists_congr (λ _, is_O_with_norm_left) }
447447

448-
alias is_O_norm_left ↔ asymptotics.is_O.of_norm_left asymptotics.is_O.norm_left
448+
alias is_O_norm_left ↔ is_O.of_norm_left is_O.norm_left
449449

450450
@[simp] theorem is_o_norm_left : (λ x, ∥f' x∥) =o[l] g ↔ f' =o[l] g :=
451451
by { unfold is_o, exact forall₂_congr (λ _ _, is_O_with_norm_left) }
452452

453-
alias is_o_norm_left ↔ asymptotics.is_o.of_norm_left asymptotics.is_o.norm_left
453+
alias is_o_norm_left ↔ is_o.of_norm_left is_o.norm_left
454454

455455
theorem is_O_with_norm_norm : is_O_with c l (λ x, ∥f' x∥) (λ x, ∥g' x∥) ↔ is_O_with c l f' g' :=
456456
is_O_with_norm_left.trans is_O_with_norm_right
457457

458-
alias is_O_with_norm_norm ↔ asymptotics.is_O_with.of_norm_norm asymptotics.is_O_with.norm_norm
458+
alias is_O_with_norm_norm ↔ is_O_with.of_norm_norm is_O_with.norm_norm
459459

460460
theorem is_O_norm_norm : (λ x, ∥f' x∥) =O[l] (λ x, ∥g' x∥) ↔ f' =O[l] g' :=
461461
is_O_norm_left.trans is_O_norm_right
462462

463-
alias is_O_norm_norm ↔ asymptotics.is_O.of_norm_norm asymptotics.is_O.norm_norm
463+
alias is_O_norm_norm ↔ is_O.of_norm_norm is_O.norm_norm
464464

465465
theorem is_o_norm_norm : (λ x, ∥f' x∥) =o[l] (λ x, ∥g' x∥) ↔ f' =o[l] g' :=
466466
is_o_norm_left.trans is_o_norm_right
467467

468-
alias is_o_norm_norm ↔ asymptotics.is_o.of_norm_norm asymptotics.is_o.norm_norm
468+
alias is_o_norm_norm ↔ is_o.of_norm_norm is_o.norm_norm
469469

470470
/-! ### Simplification: negate -/
471471

472472
@[simp] theorem is_O_with_neg_right : is_O_with c l f (λ x, -(g' x)) ↔ is_O_with c l f g' :=
473473
by simp only [is_O_with, norm_neg]
474474

475-
alias is_O_with_neg_right ↔ asymptotics.is_O_with.of_neg_right asymptotics.is_O_with.neg_right
475+
alias is_O_with_neg_right ↔ is_O_with.of_neg_right is_O_with.neg_right
476476

477477
@[simp] theorem is_O_neg_right : f =O[l] (λ x, -(g' x)) ↔ f =O[l] g' :=
478478
by { unfold is_O, exact exists_congr (λ _, is_O_with_neg_right) }
479479

480-
alias is_O_neg_right ↔ asymptotics.is_O.of_neg_right asymptotics.is_O.neg_right
480+
alias is_O_neg_right ↔ is_O.of_neg_right is_O.neg_right
481481

482482
@[simp] theorem is_o_neg_right : f =o[l] (λ x, -(g' x)) ↔ f =o[l] g' :=
483483
by { unfold is_o, exact forall₂_congr (λ _ _, is_O_with_neg_right) }
484484

485-
alias is_o_neg_right ↔ asymptotics.is_o.of_neg_right asymptotics.is_o.neg_right
485+
alias is_o_neg_right ↔ is_o.of_neg_right is_o.neg_right
486486

487487
@[simp] theorem is_O_with_neg_left : is_O_with c l (λ x, -(f' x)) g ↔ is_O_with c l f' g :=
488488
by simp only [is_O_with, norm_neg]
489489

490-
alias is_O_with_neg_left ↔ asymptotics.is_O_with.of_neg_left asymptotics.is_O_with.neg_left
490+
alias is_O_with_neg_left ↔ is_O_with.of_neg_left is_O_with.neg_left
491491

492492
@[simp] theorem is_O_neg_left : (λ x, -(f' x)) =O[l] g ↔ f' =O[l] g :=
493493
by { unfold is_O, exact exists_congr (λ _, is_O_with_neg_left) }
494494

495-
alias is_O_neg_left ↔ asymptotics.is_O.of_neg_left asymptotics.is_O.neg_left
495+
alias is_O_neg_left ↔ is_O.of_neg_left is_O.neg_left
496496

497497
@[simp] theorem is_o_neg_left : (λ x, -(f' x)) =o[l] g ↔ f' =o[l] g :=
498498
by { unfold is_o, exact forall₂_congr (λ _ _, is_O_with_neg_left) }
499499

500-
alias is_o_neg_left ↔ asymptotics.is_o.of_neg_right asymptotics.is_o.neg_left
500+
alias is_o_neg_left ↔ is_o.of_neg_right is_o.neg_left
501501

502502
/-! ### Product of functions (right) -/
503503

@@ -1223,8 +1223,8 @@ theorem is_o_iff_tendsto {f g : α → 𝕜} (hgf : ∀ x, g x = 0 → f x = 0)
12231223
f =o[l] g ↔ tendsto (λ x, f x / (g x)) l (𝓝 0) :=
12241224
is_o_iff_tendsto' (eventually_of_forall hgf)
12251225

1226-
alias is_o_iff_tendsto' ↔ _ asymptotics.is_o_of_tendsto'
1227-
alias is_o_iff_tendsto ↔ _ asymptotics.is_o_of_tendsto
1226+
alias is_o_iff_tendsto' ↔ _ is_o_of_tendsto'
1227+
alias is_o_iff_tendsto ↔ _ is_o_of_tendsto
12281228

12291229
lemma is_o_const_left_of_ne {c : E''} (hc : c ≠ 0) :
12301230
(λ x, c) =o[l] g ↔ tendsto (norm ∘ g) l at_top :=
@@ -1339,7 +1339,7 @@ begin
13391339
exact is_O_iff_is_O_with.2 ⟨c, is_O_with_of_eq_mul φ hφ huvφ⟩ }
13401340
end
13411341

1342-
alias is_O_iff_exists_eq_mul ↔ asymptotics.is_O.exists_eq_mul _
1342+
alias is_O_iff_exists_eq_mul ↔ is_O.exists_eq_mul _
13431343

13441344
lemma is_o_iff_exists_eq_mul :
13451345
u =o[l] v ↔ ∃ (φ : α → 𝕜) (hφ : tendsto φ l (𝓝 0)), u =ᶠ[l] φ * v :=
@@ -1351,7 +1351,7 @@ begin
13511351
exact is_O_with_of_eq_mul _ ((hφ c hpos).mono $ λ x, le_of_lt) huvφ }
13521352
end
13531353

1354-
alias is_o_iff_exists_eq_mul ↔ asymptotics.is_o.exists_eq_mul _
1354+
alias is_o_iff_exists_eq_mul ↔ is_o.exists_eq_mul _
13551355

13561356
end exists_mul_eq
13571357

‎src/analysis/asymptotics/theta.lean‎

Lines changed: 6 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -77,8 +77,8 @@ h₁.1.trans_is_o h₂
7777
@[simp] lemma is_Theta_norm_left : (λ x, ∥f' x∥) =Θ[l] g ↔ f' =Θ[l] g := by simp [is_Theta]
7878
@[simp] lemma is_Theta_norm_right : f =Θ[l] (λ x, ∥g' x∥) ↔ f =Θ[l] g' := by simp [is_Theta]
7979

80-
alias is_Theta_norm_left ↔ asymptotics.is_Theta.of_norm_left asymptotics.is_Theta.norm_left
81-
alias is_Theta_norm_right ↔ asymptotics.is_Theta.of_norm_right asymptotics.is_Theta.norm_right
80+
alias is_Theta_norm_left ↔ is_Theta.of_norm_left is_Theta.norm_left
81+
alias is_Theta_norm_right ↔ is_Theta.of_norm_right is_Theta.norm_right
8282

8383
lemma is_Theta_of_norm_eventually_eq (h : (λ x, ∥f x∥) =ᶠ[l] (λ x, ∥g x∥)) : f =Θ[l] g :=
8484
⟨is_O.of_bound 1 $ by simpa only [one_mul] using h.le,
@@ -171,28 +171,24 @@ lemma is_Theta_const_smul_left [normed_space 𝕜 E'] {c : 𝕜} (hc : c ≠ 0)
171171
(λ x, c • f' x) =Θ[l] g ↔ f' =Θ[l] g :=
172172
and_congr (is_O_const_smul_left hc) (is_O_const_smul_right hc)
173173

174-
alias is_Theta_const_smul_left ↔ asymptotics.is_Theta.of_const_smul_left
175-
asymptotics.is_Theta.const_smul_left
174+
alias is_Theta_const_smul_left ↔ is_Theta.of_const_smul_left is_Theta.const_smul_left
176175

177176
lemma is_Theta_const_smul_right [normed_space 𝕜 F'] {c : 𝕜} (hc : c ≠ 0) :
178177
f =Θ[l] (λ x, c • g' x) ↔ f =Θ[l] g' :=
179178
and_congr (is_O_const_smul_right hc) (is_O_const_smul_left hc)
180179

181-
alias is_Theta_const_smul_right ↔ asymptotics.is_Theta.of_const_smul_right
182-
asymptotics.is_Theta.const_smul_right
180+
alias is_Theta_const_smul_right ↔ is_Theta.of_const_smul_right is_Theta.const_smul_right
183181

184182
lemma is_Theta_const_mul_left {c : 𝕜} {f : α → 𝕜} (hc : c ≠ 0) :
185183
(λ x, c * f x) =Θ[l] g ↔ f =Θ[l] g :=
186184
by simpa only [← smul_eq_mul] using is_Theta_const_smul_left hc
187185

188-
alias is_Theta_const_mul_left ↔ asymptotics.is_Theta.of_const_mul_left
189-
asymptotics.is_Theta.const_mul_left
186+
alias is_Theta_const_mul_left ↔ is_Theta.of_const_mul_left is_Theta.const_mul_left
190187

191188
lemma is_Theta_const_mul_right {c : 𝕜} {g : α → 𝕜} (hc : c ≠ 0) :
192189
f =Θ[l] (λ x, c * g x) ↔ f =Θ[l] g :=
193190
by simpa only [← smul_eq_mul] using is_Theta_const_smul_right hc
194191

195-
alias is_Theta_const_mul_right ↔ asymptotics.is_Theta.of_const_mul_right
196-
asymptotics.is_Theta.const_mul_right
192+
alias is_Theta_const_mul_right ↔ is_Theta.of_const_mul_right is_Theta.const_mul_right
197193

198194
end asymptotics

‎src/analysis/calculus/implicit.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -391,7 +391,7 @@ begin
391391
exact h₁.prod_mk_nhds h₂
392392
end
393393

394-
alias tendsto_implicit_function ← filter.tendsto.implicit_function
394+
alias tendsto_implicit_function ← _root_.filter.tendsto.implicit_function
395395

396396
/-- `implicit_function` sends `(z, y)` to a point in `f ⁻¹' z`. -/
397397
lemma map_implicit_function_eq (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ⊤) :

‎src/analysis/calculus/inverse.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -141,7 +141,7 @@ begin
141141
end
142142

143143
alias approximates_linear_on_iff_lipschitz_on_with ↔
144-
approximates_linear_on.lipschitz_on_with lipschitz_on_with.approximates_linear_on
144+
lipschitz_on_with _root_.lipschitz_on_with.approximates_linear_on
145145

146146
lemma lipschitz_sub (hf : approximates_linear_on f f' s c) :
147147
lipschitz_with c (λ x : s, f x - f' x) :=

‎src/analysis/normed/group/hom.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -237,8 +237,8 @@ lemma mk_normed_group_hom_norm_le' (f : V₁ →+ V₂) {C : ℝ} (h : ∀x, ∥
237237
op_norm_le_bound _ (le_max_right _ _) $ λ x, (h x).trans $
238238
mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg x)
239239

240-
alias mk_normed_group_hom_norm_le ← add_monoid_hom.mk_normed_group_hom_norm_le
241-
alias mk_normed_group_hom_norm_le' ← add_monoid_hom.mk_normed_group_hom_norm_le'
240+
alias mk_normed_group_hom_norm_le ← _root_.add_monoid_hom.mk_normed_group_hom_norm_le
241+
alias mk_normed_group_hom_norm_le' ← _root_.add_monoid_hom.mk_normed_group_hom_norm_le'
242242

243243
/-! ### Addition of normed group homs -/
244244

‎src/analysis/special_functions/complex/log.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,7 @@ begin
100100
{ push_neg at hne, simp [preimage, hne] } }
101101
end
102102

103-
alias countable_preimage_exp ↔ _ set.countable.preimage_cexp
103+
alias countable_preimage_exp ↔ _ _root_.set.countable.preimage_cexp
104104

105105
lemma tendsto_log_nhds_within_im_neg_of_re_neg_of_im_zero
106106
{z : ℂ} (hre : z.re < 0) (him : z.im = 0) :

‎src/category_theory/category/Bipointed.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ def of {X : Type*} (to_prod : X × X) : Bipointed := ⟨X, to_prod⟩
3636

3737
@[simp] lemma coe_of {X : Type*} (to_prod : X × X) : ↥(of to_prod) = X := rfl
3838

39-
alias of ← prod.Bipointed
39+
alias of ← _root_.prod.Bipointed
4040

4141
instance : inhabited Bipointed := ⟨of ((), ())⟩
4242

‎src/category_theory/category/Pointed.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ def of {X : Type*} (point : X) : Pointed := ⟨X, point⟩
3737

3838
@[simp] lemma coe_of {X : Type*} (point : X) : ↥(of point) = X := rfl
3939

40-
alias of ← prod.Pointed
40+
alias of ← _root_.prod.Pointed
4141

4242
instance : inhabited Pointed := ⟨of ((), ())⟩
4343

0 commit comments

Comments
 (0)