# Zulip Chat Archive

## Stream: new members

### Topic: Equivalences determined by one direction

#### Heather Macbeth (Aug 01 2020 at 20:56):

What is the most efficient way to prove this?

```
import linear_algebra.basic
variables (R : Type*) (M₁ : Type*) (M₂ : Type*)
variables [ring R] [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂]
example (e f : linear_equiv R M₁ M₂) (h : (e : linear_map R M₁ M₂) = f) : e = f := sorry
```

I found docs#equiv.coe_fn_injective but can't figure out how to use it here.

#### Kevin Buzzard (Aug 01 2020 at 21:01):

Here's a kind of annoying proof:

```
example (e f : linear_equiv R M₁ M₂) (h : (e : linear_map R M₁ M₂) = f) : e = f :=
begin
ext x,
show (e : linear_map R M₁ M₂) x = f x,
rw h,
refl,
end
```

The coe_fn_injective thing is just the first `ext`

. Looking at the goal I think one should train `norm_cast`

to do this.

#### Kevin Buzzard (Aug 01 2020 at 21:02):

```
example (e f : linear_equiv R M₁ M₂) (h : (e : linear_map R M₁ M₂) = f) : e = f :=
begin
apply linear_equiv.ext,
rwa linear_map.ext_iff at h,
end
```

#### Kevin Buzzard (Aug 01 2020 at 21:03):

```
example (e f : linear_equiv R M₁ M₂) (h : (e : linear_map R M₁ M₂) = f) : e = f :=
linear_equiv.ext (linear_map.ext_iff.1 h)
```

#### Heather Macbeth (Aug 01 2020 at 21:12):

Thanks!

#### Bryan Gin-ge Chen (Aug 01 2020 at 21:13):

I'm sad that `library_search`

doesn't work on this. `library_search!`

and `suggest`

just time out. @Scott Morrison

#### Kevin Buzzard (Aug 01 2020 at 21:16):

Is it already in the library? I use two theorems not one.

#### Kevin Buzzard (Aug 01 2020 at 21:18):

oh, `library_search`

finds this proof of the non-linear-algebra version:

```
example (e f : equiv M₁ M₂) (h : (e : M₁ → M₂) = f) : e = f :=
equiv.ext (congr_fun h)
```

#### Bryan Gin-ge Chen (Aug 01 2020 at 21:20):

Oh, I think you're right. `library_search`

uses `solve_by_elim`

which has `congr_fun`

in its set of lemmas.

#### Bryan Gin-ge Chen (Aug 01 2020 at 21:20):

So `library_search`

can't usually apply more than one theorem.

#### Bryan Gin-ge Chen (Aug 01 2020 at 21:36):

I guess that's an argument for adding this to the library.

#### Yury G. Kudryashov (Aug 01 2020 at 23:06):

See also the proofs of src#alg_hom.coe_ring_hom_injective and src#ring_hom.coe_monoid_hom_injective

Last updated: Dec 20 2023 at 11:08 UTC