Add extra eta lemmas for the under tactic

Related: coq/coq#9651

5 files changed, 23 insertions, 2 deletions

diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index 3b12802..2580741 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -232,8 +232,13 @@ rewrite /fun_of_matrix; split=> [/= eqAB | -> //].
 by apply/val_inj/ffunP=> [[i j]]; apply: eqAB.
 Qed.
 
+Lemma eq_mx k F1 F2 : (F1 =2 F2) -> matrix_of_fun k F1 = matrix_of_fun k F2.
+Proof. by move=> eq_F; apply/matrixP => i j; rewrite !mxE eq_F. Qed.
+
 End MatrixDef.
 
+Arguments eq_mx {R m n k} [F1] F2 eq_F12.
+
 Bind Scope ring_scope with matrix.
 
 Notation "''M[' R ]_ ( m , n )" := (matrix R m n) (only parsing): type_scope.
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 702dfc4..e0feecf 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -1673,6 +1673,9 @@ apply: eq_bigr => i _; case: leqP => // /nderivn_poly0->.
 by rewrite horner0 simp.
 Qed.
 
+Lemma eq_poly n E1 E2 : E1 =1 E2 -> poly n E1 = poly n E2.
+Proof. by move=> E; rewrite !poly_def; apply: eq_bigr => i _; rewrite E. Qed.
+
 End PolynomialTheory.
 
 Prenex Implicits polyC polyCK Poly polyseqK lead_coef root horner polyOver.
@@ -1695,6 +1698,7 @@ Arguments rootPt {R p x}.
 Arguments unity_rootP {R n z}.
 Arguments polyOverP {R S0 addS kS p}.
 Arguments polyC_inj {R} [x1 x2] eq_x12P.
+Arguments eq_poly {R n} [E1] E2 eq_E12.
 
 Canonical polynomial_countZmodType (R : countRingType) :=
   [countZmodType of polynomial R].
diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v
index db1a8e7..01576fe 100644
--- a/mathcomp/ssreflect/finfun.v
+++ b/mathcomp/ssreflect/finfun.v
@@ -128,6 +128,10 @@ split=> [eq_f12 | -> //]; do 2!apply: val_inj => /=.
 by rewrite !fgraph_codom /= (eq_codom eq_f12).
 Qed.
 
+Lemma eq_ffun (g1 g2 : aT -> rT) :
+  g1 =1 g2 -> finfun g1 = finfun g2.
+Proof. by move=> eq_g; apply/ffunP => x; rewrite !ffunE eq_g. Qed.
+
 Lemma ffunK : cancel (@fun_of_fin aT rT) (@finfun aT rT).
 Proof. by move=> f; apply/ffunP/ffunE. Qed.
 
@@ -148,6 +152,7 @@ Notation family F := (family_mem (fun_of_simpl (fmem F))).
 Notation ffun_on R := (ffun_on_mem _ (mem R)).
 
 Arguments ffunK {aT rT}.
+Arguments eq_ffun {aT rT} [g1] g2 eq_g12.
 Arguments familyP {aT rT pT F f}.
 Arguments ffun_onP {aT rT R f}.
 
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 87d5da4..20b3601 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -239,11 +239,15 @@ Proof. by rewrite in_set. Qed.
 Lemma eqsVneq A B : {A = B} + {A != B}.
 Proof. exact: eqVneq. Qed.
 
+Lemma eq_finset (pA pB : pred T) : pA =1 pB -> finset pA = finset pB.
+Proof. by move=> eq_p; apply/setP => x; rewrite !(in_set, inE) eq_p. Qed.
+
 End BasicSetTheory.
 
 Definition inE := (in_set, inE).
 
 Arguments set0 {T}.
+Arguments eq_finset {T} [pA] pB eq_pAB.
 Hint Resolve in_setT : core.
 
 Notation "[ 'set' : T ]" := (setTfor (Phant T))
@@ -2210,4 +2214,3 @@ Arguments setCK {T}.
 Arguments minsetP {T P A}.
 Arguments maxsetP {T P A}.
 Prenex Implicits minset maxset.
-
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index 8f81155..c0ba403 100644
--- a/mathcomp/ssreflect/tuple.v
+++ b/mathcomp/ssreflect/tuple.v
@@ -411,10 +411,14 @@ Proof. by rewrite -tnth_nth tnth_mktuple. Qed.
 
 End MkTuple.
 
+Lemma eq_mktuple T' (f1 f2 : 'I_n -> T') :
+  f1 =1 f2 -> mktuple f1 = mktuple f2.
+Proof. by move=> eq_f; apply eq_from_tnth=> i; rewrite !tnth_map eq_f. Qed.
+
 End UseFinTuple.
 
 Notation "[ 'tuple' F | i < n ]" := (mktuple (fun i : 'I_n => F))
   (at level 0, i at level 0,
    format "[ '[hv' 'tuple'  F '/'   |  i  <  n ] ']'") : form_scope.
 
-
+Arguments eq_mktuple {n T'} [f1] f2 eq_f12.