refactor(*): remove uses of @[class] def (#6028)

Preparation for lean 4, which does not support this idiom.

src/algebra/associated.lean

@@ -125,8 +125,9 @@ end
 We explicitly avoid stating that `p` is non-zero, this would require a semiring. Assuming only a
 monoid allows us to reuse irreducible for associated elements.
 -/
-@[class] def irreducible [monoid α] (p : α) : Prop :=
-¬ is_unit p ∧ ∀a b, p = a * b → is_unit a ∨ is_unit b
+class irreducible [monoid α] (p : α) : Prop :=
+(not_unit' : ¬ is_unit p)
+(is_unit_or_is_unit' : ∀a b, p = a * b → is_unit a ∨ is_unit b)
 
 namespace irreducible
 
@@ -135,12 +136,16 @@ hp.1
 
 lemma is_unit_or_is_unit [monoid α] {p : α} (hp : irreducible p) {a b : α} (h : p = a * b) :
   is_unit a ∨ is_unit b :=
-hp.2 a b h
+irreducible.is_unit_or_is_unit' a b h
 
 end irreducible
 
+lemma irreducible_iff [monoid α] {p : α} :
+  irreducible p ↔ ¬ is_unit p ∧ ∀a b, p = a * b → is_unit a ∨ is_unit b :=
+⟨λ h, ⟨h.1, h.2⟩, λ h, ⟨h.1, h.2⟩⟩
+
 @[simp] theorem not_irreducible_one [monoid α] : ¬ irreducible (1 : α) :=
-by simp [irreducible]
+by simp [irreducible_iff]
 
 @[simp] theorem not_irreducible_zero [monoid_with_zero α] : ¬ irreducible (0 : α)
 | ⟨hn0, h⟩ := have is_unit (0:α) ∨ is_unit (0:α), from h 0 0 ((mul_zero 0).symm),
@@ -158,7 +163,7 @@ theorem irreducible_or_factor {α} [monoid α] (x : α) (h : ¬ is_unit x) :
 begin
   haveI := classical.dec,
   refine or_iff_not_imp_right.2 (λ H, _),
-  simp [h, irreducible] at H ⊢,
+  simp [h, irreducible_iff] at H ⊢,
   refine λ a b h, classical.by_contradiction $ λ o, _,
   simp [not_or_distrib] at o,
   exact H _ o.1 _ o.2 h.symm
@@ -287,7 +292,7 @@ multiset.induction_on s (by simp [mt is_unit_iff_dvd_one.2 hp.not_unit])
     { use [a, by simp],
       cases h with u hu,
       cases ((irreducible_of_prime (hs a (multiset.mem_cons.2
-        (or.inl rfl)))).2 p u hu).resolve_left hp.not_unit with v hv,
+        (or.inl rfl)))).is_unit_or_is_unit hu).resolve_left hp.not_unit with v hv,
       exact ⟨v, by simp [hu, hv]⟩ },
     { rcases ih (λ r hr, hs _ (multiset.mem_cons.2 (or.inr hr))) h with ⟨q, hq₁, hq₂⟩,
       exact ⟨q, multiset.mem_cons.2 (or.inr hq₁), hq₂⟩ }
@@ -328,7 +333,7 @@ lemma irreducible_of_associated [comm_monoid_with_zero α] {p q : α} (h : p ~
   have hpab : p = a * (b * (u⁻¹ : units α)),
     from calc p = (p * u) * (u ⁻¹ : units α) : by simp
       ... = _ : by rw hu; simp [hab, mul_assoc],
-  (hp.2 _ _ hpab).elim or.inl (λ ⟨v, hv⟩, or.inr ⟨v * u, by simp [hv]⟩)⟩
+  (hp.is_unit_or_is_unit hpab).elim or.inl (λ ⟨v, hv⟩, or.inr ⟨v * u, by simp [hv]⟩)⟩
 
 lemma irreducible_iff_of_associated [comm_monoid_with_zero α] {p q : α} (h : p ~ᵤ q) :
   irreducible p ↔ irreducible q :=
@@ -592,7 +597,7 @@ end
 
 theorem irreducible_mk (a : α) : irreducible (associates.mk a) ↔ irreducible a :=
 begin
-  simp only [irreducible, is_unit_mk],
+  simp only [irreducible_iff, is_unit_mk],
   apply and_congr iff.rfl,
   split,
   { rintro h x y rfl,

src/algebra/gcd_monoid.lean

@@ -587,7 +587,7 @@ theorem prime_of_irreducible {x : α} (hi: irreducible x) : prime x :=
 ⟨hi.ne_zero, ⟨hi.1, λ a b h,
 begin
   cases gcd_dvd_left x a with y hy,
-  cases hi.2 _ _ hy with hu hu; cases hu with u hu,
+  cases hi.is_unit_or_is_unit hy with hu hu; cases hu with u hu,
   { right, transitivity (gcd (x * b) (a * b)), apply dvd_gcd (dvd_mul_right x b) h,
     rw gcd_mul_right, rw ← hu,
     apply dvd_of_associated, transitivity (normalize b), symmetry, use u, apply mul_comm,

src/algebra/squarefree.lean

@@ -55,7 +55,7 @@ lemma irreducible.squarefree [comm_monoid R] {x : R} (h : irreducible x) :
 begin
   rintros y ⟨z, hz⟩,
   rw mul_assoc at hz,
-  rcases h.2 _ _ hz with hu | hu,
+  rcases h.is_unit_or_is_unit hz with hu | hu,
   { exact hu },
   { apply is_unit_of_mul_is_unit_left hu },
 end

src/algebraic_geometry/prime_spectrum.lean

@@ -209,7 +209,7 @@ begin
   rw mem_zero_locus at hx,
   have x_prime : x.as_ideal.is_prime := by apply_instance,
   have eq_top : x.as_ideal = ⊤, { rw ideal.eq_top_iff_one, exact hx h },
-  apply x_prime.1 eq_top,
+  apply x_prime.ne_top eq_top,
 end
 
 lemma zero_locus_empty_iff_eq_top {I : ideal R} :

src/analysis/calculus/fderiv.lean

@@ -433,7 +433,7 @@ as this statement is empty. -/
 lemma has_fderiv_within_at_of_not_mem_closure (h : x ∉ closure s) :
   has_fderiv_within_at f f' s x :=
 begin
-  simp only [mem_closure_iff_nhds_within_ne_bot, ne_bot, ne.def, not_not] at h,
+  simp only [mem_closure_iff_nhds_within_ne_bot, ne_bot_iff, ne.def, not_not] at h,
   simp [has_fderiv_within_at, has_fderiv_at_filter, h, is_o, is_O_with],
 end
 

src/computability/turing_machine.lean

@@ -606,7 +606,7 @@ trans_gen.head'_iff.trans (trans_gen.head'_iff.trans $ by rw h).symm
 theorem reaches_total {σ} {f : σ → option σ}
   {a b c} : reaches f a b → reaches f a c →
   reaches f b c ∨ reaches f c b :=
-refl_trans_gen.total_of_right_unique $ λ _ _ _, option.mem_unique
+refl_trans_gen.total_of_right_unique ⟨λ _ _ _, option.mem_unique⟩
 
 theorem reaches₁_fwd {σ} {f : σ → option σ}
   {a b c} (h₁ : reaches₁ f a c) (h₂ : b ∈ f a) : reaches f b c :=

src/data/list/forall2.lean

@@ -90,18 +90,25 @@ lemma forall₂_and_left {r : α → β → Prop} {p : α → Prop} :
 | _ []     := by simp only [map, forall₂_nil_right_iff]
 | _ (b::u) := by simp only [map, forall₂_cons_right_iff, forall₂_map_right_iff]
 
-lemma left_unique_forall₂ (hr : left_unique r) : left_unique (forall₂ r)
+lemma left_unique_forall₂' (hr : left_unique r) :
+  ∀{a b c}, forall₂ r a b → forall₂ r c b → a = c
 | a₀ nil a₁ forall₂.nil forall₂.nil := rfl
 | (a₀::l₀) (b::l) (a₁::l₁) (forall₂.cons ha₀ h₀) (forall₂.cons ha₁ h₁) :=
-  hr ha₀ ha₁ ▸ left_unique_forall₂ h₀ h₁ ▸ rfl
+  hr.unique ha₀ ha₁ ▸ left_unique_forall₂' h₀ h₁ ▸ rfl
 
-lemma right_unique_forall₂ (hr : right_unique r) : right_unique (forall₂ r)
+lemma left_unique_forall₂ (hr : left_unique r) : left_unique (forall₂ r) :=
+⟨@left_unique_forall₂' _ _ _ hr⟩
+
+lemma right_unique_forall₂' (hr : right_unique r) : ∀{a b c}, forall₂ r a b → forall₂ r a c → b = c
 | nil a₀ a₁ forall₂.nil forall₂.nil := rfl
 | (b::l) (a₀::l₀) (a₁::l₁) (forall₂.cons ha₀ h₀) (forall₂.cons ha₁ h₁) :=
-  hr ha₀ ha₁ ▸ right_unique_forall₂ h₀ h₁ ▸ rfl
+  hr.unique ha₀ ha₁ ▸ right_unique_forall₂' h₀ h₁ ▸ rfl
+
+lemma right_unique_forall₂ (hr : right_unique r) : right_unique (forall₂ r) :=
+⟨@right_unique_forall₂' _ _ _ hr⟩
 
 lemma bi_unique_forall₂ (hr : bi_unique r) : bi_unique (forall₂ r) :=
-⟨assume a b c, left_unique_forall₂ hr.1, assume a b c, right_unique_forall₂ hr.2⟩
+@@bi_unique.mk _ (left_unique_forall₂ hr.1) (right_unique_forall₂ hr.2)
 
 theorem forall₂_length_eq {R : α → β → Prop} :
   ∀ {l₁ l₂}, forall₂ R l₁ l₂ → length l₁ = length l₂

src/data/list/perm.lean

@@ -282,13 +282,13 @@ have (flip (forall₂ r) ∘r (perm ∘r forall₂ r)) b d, from ⟨a, h₁, c,
 have ((flip (forall₂ r) ∘r forall₂ r) ∘r perm) b d,
   by rwa [← forall₂_comp_perm_eq_perm_comp_forall₂, ← relation.comp_assoc] at this,
 let ⟨b', ⟨c', hbc, hcb⟩, hbd⟩ := this in
-have b' = b, from right_unique_forall₂ @hr hcb hbc,
+have b' = b, from right_unique_forall₂' hr hcb hbc,
 this ▸ hbd
 
 lemma rel_perm (hr : bi_unique r) : (forall₂ r ⇒ forall₂ r ⇒ (↔)) perm perm :=
 assume a b hab c d hcd, iff.intro
   (rel_perm_imp hr.2 hab hcd)
-  (rel_perm_imp (assume a b c, left_unique_flip hr.1) hab.flip hcd.flip)
+  (rel_perm_imp (left_unique_flip hr.1) hab.flip hcd.flip)
 
 end rel
 

src/data/option/basic.lean

@@ -36,6 +36,9 @@ by cases x; [contradiction, rw get_or_else_some]
 theorem mem_unique {o : option α} {a b : α} (ha : a ∈ o) (hb : b ∈ o) : a = b :=
 option.some.inj $ ha.symm.trans hb
 
+theorem mem.left_unique : relator.left_unique ((∈) : α → option α → Prop) :=
+⟨λ a o b, mem_unique⟩
+
 theorem some_injective (α : Type*) : function.injective (@some α) :=
 λ _ _, some_inj.mp
 

src/data/pfun.lean

@@ -61,8 +61,11 @@ instance : inhabited (roption α) := ⟨none⟩
   function returns `a`. -/
 def some (a : α) : roption α := ⟨true, λ_, a⟩
 
-theorem mem_unique : relator.left_unique ((∈) : α → roption α → Prop)
-| _ ⟨p, f⟩ _ ⟨h₁, rfl⟩ ⟨h₂, rfl⟩ := rfl
+theorem mem_unique : ∀ {a b : α} {o : roption α}, a ∈ o → b ∈ o → a = b
+| _ _ ⟨p, f⟩ ⟨h₁, rfl⟩ ⟨h₂, rfl⟩ := rfl
+
+theorem mem.left_unique : relator.left_unique ((∈) : α → roption α → Prop) :=
+⟨λ a o b, mem_unique⟩
 
 theorem get_eq_of_mem {o : roption α} {a} (h : a ∈ o) (h') : get o h' = a :=
 mem_unique ⟨_, rfl⟩ h

src/data/polynomial/field_division.lean

@@ -83,7 +83,7 @@ by rw [degree_mul, degree_C h₁, add_zero]
 
 theorem irreducible_of_monic {p : polynomial R} (hp1 : p.monic) (hp2 : p ≠ 1) :
   irreducible p ↔ (∀ f g : polynomial R, f.monic → g.monic → f * g = p → f = 1 ∨ g = 1) :=
-⟨λ hp3 f g hf hg hfg, or.cases_on (hp3.2 f g hfg.symm)
+⟨λ hp3 f g hf hg hfg, or.cases_on (hp3.is_unit_or_is_unit hfg.symm)
   (assume huf : is_unit f, or.inl $ eq_one_of_is_unit_of_monic hf huf)
   (assume hug : is_unit g, or.inr $ eq_one_of_is_unit_of_monic hg hug),
 λ hp3, ⟨mt (eq_one_of_is_unit_of_monic hp1) hp2, λ f g hp,

src/data/polynomial/ring_division.lean

@@ -525,7 +525,7 @@ let ⟨u, hu⟩ := h in by simp [hu.symm]
 lemma degree_eq_one_of_irreducible_of_root (hi : irreducible p) {x : R} (hx : is_root p x) :
   degree p = 1 :=
 let ⟨g, hg⟩ := dvd_iff_is_root.2 hx in
-have is_unit (X - C x) ∨ is_unit g, from hi.2 _ _ hg,
+have is_unit (X - C x) ∨ is_unit g, from hi.is_unit_or_is_unit hg,
 this.elim
   (λ h, have h₁ : degree (X - C x) = 1, from degree_X_sub_C x,
     have h₂ : degree (X - C x) = 0, from degree_eq_zero_of_is_unit h,
@@ -617,7 +617,7 @@ lemma monic.irreducible_of_irreducible_map (f : polynomial R)
 begin
   fsplit,
   { intro h,
-    exact h_irr.1 (is_unit.map (monoid_hom.of (map φ)) h), },
+    exact h_irr.not_unit (is_unit.map (monoid_hom.of (map φ)) h), },
   { intros a b h,
 
     have q := (leading_coeff_mul a b).symm,
@@ -631,7 +631,7 @@ begin
 
     have h' := congr_arg (map φ) h,
     simp only [map_mul] at h',
-    cases h_irr.2 _ _ h' with w w,
+    cases h_irr.is_unit_or_is_unit h' with w w,
     { left,
       exact is_unit_of_is_unit_leading_coeff_of_is_unit_map _ _ au w, },
     { right,

src/data/seq/computation.lean

@@ -233,21 +233,26 @@ theorem le_stable (s : computation α) {a m n} (h : m ≤ n) :
   s.1 m = some a → s.1 n = some a :=
 by {cases s with f al, induction h with n h IH, exacts [id, λ h2, al (IH h2)]}
 
-theorem mem_unique :
-   relator.left_unique ((∈) : α → computation α → Prop) :=
-λa s b ⟨m, ha⟩ ⟨n, hb⟩, by injection
+theorem mem_unique {s : computation α} {a b : α} : a ∈ s → b ∈ s → a = b
+| ⟨m, ha⟩ ⟨n, hb⟩ := by injection
   (le_stable s (le_max_left m n) ha.symm).symm.trans
   (le_stable s (le_max_right m n) hb.symm)
 
+theorem mem.left_unique : relator.left_unique ((∈) : α → computation α → Prop) :=
+⟨λ a s b, mem_unique⟩
+
 /-- `terminates s` asserts that the computation `s` eventually terminates with some value. -/
-@[class] def terminates (s : computation α) : Prop := ∃ a, a ∈ s
+class terminates (s : computation α) : Prop := (term : ∃ a, a ∈ s)
+
+theorem terminates_iff (s : computation α) : terminates s ↔ ∃ a, a ∈ s :=
+⟨λ h, h.1, terminates.mk⟩
 
-theorem terminates_of_mem {s : computation α} {a : α} : a ∈ s → terminates s :=
-exists.intro a
+theorem terminates_of_mem {s : computation α} {a : α} (h : a ∈ s) : terminates s :=
+⟨⟨a, h⟩⟩
 
 theorem terminates_def (s : computation α) : terminates s ↔ ∃ n, (s.1 n).is_some :=
-⟨λ⟨a, n, h⟩, ⟨n, by {dsimp [stream.nth] at h, rw ←h, exact rfl}⟩,
-λ⟨n, h⟩, ⟨option.get h, n, (option.eq_some_of_is_some h).symm⟩⟩
+⟨λ ⟨⟨a, n, h⟩⟩, ⟨n, by {dsimp [stream.nth] at h, rw ←h, exact rfl}⟩,
+ λ ⟨n, h⟩, ⟨⟨option.get h, n, (option.eq_some_of_is_some h).symm⟩⟩⟩
 
 theorem ret_mem (a : α) : a ∈ return a :=
 exists.intro 0 rfl
@@ -263,26 +268,26 @@ theorem think_mem {s : computation α} {a} : a ∈ s → a ∈ think s
 
 instance think_terminates (s : computation α) :
   ∀ [terminates s], terminates (think s)
-| ⟨a, n, h⟩ := ⟨a, n+1, h⟩
+| ⟨⟨a, n, h⟩⟩ := ⟨⟨a, n+1, h⟩⟩
 
 theorem of_think_mem {s : computation α} {a} : a ∈ think s → a ∈ s
 | ⟨n, h⟩ := by {cases n with n', contradiction, exact ⟨n', h⟩}
 
 theorem of_think_terminates {s : computation α} :
   terminates (think s) → terminates s
-| ⟨a, h⟩ := ⟨a, of_think_mem h⟩
+| ⟨⟨a, h⟩⟩ := ⟨⟨a, of_think_mem h⟩⟩
 
 theorem not_mem_empty (a : α) : a ∉ empty α :=
 λ ⟨n, h⟩, by clear _fun_match; contradiction
 
 theorem not_terminates_empty : ¬ terminates (empty α) :=
-λ ⟨a, h⟩, not_mem_empty a h
+λ ⟨⟨a, h⟩⟩, not_mem_empty a h
 
 theorem eq_empty_of_not_terminates {s} (H : ¬ terminates s) : s = empty α :=
 begin
   apply subtype.eq, funext n,
   induction h : s.val n, {refl},
-  refine absurd _ H, exact ⟨_, _, h.symm⟩
+  refine absurd _ H, exact ⟨⟨_, _, h.symm⟩⟩
 end
 
 theorem thinkN_mem {s : computation α} {a} : ∀ n, a ∈ thinkN s n ↔ a ∈ s
@@ -291,11 +296,11 @@ theorem thinkN_mem {s : computation α} {a} : ∀ n, a ∈ thinkN s n ↔ a ∈
 
 instance thinkN_terminates (s : computation α) :
   ∀ [terminates s] n, terminates (thinkN s n)
-| ⟨a, h⟩ n := ⟨a, (thinkN_mem n).2 h⟩
+| ⟨⟨a, h⟩⟩ n := ⟨⟨a, (thinkN_mem n).2 h⟩⟩
 
 theorem of_thinkN_terminates (s : computation α) (n) :
   terminates (thinkN s n) → terminates s
-| ⟨a, h⟩ := ⟨a, (thinkN_mem _).1 h⟩
+| ⟨⟨a, h⟩⟩ := ⟨⟨a, (thinkN_mem _).1 h⟩⟩
 
 /-- `promises s a`, or `s ~> a`, asserts that although the computation `s`
   may not terminate, if it does, then the result is `a`. -/
@@ -337,7 +342,7 @@ get_eq_of_mem _ $ (thinkN_mem _).2 (get_mem _)
 theorem get_promises : s ~> get s := λ a, get_eq_of_mem _
 
 theorem mem_of_promises {a} (p : s ~> a) : a ∈ s :=
-by { casesI h with a' h, rw p h, exact h }
+by { casesI h, cases h with a' h, rw p h, exact h }
 
 theorem get_eq_of_promises {a} : s ~> a → get s = a :=
 get_eq_of_mem _ ∘ mem_of_promises _
@@ -663,7 +668,8 @@ by rw ←bind_ret; apply_instance
 
 theorem terminates_map_iff (f : α → β) (s : computation α) :
   terminates (map f s) ↔ terminates s :=
-⟨λ⟨a, h⟩, let ⟨b, h1, _⟩ := exists_of_mem_map h in ⟨_, h1⟩, @computation.terminates_map _ _ _ _⟩
+⟨λ ⟨⟨a, h⟩⟩, let ⟨b, h1, _⟩ := exists_of_mem_map h in ⟨⟨_, h1⟩⟩,
+ @computation.terminates_map _ _ _ _⟩
 
 -- Parallel computation
 /-- `c₁ <|> c₂` calculates `c₁` and `c₂` simultaneously, returning
@@ -732,7 +738,7 @@ theorem equiv_of_mem {s t : computation α} {a} (h1 : a ∈ s) (h2 : a ∈ t) :
 
 theorem terminates_congr {c₁ c₂ : computation α}
   (h : c₁ ~ c₂) : terminates c₁ ↔ terminates c₂ :=
-exists_congr h
+by simp only [terminates_iff, exists_congr h]
 
 theorem promises_congr {c₁ c₂ : computation α}
   (h : c₁ ~ c₂) (a) : c₁ ~> a ↔ c₂ ~> a :=
@@ -800,8 +806,8 @@ theorem lift_rel.imp {R S : α → β → Prop} (H : ∀ {a b}, R a b → S a b)
 
 theorem terminates_of_lift_rel {R : α → β → Prop} {s t} :
  lift_rel R s t → (terminates s ↔ terminates t) | ⟨l, r⟩ :=
-⟨λ ⟨a, as⟩, let ⟨b, bt, ab⟩ := l as in ⟨b, bt⟩,
- λ ⟨b, bt⟩, let ⟨a, as, ab⟩ := r bt in ⟨a, as⟩⟩
+⟨λ ⟨⟨a, as⟩⟩, let ⟨b, bt, ab⟩ := l as in ⟨⟨b, bt⟩⟩,
+ λ ⟨⟨b, bt⟩⟩, let ⟨a, as, ab⟩ := r bt in ⟨⟨a, as⟩⟩⟩
 
 theorem rel_of_lift_rel {R : α → β → Prop} {ca cb} :
  lift_rel R ca cb → ∀ {a b}, a ∈ ca → b ∈ cb → R a b
@@ -826,8 +832,8 @@ theorem lift_rel_def {R : α → β → Prop} {ca cb} : lift_rel R ca cb ↔
 ⟨λh, ⟨terminates_of_lift_rel h, λ a b ma mb,
   let ⟨b', mb', ab⟩ := h.left ma in by rwa mem_unique mb mb'⟩,
 λ⟨l, r⟩,
- ⟨λ a ma, let ⟨b, mb⟩ := l.1 ⟨_, ma⟩ in ⟨b, mb, r ma mb⟩,
-  λ b mb, let ⟨a, ma⟩ := l.2 ⟨_, mb⟩ in ⟨a, ma, r ma mb⟩⟩⟩
+ ⟨λ a ma, let ⟨⟨b, mb⟩⟩ := l.1 ⟨⟨_, ma⟩⟩ in ⟨b, mb, r ma mb⟩,
+  λ b mb, let ⟨⟨a, ma⟩⟩ := l.2 ⟨⟨_, mb⟩⟩ in ⟨a, ma, r ma mb⟩⟩⟩
 
 theorem lift_rel_bind {δ} (R : α → β → Prop) (S : γ → δ → Prop)
   {s1 : computation α} {s2 : computation β}

src/data/seq/parallel.lean

@@ -194,7 +194,7 @@ end
 
 theorem parallel_empty (S : wseq (computation α)) (h : S.head ~> none) :
 parallel S = empty _ :=
-eq_empty_of_not_terminates $ λ ⟨a, m⟩,
+eq_empty_of_not_terminates $ λ ⟨⟨a, m⟩⟩,
 let ⟨c, cs, ac⟩ := exists_of_mem_parallel m,
     ⟨n, nm⟩ := exists_nth_of_mem cs,
     ⟨c', h'⟩ := head_some_of_nth_some nm in by injection h h'
@@ -210,7 +210,7 @@ begin
     funext c, dsimp [id, function.comp], rw [←map_comp], exact (map_id _).symm },
   have pe := congr_arg parallel this, rw ←map_parallel at pe,
   have h' := h, rw pe at h',
-  haveI : terminates (parallel T) := (terminates_map_iff _ _).1 ⟨_, h'⟩,
+  haveI : terminates (parallel T) := (terminates_map_iff _ _).1 ⟨⟨_, h'⟩⟩,
   induction e : get (parallel T) with a' c,
   have : a ∈ c ∧ c ∈ S,
   { rcases exists_of_mem_map h' with ⟨d, dT, cd⟩,