feat(data/equiv): Add congr_arg, congr_fun, and ext_iff lemmas …

…to equivs (#5367)

These members already exist on the corresponding homs

src/algebra/algebra/basic.lean

@@ -609,6 +609,14 @@ begin
   { exact congr_arg equiv.inv_fun h₁ }
 end
 
+protected lemma congr_arg {f : A₁ ≃ₐ[R] A₂} : Π {x x' : A₁}, x = x' → f x = f x'
+| _ _ rfl := rfl
+
+protected lemma congr_fun {f g : A₁ ≃ₐ[R] A₂} (h : f = g) (x : A₁) : f x = g x := h ▸ rfl
+
+lemma ext_iff {f g : A₁ ≃ₐ[R] A₂} : f = g ↔ ∀ x, f x = g x :=
+⟨λ h x, h ▸ rfl, ext⟩
+
 lemma coe_fun_injective : @function.injective (A₁ ≃ₐ[R] A₂) (A₁ → A₂) (λ e, (e : A₁ → A₂)) :=
 begin
   intros f g w,

src/algebra/module/linear_map.lean

@@ -360,6 +360,14 @@ variables {e e'}
 @[ext] lemma ext (h : ∀ x, e x = e' x) : e = e' :=
 injective_to_equiv (equiv.ext h)
 
+protected lemma congr_arg : Π {x x' : M}, x = x' → e x = e x'
+| _ _ rfl := rfl
+
+protected lemma congr_fun (h : e = e') (x : M) : e x = e' x := h ▸ rfl
+
+lemma ext_iff : e = e' ↔ ∀ x, e x = e' x :=
+⟨λ h x, h ▸ rfl, ext⟩
+
 end
 
 section

src/data/equiv/basic.lean

@@ -96,12 +96,23 @@ injective_coe_fn.eq_iff
 @[ext] lemma ext {f g : equiv α β} (H : ∀ x, f x = g x) : f = g :=
 injective_coe_fn (funext H)
 
-@[ext] lemma perm.ext {σ τ : equiv.perm α} (H : ∀ x, σ x = τ x) : σ = τ :=
-equiv.ext H
+protected lemma congr_arg {f : equiv α β} : Π {x x' : α}, x = x' → f x = f x'
+| _ _ rfl := rfl
+
+protected lemma congr_fun {f g : equiv α β} (h : f = g) (x : α) : f x = g x := h ▸ rfl
 
 lemma ext_iff {f g : equiv α β} : f = g ↔ ∀ x, f x = g x :=
 ⟨λ h x, h ▸ rfl, ext⟩
 
+@[ext] lemma perm.ext {σ τ : equiv.perm α} (H : ∀ x, σ x = τ x) : σ = τ :=
+equiv.ext H
+
+protected lemma perm.congr_arg {f : equiv.perm α} {x x' : α} : x = x' → f x = f x' :=
+equiv.congr_arg
+
+protected lemma perm.congr_fun {f g : equiv.perm α} (h : f = g) (x : α) : f x = g x :=
+equiv.congr_fun h x
+
 lemma perm.ext_iff {σ τ : equiv.perm α} : σ = τ ↔ ∀ x, σ x = τ x :=
 ext_iff
 

src/data/equiv/mul_add.lean

@@ -213,6 +213,17 @@ begin
   { exact congr_arg equiv.inv_fun h₁ }
 end
 
+@[to_additive]
+protected lemma congr_arg {f : mul_equiv M N} : Π {x x' : M}, x = x' → f x = f x'
+| _ _ rfl := rfl
+
+@[to_additive]
+protected lemma congr_fun {f g : mul_equiv M N} (h : f = g) (x : M) : f x = g x := h ▸ rfl
+
+@[to_additive]
+lemma ext_iff {f g : mul_equiv M N} : f = g ↔ ∀ x, f x = g x :=
+⟨λ h x, h ▸ rfl, ext⟩
+
 @[to_additive] lemma to_monoid_hom_injective
   {M N} [monoid M] [monoid N] : function.injective (to_monoid_hom : (M ≃* N) → M →* N) :=
 λ f g h, mul_equiv.ext (monoid_hom.ext_iff.1 h)

src/data/equiv/ring.lean

@@ -78,6 +78,14 @@ begin
   { exact congr_arg equiv.inv_fun h₁ }
 end
 
+protected lemma congr_arg {f : R ≃+* S} : Π {x x' : R}, x = x' → f x = f x'
+| _ _ rfl := rfl
+
+protected lemma congr_fun {f g : R ≃+* S} (h : f = g) (x : R) : f x = g x := h ▸ rfl
+
+lemma ext_iff {f g : R ≃+* S} : f = g ↔ ∀ x, f x = g x :=
+⟨λ h x, h ▸ rfl, ext⟩
+
 instance has_coe_to_mul_equiv : has_coe (R ≃+* S) (R ≃* S) := ⟨ring_equiv.to_mul_equiv⟩
 
 instance has_coe_to_add_equiv : has_coe (R ≃+* S) (R ≃+ S) := ⟨ring_equiv.to_add_equiv⟩