feat(tactic): add support for quotients to rcases

analysis/topology/topological_structures.lean

@@ -77,15 +77,15 @@ variables [topological_space α] [comm_monoid α] [topological_monoid α]
 lemma tendsto_multiset_prod {f : γ → β → α} {x : filter β} {a : γ → α} (s : multiset γ) :
   (∀c∈s, tendsto (f c) x (nhds (a c))) →
     tendsto (λb, (s.map (λc, f c b)).prod) x (nhds ((s.map a).prod)) :=
-quot.induction_on s $ by simp; exact tendsto_list_prod
+by { rcases s with ⟨l⟩, simp, exact tendsto_list_prod l }
 
 lemma tendsto_finset_prod {f : γ → β → α} {x : filter β} {a : γ → α} (s : finset γ) :
   (∀c∈s, tendsto (f c) x (nhds (a c))) → tendsto (λb, s.prod (λc, f c b)) x (nhds (s.prod a)) :=
 tendsto_multiset_prod _
 
 lemma continuous_multiset_prod [topological_space β] {f : γ → β → α} (s : multiset γ) :
   (∀c∈s, continuous (f c)) → continuous (λa, (s.map (λc, f c a)).prod) :=
-quot.induction_on s $ by simp; exact continuous_list_prod
+by { rcases s with ⟨l⟩, simp, exact continuous_list_prod l }
 
 lemma continuous_finset_prod [topological_space β] {f : γ → β → α} (s : finset γ) :
   (∀c∈s, continuous (f c)) → continuous (λa, s.prod (λc, f c a)) :=
@@ -142,18 +142,18 @@ end
 section
 variables [topological_space α] [add_comm_monoid α] [topological_add_monoid α]
 
-lemma tendsto_multiset_sum {f : γ → β → α} {x : filter β} {a : γ → α} (s : multiset γ) :
-  (∀c∈s, tendsto (f c) x (nhds (a c))) →
+lemma tendsto_multiset_sum {f : γ → β → α} {x : filter β} {a : γ → α} :
+  ∀ (s : multiset γ), (∀c∈s, tendsto (f c) x (nhds (a c))) →
     tendsto (λb, (s.map (λc, f c b)).sum) x (nhds ((s.map a).sum)) :=
-quot.induction_on s $ by simp; exact tendsto_list_sum
+by rintros ⟨l⟩; simp; exact tendsto_list_sum l
 
 lemma tendsto_finset_sum {f : γ → β → α} {x : filter β} {a : γ → α} (s : finset γ) :
   (∀c∈s, tendsto (f c) x (nhds (a c))) → tendsto (λb, s.sum (λc, f c b)) x (nhds (s.sum a)) :=
 tendsto_multiset_sum _
 
-lemma continuous_multiset_sum [topological_space β] {f : γ → β → α} (s : multiset γ) :
-  (∀c∈s, continuous (f c)) → continuous (λa, (s.map (λc, f c a)).sum) :=
-quot.induction_on s $ by simp; exact continuous_list_sum
+lemma continuous_multiset_sum [topological_space β] {f : γ → β → α} :
+  ∀(s : multiset γ), (∀c∈s, continuous (f c)) → continuous (λa, (s.map (λc, f c a)).sum) :=
+by rintros ⟨l⟩; simp; exact continuous_list_sum l
 
 lemma continuous_finset_sum [topological_space β] {f : γ → β → α} (s : finset γ) :
   (∀c∈s, continuous (f c)) → continuous (λa, s.sum (λc, f c a)) :=

data/equiv/encodable.lean

@@ -285,7 +285,6 @@ choose_spec (exists_rep q)
 def encodable_quotient : encodable (quotient s) :=
 ⟨λ q, encode (rep q),
  λ n, quotient.mk <$> decode α n,
- λ q, quot.induction_on q $ λ l,
-   by rw encodek; exact congr_arg some (rep_spec _)⟩
+ by rintros ⟨l⟩; rw encodek; exact congr_arg some (rep_spec _)⟩
 
 end quot

data/multiset.lean

@@ -79,13 +79,12 @@ theorem singleton_coe (a : α) : (a::0 : multiset α) = ([a] : list α) := rfl
   have [a] ++ l ~ [b] ++ l, from quotient.exact e,
   eq_singleton_of_perm $ (perm_app_right_iff _).1 this, congr_arg _⟩
 
-@[simp] theorem cons_inj_right (a : α) {s t : multiset α} :
-  a::s = a::t ↔ s = t :=
-quotient.induction_on₂ s t $ λ l₁ l₂, by simp [perm_cons]
+@[simp] theorem cons_inj_right (a : α) : ∀{s t : multiset α}, a::s = a::t ↔ s = t :=
+by rintros ⟨l₁⟩ ⟨l₂⟩; simp [perm_cons]
 
 @[recursor 5] protected theorem induction {p : multiset α → Prop}
-  (h₁ : p 0) (h₂ : ∀ ⦃a : α⦄ {s : multiset α}, p s → p (a :: s)) (s) : p s :=
-quot.induction_on s $ λ l, by induction l with _ _ ih; [exact h₁, exact h₂ ih]
+  (h₁ : p 0) (h₂ : ∀ ⦃a : α⦄ {s : multiset α}, p s → p (a :: s)) : ∀s, p s :=
+by rintros ⟨l⟩; induction l with _ _ ih; [exact h₁, exact h₂ ih]
 
 @[elab_as_eliminator] protected theorem induction_on {p : multiset α → Prop}
   (s : multiset α) (h₁ : p 0) (h₂ : ∀ ⦃a : α⦄ {s : multiset α}, p s → p (a :: s)) : p s :=
@@ -245,11 +244,10 @@ quotient.lift_on₂ s t (<+~) $ λ v₁ v₂ w₁ w₂ p₁ p₂,
   propext (p₂.subperm_left.trans p₁.subperm_right)
 
 instance : partial_order (multiset α) :=
-{ le := multiset.le,
-  le_refl := λ s, quot.induction_on s $ λ l, subperm.refl _,
-  le_trans := λ s t u, quotient.induction_on₃ s t u $ @subperm.trans _,
-  le_antisymm := λ s t, quotient.induction_on₂ s t $
-    λ l₁ l₂ h₁ h₂, quot.sound (subperm.antisymm h₁ h₂) }
+{ le          := multiset.le,
+  le_refl     := by rintros ⟨l⟩; exact subperm.refl _,
+  le_trans    := by rintros ⟨l₁⟩ ⟨l₂⟩ ⟨l₃⟩; exact @subperm.trans _ _ _ _,
+  le_antisymm := by rintros ⟨l₁⟩ ⟨l₂⟩ h₁ h₂; exact quot.sound (subperm.antisymm h₁ h₂) }
 
 theorem subset_of_le {s t : multiset α} : s ≤ t → s ⊆ t :=
 quotient.induction_on₂ s t $ λ l₁ l₂, subset_of_subperm

data/quot.lean

@@ -169,7 +169,7 @@ theorem nonempty_of_trunc (q : trunc α) : nonempty α :=
 let ⟨a, _⟩ := q.exists_rep in ⟨a⟩
 
 namespace quotient
-variables {γ : Sort*} {φ : Sort*} 
+variables {γ : Sort*} {φ : Sort*}
   {s₁ : setoid α} {s₂ : setoid β} {s₃ : setoid γ}
 
 /- Versions of quotient definitions and lemmas ending in `'` use unification instead
@@ -179,7 +179,7 @@ several different quotient relations on a type, for example quotient groups, rin
 protected def mk' (a : α) : quotient s₁ := quot.mk s₁.1 a
 
 @[elab_as_eliminator, reducible]
-protected def lift_on' (q : quotient s₁) (f : α → φ) 
+protected def lift_on' (q : quotient s₁) (f : α → φ)
   (h : ∀ a b, @setoid.r α s₁ a b → f a = f b) : φ := quotient.lift_on q f h
 
 @[elab_as_eliminator, reducible]
@@ -197,12 +197,12 @@ protected lemma induction_on₂' {p : quotient s₁ → quotient s₂ → Prop}
 quotient.induction_on₂ q₁ q₂ h
 
 @[elab_as_eliminator]
-protected lemma induction_on₃' {p : quotient s₁ → quotient s₂ → quotient s₃ → Prop} 
-  (q₁ : quotient s₁) (q₂ : quotient s₂) (q₃ : quotient s₃) 
+protected lemma induction_on₃' {p : quotient s₁ → quotient s₂ → quotient s₃ → Prop}
+  (q₁ : quotient s₁) (q₂ : quotient s₂) (q₃ : quotient s₃)
   (h : ∀ a₁ a₂ a₃, p (quotient.mk' a₁) (quotient.mk' a₂) (quotient.mk' a₃)) : p q₁ q₂ q₃ :=
 quotient.induction_on₃ q₁ q₂ q₃ h
 
-lemma exact' {a b : α} : 
+lemma exact' {a b : α} :
   (quotient.mk' a : quotient s₁) = quotient.mk' b → @setoid.r _ s₁ a b :=
 quotient.exact
 
@@ -217,6 +217,6 @@ noncomputable def out' (a : quotient s₁) : α := quotient.out a
 @[simp] theorem out_eq' (q : quotient s₁) : quotient.mk' q.out' = q := q.out_eq
 
 theorem mk_out' (a : α) : @setoid.r α s₁ (quotient.mk' a).out a :=
-quotient.exact (quotient.out_eq _) 
+quotient.exact (quotient.out_eq _)
 
 end quotient

docs/tactics.md

@@ -26,6 +26,9 @@ arguments, such as `⟨a, b, c⟩` for splitting on `∃ x, ∃ y, p x`, then it
 will be treated as `⟨a, ⟨b, c⟩⟩`, splitting the last parameter as
 necessary.
 
+`rcases` also has special support for quotient types: quotient induction into Prop works like
+matching on the constructor `quot.mk`.
+
 `rcases? e` will perform case splits on `e` in the same way as `rcases e`,
 but rather than accepting a pattern, it does a maximal cases and prints the
 pattern that would produce this case splitting. The default maximum depth is 5,
@@ -273,7 +276,7 @@ structure A :=
 example (z : A) : z.x = 1 := by rw A.a' -- rewrite tactic failed, lemma is not an equality nor a iff
 
 restate_axiom A.a'
-example (z : A) : z.x = 1 := by rw A.a 
+example (z : A) : z.x = 1 := by rw A.a
 ```
 
 By default, `restate_axiom` names the new lemma by removing a trailing `'`, or otherwise appending
@@ -303,36 +306,36 @@ the goal and recursively on new goals, until no tactic makes further progress.
 
 `tidy` can report the tactic script it found using `tidy { trace_result := tt }`. As an example
 ```
-example : ∀ x : unit, x = unit.star := 
+example : ∀ x : unit, x = unit.star :=
 begin
   tidy {trace_result:=tt} -- Prints the trace message: "intros x, exact dec_trivial"
 end
 ```
 
-The default list of tactics can be found by looking up the definition of 
+The default list of tactics can be found by looking up the definition of
 [`default_tidy_tactics`](https://github.com/leanprover/mathlib/blob/master/tactic/tidy.lean).
 
 This list can be overriden using `tidy { tactics :=  ... }`. (The list must be a list of `tactic string`.)
 
 ## linarith
 
 `linarith` attempts to find a contradiction between hypotheses that are linear (in)equalities.
-Equivalently, it can prove a linear inequality by assuming its negation and proving `false`. 
-This tactic is currently work in progress, and has various limitations. In particular, 
+Equivalently, it can prove a linear inequality by assuming its negation and proving `false`.
+This tactic is currently work in progress, and has various limitations. In particular,
 it will not work on `nat`. The tactic can be made much more efficient.
 
-An example: 
+An example:
 ```
-example (x y z : ℚ) (h1 : 2*x  < 3*y) (h2 : -4*x + 2*z < 0) 
+example (x y z : ℚ) (h1 : 2*x  < 3*y) (h2 : -4*x + 2*z < 0)
         (h3 : 12*y - 4* z < 0)  : false :=
 by linarith
 ```
 
 `linarith` will use all appropriate hypotheses and the negation of the goal, if applicable.
 `linarith h1 h2 h3` will ohly use the local hypotheses `h1`, `h2`, `h3`.
-`linarith using [t1, t2, t3] will add `t1`, `t2`, `t3` to the local context and then run 
+`linarith using [t1, t2, t3] will add `t1`, `t2`, `t3` to the local context and then run
 `linarith`.
-`linarith {discharger := tac, restrict_type := tp}` takes a config object with two optional 
+`linarith {discharger := tac, restrict_type := tp}` takes a config object with two optional
 arguments. `discharger` specifies a tactic to be used for reducing an algebraic equation in the
 proof stage. The default is `ring`. Other options currently include `ring SOP` or `simp` for basic
 problems. `restrict_type` will only use hypotheses that are inequalities over `tp`. This is useful

group_theory/free_group.lean

@@ -341,12 +341,11 @@ instance : group (free_group α) :=
 { mul := (*),
   one := 1,
   inv := has_inv.inv,
-  mul_assoc := λ x y z, quot.induction_on x $ λ L₁,
-    quot.induction_on y $ λ L₂, quot.induction_on z $ λ L₃, by simp,
-  one_mul := λ x, quot.induction_on x $ λ L, rfl,
-  mul_one := λ x, quot.induction_on x $ λ L, by simp [one_eq_mk],
-  mul_left_inv := λ x, quot.induction_on x $ λ L, list.rec_on L rfl $
-    λ ⟨x, b⟩ tl ih, eq.trans (quot.sound $ by simp [one_eq_mk]) ih }
+  mul_assoc := by rintros ⟨L₁⟩ ⟨L₂⟩ ⟨L₃⟩; simp,
+  one_mul := by rintros ⟨L⟩; refl,
+  mul_one := by rintros ⟨L⟩; simp [one_eq_mk],
+  mul_left_inv := by rintros ⟨L⟩; exact (list.rec_on L rfl $
+    λ ⟨x, b⟩ tl ih, eq.trans (quot.sound $ by simp [one_eq_mk]) ih) }
 
 /-- `of x` is the canonical injection from the type to the free group over that type by sending each
 element to the equivalence class of the letter that is the element. -/
@@ -389,7 +388,7 @@ rfl
 one_mul _
 
 instance to_group.is_group_hom : is_group_hom (to_group f) :=
-⟨λ x y, quot.induction_on x $ λ L₁, quot.induction_on y $ λ L₂, by simp⟩
+⟨by rintros ⟨L₁⟩ ⟨L₂⟩; simp⟩
 
 @[simp] lemma to_group.mul : to_group f (x * y) = to_group f x * to_group f y :=
 is_group_hom.mul _ _ _
@@ -401,26 +400,25 @@ is_group_hom.one _
 is_group_hom.inv _ _
 
 theorem to_group.unique (g : free_group α → β) [is_group_hom g]
-  (hg : ∀ x, g (of x) = f x) {x} :
-  g x = to_group f x :=
-quot.induction_on x $ λ L, list.rec_on L (is_group_hom.one g) $
-λ ⟨x, b⟩ t (ih : g (mk t) = _), bool.rec_on b
+  (hg : ∀ x, g (of x) = f x) : ∀{x}, g x = to_group f x :=
+by rintros ⟨L⟩; exact list.rec_on L (is_group_hom.one g)
+(λ ⟨x, b⟩ t (ih : g (mk t) = _), bool.rec_on b
   (show g ((of x)⁻¹ * mk t) = to_group f (mk ((x, ff) :: t)),
      by simp [is_group_hom.mul g, is_group_hom.inv g, hg, ih, to_group, to_group.aux])
   (show g (of x * mk t) = to_group f (mk ((x, tt) :: t)),
-     by simp [is_group_hom.mul g, is_group_hom.inv g, hg, ih, to_group, to_group.aux])
+     by simp [is_group_hom.mul g, is_group_hom.inv g, hg, ih, to_group, to_group.aux]))
+
 
 theorem to_group.of_eq (x : free_group α) : to_group of x = x :=
 eq.symm $ to_group.unique id (λ x, rfl)
 
 theorem to_group.range_subset {s : set β} [is_subgroup s] (H : set.range f ⊆ s) :
   set.range (to_group f) ⊆ s :=
-λ y ⟨x, H1⟩, H1 ▸ (quot.induction_on x $ λ L,
-list.rec_on L (is_submonoid.one_mem s) $ λ ⟨x, b⟩ tl ih,
-bool.rec_on b
-  (by simp at ih ⊢; from is_submonoid.mul_mem
-    (is_subgroup.inv_mem $ H ⟨x, rfl⟩) ih)
-  (by simp at ih ⊢; from is_submonoid.mul_mem (H ⟨x, rfl⟩) ih))
+by rintros _ ⟨⟨L⟩, rfl⟩; exact list.rec_on L (is_submonoid.one_mem s)
+(λ ⟨x, b⟩ tl ih, bool.rec_on b
+    (by simp at ih ⊢; from is_submonoid.mul_mem
+      (is_subgroup.inv_mem $ H ⟨x, rfl⟩) ih)
+    (by simp at ih ⊢; from is_submonoid.mul_mem (H ⟨x, rfl⟩) ih))
 
 theorem to_group.range_eq_closure :
   set.range (to_group f) = group.closure (set.range f) :=
@@ -445,8 +443,7 @@ x.lift_on (λ L, mk $ map.aux f L) $
 λ L₁ L₂ H, quot.sound $ by cases H; simp [map.aux]
 
 instance map.is_group_hom : is_group_hom (map f) :=
-⟨λ x y, quot.induction_on x $ λ L₁, quot.induction_on y $ λ L₂,
-by simp [map, map.aux]⟩
+⟨by rintros ⟨L₁⟩ ⟨L₂⟩; simp [map, map.aux]⟩
 
 variable {f}
 
@@ -455,13 +452,13 @@ rfl
 
 @[simp] lemma map.id : map id x = x :=
 have H1 : (λ (x : α × bool), x) = id := rfl,
-quot.induction_on x $ λ L, by simp [H1]
+by rcases x with ⟨L⟩; simp [H1]
 
 @[simp] lemma map.id' : map (λ z, z) x = x := map.id
 
 theorem map.comp {γ : Type*} {f : α → β} {g : β → γ} {x} :
   map g (map f x) = map (g ∘ f) x :=
-quot.induction_on x $ λ L, by simp
+by rcases x with ⟨L⟩; simp
 
 @[simp] lemma map.of {x} : map f (of x) = of (f x) := rfl
 
@@ -475,14 +472,13 @@ is_group_hom.one _
 is_group_hom.inv _ x
 
 theorem map.unique (g : free_group α → free_group β) [is_group_hom g]
-  (hg : ∀ x, g (of x) = of (f x)) {x} :
-  g x = map f x :=
-quot.induction_on x $ λ L, list.rec_on L (is_group_hom.one g) $
-λ ⟨x, b⟩ t (ih : g (mk t) = map f (mk t)), bool.rec_on b
+  (hg : ∀ x, g (of x) = of (f x)) : ∀{x}, g x = map f x :=
+by rintros ⟨L⟩; exact list.rec_on L (is_group_hom.one g)
+(λ ⟨x, b⟩ t (ih : g (mk t) = map f (mk t)), bool.rec_on b
   (show g ((of x)⁻¹ * mk t) = map f ((of x)⁻¹ * mk t),
      by simp [is_group_hom.mul g, is_group_hom.inv g, hg, ih])
   (show g (of x * mk t) = map f (of x * mk t),
-     by simp [is_group_hom.mul g, hg, ih])
+     by simp [is_group_hom.mul g, hg, ih]))
 
 /-- Equivalent types give rise to equivalent free groups. -/
 def free_group_congr {α β} (e : α ≃ β) : free_group α ≃ free_group β :=
@@ -575,15 +571,14 @@ end sum
 def free_group_empty_equiv_unit : free_group empty ≃ unit :=
 { to_fun    := λ _, (),
   inv_fun   := λ _, 1,
-  left_inv  := λ x, quot.induction_on x $ λ L,
-    match L with [] := rfl end,
+  left_inv  := by rintros ⟨_ | ⟨⟨⟨⟩, _⟩, _⟩⟩; refl,
   right_inv := λ ⟨⟩, rfl }
 
 def free_group_unit_equiv_int : free_group unit ≃ int :=
 { to_fun    := λ x, sum $ map (λ _, 1) x,
   inv_fun   := λ x, of () ^ x,
-  left_inv  := λ x, quot.induction_on x $ λ L, list.rec_on L rfl $
-    λ ⟨⟨⟩, b⟩ tl ih, by cases b; simp [gpow_add] at ih ⊢; rw ih; refl,
+  left_inv  := by rintros ⟨L⟩; exact list.rec_on L rfl
+    (λ ⟨⟨⟩, b⟩ tl ih, by cases b; simp [gpow_add] at ih ⊢; rw ih; refl),
   right_inv := λ x, int.induction_on x (by simp)
     (λ i ih, by simp at ih; simp [gpow_add, ih])
     (λ i ih, by simp at ih; simp [gpow_add, ih]) }
@@ -710,11 +705,11 @@ group to its maximal reduction. -/
 def to_word : free_group α → list (α × bool) :=
 quot.lift reduce $ λ L₁ L₂ H, reduce.step.eq H
 
-def to_word.mk {x : free_group α} : mk (to_word x) = x :=
-quot.induction_on x $ λ L₁, reduce.self
+def to_word.mk : ∀{x : free_group α}, mk (to_word x) = x :=
+by rintros ⟨L⟩; exact reduce.self
 
-def to_word.inj (x y : free_group α) : to_word x = to_word y → x = y :=
-quot.induction_on x $ λ L₁, quot.induction_on y $ λ L₂, reduce.exact
+def to_word.inj : ∀(x y : free_group α), to_word x = to_word y → x = y :=
+by rintros ⟨L₁⟩ ⟨L₂⟩; exact reduce.exact
 
 /-- Constructive Church-Rosser theorem (compare `church_rosser`). -/
 def reduce.church_rosser (H12 : red L₁ L₂) (H13 : red L₁ L₃) :

ring_theory/associated.lean

@@ -273,11 +273,11 @@ variables [comm_semiring α]
 @[simp] theorem mk_zero_eq (a : α) : associates.mk a = 0 ↔ a = 0 :=
 ⟨assume h, (associated_zero_iff_eq_zero a).1 $ quotient.exact h, assume h, h.symm ▸ rfl⟩
 
-@[simp] theorem mul_zero (a : associates α) : a * 0 = 0 :=
-quot.induction_on a $ assume a, show associates.mk (a * 0) = associates.mk 0, by rw [mul_zero]
+@[simp] theorem mul_zero : ∀(a : associates α), a * 0 = 0 :=
+by rintros ⟨a⟩; show associates.mk (a * 0) = associates.mk 0; rw [mul_zero]
 
-@[simp] theorem zero_mul (a : associates α) : 0 * a = 0 :=
-quot.induction_on a $ assume a, show associates.mk (0 * a) = associates.mk 0, by rw [zero_mul]
+@[simp] theorem zero_mul : ∀(a : associates α), 0 * a = 0 :=
+by rintros ⟨a⟩; show associates.mk (0 * a) = associates.mk 0; rw [zero_mul]
 
 theorem mk_eq_zero_iff_eq_zero {a : α} : associates.mk a = 0 ↔ a = 0 :=
 calc associates.mk a = 0 ↔ (a ~ᵤ 0) :  mk_eq_mk_iff_associated

ring_theory/unique_factorization_domain.lean

@@ -66,14 +66,11 @@ theorem prod_le_prod_iff_le {p q : multiset (associates α)}
   p.prod ≤ q.prod ↔ p ≤ q :=
 iff.intro
   begin
-    rintros ⟨c, eq⟩,
-    have : c ≠ 0, from assume hc,
-      have q.prod = 0, by simp * at *,
-      have (0 : associates α) ∈ q, from prod_eq_zero_iff.1 this,
-      not_irreducible_zero ((irreducible_mk_iff 0).1 $ hq _ this),
-
-    induction c using quot.induction_on,
-    have : c ≠ 0, from mt mk_eq_zero_iff_eq_zero.2 this,
+    rintros ⟨⟨c⟩, eq⟩,
+    have : c ≠ 0, from (mt mk_eq_zero_iff_eq_zero.2 $
+      assume (hc : quot.mk setoid.r c = 0),
+      have (0 : associates α) ∈ q, from prod_eq_zero_iff.1 $ eq ▸ hc.symm ▸ mul_zero _,
+      not_irreducible_zero ((irreducible_mk_iff 0).1 $ hq _ this)),
     have : associates.mk (factors c).prod = quot.mk setoid.r c,
       from mk_eq_mk_iff_associated.2 (factors_prod this),
 
@@ -150,7 +147,7 @@ theorem prod_factors : ∀(s : factor_set α), s.prod.factors = s
   begin
     unfold factor_set.prod,
     generalize eq_a : (s.map subtype.val).prod = a,
-    induction a using quot.induction_on,
+    rcases a with ⟨a⟩,
     rw quot_mk_eq_mk at *,
 
     have : (s.map subtype.val).prod ≠ 0, from assume ha,