refactor(*): touching up proofs from 'faster' branch

Author: digama0

algebra/big_operators.lean

@@ -7,6 +7,7 @@ Some big operators for lists and finite sets.
 -/
 import data.list.basic data.list.perm data.finset
   algebra.group algebra.ordered_group algebra.group_power
+  tactic.squeeze
 
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
@@ -15,7 +16,7 @@ theorem directed.finset_le {r : α → α → Prop} [is_trans α r]
   {ι} (hι : nonempty ι) {f : ι → α} (D : directed r f) (s : finset ι) :
   ∃ z, ∀ i ∈ s, r (f i) (f z) :=
 show ∃ z, ∀ i ∈ s.1, r (f i) (f z), from
-multiset.induction_on s.1 (match hι with ⟨z⟩ := ⟨z, λ _, false.elim⟩ end) $
+multiset.induction_on s.1 (let ⟨z⟩ := hι in ⟨z, λ _, false.elim⟩) $
 λ i s ⟨j, H⟩, let ⟨k, h₁, h₂⟩ := D i j in
 ⟨k, λ a h, or.cases_on (multiset.mem_cons.1 h)
   (λ h, h.symm ▸ h₁)
@@ -373,29 +374,28 @@ lemma prod_sum {δ : α → Type*} [∀a, decidable_eq (δ a)]
 begin
   induction s using finset.induction with a s ha ih,
   { rw [pi_empty, sum_singleton], refl },
-  { have h₁ : ∀x ∈ t a, ∀y∈t a, ∀h : x ≠ y,
+  { have h₁ : ∀x ∈ t a, ∀y ∈ t a, ∀h : x ≠ y,
         image (pi.cons s a x) (pi s t) ∩ image (pi.cons s a y) (pi s t) = ∅,
     { assume x hx y hy h,
       apply eq_empty_of_forall_not_mem,
       simp only [mem_inter, mem_image],
       rintro p₁ ⟨⟨p₂, hp, eq⟩, ⟨p₃, hp₃, rfl⟩⟩,
       have : pi.cons s a x p₂ a (mem_insert_self _ _) = pi.cons s a y p₃ a (mem_insert_self _ _),
       { rw [eq] },
-      rw [pi.cons_same, pi.cons_same] at this, cc },
+      rw [pi.cons_same, pi.cons_same] at this,
+      exact h this },
     rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_bind h₁],
-    refine sum_congr rfl (λ x hx, _),
-    have h₂ : ∀p₁∈pi s t, ∀p₂∈pi s t, pi.cons s a x p₁ = pi.cons s a x p₂ → p₁ = p₂, from
+    refine sum_congr rfl (λ b _, _),
+    have h₂ : ∀p₁∈pi s t, ∀p₂∈pi s t, pi.cons s a b p₁ = pi.cons s a b p₂ → p₁ = p₂, from
       assume p₁ h₁ p₂ h₂ eq, injective_pi_cons ha eq,
     rw [sum_image h₂, mul_sum],
-    refine sum_congr rfl (λ g hg, _),
-    have h₃ : ∀ x ∈ attach s, ∀ y ∈ attach s, (⟨x.1, mem_insert_of_mem x.2⟩ : {x // x ∈ insert a s}) = ⟨y.1, mem_insert_of_mem y.2⟩ → x = y, from
-      λ _ _ _ _, subtype.eq ∘ subtype.mk.inj,
-    have h₄ : (⟨a, _⟩ : {x // x ∈ insert a s}) ∉ image (λ (x : {x // x ∈ s}), (⟨x.1, _⟩ : {x // x ∈ insert a s})) (attach s),
-    { simp only [mem_image], rintro ⟨⟨_, _⟩, _, rfl⟩, cc },
-    rw [attach_insert, prod_insert h₄, prod_image h₃],
-    simp only [pi.cons_same],
-    refine congr_arg _ (prod_congr rfl (λ v hv, congr_arg _ _)),
-    exact (pi.cons_ne (by rintro rfl; exact ha v.2)).symm }
+    refine sum_congr rfl (λ g _, _),
+    rw [attach_insert, prod_insert, prod_image],
+    { simp only [pi.cons_same],
+      congr', ext ⟨v, hv⟩, congr',
+      exact (pi.cons_ne (by rintro rfl; exact ha hv)).symm },
+    { exact λ _ _ _ _, subtype.eq ∘ subtype.mk.inj },
+    { simp only [mem_image], rintro ⟨⟨_, hm⟩, _, rfl⟩, exact ha hm } }
 end
 
 end comm_semiring
@@ -404,13 +404,9 @@ section integral_domain /- add integral_semi_domain to support nat and ennreal -
 variables [decidable_eq α] [integral_domain β]
 
 lemma prod_eq_zero_iff : s.prod f = 0 ↔ (∃a∈s, f a = 0) :=
-finset.induction_on s ⟨false.elim ∘ one_ne_zero, λ ⟨_, H, _⟩, H.elim⟩
-begin
-  intros a s ha,
-  rw [bex_def, bex_def, exists_mem_insert],
-  intro ih,
-  simp only [prod_insert ha, mul_eq_zero_iff_eq_zero_or_eq_zero, ih]
-end
+finset.induction_on s ⟨not.elim one_ne_zero, λ ⟨_, H, _⟩, H.elim⟩ $ λ a s ha ih,
+by rw [prod_insert ha, mul_eq_zero_iff_eq_zero_or_eq_zero,
+  bex_def, exists_mem_insert, ih, ← bex_def]
 
 end integral_domain
 
@@ -436,9 +432,9 @@ calc s₁.sum f ≤ (s₂ \ s₁).sum f + s₁.sum f :
 lemma sum_eq_zero_iff_of_nonneg : (∀x∈s, 0 ≤ f x) → (s.sum f = 0 ↔ ∀x∈s, f x = 0) :=
 finset.induction_on s (λ _, ⟨λ _ _, false.elim, λ _, rfl⟩) $ λ a s ha ih H,
 have ∀ x ∈ s, 0 ≤ f x, from λ _, H _ ∘ mem_insert_of_mem,
-⟨by rw [sum_insert ha, add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg' (H _ $ mem_insert_self _ _) (zero_le_sum' this)];
-  simp only [mem_insert]; rintro ⟨_, _⟩ x (rfl | h2); cases ih this; solve_by_elim,
-λ h1, (sum_congr rfl h1).trans sum_const_zero⟩
+by rw [sum_insert ha,
+  add_eq_zero_iff' (H _ $ mem_insert_self _ _) (zero_le_sum' this),
+  forall_mem_insert, ih this]
 
 lemma single_le_sum (hf : ∀x∈s, 0 ≤ f x) {a} (h : a ∈ s) : f a ≤ s.sum f :=
 have (singleton a).sum f ≤ s.sum f,

algebra/euclidean_domain.lean

@@ -200,9 +200,9 @@ theorem xgcd_aux_P (a b : α) {r r' : α} : ∀ {s t s' t'}, P a b (r, s, t) →
   P a b (r', s', t') → P a b (xgcd_aux r s t r' s' t') :=
 gcd.induction r r' (by intros; simpa only [xgcd_zero_left]) $ λ x y h IH s t s' t' p p', begin
   rw [xgcd_aux_rec h], refine IH _ p, unfold P at p p' ⊢,
-  conv {to_lhs, rw mod_eq_sub_mul_div, congr, rw p', skip, congr, rw p },
-  rw [add_mul, mul_sub, mul_sub, sub_add_eq_sub_sub, add_sub, sub_add_eq_add_sub],
-  simp only [mul_assoc, mul_comm, mul_left_comm]
+  rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub,
+    mul_comm _ s, ← mul_assoc, mul_comm _ t, ← mul_assoc, ← add_mul, ← p,
+    mod_eq_sub_mul_div]
 end
 
 theorem gcd_eq_gcd_ab (a b : α) : (gcd a b : α) = a * gcd_a a b + b * gcd_b a b :=

algebra/field.lean

@@ -155,9 +155,6 @@ variables [discrete_field α] {a b c : α}
 
 attribute [simp] inv_zero div_zero
 
-lemma inv_sub_inv_eq (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ - b⁻¹ = (b - a) / (a * b) :=
-inv_sub_inv ha hb
-
 lemma div_right_comm (a b c : α) : (a / b) / c = (a / c) / b :=
 if b0 : b = 0 then by simp only [b0, div_zero, zero_div] else
 if c0 : c = 0 then by simp only [c0, div_zero, zero_div] else

algebra/gcd_domain.lean

@@ -189,7 +189,7 @@ end gcd
 
 section lcm
 
-lemma lcm_dvd_iff (a b c : α) : lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c :=
+lemma lcm_dvd_iff {a b c : α} : lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c :=
 classical.by_cases
   (assume : a = 0 ∨ b = 0, by rcases this with rfl | rfl;
     simp only [iff_def, lcm_zero_left, lcm_zero_right, zero_dvd_iff, dvd_zero,
@@ -202,14 +202,12 @@ classical.by_cases
         ← gcd_mul_left, dvd_gcd_iff, mul_comm c a, mul_dvd_mul_iff_left h1,
         mul_dvd_mul_iff_right h2, and_comm])
 
-lemma dvd_lcm_left (a b : α) : a ∣ lcm a b :=
-((lcm_dvd_iff _ _ _).1 (dvd_refl _)).1
+lemma dvd_lcm_left (a b : α) : a ∣ lcm a b := (lcm_dvd_iff.1 (dvd_refl _)).1
 
-lemma dvd_lcm_right (a b : α) : b ∣ lcm a b :=
-((lcm_dvd_iff _ _ _).1 (dvd_refl _)).2
+lemma dvd_lcm_right (a b : α) : b ∣ lcm a b := (lcm_dvd_iff.1 (dvd_refl _)).2
 
 lemma lcm_dvd {a b c : α} (hab : a ∣ b) (hcb : c ∣ b) : lcm a c ∣ b :=
-(lcm_dvd_iff _ _ _).2 ⟨hab, hcb⟩
+lcm_dvd_iff.2 ⟨hab, hcb⟩
 
 @[simp] theorem lcm_eq_zero_iff (a b : α) : lcm a b = 0 ↔ a = 0 ∨ b = 0 :=
 iff.intro

algebra/group_power.lean

@@ -354,13 +354,11 @@ theorem is_semiring_hom.map_pow {β} [semiring α] [semiring β]
 by induction n with n ih; [exact is_semiring_hom.map_one f,
   rw [pow_succ, pow_succ, is_semiring_hom.map_mul f, ih]]
 
-theorem neg_one_pow_eq_or {R} [ring R] (n : ℕ) : (-1 : R)^n = 1 ∨ (-1 : R)^n = -1 :=
-begin
-  induction n with n ih, {left, refl},
-  cases ih with h h,
-  { right, rw [pow_succ, h, mul_one] },
-  { left, rw [pow_succ, h, neg_one_mul, neg_neg] }
-end
+theorem neg_one_pow_eq_or {R} [ring R] : ∀ n : ℕ, (-1 : R)^n = 1 ∨ (-1 : R)^n = -1
+| 0     := or.inl rfl
+| (n+1) := (neg_one_pow_eq_or n).swap.imp
+  (λ h, by rw [pow_succ, h, neg_one_mul, neg_neg])
+  (λ h, by rw [pow_succ, h, mul_one])
 
 theorem gsmul_eq_mul [ring α] (a : α) : ∀ n, n •ℤ a = n * a
 | (n : ℕ) := add_monoid.smul_eq_mul _ _
@@ -384,11 +382,10 @@ by rw [← nat.mod_add_div n 2, pow_add, pow_mul]; simp [pow_two]
 
 theorem pow_ne_zero [domain α] {a : α} (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 :=
 begin
-  induction n with n ih, { exact one_ne_zero },
+  induction n with n ih, {exact one_ne_zero},
   intro H,
   cases mul_eq_zero.1 H with h1 h1,
-  { exact h h1 },
-  { exact ih h1 }
+  exacts [h h1, ih h1]
 end
 
 @[simp] theorem one_div_pow [division_ring α] {a : α} (ha : a ≠ 0) (n : ℕ) : (1 / a) ^ n = 1 / a ^ n :=
@@ -499,6 +496,7 @@ lemma units_pow_eq_pow_mod_two (u : units ℤ) (n : ℕ) : u ^ n = u ^ (n % 2) :
 by conv {to_lhs, rw ← nat.mod_add_div n 2}; rw [pow_add, pow_mul, units_pow_two, one_pow, mul_one]
 
 end int
+
 @[simp] lemma neg_square {α} [ring α] (z : α) : (-z)^2 = z^2 :=
 by simp [pow, monoid.pow]
 

algebra/ordered_group.lean

@@ -119,8 +119,7 @@ add_lt_of_nonpos_of_lt' (le_of_lt ha) hbc
 lemma add_lt_of_lt_of_neg' (hbc : b < c) (ha : a < 0) : b + a < c :=
 add_lt_of_lt_of_nonpos' hbc (le_of_lt ha)
 
-lemma add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg'
-  (ha : 0 ≤ a) (hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 :=
+lemma add_eq_zero_iff' (ha : 0 ≤ a) (hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 :=
 iff.intro
   (assume hab : a + b = 0,
    have a ≤ 0, from hab ▸ le_add_of_le_of_nonneg' (le_refl _) hb,
@@ -340,7 +339,7 @@ canonically_ordered_monoid.le_iff_exists_add a b
 @[simp] lemma zero_le (a : α) : 0 ≤ a := le_iff_exists_add.mpr ⟨a, by simp⟩
 
 @[simp] lemma add_eq_zero_iff : a + b = 0 ↔ a = 0 ∧ b = 0 :=
-add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg' (zero_le _) (zero_le _)
+add_eq_zero_iff' (zero_le _) (zero_le _)
 
 @[simp] lemma le_zero_iff_eq : a ≤ 0 ↔ a = 0 :=
 iff.intro

analysis/topology/topological_space.lean

@@ -55,27 +55,23 @@ rfl
 
 variables [topological_space α]
 
-lemma is_open_union (h₁ : is_open s₁) (h₂ : is_open s₂) : is_open (s₁ ∪ s₂) :=
-have (⋃₀ {s₁, s₂}) = (s₁ ∪ s₂), from (sUnion_insert _ _).trans $ by rw [sUnion_singleton, union_comm],
-this ▸ is_open_sUnion $ show ∀(t : set α), t ∈ ({s₁, s₂} : set (set α)) → is_open t,
-  from by rintro t (rfl|⟨rfl|ht⟩); [exact h₂, exact h₁, cases ht]
-
 lemma is_open_Union {f : ι → set α} (h : ∀i, is_open (f i)) : is_open (⋃i, f i) :=
-is_open_sUnion $ assume t ⟨i, (heq : t = f i)⟩, heq.symm ▸ h i
+is_open_sUnion $ by rintro _ ⟨i, rfl⟩; exact h i
 
 lemma is_open_bUnion {s : set β} {f : β → set α} (h : ∀i∈s, is_open (f i)) :
   is_open (⋃i∈s, f i) :=
 is_open_Union $ assume i, is_open_Union $ assume hi, h i hi
 
+lemma is_open_union (h₁ : is_open s₁) (h₂ : is_open s₂) : is_open (s₁ ∪ s₂) :=
+by rw union_eq_Union; exact is_open_Union (bool.forall_bool.2 ⟨h₂, h₁⟩)
+
 @[simp] lemma is_open_empty : is_open (∅ : set α) :=
-have is_open (⋃₀ ∅ : set α), from is_open_sUnion (assume a, false.elim),
-by rwa sUnion_empty at this
+by rw ← sUnion_empty; exact is_open_sUnion (assume a, false.elim)
 
 lemma is_open_sInter {s : set (set α)} (hs : finite s) : (∀t ∈ s, is_open t) → is_open (⋂₀ s) :=
-finite.induction_on hs (λ _, by rw sInter_empty; exact is_open_univ) $ λ a s has hs ih h, begin
-  suffices : is_open (a ∩ ⋂₀ s), { rwa sInter_insert },
-  exact is_open_inter (h _ $ mem_insert _ _) (ih $ assume t ht, h _ $ mem_insert_of_mem _ ht)
-end
+finite.induction_on hs (λ _, by rw sInter_empty; exact is_open_univ) $
+λ a s has hs ih h, by rw sInter_insert; exact
+is_open_inter (h _ $ mem_insert _ _) (ih $ λ t, h t ∘ mem_insert_of_mem _)
 
 lemma is_open_bInter {s : set β} {f : β → set α} (hs : finite s) :
   (∀i∈s, is_open (f i)) → is_open (⋂i∈s, f i) :=
@@ -562,7 +558,7 @@ lemma compact_of_finite_subcover {s : set α}
   (h : ∀c, (∀t∈c, is_open t) → s ⊆ ⋃₀ c → ∃c'⊆c, finite c' ∧ s ⊆ ⋃₀ c') : compact s :=
 assume f hfn hfs, classical.by_contradiction $ assume : ¬ (∃x∈s, f ⊓ nhds x ≠ ⊥),
   have hf : ∀x∈s, nhds x ⊓ f = ⊥,
-    by simpa only [not_exists, not_not, inf_comm] using this,
+    by simpa only [not_exists, not_not, inf_comm],
   have ¬ ∃x∈s, ∀t∈f.sets, x ∈ closure t,
     from assume ⟨x, hxs, hx⟩,
     have ∅ ∈ (nhds x ⊓ f).sets, by rw [empty_in_sets_eq_bot, hf x hxs],
@@ -572,7 +568,7 @@ assume f hfn hfs, classical.by_contradiction $ assume : ¬ (∃x∈s, f ⊓ nhds
     have nhds x ⊓ principal t₂ = ⊥,
       by rwa [empty_in_sets_eq_bot] at this,
     by simp only [closure_eq_nhds] at hx; exact hx t₂ ht₂ this,
-  have ∀x∈s, ∃t∈f.sets, x ∉ closure t, by simpa only [not_exists, not_forall] using this,
+  have ∀x∈s, ∃t∈f.sets, x ∉ closure t, by simpa only [not_exists, not_forall],
   let c := (λt, - closure t) '' f.sets, ⟨c', hcc', hcf, hsc'⟩ := h c
     (assume t ⟨s, hs, h⟩, h ▸ is_closed_closure) (by simpa only [subset_def, sUnion_image, mem_Union]) in
   let ⟨b, hb⟩ := axiom_of_choice $
@@ -1022,8 +1018,7 @@ end
 
 lemma quotient_dense_of_dense [setoid α] [topological_space α] {s : set α} (H : ∀ x, x ∈ closure s) :
   closure (quotient.mk '' s) = univ :=
-begin
-  refine eq_univ_of_forall (λ x, _),
+eq_univ_of_forall $ λ x, begin
   rw mem_closure_iff,
   intros U U_op x_in_U,
   let V := quotient.mk ⁻¹' U,
@@ -1032,7 +1027,7 @@ begin
   have V_op : is_open V := U_op,
   have : V ∩ s ≠ ∅ := mem_closure_iff.1 (H y) V V_op y_in_V,
   rcases exists_mem_of_ne_empty this with ⟨w, w_in_V, w_in_range⟩,
-  exact ne_empty_of_mem ⟨by tauto, mem_image_of_mem quotient.mk w_in_range⟩
+  exact ne_empty_of_mem ⟨w_in_V, mem_image_of_mem quotient.mk w_in_range⟩
 end
 
 lemma generate_from_le {t : topological_space α} { g : set (set α) } (h : ∀s∈g, is_open s) :
@@ -1157,8 +1152,8 @@ begin
       let ⟨u, hu₁, hu₂, hu₃⟩ := hb.1 _ hs₂ _ ht₂ _ this in
       ⟨u, ⟨hu₂, hu₁⟩, le_principal_iff.2 (subset.trans hu₃ (inter_subset_left _ _)),
         le_principal_iff.2 (subset.trans hu₃ (inter_subset_right _ _))⟩ },
-  { suffices : a ∈ (⋃₀ b), { rcases this with ⟨i, h1, h2⟩, exact ⟨i, h2, h1⟩ },
-    { rw [hb.2.1], trivial } }
+  { rcases eq_univ_iff_forall.1 hb.2.1 a with ⟨i, h1, h2⟩,
+    exact ⟨i, h2, h1⟩ }
 end
 
 lemma is_open_of_is_topological_basis {s : set α} {b : set (set α)}