clean up some more sub-proofs

StoneDuality/PIT.lean

@@ -93,64 +93,39 @@ theorem prime_ideal_of_disjoint_filter_ideal
   obtain ⟨⟨Jidl, IJ, JF⟩, ⟨_, Jmax⟩⟩ := hJ
   set J := IsIdeal.toIdeal Jidl
   use J
+  have IJ' : I ≤ J := IJ
 
   clear chainub IinS
 
   -- By construction, J contains I and is disjoint from F. It remains to prove that J is prime.
   refine ⟨?_, ⟨IJ, JF⟩⟩
 
   -- First note that J is proper: ⊤ ∈ F so ⊤ ∉ J because F and J are disjoint.
-  have Jpr : IsProper J := by
-    apply isProper_of_not_mem ?_
-    use ⊤
-    exact Set.disjoint_left.1 JF F.top_mem
+  have Jpr : IsProper J := isProper_of_not_mem (Set.disjoint_left.1 JF F.top_mem)
 
+  -- Suppose that a₁ ∉ J, a₂ ∉ J. We need to prove that a₁ ⊔ a₂ ∉ J.
   rw [isPrime_iff_mem_or_mem]
-
   intros a₁ a₂
   contrapose!
-
-  -- Suppose that a₁ ∉ J, a₂ ∉ J. We need to prove that a₁ ⊔ a₂ ∉ J.
   intro ⟨ha₁, ha₂⟩
 
   -- Consider the ideals J₁, J₂ generated by J ∪ {a₁} and J ∪ {a₂}, respectively.
   let J₁ := J ⊔ principal a₁
   let J₂ := J ⊔ principal a₂
 
-  have IJ' : I ≤ J := IJ
-  -- For each i, Jᵢ is an ideal that contains I, and is not equal to J.
-  have IJ₁ : I ≤ J₁ := le_trans IJ' le_sup_left
-  have IJ₂ : I ≤ J₂ := le_trans IJ' le_sup_left
-  have a₁J₁ : a₁ ∈ J₁ :=
-    mem_of_subset_of_mem (le_sup_right : principal _ ≤ _) (mem_principal_self _)
-  have a₂J₂ : a₂ ∈ J₂ :=
-    mem_of_subset_of_mem (le_sup_right : principal _ ≤ _) (mem_principal_self _)
-
+  -- For each i, Jᵢ is an ideal that contains J, I and aᵢ, and is not equal to J.
   have JsubJ₁ : J ≤ J₁ := le_sup_left
   have JsubJ₂ : J ≤ J₂ := le_sup_left
-  have J₁J : J₁ ≠ J := by refine ne_of_mem_of_not_mem' a₁J₁ ha₁
-  have J₂J : J₂ ≠ J := by refine ne_of_mem_of_not_mem' a₂J₂ ha₂
+  have IJ₁ : I ≤ J₁ := le_trans IJ' le_sup_left
+  have IJ₂ : I ≤ J₂ := le_trans IJ' le_sup_left
+  have a₁J₁ : a₁ ∈ J₁ := mem_of_subset_of_mem (le_sup_right : _ ≤ J ⊔ _) (mem_principal_self _)
+  have a₂J₂ : a₂ ∈ J₂ := mem_of_subset_of_mem (le_sup_right : _ ≤ J ⊔ _) (mem_principal_self _)
+  have J₁J : ↑J₁ ≠ Jset := by refine ne_of_mem_of_not_mem' a₁J₁ ha₁
+  have J₂J : ↑J₂ ≠ Jset := by refine ne_of_mem_of_not_mem' a₂J₂ ha₂
 
-  have Jcoe : J = Jset := by rfl
   -- Therefore, since J is maximal, we must have Jᵢ ∉ S.
-  have J₁S : ↑J₁ ∉ S := by
-    intro h
-    apply J₁J
-    apply Jmax at h
-    have := h JsubJ₁
-    -- TODO fix this coercion problem
-    rw [←Jcoe] at this
-    simp only [SetLike.coe_set_eq] at this
-    exact this
-  have J₂S : ↑J₂ ∉ S := by
-    intro h
-    apply J₂J
-    apply Jmax at h
-    have := h JsubJ₂
-    -- TODO fix this coercion problem
-    rw [←Jcoe] at this
-    simp only [SetLike.coe_set_eq] at this
-    exact this
+  have J₁S : ↑J₁ ∉ S := fun h => J₁J (Jmax J₁ h JsubJ₁)
+  have J₂S : ↑J₂ ∉ S := fun h => J₂J (Jmax J₂ h JsubJ₂)
 
   -- Since Jᵢ is an ideal that contains I, we have that Jᵢ is not disjoint from F.
   have J₁F : ¬ (Disjoint (F : Set α) J₁) := by