[Merged by Bors] - refactor(tactic/wlog): simplify and speed up wlog

archive/imo/imo1988_q6.lean

@@ -70,7 +70,8 @@ lemma constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → ℕ
 begin
   -- First of all, we may assume that x ≤ y.
   -- We justify this using H_symm.
-  wlog hxy : x ≤ y, swap, { rw H_symm at h₀, solve_by_elim },
+  wlog hxy : x ≤ y,
+  { rw H_symm at h₀, apply this y x h₀ B C base _ _ _ _ _ _ (le_of_not_le hxy), assumption' },
   -- In fact, we can easily deal with the case x = y.
   by_cases x_eq_y : x = y, {subst x_eq_y, exact H_diag h₀},
   -- Hence we may assume that x < y.

archive/imo/imo2006_q3.lean

@@ -89,17 +89,16 @@ le_of_pow_le_pow _ (mul_nonneg (sqrt_nonneg _) (sq_nonneg _)) nat.succ_pos' $
 theorem subst_proof₁ (x y z s : ℝ) (hxyz : x + y + z = 0) :
   |x * y * z * s| ≤ sqrt 2 / 32 * (x^2 + y^2 + z^2 + s^2)^2 :=
 begin
-  wlog h' := mul_nonneg_of_three x y z using [x y z, y z x, z x y] tactic.skip,
+  wlog h' : 0 ≤ x * y generalizing x y z, swap,
   { rw [div_mul_eq_mul_div, le_div_iff' zero_lt_32],
     exact subst_wlog h' hxyz },
-  { intro h,
-    rw [add_assoc, add_comm] at h,
-    rw [mul_assoc x, mul_comm x, add_assoc (x^2), add_comm (x^2)],
-    exact this h },
-  { intro h,
-    rw [add_comm, ← add_assoc] at h,
-    rw [mul_comm _ z, ← mul_assoc, add_comm _ (z^2), ← add_assoc],
-    exact this h }
+  cases (mul_nonneg_of_three x y z).resolve_left h' with h h,
+  { specialize this y z x _ h,
+    { rw ← hxyz, ring, },
+    { convert this using 2; ring } },
+  { specialize this z x y _ h,
+    { rw ← hxyz, ring, },
+    { convert this using 2; ring } },
 end
 
 lemma lhs_identity (a b c : ℝ) :

src/algebra/order/hom/ring.lean

@@ -325,9 +325,9 @@ instance order_ring_hom.subsingleton [linear_ordered_field α] [linear_ordered_f
   subsingleton (α →+*o β) :=
 ⟨λ f g, begin
   ext x,
-  by_contra' h,
-  wlog h : f x < g x using [f g, g f],
-  { exact ne.lt_or_lt h },
+  by_contra' h' : f x ≠ g x,
+  wlog h : f x < g x,
+  { exact this g f x (ne.symm h') (h'.lt_or_lt.resolve_left h), },
   obtain ⟨q, hf, hg⟩ := exists_rat_btwn h,
   rw ←map_rat_cast f at hf,
   rw ←map_rat_cast g at hg,

src/analysis/bounded_variation.lean

@@ -181,10 +181,9 @@ lemma _root_.has_bounded_variation_on.has_locally_bounded_variation_on {f : α 
 lemma edist_le (f : α → E) {s : set α} {x y : α} (hx : x ∈ s) (hy : y ∈ s) :
   edist (f x) (f y) ≤ evariation_on f s :=
 begin
-  wlog hxy : x ≤ y := le_total x y using [x y, y x] tactic.skip, swap,
-  { assume hx hy,
-    rw edist_comm,
-    exact this hy hx },
+  wlog hxy : x ≤ y,
+  { rw edist_comm,
+    exact this f hy hx (le_of_not_le hxy) },
   let u : ℕ → α := λ n, if n = 0 then x else y,
   have hu : monotone u,
   { assume m n hmn,
@@ -798,15 +797,14 @@ lemma edist_zero_of_eq_zero
   {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : variation_on_from_to f s a b = 0) :
   edist (f a) (f b) = 0 :=
 begin
-  wlog h' : a ≤ b := le_total a b using [b a, a b] tactic.skip,
+  wlog h' : a ≤ b,
+  { rw edist_comm,
+    apply this hf hb ha _ (le_of_not_le h'),
+    rw [eq_neg_swap, h, neg_zero] },
   { apply le_antisymm _ (zero_le _),
     rw [←ennreal.of_real_zero, ←h, eq_of_le f s h', ennreal.of_real_to_real (hf a b ha hb)],
     apply evariation_on.edist_le,
     exacts [⟨ha, ⟨le_rfl, h'⟩⟩, ⟨hb, ⟨h', le_rfl⟩⟩] },
-  { assume ha hb hab,
-    rw edist_comm,
-    apply this hb ha,
-    rw [eq_neg_swap, hab, neg_zero] }
 end
 
 @[protected]

src/analysis/box_integral/partition/filter.lean

@@ -333,14 +333,13 @@ lemma mem_base_set.exists_common_compl (h₁ : l.mem_base_set I c₁ r₁ π₁)
   ∃ π : prepartition I, π.Union = I \ π₁.Union ∧
     (l.bDistortion → π.distortion ≤ c₁) ∧ (l.bDistortion → π.distortion ≤ c₂) :=
 begin
-  wlog hc : c₁ ≤ c₂ := le_total c₁ c₂ using [c₁ c₂ r₁ r₂ π₁ π₂, c₂ c₁ r₂ r₁ π₂ π₁] tactic.skip,
-  { by_cases hD : (l.bDistortion : Prop),
-    { rcases h₁.4 hD with ⟨π, hπU, hπc⟩,
-      exact ⟨π, hπU, λ _, hπc, λ _, hπc.trans hc⟩ },
-    { exact ⟨π₁.to_prepartition.compl, π₁.to_prepartition.Union_compl,
-        λ h, (hD h).elim, λ h, (hD h).elim⟩ } },
-  { intros h₁ h₂ hU,
-    simpa [hU, and_comm] using this h₂ h₁ hU.symm }
+  wlog hc : c₁ ≤ c₂,
+  { simpa [hU, and_comm] using this h₂ h₁ hU.symm (le_of_not_le hc) },
+  by_cases hD : (l.bDistortion : Prop),
+  { rcases h₁.4 hD with ⟨π, hπU, hπc⟩,
+    exact ⟨π, hπU, λ _, hπc, λ _, hπc.trans hc⟩ },
+  { exact ⟨π₁.to_prepartition.compl, π₁.to_prepartition.Union_compl,
+      λ h, (hD h).elim, λ h, (hD h).elim⟩ }
 end
 
 protected lemma mem_base_set.union_compl_to_subordinate (hπ₁ : l.mem_base_set I c r₁ π₁)

src/analysis/convex/function.lean

@@ -342,9 +342,10 @@ lemma linear_order.convex_on_of_lt (hs : convex 𝕜 s)
     f (a • x + b • y) ≤ a • f x + b • f y) : convex_on 𝕜 s f :=
 begin
   refine convex_on_iff_pairwise_pos.2 ⟨hs, λ x hx y hy hxy a b ha hb hab, _⟩,
-  wlog h : x ≤ y using [x y a b, y x b a],
-  { exact le_total _ _ },
-  exact hf hx hy (h.lt_of_ne hxy) ha hb hab,
+  wlog h : x < y,
+  { rw [add_comm (a • x), add_comm (a • f x)], rw add_comm at hab,
+    refine this hs hf y hy x hx hxy.symm b a hb ha hab (hxy.lt_or_lt.resolve_left h), },
+  exact hf hx hy h ha hb hab,
 end
 
 /-- 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)
     f (a • x + b • y) < a • f x + b • f y) : strict_convex_on 𝕜 s f :=
 begin
   refine ⟨hs, λ x hx y hy hxy a b ha hb hab, _⟩,
-  wlog h : x ≤ y using [x y a b, y x b a],
-  { exact le_total _ _ },
-  exact hf hx hy (h.lt_of_ne hxy) ha hb hab,
+  wlog h : x < y,
+  { rw [add_comm (a • x), add_comm (a • f x)], rw add_comm at hab,
+    refine this hs hf y hy x hx hxy.symm b a hb ha hab (hxy.lt_or_lt.resolve_left h), },
+  exact hf hx hy h ha hb hab,
 end
 
 /-- For a function on a convex set in a linearly ordered space (where the order and the algebraic

src/analysis/normed_space/ray.lean

@@ -36,12 +36,12 @@ end
 lemma norm_sub (h : same_ray ℝ x y) : ‖x - y‖ = |‖x‖ - ‖y‖| :=
 begin
   rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩,
-  wlog hab : b ≤ a := le_total b a using [a b, b a] tactic.skip,
-  { rw ← sub_nonneg at hab,
-    rw [← sub_smul, norm_smul_of_nonneg hab, norm_smul_of_nonneg ha,
-      norm_smul_of_nonneg hb, ← sub_mul, abs_of_nonneg (mul_nonneg hab (norm_nonneg _))] },
-  { intros ha hb hab,
-    rw [norm_sub_rev, this hb ha hab.symm, abs_sub_comm] }
+  wlog hab : b ≤ a,
+  { rw same_ray_comm at h, rw [norm_sub_rev, abs_sub_comm],
+    exact this u b a hb ha h (le_of_not_le hab), },
+  rw ← sub_nonneg at hab,
+  rw [← sub_smul, norm_smul_of_nonneg hab, norm_smul_of_nonneg ha,
+    norm_smul_of_nonneg hb, ← sub_mul, abs_of_nonneg (mul_nonneg hab (norm_nonneg _))]
 end
 
 lemma norm_smul_eq (h : same_ray ℝ x y) : ‖x‖ • y = ‖y‖ • x :=

src/analysis/special_functions/pow.lean

@@ -1783,16 +1783,16 @@ lemma mul_rpow_eq_ite (x y : ℝ≥0∞) (z : ℝ) :
 begin
   rcases eq_or_ne z 0 with rfl|hz, { simp },
   replace hz := hz.lt_or_lt,
-  wlog hxy : x ≤ y := le_total x y using [x y, y x] tactic.skip,
-  { rcases eq_or_ne x 0 with rfl|hx0,
-    { induction y using with_top.rec_top_coe; cases hz with hz hz; simp [*, hz.not_lt] },
-    rcases eq_or_ne y 0 with rfl|hy0, { exact (hx0 (bot_unique hxy)).elim },
-    induction x using with_top.rec_top_coe, { cases hz with hz hz; simp [hz, top_unique hxy] },
-    induction y using with_top.rec_top_coe, { cases hz with hz hz; simp * },
-    simp only [*, false_and, and_false, false_or, if_false],
-    norm_cast at *,
-    rw [coe_rpow_of_ne_zero (mul_ne_zero hx0 hy0), nnreal.mul_rpow] },
-  { convert this using 2; simp only [mul_comm, and_comm, or_comm] }
+  wlog hxy : x ≤ y,
+  { convert this y x z hz (le_of_not_le hxy) using 2; simp only [mul_comm, and_comm, or_comm], },
+  rcases eq_or_ne x 0 with rfl|hx0,
+  { induction y using with_top.rec_top_coe; cases hz with hz hz; simp [*, hz.not_lt] },
+  rcases eq_or_ne y 0 with rfl|hy0, { exact (hx0 (bot_unique hxy)).elim },
+  induction x using with_top.rec_top_coe, { cases hz with hz hz; simp [hz, top_unique hxy] },
+  induction y using with_top.rec_top_coe, { cases hz with hz hz; simp * },
+  simp only [*, false_and, and_false, false_or, if_false],
+  norm_cast at *,
+  rw [coe_rpow_of_ne_zero (mul_ne_zero hx0 hy0), nnreal.mul_rpow]
 end
 
 lemma mul_rpow_of_ne_top {x y : ℝ≥0∞} (hx : x ≠ ⊤) (hy : y ≠ ⊤) (z : ℝ) :

src/combinatorics/composition.lean

@@ -341,14 +341,12 @@ lemma disjoint_range {i₁ i₂ : fin c.length} (h : i₁ ≠ i₂) :
   disjoint (set.range (c.embedding i₁)) (set.range (c.embedding i₂)) :=
 begin
   classical,
-  wlog h' : i₁ ≤ i₂ using i₁ i₂,
-  swap, exact (this h.symm).symm,
+  wlog h' : i₁ < i₂, { exact (this c h.symm (h.lt_or_lt.resolve_left h')).symm },
   by_contradiction d,
   obtain ⟨x, hx₁, hx₂⟩ :
     ∃ x : fin n, (x ∈ set.range (c.embedding i₁) ∧ x ∈ set.range (c.embedding i₂)) :=
   set.not_disjoint_iff.1 d,
-  have : i₁ < i₂ := lt_of_le_of_ne h' h,
-  have A : (i₁ : ℕ).succ ≤ i₂ := nat.succ_le_of_lt this,
+  have A : (i₁ : ℕ).succ ≤ i₂ := nat.succ_le_of_lt h',
   apply lt_irrefl (x : ℕ),
   calc (x : ℕ) < c.size_up_to (i₁ : ℕ).succ : (c.mem_range_embedding_iff.1 hx₁).2
   ... ≤ c.size_up_to (i₂ : ℕ) : monotone_sum_take _ A

src/computability/DFA.lean

@@ -77,8 +77,7 @@ lemma eval_from_split [fintype σ] {x : list α} {s t : σ} (hlen : fintype.card
 begin
   obtain ⟨n, m, hneq, heq⟩ := fintype.exists_ne_map_eq_of_card_lt
     (λ n : fin (fintype.card σ + 1), M.eval_from s (x.take n)) (by norm_num),
-  wlog hle : (n : ℕ) ≤ m using n m,
-  have hlt : (n : ℕ) < m := (ne.le_iff_lt hneq).mp hle,
+  wlog hle : (n : ℕ) ≤ m, { exact this hlen hx _ _ hneq.symm heq.symm (le_of_not_le hle), },
   have hm : (m : ℕ) ≤ fintype.card σ := fin.is_le m,
   dsimp at heq,
 

src/computability/turing_machine.lean

@@ -268,8 +268,9 @@ end
   (∀ i, L₁.nth i = L₂.nth i) → L₁ = L₂ :=
 list_blank.induction_on L₁ $ λ l₁, list_blank.induction_on L₂ $ λ l₂ H,
 begin
-  wlog h : l₁.length ≤ l₂.length using l₁ l₂,
-  swap, { exact (this $ λ i, (H i).symm).symm },
+  wlog h : l₁.length ≤ l₂.length,
+  { cases le_total l₁.length l₂.length; [skip, symmetry]; apply_assumption; try {assumption},
+    intro, rw H },
   refine quotient.sound' (or.inl ⟨l₂.length - l₁.length, _⟩),
   refine list.ext_le _ (λ i h h₂, eq.symm _),
   { simp only [add_tsub_cancel_of_le h, list.length_append, list.length_replicate] },

src/control/lawful_fix.lean

@@ -74,7 +74,8 @@ begin
     suffices : y = b, subst this, exact h₁,
     cases hh with i hh,
     revert h₁, generalize : (succ (nat.find h₀)) = j, intro,
-    wlog : i ≤ j := le_total i j using [i j b y,j i y b],
+    wlog case : i ≤ j,
+    { cases le_total i j with H H; [skip, symmetry]; apply_assumption; assumption },
     replace hh := approx_mono f case _ _ hh,
     apply part.mem_unique h₁ hh },
   { simp only [fix_def' ⇑f h₀, not_exists, false_iff, not_mem_none],

src/data/complex/basic.lean

@@ -582,15 +582,13 @@ by simpa [re_add_im] using abs.add_le z.re (z.im * I)
 lemma abs_le_sqrt_two_mul_max (z : ℂ) : abs z ≤ real.sqrt 2 * max (|z.re|) (|z.im|) :=
 begin
   cases z with x y,
-  simp only [abs, norm_sq_mk, ← sq],
-  wlog hle : |x| ≤ |y| := le_total (|x|) (|y|) using [x y, y x] tactic.skip,
-  { simp only [absolute_value.coe_mk, mul_hom.coe_mk, norm_sq_mk, ←sq],
-    calc real.sqrt (x ^ 2 + y ^ 2) ≤ real.sqrt (y ^ 2 + y ^ 2) :
-      real.sqrt_le_sqrt (add_le_add_right (sq_le_sq.2 hle) _)
-    ... = real.sqrt 2 * max (|x|) (|y|) :
-      by rw [max_eq_right hle, ← two_mul, real.sqrt_mul two_pos.le, real.sqrt_sq_eq_abs] },
-  { dsimp,
-    rwa [add_comm, max_comm] }
+  simp only [abs_apply, norm_sq_mk, ← sq],
+  wlog hle : |x| ≤ |y|,
+  { rw [add_comm, max_comm], exact this _ _ (le_of_not_le hle), },
+  calc real.sqrt (x ^ 2 + y ^ 2) ≤ real.sqrt (y ^ 2 + y ^ 2) :
+    real.sqrt_le_sqrt (add_le_add_right (sq_le_sq.2 hle) _)
+  ... = real.sqrt 2 * max (|x|) (|y|) :
+    by rw [max_eq_right hle, ← two_mul, real.sqrt_mul two_pos.le, real.sqrt_sq_eq_abs],
 end
 
 lemma abs_re_div_abs_le_one (z : ℂ) : |z.re / z.abs| ≤ 1 :=

src/data/fintype/card.lean

@@ -864,7 +864,8 @@ private lemma nat_embedding_aux_injective (α : Type*) [infinite α] :
 begin
   rintro m n h,
   letI := classical.dec_eq α,
-  wlog hmlen : m ≤ n using m n,
+  wlog hmlen : m ≤ n generalizing m n,
+  { exact (this h.symm $ le_of_not_le hmlen).symm },
   by_contradiction hmn,
   have hmn : m < n, from lt_of_le_of_ne hmlen hmn,
   refine (classical.some_spec (exists_not_mem_finset

src/data/nat/count.lean

@@ -102,9 +102,9 @@ lemma count_strict_mono {m n : ℕ} (hm : p m) (hmn : m < n) : count p m < count
 
 lemma count_injective {m n : ℕ} (hm : p m) (hn : p n) (heq : count p m = count p n) : m = n :=
 begin
-  by_contra,
+  by_contra' h : m ≠ n,
   wlog hmn : m < n,
-  { exact ne.lt_or_lt h },
+  { exact this hn hm heq.symm h.symm (h.lt_or_lt.resolve_left hmn) },
   { simpa [heq] using count_strict_mono hm hmn }
 end
 

src/data/nat/fib.lean

@@ -222,15 +222,13 @@ lemma gcd_fib_add_mul_self (m n : ℕ) : ∀ k, gcd (fib m) (fib (n + k * m)) =
   see https://proofwiki.org/wiki/GCD_of_Fibonacci_Numbers -/
 lemma fib_gcd (m n : ℕ) : fib (gcd m n) = gcd (fib m) (fib n) :=
 begin
-  wlog h : m ≤ n using [n m, m n],
-  exact le_total m n,
-  { apply gcd.induction m n,
-    { simp },
-    intros m n mpos h,
-    rw ← gcd_rec m n at h,
-    conv_rhs { rw ← mod_add_div' n m },
-    rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _] },
-  rwa [gcd_comm, gcd_comm (fib m)]
+  wlog h : m ≤ n, { simpa only [gcd_comm] using this _ _ (le_of_not_le h) },
+  apply gcd.induction m n,
+  { simp },
+  intros m n mpos h,
+  rw ← gcd_rec m n at h,
+  conv_rhs { rw ← mod_add_div' n m },
+  rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _]
 end
 
 lemma fib_dvd (m n : ℕ) (h : m ∣ n) : fib m ∣ fib n :=

src/data/nat/nth.lean

@@ -150,6 +150,7 @@ lemma nth_injective_of_infinite (hp : (set_of p).infinite) : function.injective
 begin
   intros m n h,
   wlog h' : m ≤ n,
+  { exact (this p hp h.symm (le_of_not_le h')).symm },
   rw le_iff_lt_or_eq at h',
   obtain (h' | rfl) := h',
   { simpa [h] using nth_strict_mono p hp h' },

src/data/set/enumerate.lean

@@ -3,8 +3,9 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import tactic.wlog
+import data.set.lattice
 import data.nat.order.basic
+import tactic.wlog
 
 /-!
 # Set enumeration
@@ -72,6 +73,7 @@ lemma enumerate_inj {n₁ n₂ : ℕ} {a : α} {s : set α} (h_sel : ∀ s a, se
   (h₁ : enumerate s n₁ = some a) (h₂ : enumerate s n₂ = some a) : n₁ = n₂ :=
 begin
   wlog hn : n₁ ≤ n₂,
+  { cases le_total n₁ n₂ with H H; [skip, symmetry]; apply_assumption; assumption },
   { rcases nat.le.dest hn with ⟨m, rfl⟩, clear hn,
     induction n₁ generalizing s,
     case nat.zero

src/data/set/intervals/ord_connected_component.lean

@@ -165,8 +165,8 @@ begin
   rcases mem_Union₂.1 hx₁ with ⟨a, has, ha⟩, clear hx₁,
   rcases mem_Union₂.1 hx₂ with ⟨b, hbt, hb⟩, clear hx₂,
   rw [mem_ord_connected_component, subset_inter_iff] at ha hb,
-  wlog hab : a ≤ b := le_total a b using [a b s t, b a t s] tactic.skip,
-  rotate, from λ h₁ h₂ h₃ h₄, this h₂ h₁ h₄ h₃,
+  wlog hab : a ≤ b,
+  { exact this b hbt a has ha hb (le_of_not_le hab) },
   cases ha with ha ha', cases hb with hb hb',
   have hsub : [a, b] ⊆ (ord_separating_set s t).ord_connected_sectionᶜ,
   { rw [ord_separating_set_comm, uIcc_comm] at hb',

src/dynamics/ergodic/measure_preserving.lean

@@ -137,12 +137,11 @@ begin
     by simpa only [B, nsmul_eq_mul, finset.sum_const, finset.card_range],
   rcases exists_nonempty_inter_of_measure_univ_lt_sum_measure μ (λ m hm, A m) this
     with ⟨i, hi, j, hj, hij, x, hxi, hxj⟩,
-  -- without `tactic.skip` Lean closes the extra goal but it takes a long time; not sure why
-  wlog hlt : i < j := hij.lt_or_lt using [i j, j i] tactic.skip,
-  { simp only [set.mem_preimage, finset.mem_range] at hi hj hxi hxj,
-    refine ⟨f^[i] x, hxi, j - i, ⟨tsub_pos_of_lt hlt, lt_of_le_of_lt (j.sub_le i) hj⟩, _⟩,
-    rwa [← iterate_add_apply, tsub_add_cancel_of_le hlt.le] },
-  { exact λ hi hj hij hxi hxj, this hj hi hij.symm hxj hxi }
+  wlog hlt : i < j generalizing i j,
+  { exact this j hj i hi hij.symm hxj hxi (hij.lt_or_lt.resolve_left hlt) },
+  simp only [set.mem_preimage, finset.mem_range] at hi hj hxi hxj,
+  refine ⟨f^[i] x, hxi, j - i, ⟨tsub_pos_of_lt hlt, lt_of_le_of_lt (j.sub_le i) hj⟩, _⟩,
+  rwa [← iterate_add_apply, tsub_add_cancel_of_le hlt.le]
 end
 
 /-- A self-map preserving a finite measure is conservative: if `μ s ≠ 0`, then at least one point

src/field_theory/separable.lean

@@ -335,7 +335,9 @@ theorem unique_separable_of_irreducible {f : F[X]} (hf : irreducible f) (hp : 0
   n₁ = n₂ ∧ g₁ = g₂ :=
 begin
   revert g₁ g₂,
-  wlog hn : n₁ ≤ n₂ := le_total n₁ n₂ using [n₁ n₂, n₂ n₁],
+  wlog hn : n₁ ≤ n₂,
+  { intros g₁ g₂ hg₁ Hg₁ hg₂ Hg₂,
+    simpa only [eq_comm] using this hf hp n₂ n₁ (le_of_not_le hn) g₂ g₁ hg₂ Hg₂ hg₁ Hg₁ },
   have hf0 : f ≠ 0 := hf.ne_zero,
   unfreezingI { intros, rw le_iff_exists_add at hn, rcases hn with ⟨k, rfl⟩,
     rw [← hgf₁, pow_add, expand_mul, expand_inj (pow_pos hp n₁)] at hgf₂, subst hgf₂,
@@ -344,8 +346,6 @@ begin
     { rw is_unit_iff at h, rcases h with ⟨r, hr, rfl⟩,
       simp_rw expand_C at hf, exact absurd (is_unit_C.2 hr) hf.1 },
     { rw [add_zero, pow_zero, expand_one], split; refl } },
-  obtain ⟨hn, hg⟩ := this g₂ g₁ hg₂ hgf₂ hg₁ hgf₁,
-  exact ⟨hn.symm, hg.symm⟩
 end
 
 end char_p

src/field_theory/separable_degree.lean

@@ -109,7 +109,8 @@ theorem contraction_degree_eq_or_insep
   (hg : g.separable) (hg' : g'.separable) :
   g.nat_degree = g'.nat_degree :=
 begin
-  wlog hm : m ≤ m' := le_total m m' using [m m' g g', m' m g' g],
+  wlog hm : m ≤ m',
+  { exact (this g' g m' m h_expand.symm hg' hg (le_of_not_le hm)).symm },
   obtain ⟨s, rfl⟩ := exists_add_of_le hm,
   rw [pow_add, expand_mul, expand_inj (pow_pos (ne_zero.pos q) m)] at h_expand,
   subst h_expand,

src/group_theory/order_of_element.lean

@@ -410,7 +410,8 @@ by rw [modeq_zero_iff_dvd, order_of_dvd_iff_pow_eq_one]
 @[to_additive]
 lemma pow_eq_pow_iff_modeq : x ^ n = x ^ m ↔ n ≡ m [MOD (order_of x)] :=
 begin
-  wlog hmn : m ≤ n,
+  wlog hmn : m ≤ n generalizing m n,
+  { rw [eq_comm, modeq.comm, this (le_of_not_le hmn)], },
   obtain ⟨k, rfl⟩ := nat.exists_eq_add_of_le hmn,
   rw [← mul_one (x ^ m), pow_add, mul_left_cancel_iff, pow_eq_one_iff_modeq],
   exact ⟨λ h, nat.modeq.add_left _ h, λ h, nat.modeq.add_left_cancel' _ h⟩,