lint(*): split long lines (#6918)

src/control/functor/multivariate.lean

@@ -169,13 +169,18 @@ end
 open function
 variables (rr : β → β → Prop)
 
-private def f : Π (n α), (λ (i : fin2 (n + 1)), {p_1 : _ × _ // of_repeat (rel_last' α rr i (typevec.prod.mk _ p_1.fst p_1.snd))}) ⟹
+private def f :
+  Π (n α),
+    (λ (i : fin2 (n + 1)),
+      {p_1 : _ × _ // of_repeat (rel_last' α rr i (typevec.prod.mk _ p_1.fst p_1.snd))}) ⟹
     λ (i : fin2 (n + 1)), {p_1 : (α ::: β) i × _ // rel_last α rr (p_1.fst) (p_1.snd)}
 | _ α (fin2.fs i) x := ⟨ x.val, cast (by simp only [rel_last]; erw repeat_eq_iff_eq) x.property ⟩
 | _ α fin2.fz x := ⟨ x.val, x.property ⟩
 
-private def g : Π (n α), (λ (i : fin2 (n + 1)), {p_1 : (α ::: β) i × _ // rel_last α rr (p_1.fst) (p_1.snd)}) ⟹
-    (λ (i : fin2 (n + 1)), {p_1 : _ × _ // of_repeat (rel_last' α rr i (typevec.prod.mk _ p_1.fst p_1.snd))})
+private def g :
+  Π (n α), (λ (i : fin2 (n + 1)), {p_1 : (α ::: β) i × _ // rel_last α rr (p_1.fst) (p_1.snd)}) ⟹
+    (λ (i : fin2 (n + 1)),
+      {p_1 : _ × _ // of_repeat (rel_last' α rr i (typevec.prod.mk _ p_1.1 p_1.2))})
 | _ α (fin2.fs i) x := ⟨ x.val, cast (by simp only [rel_last]; erw repeat_eq_iff_eq) x.property ⟩
 | _ α fin2.fz x := ⟨ x.val, x.property ⟩
 

src/control/monad/writer.lean

@@ -150,7 +150,8 @@ implementing `monad_functor`.
 Note: This class can be seen as a simplification of the more "principled" definition
 ```
 class monad_reader_functor (ρ ρ' : out_param (Type u)) (n n' : Type u → Type u) :=
-(map {α : Type u} : (∀ {m : Type u → Type u} [monad m], reader_t ρ m α → reader_t ρ' m α) → n α → n' α)
+(map {α : Type u} :
+  (∀ {m : Type u → Type u} [monad m], reader_t ρ m α → reader_t ρ' m α) → n α → n' α)
 ```
 -/
 class monad_writer_adapter (ω ω' : out_param (Type u)) (m m' : Type u → Type v) :=

src/data/mv_polynomial/variables.lean

@@ -625,7 +625,8 @@ begin
   calc (bind₁ f φ).vars
       = (φ.support.sum (λ (x : σ →₀ ℕ), (bind₁ f) (monomial x (coeff x φ)))).vars :
         by { rw [← alg_hom.map_sum, ← φ.as_sum], }
-  ... ≤ φ.support.bUnion (λ (i : σ →₀ ℕ), ((bind₁ f) (monomial i (coeff i φ))).vars) : vars_sum_subset _ _
+  ... ≤ φ.support.bUnion (λ (i : σ →₀ ℕ), ((bind₁ f) (monomial i (coeff i φ))).vars) :
+        vars_sum_subset _ _
   ... = φ.support.bUnion (λ (d : σ →₀ ℕ), (C (coeff d φ) * ∏ i in d.support, f i ^ d i).vars) :
         by simp only [bind₁_monomial]
   ... ≤ φ.support.bUnion (λ (d : σ →₀ ℕ), d.support.bUnion (λ i, (f i).vars)) : _ -- proof below

src/data/nat/basic.lean

@@ -902,10 +902,13 @@ protected lemma div_div_self : ∀ {a b : ℕ}, b ∣ a → 0 < a → a / (a / b
   by rw [nat.div_mul_cancel (div_dvd_of_dvd h₁), nat.mul_div_cancel' h₁]
 
 lemma mod_mul_right_div_self (a b c : ℕ) : a % (b * c) / b = (a / b) % c :=
-if hb : b = 0 then by simp [hb] else if hc : c = 0 then by simp [hc]
-else by conv {to_rhs, rw ← mod_add_div a (b * c)};
-rw [mul_assoc, nat.add_mul_div_left _ _ (nat.pos_of_ne_zero hb), add_mul_mod_self_left,
-  mod_eq_of_lt (nat.div_lt_of_lt_mul (mod_lt _ (mul_pos (nat.pos_of_ne_zero hb) (nat.pos_of_ne_zero hc))))]
+begin
+  rcases (zero_le b).eq_or_lt with rfl|hb, { simp },
+  rcases (zero_le c).eq_or_lt with rfl|hc, { simp },
+  conv_rhs { rw ← mod_add_div a (b * c) },
+  rw [mul_assoc, nat.add_mul_div_left _ _ hb, add_mul_mod_self_left,
+    mod_eq_of_lt (nat.div_lt_of_lt_mul (mod_lt _ (mul_pos hb hc)))]
+end
 
 lemma mod_mul_left_div_self (a b c : ℕ) : a % (c * b) / b = (a / b) % c :=
 by rw [mul_comm c, mod_mul_right_div_self]

src/data/nat/gcd.lean

@@ -51,7 +51,8 @@ theorem gcd_assoc (m n k : ℕ) : gcd (gcd m n) k = gcd m (gcd n k) :=
 dvd_antisymm
   (dvd_gcd
     (dvd.trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_left m n))
-    (dvd_gcd (dvd.trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_right m n)) (gcd_dvd_right (gcd m n) k)))
+    (dvd_gcd (dvd.trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_right m n))
+      (gcd_dvd_right (gcd m n) k)))
   (dvd_gcd
     (dvd_gcd (gcd_dvd_left m (gcd n k)) (dvd.trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_left n k)))
     (dvd.trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_right n k)))
@@ -197,7 +198,8 @@ dvd_antisymm
     (dvd.trans (dvd_lcm_right n k) (dvd_lcm_right m (lcm n k))))
   (lcm_dvd
     (dvd.trans (dvd_lcm_left m n) (dvd_lcm_left (lcm m n) k))
-    (lcm_dvd (dvd.trans (dvd_lcm_right m n) (dvd_lcm_left (lcm m n) k)) (dvd_lcm_right (lcm m n) k)))
+    (lcm_dvd (dvd.trans (dvd_lcm_right m n) (dvd_lcm_left (lcm m n) k))
+      (dvd_lcm_right (lcm m n) k)))
 
 theorem lcm_ne_zero {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0 :=
 by { intro h, simpa [h, hm, hn] using gcd_mul_lcm m n, }

src/data/nat/modeq.lean

@@ -211,7 +211,8 @@ lemma add_div {a b c : ℕ} (hc0 : 0 < c) : (a + b) / c = a / c + b / c +
 begin
   rw [← nat.mul_right_inj hc0, ← @add_left_cancel_iff _ _ ((a + b) % c + a % c + b % c)],
   suffices : (a + b) % c + c * ((a + b) / c) + a % c + b % c =
-    a % c + c * (a / c) + (b % c + c * (b / c)) + c * (if c ≤ a % c + b % c then 1 else 0) + (a + b) % c,
+    a % c + c * (a / c) + (b % c + c * (b / c)) + c * (if c ≤ a % c + b % c then 1 else 0) +
+      (a + b) % c,
   { simpa only [mul_add, add_comm, add_left_comm, add_assoc] },
   rw [mod_add_div, mod_add_div, mod_add_div, mul_ite, add_assoc, add_assoc],
   conv_lhs { rw ← add_mod_add_ite },

src/data/nat/multiplicity.lean

@@ -140,8 +140,9 @@ calc ∑ i in finset.Ico 1 b, n / p ^ i
     = ∑ i in finset.Ico 1 b, (k + (n - k)) / p ^ i :
     by simp only [nat.add_sub_cancel' hkn]
 ... = ∑ i in finset.Ico 1 b, (k / p ^ i + (n - k) / p ^ i +
-      if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0) : by simp only [nat.add_div (pow_pos hp.pos _)]
-... = _ : begin simp only [sum_add_distrib], simp [sum_boole], end -- we have to use `sum_add_distrib` before `add_ite` fires.
+      if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0) :
+    by simp only [nat.add_div (pow_pos hp.pos _)]
+... = _ : by simp [sum_add_distrib, sum_boole]
 
 /-- The multiplity of `p` in `choose n k` is the number of carries when `k` and `n - k`
   are added in base `p`. The set is expressed by filtering `Ico 1 b` where `b`
@@ -162,7 +163,8 @@ have h₁ : multiplicity p (choose n k) + multiplicity p (k! * (n - k)!) =
   end,
 (enat.add_right_cancel_iff
   (enat.ne_top_iff_dom.2 $
-    by exact finite_nat_iff.2 ⟨ne_of_gt hp.one_lt, mul_pos (factorial_pos k) (factorial_pos (n - k))⟩)).1
+    by exact finite_nat_iff.2
+      ⟨ne_of_gt hp.one_lt, mul_pos (factorial_pos k) (factorial_pos (n - k))⟩)).1
   h₁
 
 /-- A lower bound on the multiplicity of `p` in `choose n k`. -/

src/data/nat/totient.lean

@@ -58,18 +58,20 @@ calc ∑ m in (range n.succ).filter (∣ n), φ m
           by rw [← nat.mul_div_cancel' hd, gcd_mul_left, hm.2, mul_one]⟩)
       (λ a b ha hb h, (nat.mul_right_inj hd0).1 h)
       (λ b hb, have hb : b < n ∧ gcd n b = d, by simpa using hb,
-        ⟨b / d, mem_filter.2 ⟨mem_range.2 ((mul_lt_mul_left (show 0 < d, from hb.2 ▸ hb.2.symm ▸ hd0)).1
-            (by rw [← hb.2, nat.mul_div_cancel' (gcd_dvd_left _ _),
-              nat.mul_div_cancel' (gcd_dvd_right _ _)]; exact hb.1)),
-                hb.2 ▸ coprime_div_gcd_div_gcd (hb.2.symm ▸ hd0)⟩,
+        ⟨b / d, mem_filter.2 ⟨mem_range.2
+            ((mul_lt_mul_left (show 0 < d, from hb.2 ▸ hb.2.symm ▸ hd0)).1
+              (by rw [← hb.2, nat.mul_div_cancel' (gcd_dvd_left _ _),
+                nat.mul_div_cancel' (gcd_dvd_right _ _)]; exact hb.1)),
+            hb.2 ▸ coprime_div_gcd_div_gcd (hb.2.symm ▸ hd0)⟩,
           hb.2 ▸ nat.mul_div_cancel' (gcd_dvd_right _ _)⟩))
 ... = ((filter (∣ n) (range n.succ)).bUnion (λ d, (range n).filter (λ m, gcd n m = d))).card :
   (card_bUnion (by intros; apply disjoint_filter.2; cc)).symm
 ... = (range n).card :
   congr_arg card (finset.ext (λ m, ⟨by finish,
     λ hm, have h : m < n, from mem_range.1 hm,
-      mem_bUnion.2 ⟨gcd n m, mem_filter.2 ⟨mem_range.2 (lt_succ_of_le (le_of_dvd (lt_of_le_of_lt (nat.zero_le _) h)
-        (gcd_dvd_left _ _))), gcd_dvd_left _ _⟩, mem_filter.2 ⟨hm, rfl⟩⟩⟩))
+      mem_bUnion.2 ⟨gcd n m, mem_filter.2
+        ⟨mem_range.2 (lt_succ_of_le (le_of_dvd (lt_of_le_of_lt (zero_le _) h)
+          (gcd_dvd_left _ _))), gcd_dvd_left _ _⟩, mem_filter.2 ⟨hm, rfl⟩⟩⟩))
 ... = n : card_range _
 
 end nat

src/geometry/euclidean/circumcenter.lean

@@ -541,7 +541,8 @@ def centroid_weights_with_circumcenter {n : ℕ} (fs : finset (fin (n + 1)))
 
 /-- `centroid_weights_with_circumcenter` sums to 1, if the `finset` is
 nonempty. -/
-@[simp] lemma sum_centroid_weights_with_circumcenter {n : ℕ} {fs : finset (fin (n + 1))} (h : fs.nonempty) :
+@[simp] lemma sum_centroid_weights_with_circumcenter {n : ℕ} {fs : finset (fin (n + 1))}
+  (h : fs.nonempty) :
   ∑ i, centroid_weights_with_circumcenter fs i = 1 :=
 begin
   simp_rw [sum_points_with_circumcenter, centroid_weights_with_circumcenter, add_zero,
@@ -837,17 +838,17 @@ begin
   have hd₁ : dist p₁ s.circumcenter * dist p₁ s.circumcenter =
     r * r - s.circumradius * s.circumradius,
   { rw [dist_comm, ←h₁ 0,
-        dist_square_eq_dist_orthogonal_projection_square_add_dist_orthogonal_projection_square p₁ h],
+      dist_square_eq_dist_orthogonal_projection_square_add_dist_orthogonal_projection_square p₁ h],
     simp [h₁', dist_comm p₁] },
   have hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter =
     r * r - s.circumradius * s.circumradius,
   { rw [dist_comm, ←h₂ 0,
-        dist_square_eq_dist_orthogonal_projection_square_add_dist_orthogonal_projection_square p₂ h],
+      dist_square_eq_dist_orthogonal_projection_square_add_dist_orthogonal_projection_square p₂ h],
     simp [h₂', dist_comm p₂] },
   rw [←hd₂, hp₁, hp₂, dist_eq_norm_vsub V _ s.circumcenter,
       dist_eq_norm_vsub V _ s.circumcenter, vadd_vsub, vadd_vsub, ←real_inner_self_eq_norm_square,
-      ←real_inner_self_eq_norm_square, real_inner_smul_left, real_inner_smul_left, real_inner_smul_right,
-      real_inner_smul_right, ←mul_assoc, ←mul_assoc] at hd₁,
+      ←real_inner_self_eq_norm_square, real_inner_smul_left, real_inner_smul_left,
+      real_inner_smul_right, real_inner_smul_right, ←mul_assoc, ←mul_assoc] at hd₁,
   by_cases hp : p = orthogonal_projection span_s p,
   { rw [hp₁, hp₂, ←hp],
     simp },

src/geometry/manifold/charted_space.lean

@@ -571,7 +571,7 @@ instance prod_charted_space (H : Type*) [topological_space H]
     use (charted_space.chart_at H x.1),
     split,
     { apply chart_mem_atlas _, },
-    { use (charted_space.chart_at H' x.2), simp only [chart_mem_atlas, eq_self_iff_true, and_self], }
+    { use (charted_space.chart_at H' x.2), simp only [chart_mem_atlas, and_self, true_and] }
   end }
 
 section prod_charted_space
@@ -843,7 +843,8 @@ instance [closed_under_restriction G] : has_groupoid s G :=
     simp only [hc.symm, mem_singleton_iff, subtype.val_eq_coe] at he,
     simp only [hc'.symm, mem_singleton_iff, subtype.val_eq_coe] at he',
     rw [he, he'],
-    convert G.eq_on_source _ (subtype_restr_symm_trans_subtype_restr s (chart_at H x) (chart_at H x')),
+    convert G.eq_on_source _
+      (subtype_restr_symm_trans_subtype_restr s (chart_at H x) (chart_at H x')),
     apply closed_under_restriction',
     { exact G.compatible (chart_mem_atlas H x) (chart_mem_atlas H x') },
     { exact preimage_open_of_open_symm (chart_at H x) s.2 },
@@ -888,7 +889,8 @@ def structomorph.symm (e : structomorph G M M') : structomorph G M' M :=
   ..e.to_homeomorph.symm}
 
 /-- The composition of structomorphisms is a structomorphism -/
-def structomorph.trans (e : structomorph G M M') (e' : structomorph G M' M'') : structomorph G M M'' :=
+def structomorph.trans (e : structomorph G M M') (e' : structomorph G M' M'') :
+  structomorph G M M'' :=
 { mem_groupoid := begin
     /- Let c and c' be two charts in M and M''. We want to show that e' ∘ e is smooth in these
     charts, around any point x. For this, let y = e (c⁻¹ x), and consider a chart g around y.

src/geometry/manifold/local_invariant_properties.lean

@@ -208,13 +208,14 @@ lemma lift_prop_within_at_indep_chart [has_groupoid M G] [has_groupoid M' G']
   (he : e ∈ G.maximal_atlas M) (xe : x ∈ e.source)
   (hf : f ∈ G'.maximal_atlas M') (xf : g x ∈ f.source) :
   lift_prop_within_at P g s x ↔
-  continuous_within_at g s x ∧ P (f ∘ g ∘ e.symm) (e.target ∩ e.symm ⁻¹' (s ∩ g⁻¹' f.source)) (e x) :=
+    continuous_within_at g s x ∧ P (f ∘ g ∘ e.symm)
+      (e.target ∩ e.symm ⁻¹' (s ∩ g⁻¹' f.source)) (e x) :=
 ⟨λ H, ⟨H.1,
   hG.lift_prop_within_at_indep_chart_aux (chart_mem_maximal_atlas _ _) (mem_chart_source _ _) he xe
   (chart_mem_maximal_atlas _ _) (mem_chart_source _ _) hf xf H.1 H.2⟩,
 λ H, ⟨H.1,
-  hG.lift_prop_within_at_indep_chart_aux he xe (chart_mem_maximal_atlas _ _) (mem_chart_source _ _) hf xf
-  (chart_mem_maximal_atlas _ _) (mem_chart_source _ _) H.1 H.2⟩⟩
+  hG.lift_prop_within_at_indep_chart_aux he xe (chart_mem_maximal_atlas _ _) (mem_chart_source _ _)
+    hf xf (chart_mem_maximal_atlas _ _) (mem_chart_source _ _) H.1 H.2⟩⟩
 
 lemma lift_prop_on_indep_chart [has_groupoid M G] [has_groupoid M' G']
   (he : e ∈ G.maximal_atlas M) (hf : f ∈ G'.maximal_atlas M') (h : lift_prop_on P g s) :
@@ -384,8 +385,8 @@ begin
   exact lift_prop_within_at_mono mono h (subset_univ _),
 end
 
-lemma lift_prop_on_mono
-  (mono : ∀ ⦃s x t⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x) (h : lift_prop_on P g t) (hst : s ⊆ t) :
+lemma lift_prop_on_mono (mono : ∀ ⦃s x t⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x)
+  (h : lift_prop_on P g t) (hst : s ⊆ t) :
   lift_prop_on P g s :=
 λ x hx, lift_prop_within_at_mono mono (h x (hst hx)) hst
 
@@ -430,7 +431,8 @@ begin
   { have A : e.symm ⁻¹' e.source ∩ e.target = e.target,
       by mfld_set_tac,
     have : e.symm x ∈ e.source, by simp only [hx] with mfld_simps,
-    rw [lift_prop_at, hG.lift_prop_within_at_indep_chart G.id_mem_maximal_atlas (mem_univ _) he this],
+    rw [lift_prop_at,
+      hG.lift_prop_within_at_indep_chart G.id_mem_maximal_atlas (mem_univ _) he this],
     refine ⟨(e.symm.continuous_at hx).continuous_within_at, _⟩,
     simp only with mfld_simps,
     rwa [hG.is_local e.open_target hx, A] },

src/meta/coinductive_predicates.lean

@@ -9,7 +9,8 @@ section
 universe u
 
 @[user_attribute]
-meta def monotonicity : user_attribute := { name := `monotonicity, descr := "Monotonicity rules for predicates" }
+meta def monotonicity : user_attribute :=
+{ name := `monotonicity, descr := "Monotonicity rules for predicates" }
 
 lemma monotonicity.pi {α : Sort u} {p q : α → Prop} (h : ∀a, implies (p a) (q a)) :
   implies (Πa, p a) (Πa, q a) :=
@@ -73,8 +74,10 @@ private meta def mono_aux (ns : list name) (hs : list expr) : tactic unit := do
         let q' := qb.lower_vars 0 1,
         eapply ((const `monotonicity.imp []: expr) pd p' qd q'),
         skip))) <|>
-  first (hs.map $ λh, apply_core h {md := transparency.none, new_goals := new_goals.non_dep_only} >> skip) <|>
-  first (ns.map $ λn, do c ← mk_const n, apply_core c {md := transparency.none, new_goals := new_goals.non_dep_only}, skip),
+  first (hs.map $ λh,
+    apply_core h {md := transparency.none, new_goals := new_goals.non_dep_only} >> skip) <|>
+  first (ns.map $ λn, do c ← mk_const n,
+    apply_core c {md := transparency.none, new_goals := new_goals.non_dep_only}, skip),
   all_goals' mono_aux
 
 meta def mono (e : expr) (hs : list expr) : tactic unit := do
@@ -112,7 +115,8 @@ where
   def {u} pred_i (A) (a) : Prop :=
   ∃[pred'], (Λi, ∀a, pred_i a → pred_i.functional A [pred] a) ∧ pred'_i a
 
-  lemma {u} pred_i.corec_functional (A) [Λi, C_i : a_i → Prop] [Λi, h : ∀a, C_i a → pred_i.functional A C_i a] :
+  lemma {u} pred_i.corec_functional (A) [Λi, C_i : a_i → Prop]
+    [Λi, h : ∀a, C_i a → pred_i.functional A C_i a] :
     ∀a, C_i a → pred_i A a
 
   lemma {u} pred_i.destruct (A) (a) : pred A a → pred.functional A [pred A] a
@@ -278,7 +282,8 @@ meta def add_coinductive_predicate
       let t := instantiate_local pd.f₂.local_uniq_name (pd.func_g.app_of_list fs₁) r.loc_type,
       return (r.func_nm, r.orig_nm, t.pis $ params ++ fs₁)),
     add_inductive pd.func.const_name u_names
-      (params.length + preds.length) (pd.type.pis $ params ++ fs₁) (func_intros.map $ λ⟨t, _, r⟩, (t, r)),
+      (params.length + preds.length) (pd.type.pis $ params ++ fs₁)
+        (func_intros.map $ λ⟨t, _, r⟩, (t, r)),
 
     /- Prove monotonicity rule -/
     mono_params ← pds.mmap (λpd, do
@@ -292,15 +297,16 @@ meta def add_coinductive_predicate
         [f₁, f₂, h] ← intro_lst [pd.f₁.local_pp_name, pd.f₂.local_pp_name, `h],
         -- the type of h' reduces to h
         let h' := local_const h.local_uniq_name h.local_pp_name h.local_binding_info $
-          (((const `implies [] : expr)
-            (f₁.app_of_list pd.locals) (f₂.app_of_list pd.locals)).pis pd.locals).instantiate_locals $
+          (((const `implies [] : expr) (f₁.app_of_list pd.locals)
+            (f₂.app_of_list pd.locals)).pis pd.locals).instantiate_locals $
           (ps.zip params).map $ λ⟨lv, p⟩, (p.local_uniq_name, lv),
         return (f₂, h')),
       m ← pd.rec',
       eapply $ m.app_of_list ps, -- somehow `induction` / `cases` doesn't work?
       func_intros.mmap' (λ⟨n, pp_n, t⟩, solve1 $ do
         bs ← intros,
-        ms ← apply_core ((const n u_params).app_of_list $ ps ++ fs.map prod.fst) {new_goals := new_goals.all},
+        ms ← apply_core
+          ((const n u_params).app_of_list $ ps ++ fs.map prod.fst) {new_goals := new_goals.all},
         params ← (ms.zip bs).enum.mfilter (λ⟨n, m, d⟩, bnot <$> is_assigned m.2),
         params.mmap' (λ⟨n, m, d⟩, mono d (fs.map prod.snd) <|>
           fail format! "failed to prove montonoicity of {n+1}. parameter of intro-rule {pp_n}")))),
@@ -435,7 +441,8 @@ meta def add_coinductive_predicate
       ps ← intro_lst $ params.map local_pp_name,
       bs ← intros,
       eapply $ pd.construct,
-      exact $ (const r.func_nm u_params).app_of_list $ ps ++ pds.map (λpd, pd.pred.app_of_list ps) ++ bs)),
+      exact $ (const r.func_nm u_params).app_of_list $
+        ps ++ pds.map (λpd, pd.pred.app_of_list ps) ++ bs)),
 
   pds.mmap' (λpd:coind_pred, set_basic_attribute `irreducible pd.pd_name),
 
@@ -445,16 +452,16 @@ open lean.parser
 open interactive
 
 @[user_command]
-meta def coinductive_predicate (meta_info : decl_meta_info) (_ : parse $ tk "coinductive") : lean.parser unit := do
-  decl ← inductive_decl.parse meta_info,
+meta def coinductive_predicate (meta_info : decl_meta_info) (_ : parse $ tk "coinductive") :
+  lean.parser unit := do
+{ decl ← inductive_decl.parse meta_info,
   add_coinductive_predicate decl.u_names decl.params $ decl.decls.map $ λ d, (d.sig, d.intros),
-  decl.decls.mmap' $ λ d, do {
-    get_env >>= λ env, set_env $ env.add_namespace d.name,
+  decl.decls.mmap' $ λ d, do
+  { get_env >>= λ env, set_env $ env.add_namespace d.name,
     meta_info.attrs.apply d.name,
     d.attrs.apply d.name,
     some doc_string ← pure meta_info.doc_string | skip,
-    add_doc_string d.name doc_string
-  }
+    add_doc_string d.name doc_string } }
 
 /-- Prepares coinduction proofs. This tactic constructs the coinduction invariant from
 the quantifiers in the current goal.
@@ -485,7 +492,8 @@ do
     exact (rel.lambdas is)),
   -- prove predicate
   solve1 (do
-    target >>= instantiate_mvars >>= change, -- TODO: bug in existsi & constructor when mvars in hyptohesis
+    target >>= instantiate_mvars >>= change,
+    -- TODO: bug in existsi & constructor when mvars in hyptohesis
     bs.mmap existsi,
     iterate' (econstructor >> skip)),