From faa0031d4ec1c44418d265932ba9111092594854 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Feb 2016 13:15:48 -0800 Subject: [PATCH] refactor(library,hott): remove 'by+' and 'begin+' --- hott/algebra/ring.hlean | 2 +- library/algebra/group_bigops.lean | 6 +++--- library/algebra/interval.lean | 2 +- library/algebra/ring.lean | 4 ++-- library/data/complex.lean | 2 +- library/data/list/sorted.lean | 2 +- library/data/nat/bigops.lean | 6 +++--- library/data/rat/basic.lean | 2 +- library/data/set/basic.lean | 2 +- library/data/set/equinumerosity.lean | 4 ++-- library/data/set/filter.lean | 2 +- library/data/set/function.lean | 2 +- library/theories/analysis/complex_norm.lean | 2 +- library/theories/analysis/inner_product.lean | 2 +- library/theories/analysis/metric_space.lean | 4 ++-- library/theories/analysis/normed_space.lean | 8 ++++---- library/theories/analysis/real_limit.lean | 14 +++++++------- library/theories/group_theory/cyclic.lean | 2 +- library/theories/measure_theory/extended_real.lean | 4 ++-- 19 files changed, 36 insertions(+), 36 deletions(-) diff --git a/hott/algebra/ring.hlean b/hott/algebra/ring.hlean index f7c5ab9f5..ce8105ceb 100644 --- a/hott/algebra/ring.hlean +++ b/hott/algebra/ring.hlean @@ -361,7 +361,7 @@ section have b - 1 ≠ 0, from suppose b - 1 = 0, H₁ (!zero_add ▸ eq_add_of_sub_eq this), have a * b - a = 0, by rewrite H₂; apply sub_self, - have a * (b - 1) = 0, by+ rewrite [mul_sub_left_distrib, mul_one]; apply this, + have a * (b - 1) = 0, by rewrite [mul_sub_left_distrib, mul_one]; apply this, show a = 0, from sum_resolve_left (eq_zero_sum_eq_zero_of_mul_eq_zero this) `b - 1 ≠ 0` theorem eq_zero_of_mul_eq_self_left {a b : A} (H₁ : b ≠ 1) (H₂ : b * a = a) : a = 0 := diff --git a/library/algebra/group_bigops.lean b/library/algebra/group_bigops.lean index 18c7d21b8..9321e7a96 100644 --- a/library/algebra/group_bigops.lean +++ b/library/algebra/group_bigops.lean @@ -244,7 +244,7 @@ namespace finset Prod_semigroup dflt (insert a s) f = f a * Prod_semigroup dflt s f := obtain a' (a's : a' ∈ s), from exists_mem_of_ne_empty sne, have H : s = insert a' (erase a' s), from eq.symm (insert_erase a's), - begin+ + begin rewrite [H, Prod_semigroup_insert_insert dflt f !not_mem_erase (eq.subst H anins)] end end deceqA @@ -311,7 +311,7 @@ namespace finset theorem Prod_singleton (a : A) (f : A → B) : Prod '{a} f = f a := have a ∉ ∅, from not_mem_empty a, - by+ rewrite [Prod_insert_of_not_mem f this, Prod_empty, mul_one] + by rewrite [Prod_insert_of_not_mem f this, Prod_empty, mul_one] theorem Prod_image {C : Type} [deceqC : decidable_eq C] {s : finset A} (f : C → B) {g : A → C} (H : set.inj_on g (to_set s)) : @@ -463,7 +463,7 @@ section Prod suppose finite t, have finite s, from finite_of_bij_on' H, show false, from nfins this, - by+ rewrite [Prod_of_not_finite nfins, Prod_of_not_finite nfint]) + by rewrite [Prod_of_not_finite nfins, Prod_of_not_finite nfint]) end Prod /- Sum: sum indexed by a set -/ diff --git a/library/algebra/interval.lean b/library/algebra/interval.lean index 93836927b..57dfd054a 100644 --- a/library/algebra/interval.lean +++ b/library/algebra/interval.lean @@ -127,7 +127,7 @@ open nat eq.ops proposition Icc_zero (n : ℕ) : '[0, n] = '(-∞, n] := have '[0, n] = '[0, ∞) ∩ '(-∞, n], from rfl, - by+ rewrite [this, Ici_zero, univ_inter] + by rewrite [this, Ici_zero, univ_inter] proposition bij_on_add_Icc_zero (m n : ℕ) : bij_on (add m) ('[0, n]) ('[m, m+n]) := have mapsto : ∀₀ i ∈ '[0, n], m + i ∈ '[m, m+n], from diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index e372057c4..93849ba91 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -362,8 +362,8 @@ section theorem eq_zero_of_mul_eq_self_right {a b : A} (H₁ : b ≠ 1) (H₂ : a * b = a) : a = 0 := have b - 1 ≠ 0, from suppose b - 1 = 0, H₁ (!zero_add ▸ eq_add_of_sub_eq this), - have a * b - a = 0, by simp, - have a * (b - 1) = 0, by+ rewrite [mul_sub_left_distrib, mul_one]; apply this, + have a * b - a = 0, by simp, + have a * (b - 1) = 0, by rewrite [mul_sub_left_distrib, mul_one]; apply this, show a = 0, from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero this) `b - 1 ≠ 0` theorem eq_zero_of_mul_eq_self_left {a b : A} (H₁ : b ≠ 1) (H₂ : b * a = a) : a = 0 := diff --git a/library/data/complex.lean b/library/data/complex.lean index e70eb3560..74e2ad828 100644 --- a/library/data/complex.lean +++ b/library/data/complex.lean @@ -260,7 +260,7 @@ protected theorem div_def (z w : ℂ) : z / w = z * w⁻¹ := rfl theorem of_real_div (x y : ℝ) : of_real (x / y) = of_real x / of_real y := have H : x / y = x * y⁻¹, from rfl, -by+ rewrite [H, complex.div_def, of_real_mul, of_real_inv] +by rewrite [H, complex.div_def, of_real_mul, of_real_inv] theorem conj_inv (z : ℂ) : (conj z)⁻¹ = conj (z⁻¹) := by rewrite [*complex.inv_def, conj_mul, *conj_conj, conj_of_real, cmod_conj] diff --git a/library/data/list/sorted.lean b/library/data/list/sorted.lean index 38cbfb791..bc07eaa1d 100644 --- a/library/data/list/sorted.lean +++ b/library/data/list/sorted.lean @@ -82,7 +82,7 @@ lemma sorted_extends (trans : transitive R) : ∀ {a l}, sorted R (a::l) → all have all l (R b), from sorted_extends (and.right (sorted_inv h)), all_of_forall (take x, suppose x ∈ b::l, or.elim (eq_or_mem_of_mem_cons this) - (suppose x = b, by+ subst x; assumption) + (suppose x = b, by subst x; assumption) (suppose x ∈ l, have R b x, from of_mem_of_all this `all l (R b)`, trans `R a b` `R b x`)) diff --git a/library/data/nat/bigops.lean b/library/data/nat/bigops.lean index 1f8b403e2..2aa1ab72e 100644 --- a/library/data/nat/bigops.lean +++ b/library/data/nat/bigops.lean @@ -96,7 +96,7 @@ proposition sum_range_eq_sum_interval {m n : ℕ} (f : ℕ → A) (H : m ≤ n) proposition sum_range_offset (m n : ℕ) (f : ℕ → A) : (∑ i = m...m+n, f i) = (∑ i = 0...n, f (m + i)) := have bij_on (add m) ('[0, n]) ('[m, m+n]), from !nat.bij_on_add_Icc_zero, - by+ rewrite [-zero_add n at {2}, *sum_range_eq_sum_interval_aux, Sum_eq_of_bij_on f this, zero_add] + by rewrite [-zero_add n at {2}, *sum_range_eq_sum_interval_aux, Sum_eq_of_bij_on f this, zero_add] end set @@ -187,8 +187,8 @@ proposition prod_range_eq_prod_interval {m n : ℕ} (f : ℕ → A) (H : m ≤ n proposition prod_range_offset (m n : ℕ) (f : ℕ → A) : (∏ i = m...m+n, f i) = (∏ i = 0...n, f (m + i)) := have bij_on (add m) ('[0, n]) ('[m, m+n]), from !nat.bij_on_add_Icc_zero, - by+ rewrite [-zero_add n at {2}, *prod_range_eq_prod_interval_aux, Prod_eq_of_bij_on f this, - zero_add] + by rewrite [-zero_add n at {2}, *prod_range_eq_prod_interval_aux, Prod_eq_of_bij_on f this, + zero_add] end set diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean index f813b7b1a..c2ed324b6 100644 --- a/library/data/rat/basic.lean +++ b/library/data/rat/basic.lean @@ -598,7 +598,7 @@ decidable.by_cases theorem of_nat_div {a b : ℕ} (H : b ∣ a) : of_nat (a / b) = of_nat a / of_nat b := have H' : (int.of_nat b ∣ int.of_nat a), by rewrite [int.of_nat_dvd_of_nat_iff]; exact H, -by+ rewrite [of_nat_eq, int.of_nat_div, of_int_div H'] +by rewrite [of_nat_eq, int.of_nat_div, of_int_div H'] theorem of_int_pow (a : ℤ) (n : ℕ) : of_int (a^n) = (of_int a)^n := begin diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean index 97308cbab..e24589874 100644 --- a/library/data/set/basic.lean +++ b/library/data/set/basic.lean @@ -758,7 +758,7 @@ theorem sInter_singleton (s : set X) : ⋂₀ '{s} = s := ext (take x, iff.intro (suppose x ∈ ⋂₀ '{s}, show x ∈ s, from this (mem_singleton s)) (suppose x ∈ s, take u, suppose u ∈ '{s}, - show x ∈ u, by+ rewrite [eq_of_mem_singleton this]; assumption)) + show x ∈ u, by rewrite [eq_of_mem_singleton this]; assumption)) theorem sUnion_union (S T : set (set X)) : ⋃₀ (S ∪ T) = ⋃₀ S ∪ ⋃₀ T := ext (take x, iff.intro diff --git a/library/data/set/equinumerosity.lean b/library/data/set/equinumerosity.lean index 4d6b13f9f..65738dcca 100644 --- a/library/data/set/equinumerosity.lean +++ b/library/data/set/equinumerosity.lean @@ -116,9 +116,9 @@ open set show h a ∈ B, from by_cases (suppose a ∈ Union U, - by+ rewrite [↑h, if_pos this]; exact f_maps_to `a ∈ A`) + by rewrite [↑h, if_pos this]; exact f_maps_to `a ∈ A`) (suppose a ∉ Union U, - by+ rewrite [↑h, if_neg this]; exact ginv_maps_to `a ∈ A`) + by rewrite [↑h, if_neg this]; exact ginv_maps_to `a ∈ A`) /- h is injective -/ diff --git a/library/data/set/filter.lean b/library/data/set/filter.lean index 238fa00aa..64fd71489 100644 --- a/library/data/set/filter.lean +++ b/library/data/set/filter.lean @@ -409,7 +409,7 @@ le.antisymm (le_of_forall_eventually (λ P H, have P = univ, from eq_of_mem_singleton H, - by+ rewrite this; apply eventually_true ⊤)) + by rewrite this; apply eventually_true ⊤)) !le_top theorem sets_bot_eq : sets ⊥ = (univ : set (set A)) := diff --git a/library/data/set/function.lean b/library/data/set/function.lean index f0bb4e9af..78ddebc53 100644 --- a/library/data/set/function.lean +++ b/library/data/set/function.lean @@ -104,7 +104,7 @@ take y, assume H, obtain x [xmem fxeqy], from H, or.elim xmem (suppose x ∈ s, or.inl (mem_image this fxeqy)) - (suppose x ∈ f '- t, or.inr (show y ∈ t, by+ rewrite -fxeqy; exact mem_of_mem_preimage this)) + (suppose x ∈ f '- t, or.inr (show y ∈ t, by rewrite -fxeqy; exact mem_of_mem_preimage this)) /- maps to -/ diff --git a/library/theories/analysis/complex_norm.lean b/library/theories/analysis/complex_norm.lean index 94e8cd04f..236cc21a1 100644 --- a/library/theories/analysis/complex_norm.lean +++ b/library/theories/analysis/complex_norm.lean @@ -43,7 +43,7 @@ namespace complex have re x = 0, from eq_zero_of_mul_self_add_mul_self_eq_zero H, have im x = 0, from eq_zero_of_mul_self_add_mul_self_eq_zero (by rewrite [↑ip at H, add.comm at H]; exact H), - by+ rewrite [-complex.eta, `re x = 0`, `im x = 0`] + by rewrite [-complex.eta, `re x = 0`, `im x = 0`] end real_inner_product_space protected definition real_inner_product_space [reducible] : inner_product_space ℂ := diff --git a/library/theories/analysis/inner_product.lean b/library/theories/analysis/inner_product.lean index 6334b0d2d..4a0a0f063 100644 --- a/library/theories/analysis/inner_product.lean +++ b/library/theories/analysis/inner_product.lean @@ -114,7 +114,7 @@ end private proposition ip_norm_proj_on_eq (u : V) {v : V} (H : v ≠ 0) : ip_norm (ip_proj_on u H) = abs ⟨u, v⟩ / ip_norm v := have H1 : ip_norm v ≠ 0, from assume H', H (eq_zero_of_ip_norm_eq_zero H'), -begin+ +begin rewrite [↑ip_proj_on, ip_norm_smul, abs_div, abs_of_nonneg (squared_nonneg (ip_norm v)), pow_two], rewrite [div_mul_eq_mul_div, -div_mul_div, div_self H1, mul_one] end diff --git a/library/theories/analysis/metric_space.lean b/library/theories/analysis/metric_space.lean index 978e7eb80..ec45a736d 100644 --- a/library/theories/analysis/metric_space.lean +++ b/library/theories/analysis/metric_space.lean @@ -120,7 +120,7 @@ exists.intro N proposition converges_to_seq_offset_left {X : ℕ → M} {y : M} (k : ℕ) (H : X ⟶ y in ℕ) : (λ n, X (k + n)) ⟶ y in ℕ := have aux : (λ n, X (k + n)) = (λ n, X (n + k)), from funext (take n, by rewrite add.comm), -by+ rewrite aux; exact converges_to_seq_offset k H +by rewrite aux; exact converges_to_seq_offset k H proposition converges_to_seq_offset_succ {X : ℕ → M} {y : M} (H : X ⟶ y in ℕ) : (λ n, X (succ n)) ⟶ y in ℕ := @@ -142,7 +142,7 @@ proposition converges_to_seq_of_converges_to_seq_offset_left {X : ℕ → M} {y : M} {k : ℕ} (H : (λ n, X (k + n)) ⟶ y in ℕ) : X ⟶ y in ℕ := have aux : (λ n, X (k + n)) = (λ n, X (n + k)), from funext (take n, by rewrite add.comm), -by+ rewrite aux at H; exact converges_to_seq_of_converges_to_seq_offset H +by rewrite aux at H; exact converges_to_seq_of_converges_to_seq_offset H proposition converges_to_seq_of_converges_to_seq_offset_succ {X : ℕ → M} {y : M} (H : (λ n, X (succ n)) ⟶ y in ℕ) : diff --git a/library/theories/analysis/normed_space.lean b/library/theories/analysis/normed_space.lean index 5a901929e..6329f0b6f 100644 --- a/library/theories/analysis/normed_space.lean +++ b/library/theories/analysis/normed_space.lean @@ -74,7 +74,7 @@ namespace analysis proposition norm_neg (v : V) : ∥ -v ∥ = ∥ v ∥ := have abs (1 : ℝ) = 1, from abs_of_nonneg zero_le_one, - by+ rewrite [-@neg_one_smul ℝ V, norm_smul, abs_neg, this, one_mul] + by rewrite [-@neg_one_smul ℝ V, norm_smul, abs_neg, this, one_mul] proposition norm_sub (u v : V) : ∥u - v∥ = ∥v - u∥ := by rewrite [-norm_neg, neg_sub] @@ -188,7 +188,7 @@ proposition smul_converges_to_seq (c : ℝ) (HX : X ⟶ x in ℕ) : by_cases (assume cz : c = 0, have (λ n, c • X n) = (λ n, 0), from funext (take x, by rewrite [cz, zero_smul]), - begin+ rewrite [this, cz, zero_smul], apply converges_to_seq_constant end) + begin rewrite [this, cz, zero_smul], apply converges_to_seq_constant end) (suppose c ≠ 0, smul_converges_to_seq_aux this HX) proposition neg_converges_to_seq (HX : X ⟶ x in ℕ) : @@ -205,7 +205,7 @@ proposition neg_converges_to_seq_iff : ((λ n, - X n) ⟶ - x in ℕ) ↔ (X ⟶ have aux : X = λ n, (- (- X n)), from funext (take n, by rewrite neg_neg), iff.intro (assume H : (λ n, -X n)⟶ -x in ℕ, - show X ⟶ x in ℕ, by+ rewrite [aux, -neg_neg x]; exact neg_converges_to_seq H) + show X ⟶ x in ℕ, by rewrite [aux, -neg_neg x]; exact neg_converges_to_seq H) neg_converges_to_seq proposition norm_converges_to_seq_zero (HX : X ⟶ 0 in ℕ) : (λ n, norm (X n)) ⟶ 0 in ℕ := @@ -226,7 +226,7 @@ exists.intro (N : ℕ) (take n : ℕ, assume Hn : n ≥ N, have HN' : abs (norm (X n) - 0) < ε, from HN n Hn, have norm (X n) < ε, - by+ rewrite [sub_zero at HN', abs_of_nonneg !norm_nonneg at HN']; apply HN', + by rewrite [sub_zero at HN', abs_of_nonneg !norm_nonneg at HN']; apply HN', show norm (X n - 0) < ε, by rewrite sub_zero; apply this) diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean index 084e4db7a..e0704e58b 100644 --- a/library/theories/analysis/real_limit.lean +++ b/library/theories/analysis/real_limit.lean @@ -39,13 +39,13 @@ proposition le_sup {x : ℝ} {X : set ℝ} (Hx : x ∈ X) {b : ℝ} (Hb : ∀ x, x ≤ sup X := have H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b), from and.intro (exists.intro x Hx) (exists.intro b Hb), -by+ rewrite [↑sup, dif_pos H]; exact and.left (sup_aux_spec H) x Hx +by rewrite [↑sup, dif_pos H]; exact and.left (sup_aux_spec H) x Hx proposition sup_le {X : set ℝ} (HX : ∃ x, x ∈ X) {b : ℝ} (Hb : ∀ x, x ∈ X → x ≤ b) : sup X ≤ b := have H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b), from and.intro HX (exists.intro b Hb), -by+ rewrite [↑sup, dif_pos H]; exact and.right (sup_aux_spec H) b Hb +by rewrite [↑sup, dif_pos H]; exact and.right (sup_aux_spec H) b Hb proposition exists_mem_and_lt_of_lt_sup {X : set ℝ} (HX : ∃ x, x ∈ X) {b : ℝ} (Hb : b < sup X) : ∃ x, x ∈ X ∧ b < x := @@ -74,13 +74,13 @@ proposition inf_le {x : ℝ} {X : set ℝ} (Hx : x ∈ X) {b : ℝ} (Hb : ∀ x, inf X ≤ x := have H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → b ≤ x), from and.intro (exists.intro x Hx) (exists.intro b Hb), -by+ rewrite [↑inf, dif_pos H]; exact and.left (inf_aux_spec H) x Hx +by rewrite [↑inf, dif_pos H]; exact and.left (inf_aux_spec H) x Hx proposition le_inf {X : set ℝ} (HX : ∃ x, x ∈ X) {b : ℝ} (Hb : ∀ x, x ∈ X → b ≤ x) : b ≤ inf X := have H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → b ≤ x), from and.intro HX (exists.intro b Hb), -by+ rewrite [↑inf, dif_pos H]; exact and.right (inf_aux_spec H) b Hb +by rewrite [↑inf, dif_pos H]; exact and.right (inf_aux_spec H) b Hb proposition exists_mem_and_lt_of_inf_lt {X : set ℝ} (HX : ∃ x, x ∈ X) {b : ℝ} (Hb : inf X < b) : ∃ x, x ∈ X ∧ x < b := @@ -261,7 +261,7 @@ smul_converges_to_seq c HX proposition mul_right_converges_to_seq (c : ℝ) (HX : X ⟶ x in ℕ) : (λ n, X n * c) ⟶ x * c in ℕ := have (λ n, X n * c) = (λ n, c * X n), from funext (take x, !mul.comm), -by+ rewrite [this, mul.comm]; apply mul_left_converges_to_seq c HX +by rewrite [this, mul.comm]; apply mul_left_converges_to_seq c HX theorem converges_to_seq_squeeze (HX : X ⟶ x in ℕ) (HY : Y ⟶ x in ℕ) {Z : ℕ → ℝ} (HZX : ∀ n, X n ≤ Z n) (HZY : ∀ n, Z n ≤ Y n) : Z ⟶ x in ℕ := @@ -429,7 +429,7 @@ have ∀ n, X i ≤ X (i + n), from (by rewrite nat.add_zero; apply le.refl) (take n, assume ih, le.trans ih (H (i + n))), have X i ≤ X (i + (j - i)), from !this, -by+ rewrite [add_sub_of_le `i ≤ j` at this]; exact this +by rewrite [add_sub_of_le `i ≤ j` at this]; exact this proposition converges_to_seq_sup_of_nondecreasing (nondecX : nondecreasing X) {b : ℝ} (Hb : ∀ i, X i ≤ b) : X ⟶ sup (X ' univ) in ℕ := @@ -505,7 +505,7 @@ have H₃ : {x : ℝ | -x ∈ X ' univ} = {x : ℝ | x ∈ (λ n, -X n) ' univ}, {x : ℝ | -x ∈ X ' univ} = (λ y, -y) ' (X ' univ) : by rewrite image_neg_eq ... = {x : ℝ | x ∈ (λ n, -X n) ' univ} : image_comp, have H₄ : ∀ i, - X i ≤ - b, from take i, neg_le_neg (Hb i), -begin+ +begin -- need krewrite here krewrite [-neg_converges_to_seq_iff, -sup_neg H₁ H₂, H₃, -nondecreasing_neg_iff at nonincX], apply converges_to_seq_sup_of_nondecreasing nonincX H₄ diff --git a/library/theories/group_theory/cyclic.lean b/library/theories/group_theory/cyclic.lean index d1ee1a693..08aecb5f8 100644 --- a/library/theories/group_theory/cyclic.lean +++ b/library/theories/group_theory/cyclic.lean @@ -232,7 +232,7 @@ end definition pow_fin_is_iso (a : A) : is_iso_class (pow_fin' a) := is_iso_class.mk (pow_fin_hom a) (have H : injective (λ (i : fin (order a)), a ^ (val i + 0)), from pow_fin_inj a 0, - begin+ rewrite [↑pow_fin', succ_pred_of_pos !order_pos]; exact H end) + begin rewrite [↑pow_fin', succ_pred_of_pos !order_pos]; exact H end) end cyclic diff --git a/library/theories/measure_theory/extended_real.lean b/library/theories/measure_theory/extended_real.lean index 035762f04..524925810 100644 --- a/library/theories/measure_theory/extended_real.lean +++ b/library/theories/measure_theory/extended_real.lean @@ -161,7 +161,7 @@ protected theorem neg_zero : -(0 : ereal) = 0 := rfl theorem infty_mul_pos {x : real} (H : x > 0) : ∞ * x = ∞ := have H1 : x ≠ 0, from ne_of_gt H, -by+ rewrite [*ereal.mul_def, ↑ereal.mul, if_neg H1, if_pos H] +by rewrite [*ereal.mul_def, ↑ereal.mul, if_neg H1, if_pos H] theorem pos_mul_infty {x : real} (H : x > 0) : x * ∞ = ∞ := by rewrite [ereal.mul_comm, infty_mul_pos H] @@ -169,7 +169,7 @@ by rewrite [ereal.mul_comm, infty_mul_pos H] theorem infty_mul_neg {x : real} (H : x < 0) : ∞ * x = -∞ := have H1 : x ≠ 0, from ne_of_lt H, have H2 : ¬ x > 0, from not_lt_of_gt H, -by+ rewrite [*ereal.mul_def, ↑ereal.mul, if_neg H1, if_neg H2] +by rewrite [*ereal.mul_def, ↑ereal.mul, if_neg H1, if_neg H2] theorem neg_mul_infty {x : real} (H : x < 0) : x * ∞ = -∞ := by rewrite [ereal.mul_comm, infty_mul_neg H]