chore(linear_algebra/projection): golf (#17244)

leanprover-community · Oct 30, 2022 · 7a7d4dd · 7a7d4dd
1 parent 669eee9
commit 7a7d4dd
Showing 1 changed file with 3 additions and 7 deletions.
diff --git a/src/linear_algebra/projection.lean b/src/linear_algebra/projection.lean
@@ -92,13 +92,9 @@ linear map `f : E → p` such that `f x = x` for `x ∈ p` and `f x = 0` for `x
 def prod_equiv_of_is_compl (h : is_compl p q) : (p × q) ≃ₗ[R] E :=
 begin
   apply linear_equiv.of_bijective (p.subtype.coprod q.subtype),
-  { simp only [←ker_eq_bot, ker_eq_bot', prod.forall, subtype_apply, prod.mk_eq_zero, coprod_apply],
-    -- TODO: if I add `submodule.forall`, it unfolds the outer `∀` but not the inner one.
-    rintros ⟨x, hx⟩ ⟨y, hy⟩,
-    simp only [coe_mk, mk_eq_zero, ← eq_neg_iff_add_eq_zero],
-    rintro rfl,
-    rw [neg_mem_iff] at hx,
-    simp [disjoint_def.1 h.disjoint y hx hy] },
+  { rw [← ker_eq_bot, ker_coprod_of_disjoint_range, ker_subtype, ker_subtype, prod_bot],
+    rw [range_subtype, range_subtype],
+    exact h.1 },
   { rw [← range_eq_top, ← sup_eq_range, h.sup_eq_top] }
 end