style(tactic/omega): whitespace and minor tweaks

missed the PR review cycle
leanprover-community · Apr 19, 2019 · c1aff1b · c1aff1b
1 parent d0140dd
commit c1aff1b
Show file tree

Hide file tree

Showing 17 changed files with 481 additions and 477 deletions.
diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean
@@ -4517,10 +4517,10 @@ end choose
 
 namespace func
 
-variables {a : α} 
+variables {a : α}
 variables {as as1 as2 as3 : list α}
 
-local notation as `{` m `↦` a `}` := set a as m
+local notation as ` {` m ` ↦ ` a `}` := set a as m
 
 /- set -/
 
@@ -4531,8 +4531,8 @@ lemma length_set [inhabited α] : ∀ {m : ℕ} {as : list α},
 | (m+1) []      := by simp only [set, nat.zero_max, length, @length_set m]
 | (m+1) (a::as) := by simp only [set, nat.max_succ_succ, length, @length_set m]
 
-@[simp] lemma get_nil [inhabited α] {k : ℕ} : get k [] = default α := 
-by {cases k; refl} 
+@[simp] lemma get_nil [inhabited α] {k : ℕ} : get k [] = default α :=
+by {cases k; refl}
 
 lemma get_eq_default_of_le [inhabited α] :
   ∀ (k : ℕ) {as : list α}, as.length ≤ k → get k as = default α
@@ -4548,7 +4548,7 @@ lemma get_eq_default_of_le [inhabited α] :
 @[simp] lemma get_set [inhabited α] {a : α} :
   ∀ {k : ℕ} {as : list α}, get k (as {k ↦ a}) = a
 | 0 as     := by {cases as; refl, }
-| (k+1) as := by {cases as; simp [get_set]} 
+| (k+1) as := by {cases as; simp [get_set]}
 
 lemma eq_get_of_mem [inhabited α] {a : α} :
   ∀ {as : list α}, a ∈ as → ∃ n : nat, ∀ d : α, a = (get n as)
@@ -4588,7 +4588,7 @@ lemma get_set_eq_of_ne [inhabited α] {a : α} :
   ∀ {as : list α} (k : ℕ) (m : ℕ),
   m ≠ k → get m (as {k ↦ a}) = get m as
 | as 0 m h1 :=
-  by { cases m, contradiction, cases as; 
+  by { cases m, contradiction, cases as;
        simp only [set, get, get_nil] }
 | as (k+1) m h1 :=
   begin
@@ -4599,36 +4599,36 @@ lemma get_set_eq_of_ne [inhabited α] {a : α} :
         intro hc, apply h1, simp [hc] },
       apply h3 },
     simp only [set, get],
-    { apply get_set_eq_of_ne k m, 
+    { apply get_set_eq_of_ne k m,
       intro hc, apply h1, simp [hc], }
   end
 
-lemma get_map [inhabited α] [inhabited β] {f : α → β} : 
-  ∀ {n : ℕ} {as : list α}, n < as.length → 
+lemma get_map [inhabited α] [inhabited β] {f : α → β} :
+  ∀ {n : ℕ} {as : list α}, n < as.length →
   get n (as.map f) = f (get n as)
 | _ [] h := by cases h
 | 0 (a::as) h := rfl
 | (n+1) (a::as) h1 :=
   begin
-    have h2 : n < length as, 
-    { rw [← nat.succ_le_iff, ← nat.lt_succ_iff], 
+    have h2 : n < length as,
+    { rw [← nat.succ_le_iff, ← nat.lt_succ_iff],
       apply h1 },
     apply get_map h2,
   end
 
-lemma get_map' [inhabited α] [inhabited β] 
+lemma get_map' [inhabited α] [inhabited β]
   {f : α → β} {n : ℕ} {as : list α} :
-  f (default α) = (default β) → 
+  f (default α) = (default β) →
   get n (as.map f) = f (get n as) :=
 begin
   intro h1, by_cases h2 : n < as.length,
   { apply get_map h2, },
   { rw not_lt at h2,
-    rw [get_eq_default_of_le _ h2, get_eq_default_of_le, h1], 
+    rw [get_eq_default_of_le _ h2, get_eq_default_of_le, h1],
     rw [length_map], apply h2 }
 end
 
-lemma forall_val_of_forall_mem [inhabited α] 
+lemma forall_val_of_forall_mem [inhabited α]
   {as : list α} {p : α → Prop} :
   p (default α) → (∀ x ∈ as, p x) → (∀ n, p (get n as)) :=
 begin
@@ -4643,93 +4643,93 @@ end
 
 lemma equiv_refl [inhabited α] : equiv as as := λ k, rfl
 
-lemma equiv_symm [inhabited α] : equiv as1 as2 → equiv as2 as1 := 
+lemma equiv_symm [inhabited α] : equiv as1 as2 → equiv as2 as1 :=
 λ h1 k, (h1 k).symm
 
 lemma equiv_trans [inhabited α] :
   equiv as1 as2 → equiv as2 as3 → equiv as1 as3 :=
 λ h1 h2 k, eq.trans (h1 k) (h2 k)
 
-lemma equiv_of_eq [inhabited α] : as1 = as2 → equiv as1 as2 := 
+lemma equiv_of_eq [inhabited α] : as1 = as2 → equiv as1 as2 :=
 begin intro h1, rw h1, apply equiv_refl end
 
 lemma eq_of_equiv [inhabited α] :
-  ∀ {as1 as2 : list α}, as1.length = as2.length → 
-  equiv as1 as2 → as1 = as2 
+  ∀ {as1 as2 : list α}, as1.length = as2.length →
+  equiv as1 as2 → as1 = as2
 | []     [] h1 h2 := rfl
 | (_::_) [] h1 h2 := by cases h1
 | [] (_::_) h1 h2 := by cases h1
-| (a1::as1) (a2::as2) h1 h2 := 
+| (a1::as1) (a2::as2) h1 h2 :=
   begin
     congr,
     { apply h2 0 },
-    have h3 : as1.length = as2.length, 
+    have h3 : as1.length = as2.length,
     { simpa [add_left_inj, add_comm, length] using h1 },
     apply eq_of_equiv h3,
-    intro m, apply h2 (m+1) 
+    intro m, apply h2 (m+1)
   end
 
 /- neg -/
 
-@[simp] lemma get_neg [inhabited α] [add_group α] 
+@[simp] lemma get_neg [inhabited α] [add_group α]
   {k : ℕ} {as : list α} : @get α ⟨0⟩ k (neg as) = -(@get α ⟨0⟩ k as) :=
 by {unfold neg, rw (@get_map' α α ⟨0⟩), apply neg_zero}
 
-@[simp] lemma length_neg 
-  [inhabited α] [has_neg α] (as : list α) : 
-  (neg as).length = as.length := 
+@[simp] lemma length_neg
+  [inhabited α] [has_neg α] (as : list α) :
+  (neg as).length = as.length :=
 by simp only [neg, length_map]
 
 /- pointwise -/
 
-lemma nil_pointwise [inhabited α] [inhabited β] {f : α → β → γ} : 
-  ∀ bs : list β, pointwise f [] bs = bs.map (f $ default α) 
+lemma nil_pointwise [inhabited α] [inhabited β] {f : α → β → γ} :
+  ∀ bs : list β, pointwise f [] bs = bs.map (f $ default α)
 | []      := rfl
-| (b::bs) := 
-  by simp only [nil_pointwise bs, pointwise, 
-     eq_self_iff_true, and_self, map] 
+| (b::bs) :=
+  by simp only [nil_pointwise bs, pointwise,
+     eq_self_iff_true, and_self, map]
 
-lemma pointwise_nil [inhabited α] [inhabited β] {f : α → β → γ} : 
-  ∀ as : list α, pointwise f as [] = as.map (λ a, f a $ default β) 
+lemma pointwise_nil [inhabited α] [inhabited β] {f : α → β → γ} :
+  ∀ as : list α, pointwise f as [] = as.map (λ a, f a $ default β)
 | []      := rfl
-| (a::as) := 
-  by simp only [pointwise_nil as, pointwise, 
-     eq_self_iff_true, and_self, list.map] 
-
-lemma get_pointwise [inhabited α] [inhabited β] [inhabited γ] 
-  {f : α → β → γ} (h1 : f (default α) (default β) = default γ) : 
-  ∀ (k : nat) (as : list α) (bs : list β), 
-  get k (pointwise f as bs) = f (get k as) (get k bs) 
+| (a::as) :=
+  by simp only [pointwise_nil as, pointwise,
+     eq_self_iff_true, and_self, list.map]
+
+lemma get_pointwise [inhabited α] [inhabited β] [inhabited γ]
+  {f : α → β → γ} (h1 : f (default α) (default β) = default γ) :
+  ∀ (k : nat) (as : list α) (bs : list β),
+  get k (pointwise f as bs) = f (get k as) (get k bs)
 | k [] [] := by simp only [h1, get_nil, pointwise, get]
-| 0 [] (b::bs) := 
-  by simp only [get_pointwise, get_nil, 
-      pointwise, get, nat.nat_zero_eq_zero, map] 
-| (k+1) [] (b::bs) := 
+| 0 [] (b::bs) :=
+  by simp only [get_pointwise, get_nil,
+      pointwise, get, nat.nat_zero_eq_zero, map]
+| (k+1) [] (b::bs) :=
   by { have : get k (map (f $ default α) bs) = f (default α) (get k bs),
        { simpa [nil_pointwise, get_nil] using (get_pointwise k [] bs) },
        simpa [get, get_nil, pointwise, map] }
-| 0 (a::as) [] := 
-  by simp only [get_pointwise, get_nil, 
-     pointwise, get, nat.nat_zero_eq_zero, map] 
-| (k+1) (a::as) [] := 
-  by simpa [get, get_nil, pointwise, map, pointwise_nil, get_nil] 
+| 0 (a::as) [] :=
+  by simp only [get_pointwise, get_nil,
+     pointwise, get, nat.nat_zero_eq_zero, map]
+| (k+1) (a::as) [] :=
+  by simpa [get, get_nil, pointwise, map, pointwise_nil, get_nil]
      using get_pointwise k as []
-| 0 (a::as) (b::bs) := by simp only [pointwise, get] 
-| (k+1) (a::as) (b::bs) := 
-  by simp only [pointwise, get, get_pointwise k] 
+| 0 (a::as) (b::bs) := by simp only [pointwise, get]
+| (k+1) (a::as) (b::bs) :=
+  by simp only [pointwise, get, get_pointwise k]
 
-lemma length_pointwise [inhabited α] [inhabited β] {f : α → β → γ} : 
-  ∀ {as : list α} {bs : list β}, 
-  (pointwise f as bs).length = _root_.max as.length bs.length 
+lemma length_pointwise [inhabited α] [inhabited β] {f : α → β → γ} :
+  ∀ {as : list α} {bs : list β},
+  (pointwise f as bs).length = _root_.max as.length bs.length
 | []      []      := rfl
-| []      (b::bs) := 
+| []      (b::bs) :=
   by simp only [pointwise, length, length_map,
      max_eq_right (nat.zero_le (length bs + 1))]
-| (a::as) []      := 
+| (a::as) []      :=
   by simp only [pointwise, length, length_map,
      max_eq_left (nat.zero_le (length as + 1))]
 | (a::as) (b::bs) :=
-  by simp only [pointwise, length, 
+  by simp only [pointwise, length,
      nat.max_succ_succ, @length_pointwise as bs]
 
 /- add -/
@@ -4738,27 +4738,27 @@ lemma length_pointwise [inhabited α] [inhabited β] {f : α → β → γ} :
   @get α ⟨0⟩ k (add xs ys) = ( @get α ⟨0⟩ k xs + @get α ⟨0⟩ k ys) :=
 by {apply get_pointwise, apply zero_add}
 
-@[simp] lemma length_add {α : Type u} 
-  [has_zero α] [has_add α] {xs ys : list α} : 
-  (add xs ys).length = _root_.max xs.length ys.length := 
+@[simp] lemma length_add {α : Type u}
+  [has_zero α] [has_add α] {xs ys : list α} :
+  (add xs ys).length = _root_.max xs.length ys.length :=
 @length_pointwise α α α ⟨0⟩ ⟨0⟩ _ _ _
 
-@[simp] lemma nil_add {α : Type u} [add_monoid α] 
-  (as : list α) : add [] as = as := 
+@[simp] lemma nil_add {α : Type u} [add_monoid α]
+  (as : list α) : add [] as = as :=
 begin
   rw [add, @nil_pointwise α α α ⟨0⟩ ⟨0⟩],
-  apply eq.trans _ (map_id as), 
-  congr, ext, 
+  apply eq.trans _ (map_id as),
+  congr, ext,
   have : @default α ⟨0⟩ = 0 := rfl,
   rw [this, zero_add], refl
 end
 
-@[simp] lemma add_nil {α : Type u} [add_monoid α] 
-  (as : list α) : add as [] = as := 
+@[simp] lemma add_nil {α : Type u} [add_monoid α]
+  (as : list α) : add as [] = as :=
 begin
-  rw [add, @pointwise_nil α α α ⟨0⟩ ⟨0⟩], 
-  apply eq.trans _ (map_id as), 
-  congr, ext, 
+  rw [add, @pointwise_nil α α α ⟨0⟩ ⟨0⟩],
+  apply eq.trans _ (map_id as),
+  congr, ext,
   have : @default α ⟨0⟩ = 0 := rfl,
   rw [this, add_zero], refl
 end
@@ -4768,10 +4768,10 @@ lemma map_add_map {α : Type u} [add_monoid α] (f g : α → α) {as : list α}
 begin
   apply @eq_of_equiv _ (⟨0⟩ : inhabited α),
   { rw [length_map, length_add, max_eq_left, length_map],
-    apply le_of_eq, 
+    apply le_of_eq,
     rw [length_map, length_map] },
-  intros m, 
-  rw [get_add], 
+  intros m,
+  rw [get_add],
   by_cases h : m < length as,
   { repeat {rw [@get_map α α ⟨0⟩ ⟨0⟩ _ _ _ h]} },
   rw not_lt at h,
@@ -4782,30 +4782,30 @@ end
 
 /- sub -/
 
-@[simp] lemma get_sub {α : Type u} 
+@[simp] lemma get_sub {α : Type u}
   [add_group α] {k : ℕ} {xs ys : list α} :
   @get α ⟨0⟩ k (sub xs ys) = (@get α ⟨0⟩ k xs - @get α ⟨0⟩ k ys) :=
 by {apply get_pointwise, apply sub_zero}
 
-@[simp] lemma length_sub [has_zero α] [has_sub α] {xs ys : list α} : 
-  (sub xs ys).length = _root_.max xs.length ys.length := 
+@[simp] lemma length_sub [has_zero α] [has_sub α] {xs ys : list α} :
+  (sub xs ys).length = _root_.max xs.length ys.length :=
 @length_pointwise α α α ⟨0⟩ ⟨0⟩ _ _ _
 
-@[simp] lemma nil_sub {α : Type} [add_group α] 
-  (as : list α) : sub [] as = @neg α ⟨0⟩ _ as := 
+@[simp] lemma nil_sub {α : Type} [add_group α]
+  (as : list α) : sub [] as = @neg α ⟨0⟩ _ as :=
 begin
-  rw [sub, nil_pointwise], 
-  congr, ext, 
+  rw [sub, nil_pointwise],
+  congr, ext,
   have : @default α ⟨0⟩ = 0 := rfl,
   rw [this, zero_sub]
 end
 
-@[simp] lemma sub_nil {α : Type} [add_group α] 
-  (as : list α) : sub as [] = as := 
+@[simp] lemma sub_nil {α : Type} [add_group α]
+  (as : list α) : sub as [] = as :=
 begin
-  rw [sub, pointwise_nil], 
-  apply eq.trans _ (map_id as), 
-  congr, ext, 
+  rw [sub, pointwise_nil],
+  apply eq.trans _ (map_id as),
+  congr, ext,
   have : @default α ⟨0⟩ = 0 := rfl,
   rw [this, sub_zero], refl
 end
@@ -4816,4 +4816,4 @@ end list
 
 theorem option.to_list_nodup {α} : ∀ o : option α, o.to_list.nodup
 | none     := list.nodup_nil
-| (some x) := list.nodup_singleton x
+| (some x) := list.nodup_singleton x