Remove spurious injections

math-comp · Dec 4, 2015 · 19ac062 · 19ac062
1 parent 03363b8
commit 19ac062
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 4 deletions.
diff --git a/mathcomp/odd_order/BGsection15.v b/mathcomp/odd_order/BGsection15.v
@@ -1248,7 +1248,7 @@ Lemma nonTI_Fitting_facts M :
   [/\ M \in 'M_'F :|: 'M_'P1, M`_\F = M`_\sigma & M^`(1) \subset 'F(M)].
 Proof.
 move=> maxM nonTI; suff: [exists (y | y \notin M), 'F(M) :&: 'F(M) :^ y != 1].
-  by case/exists_inP=> y notMy /nonTI_Fitting_structure[] // [[-> ?] _ []].
+  by case/exists_inP=> y notMy /nonTI_Fitting_structure[] // [-> dMF] _ [].
 rewrite -negb_forall_in; apply: contra nonTI => /forall_inP tiF.
 apply/normedTI_P; rewrite normD1 setTI gFnorm setD_eq0 subG1.
 split=> // [|g _]; first by rewrite (trivg_Fitting (mmax_sol maxM)) mmax_neq1.
@@ -1509,5 +1509,3 @@ by rewrite (subG1_contra _ ntCMsx) ?setIS //= -cent_cycle centS.
 Qed.
 
 End Section15.
-
-
diff --git a/mathcomp/odd_order/BGsection16.v b/mathcomp/odd_order/BGsection16.v
@@ -786,7 +786,7 @@ split; first by have [_ _ _ _ []] := Ptype_structure PmaxM hallK.
 have [<- | neqMF_Ms] := eqVneq M`_\F M`_\sigma; first exact: Fcore_sub_Fitting.
 have solMs: solvable M`_\sigma := solvableS (pcore_sub _ _) (mmax_sol maxM).
 have [D hallD] := Hall_exists #|Kstar|^' solMs.
-by case: (Fcore_structure maxM) notP1maxM => _ /(_ K D)[] // [[->]].
+by case: (Fcore_structure maxM) notP1maxM => _ /(_ K D)[] // [->].
 Qed.
 
 End SingleGroupSummaries.