extract aux lemma

Author: wwylele

Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Shift.lean

@@ -241,56 +241,54 @@ section Field
 variable [Field k] [LinearOrder k] [IsOrderedRing k] [AddCommGroup V] [AddTorsor V P]
   [Module k V] {n : ℕ} [NeZero n] (s : Affine.Simplex k P n) (i : Fin (n + 1)) {x : k}
 
+private theorem closedInterior_inter_shift_aux {n : ℕ} (i : Fin n) {x : k} (hxpos : 0 < x)
+    (hx1 : x ≤ 1) {w : Fin n → k} (hw : ∑ i, w i = 1) :
+    (∀ j, w j ∈ Set.Icc 0 1) ∧ w i = 1 - x ↔
+    (∀ j, j ≠ i → x⁻¹ * w j ∈ Set.Icc 0 1) ∧ x⁻¹ * (w i - 1) + 1 = 0 := by
+  refine ⟨fun ⟨hj, hi⟩ ↦ ⟨fun j hji ↦ ⟨?_, ?_⟩, ?_⟩, fun ⟨hj, hi⟩ ↦ ?_⟩
+  · exact mul_nonneg (by simpa using hxpos.le) (hj j).1
+  · rw [eq_sub_iff_add_eq, add_comm, ← eq_sub_iff_add_eq] at hi
+    rw [inv_mul_le_one₀ hxpos, hi, le_sub_iff_add_le, ← hw]
+    apply add_le_sum (fun i _ ↦ (hj i).1) (mem_univ j) (mem_univ i)
+    simpa using hji
+  · simp [hi, hxpos.ne.symm]
+  · have hix : w i = 1 - x := by grind
+    refine ⟨?_, hix⟩
+    suffices ∀ (j : Fin n), 0 ≤ w j by
+      refine fun j ↦ ⟨this j, ?_⟩
+      contrapose! hw
+      apply ne_of_gt
+      rw [← sum_erase_add _ _ (mem_univ j)]
+      apply lt_add_of_nonneg_of_lt (sum_nonneg fun i _ ↦ this i) hw
+    intro j
+    by_cases hji : j = i
+    · rw [hji, hix]
+      simpa using hx1
+    · specialize hj j (by simpa using hji)
+      apply nonneg_of_mul_nonneg_right hj.1
+      simpa using hxpos
+
 theorem closedInterior_inter_shift (hx : x ∈ Set.Icc 0 1) :
     s.closedInterior ∩ (affineSpan k (Set.range (s.faceOpposite i).points)).shift (s.points i) x =
     homothety (s.points i) x '' (s.faceOpposite i).closedInterior := by
-  by_cases! hx0 : x = 0
-  · simpa [hx0, (s.faceOpposite i).nonempty_closedInterior]
+  rcases eq_or_lt_of_le hx.1 with hx0 | hxpos
+  · simpa [hx0.symm, (s.faceOpposite i).nonempty_closedInterior]
       using s.closedInterior_inter_shift_zero i
-  have hxpos : 0 < x := lt_of_le_of_ne hx.1 hx0.symm
   ext p
   by_cases hp : p ∈ affineSpan k (Set.range s.points)
   · obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hp
     rw [Set.mem_inter_iff, range_faceOpposite_points, SetLike.mem_coe,
       s.independent.affineCombination_mem_shift_iff i hw,
       affineCombination_mem_closedInterior_iff hw, Set.mem_image]
-    simp_rw [AffineMap.homothety_eq_iff_of_mul_eq_one (mul_inv_cancel₀ hx0),
+    simp_rw [AffineMap.homothety_eq_iff_of_mul_eq_one (mul_inv_cancel₀ hxpos.ne.symm),
       univ.homothety_affineCombination _ _ (mem_univ i)]
     simp only [↓existsAndEq, and_true]
     rw [faceOpposite, affineCombination_mem_closedInterior_face_iff_mem_Icc _ _ (by
       simp [AffineMap.lineMap_apply, Finset.sum_add_distrib, ← Finset.mul_sum,
       Finset.sum_sub_distrib, hw])]
-    trans (∀ j ∈ ({i}ᶜ : Finset _), x⁻¹ * w j ∈ Set.Icc 0 1) ∧
-      ∀ j ∉ ({i}ᶜ : Finset _), x⁻¹ * (w j - 1) + 1 = 0
-    · refine ⟨fun ⟨hj, hi⟩ ↦ ⟨fun j hji ↦ ⟨?_, ?_⟩, fun j hji ↦ ?_⟩, fun ⟨hj, hi⟩ ↦ ?_⟩
-      · exact mul_nonneg (by simpa using hx.1) (hj j).1
-      · rw [eq_sub_iff_add_eq, add_comm, ← eq_sub_iff_add_eq] at hi
-        rw [inv_mul_le_one₀ hxpos, hi, le_sub_iff_add_le, ← hw]
-        apply Finset.add_le_sum (fun i _ ↦ (hj i).1) (mem_univ j) (mem_univ i)
-        simpa using hji
-      · have hji : j = i := by simpa using hji
-        simp [hji, hi, hx0]
-      · specialize hi i (by simp)
-        have hix : w i = 1 - x := by grind
-        refine ⟨?_, hix⟩
-        suffices ∀ (j : Fin (n + 1)), 0 ≤ w j by
-          refine fun j ↦ ⟨this j, ?_⟩
-          contrapose! hw
-          apply ne_of_gt
-          rw [← Finset.sum_erase_add _ _ (mem_univ j)]
-          apply lt_add_of_nonneg_of_lt (sum_nonneg fun i _ ↦ this i) hw
-        intro j
-        by_cases hji : j = i
-        · rw [hji, hix]
-          simpa using hx.2
-        · specialize hj j (by simpa using hji)
-          apply nonneg_of_mul_nonneg_right hj.1
-          simpa using hxpos
-    · congrm (∀ j, (hj : _) → ?_) ∧ ∀ j, (hj : _) → ?_
-      · have hj : j ≠ i := by simpa using hj
-        simp [lineMap_apply, hj]
-      · have hj : j = i := by simpa using hj
-        simp [lineMap_apply, hj]
+    rw [closedInterior_inter_shift_aux i hxpos hx.2 hw]
+    simp only [mem_compl, mem_singleton, not_not, forall_eq]
+    congrm (∀ j, (hj : _) → $(by simp [lineMap_apply, hj])) ∧ $(by simp [lineMap_apply])
   · apply iff_of_false
     · apply not_and_of_not_left
       contrapose hp