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

Commit 92ca63f

Browse files
jcommelinurkudkim-em
committed
refactor(tactic/wlog): simplify and speed up wlog (#16495)
Benefits: - The tactic is faster - The tactic is easier to port to Lean 4 Downside: - The tactic doesn't do any heavy-lifting for the user Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/wlog/near/296996966 Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
1 parent bed4f05 commit 92ca63f

48 files changed

Lines changed: 309 additions & 555 deletions

File tree

Some content is hidden

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

‎archive/imo/imo1988_q6.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,8 @@ lemma constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → ℕ
7070
begin
7171
-- First of all, we may assume that x ≤ y.
7272
-- We justify this using H_symm.
73-
wlog hxy : x ≤ y, swap, { rw H_symm at h₀, solve_by_elim },
73+
wlog hxy : x ≤ y,
74+
{ rw H_symm at h₀, apply this y x h₀ B C base _ _ _ _ _ _ (le_of_not_le hxy), assumption' },
7475
-- In fact, we can easily deal with the case x = y.
7576
by_cases x_eq_y : x = y, {subst x_eq_y, exact H_diag h₀},
7677
-- Hence we may assume that x < y.

‎archive/imo/imo2006_q3.lean‎

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -89,17 +89,16 @@ le_of_pow_le_pow _ (mul_nonneg (sqrt_nonneg _) (sq_nonneg _)) nat.succ_pos' $
8989
theorem subst_proof₁ (x y z s : ℝ) (hxyz : x + y + z = 0) :
9090
|x * y * z * s| ≤ sqrt 2 / 32 * (x^2 + y^2 + z^2 + s^2)^2 :=
9191
begin
92-
wlog h' := mul_nonneg_of_three x y z using [x y z, y z x, z x y] tactic.skip,
92+
wlog h' : 0 ≤ x * y generalizing x y z, swap,
9393
{ rw [div_mul_eq_mul_div, le_div_iff' zero_lt_32],
9494
exact subst_wlog h' hxyz },
95-
{ intro h,
96-
rw [add_assoc, add_comm] at h,
97-
rw [mul_assoc x, mul_comm x, add_assoc (x^2), add_comm (x^2)],
98-
exact this h },
99-
{ intro h,
100-
rw [add_comm, ← add_assoc] at h,
101-
rw [mul_comm _ z, ← mul_assoc, add_comm _ (z^2), ← add_assoc],
102-
exact this h }
95+
cases (mul_nonneg_of_three x y z).resolve_left h' with h h,
96+
{ specialize this y z x _ h,
97+
{ rw ← hxyz, ring, },
98+
{ convert this using 2; ring } },
99+
{ specialize this z x y _ h,
100+
{ rw ← hxyz, ring, },
101+
{ convert this using 2; ring } },
103102
end
104103

105104
lemma lhs_identity (a b c : ℝ) :

‎src/algebra/order/hom/ring.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -325,9 +325,9 @@ instance order_ring_hom.subsingleton [linear_ordered_field α] [linear_ordered_f
325325
subsingleton (α →+*o β) :=
326326
⟨λ f g, begin
327327
ext x,
328-
by_contra' h,
329-
wlog h : f x < g x using [f g, g f],
330-
{ exact ne.lt_or_lt h },
328+
by_contra' h' : f x ≠ g x,
329+
wlog h : f x < g x,
330+
{ exact this g f x (ne.symm h') (h'.lt_or_lt.resolve_left h), },
331331
obtain ⟨q, hf, hg⟩ := exists_rat_btwn h,
332332
rw ←map_rat_cast f at hf,
333333
rw ←map_rat_cast g at hg,

‎src/analysis/bounded_variation.lean‎

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -181,10 +181,9 @@ lemma _root_.has_bounded_variation_on.has_locally_bounded_variation_on {f : α
181181
lemma edist_le (f : α → E) {s : set α} {x y : α} (hx : x ∈ s) (hy : y ∈ s) :
182182
edist (f x) (f y) ≤ evariation_on f s :=
183183
begin
184-
wlog hxy : x ≤ y := le_total x y using [x y, y x] tactic.skip, swap,
185-
{ assume hx hy,
186-
rw edist_comm,
187-
exact this hy hx },
184+
wlog hxy : x ≤ y,
185+
{ rw edist_comm,
186+
exact this f hy hx (le_of_not_le hxy) },
188187
let u : ℕ → α := λ n, if n = 0 then x else y,
189188
have hu : monotone u,
190189
{ assume m n hmn,
@@ -798,15 +797,14 @@ lemma edist_zero_of_eq_zero
798797
{a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : variation_on_from_to f s a b = 0) :
799798
edist (f a) (f b) = 0 :=
800799
begin
801-
wlog h' : a ≤ b := le_total a b using [b a, a b] tactic.skip,
800+
wlog h' : a ≤ b,
801+
{ rw edist_comm,
802+
apply this hf hb ha _ (le_of_not_le h'),
803+
rw [eq_neg_swap, h, neg_zero] },
802804
{ apply le_antisymm _ (zero_le _),
803805
rw [←ennreal.of_real_zero, ←h, eq_of_le f s h', ennreal.of_real_to_real (hf a b ha hb)],
804806
apply evariation_on.edist_le,
805807
exacts [⟨ha, ⟨le_rfl, h'⟩⟩, ⟨hb, ⟨h', le_rfl⟩⟩] },
806-
{ assume ha hb hab,
807-
rw edist_comm,
808-
apply this hb ha,
809-
rw [eq_neg_swap, hab, neg_zero] }
810808
end
811809

812810
@[protected]

‎src/analysis/box_integral/partition/filter.lean‎

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -333,14 +333,13 @@ lemma mem_base_set.exists_common_compl (h₁ : l.mem_base_set I c₁ r₁ π₁)
333333
∃ π : prepartition I, π.Union = I \ π₁.Union ∧
334334
(l.bDistortion → π.distortion ≤ c₁) ∧ (l.bDistortion → π.distortion ≤ c₂) :=
335335
begin
336-
wlog hc : c₁ ≤ c₂ := le_total c₁ c₂ using [c₁ c₂ r₁ r₂ π₁ π₂, c₂ c₁ r₂ r₁ π₂ π₁] tactic.skip,
337-
{ by_cases hD : (l.bDistortion : Prop),
338-
{ rcases h₁.4 hD with ⟨π, hπU, hπc⟩,
339-
exact ⟨π, hπU, λ _, hπc, λ _, hπc.trans hc⟩ },
340-
{ exact ⟨π₁.to_prepartition.compl, π₁.to_prepartition.Union_compl,
341-
λ h, (hD h).elim, λ h, (hD h).elim⟩ } },
342-
{ intros h₁ h₂ hU,
343-
simpa [hU, and_comm] using this h₂ h₁ hU.symm }
336+
wlog hc : c₁ ≤ c₂,
337+
{ simpa [hU, and_comm] using this h₂ h₁ hU.symm (le_of_not_le hc) },
338+
by_cases hD : (l.bDistortion : Prop),
339+
{ rcases h₁.4 hD with ⟨π, hπU, hπc⟩,
340+
exact ⟨π, hπU, λ _, hπc, λ _, hπc.trans hc⟩ },
341+
{ exact ⟨π₁.to_prepartition.compl, π₁.to_prepartition.Union_compl,
342+
λ h, (hD h).elim, λ h, (hD h).elim⟩ }
344343
end
345344

346345
protected lemma mem_base_set.union_compl_to_subordinate (hπ₁ : l.mem_base_set I c r₁ π₁)

‎src/analysis/convex/function.lean‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -342,9 +342,10 @@ lemma linear_order.convex_on_of_lt (hs : convex 𝕜 s)
342342
f (a • x + b • y) ≤ a • f x + b • f y) : convex_on 𝕜 s f :=
343343
begin
344344
refine convex_on_iff_pairwise_pos.2 ⟨hs, λ x hx y hy hxy a b ha hb hab, _⟩,
345-
wlog h : x ≤ y using [x y a b, y x b a],
346-
{ exact le_total _ _ },
347-
exact hf hx hy (h.lt_of_ne hxy) ha hb hab,
345+
wlog h : x < y,
346+
{ rw [add_comm (a • x), add_comm (a • f x)], rw add_comm at hab,
347+
refine this hs hf y hy x hx hxy.symm b a hb ha hab (hxy.lt_or_lt.resolve_left h), },
348+
exact hf hx hy h ha hb hab,
348349
end
349350

350351
/-- For a function on a convex set in a linearly ordered space (where the order and the algebraic
@@ -365,9 +366,10 @@ lemma linear_order.strict_convex_on_of_lt (hs : convex 𝕜 s)
365366
f (a • x + b • y) < a • f x + b • f y) : strict_convex_on 𝕜 s f :=
366367
begin
367368
refine ⟨hs, λ x hx y hy hxy a b ha hb hab, _⟩,
368-
wlog h : x ≤ y using [x y a b, y x b a],
369-
{ exact le_total _ _ },
370-
exact hf hx hy (h.lt_of_ne hxy) ha hb hab,
369+
wlog h : x < y,
370+
{ rw [add_comm (a • x), add_comm (a • f x)], rw add_comm at hab,
371+
refine this hs hf y hy x hx hxy.symm b a hb ha hab (hxy.lt_or_lt.resolve_left h), },
372+
exact hf hx hy h ha hb hab,
371373
end
372374

373375
/-- For a function on a convex set in a linearly ordered space (where the order and the algebraic

‎src/analysis/normed_space/ray.lean‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -36,12 +36,12 @@ end
3636
lemma norm_sub (h : same_ray ℝ x y) : ‖x - y‖ = |‖x‖ - ‖y‖| :=
3737
begin
3838
rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩,
39-
wlog hab : b ≤ a := le_total b a using [a b, b a] tactic.skip,
40-
{ rw ← sub_nonneg at hab,
41-
rw [← sub_smul, norm_smul_of_nonneg hab, norm_smul_of_nonneg ha,
42-
norm_smul_of_nonneg hb, ← sub_mul, abs_of_nonneg (mul_nonneg hab (norm_nonneg _))] },
43-
{ intros ha hb hab,
44-
rw [norm_sub_rev, this hb ha hab.symm, abs_sub_comm] }
39+
wlog hab : b ≤ a,
40+
{ rw same_ray_comm at h, rw [norm_sub_rev, abs_sub_comm],
41+
exact this u b a hb ha h (le_of_not_le hab), },
42+
rw ← sub_nonneg at hab,
43+
rw [← sub_smul, norm_smul_of_nonneg hab, norm_smul_of_nonneg ha,
44+
norm_smul_of_nonneg hb, ← sub_mul, abs_of_nonneg (mul_nonneg hab (norm_nonneg _))]
4545
end
4646

4747
lemma norm_smul_eq (h : same_ray ℝ x y) : ‖x‖ • y = ‖y‖ • x :=

‎src/analysis/special_functions/pow.lean‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1783,16 +1783,16 @@ lemma mul_rpow_eq_ite (x y : ℝ≥0∞) (z : ℝ) :
17831783
begin
17841784
rcases eq_or_ne z 0 with rfl|hz, { simp },
17851785
replace hz := hz.lt_or_lt,
1786-
wlog hxy : x ≤ y := le_total x y using [x y, y x] tactic.skip,
1787-
{ rcases eq_or_ne x 0 with rfl|hx0,
1788-
{ induction y using with_top.rec_top_coe; cases hz with hz hz; simp [*, hz.not_lt] },
1789-
rcases eq_or_ne y 0 with rfl|hy0, { exact (hx0 (bot_unique hxy)).elim },
1790-
induction x using with_top.rec_top_coe, { cases hz with hz hz; simp [hz, top_unique hxy] },
1791-
induction y using with_top.rec_top_coe, { cases hz with hz hz; simp * },
1792-
simp only [*, false_and, and_false, false_or, if_false],
1793-
norm_cast at *,
1794-
rw [coe_rpow_of_ne_zero (mul_ne_zero hx0 hy0), nnreal.mul_rpow] },
1795-
{ convert this using 2; simp only [mul_comm, and_comm, or_comm] }
1786+
wlog hxy : x ≤ y,
1787+
{ convert this y x z hz (le_of_not_le hxy) using 2; simp only [mul_comm, and_comm, or_comm], },
1788+
rcases eq_or_ne x 0 with rfl|hx0,
1789+
{ induction y using with_top.rec_top_coe; cases hz with hz hz; simp [*, hz.not_lt] },
1790+
rcases eq_or_ne y 0 with rfl|hy0, { exact (hx0 (bot_unique hxy)).elim },
1791+
induction x using with_top.rec_top_coe, { cases hz with hz hz; simp [hz, top_unique hxy] },
1792+
induction y using with_top.rec_top_coe, { cases hz with hz hz; simp * },
1793+
simp only [*, false_and, and_false, false_or, if_false],
1794+
norm_cast at *,
1795+
rw [coe_rpow_of_ne_zero (mul_ne_zero hx0 hy0), nnreal.mul_rpow]
17961796
end
17971797

17981798
lemma mul_rpow_of_ne_top {x y : ℝ≥0∞} (hx : x ≠ ⊤) (hy : y ≠ ⊤) (z : ℝ) :

‎src/combinatorics/composition.lean‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -341,14 +341,12 @@ lemma disjoint_range {i₁ i₂ : fin c.length} (h : i₁ ≠ i₂) :
341341
disjoint (set.range (c.embedding i₁)) (set.range (c.embedding i₂)) :=
342342
begin
343343
classical,
344-
wlog h' : i₁ ≤ i₂ using i₁ i₂,
345-
swap, exact (this h.symm).symm,
344+
wlog h' : i₁ < i₂, { exact (this c h.symm (h.lt_or_lt.resolve_left h')).symm },
346345
by_contradiction d,
347346
obtain ⟨x, hx₁, hx₂⟩ :
348347
∃ x : fin n, (x ∈ set.range (c.embedding i₁) ∧ x ∈ set.range (c.embedding i₂)) :=
349348
set.not_disjoint_iff.1 d,
350-
have : i₁ < i₂ := lt_of_le_of_ne h' h,
351-
have A : (i₁ : ℕ).succ ≤ i₂ := nat.succ_le_of_lt this,
349+
have A : (i₁ : ℕ).succ ≤ i₂ := nat.succ_le_of_lt h',
352350
apply lt_irrefl (x : ℕ),
353351
calc (x : ℕ) < c.size_up_to (i₁ : ℕ).succ : (c.mem_range_embedding_iff.1 hx₁).2
354352
... ≤ c.size_up_to (i₂ : ℕ) : monotone_sum_take _ A

‎src/computability/DFA.lean‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -77,8 +77,7 @@ lemma eval_from_split [fintype σ] {x : list α} {s t : σ} (hlen : fintype.card
7777
begin
7878
obtain ⟨n, m, hneq, heq⟩ := fintype.exists_ne_map_eq_of_card_lt
7979
(λ n : fin (fintype.card σ + 1), M.eval_from s (x.take n)) (by norm_num),
80-
wlog hle : (n : ℕ) ≤ m using n m,
81-
have hlt : (n : ℕ) < m := (ne.le_iff_lt hneq).mp hle,
80+
wlog hle : (n : ℕ) ≤ m, { exact this hlen hx _ _ hneq.symm heq.symm (le_of_not_le hle), },
8281
have hm : (m : ℕ) ≤ fintype.card σ := fin.is_le m,
8382
dsimp at heq,
8483

0 commit comments

Comments
 (0)