# Zulip Chat Archive

## Stream: new members

### Topic: Statements that require a previous result

#### Markus Himmel (Feb 09 2020 at 13:31):

How do you state something that only makes sense using some previous result? Consider the following MWE:

section parameters {A : Type} {B : Type} def f : A → A := id def g : B → B := id lemma A_eq_B : A = B := sorry lemma does_not_typecheck : f = g := sorry -- this one is problematic end

The lemma generates the error "type mismatch at application f = g term has type B → B but is expected to have type A → A". What would be the correct way to state this lemma in Lean that somehow uses the fact that A = B?

#### Mario Carneiro (Feb 09 2020 at 13:33):

There are two ways, neither very good. You can use `f == g`

to assert that `f`

and `g`

have the same type, or you can use `eq.rec`

to convert one type to the other

#### Mario Carneiro (Feb 09 2020 at 13:35):

section parameters {A : Type} {B : Type} def f : A → A := id def g : B → B := id lemma A_eq_B : A = B := sorry example : f == g := by cases A_eq_B; refl example : (eq.rec_on A_eq_B f : B → B) = g := by cases A_eq_B; refl end

#### Mario Carneiro (Feb 09 2020 at 13:35):

But the real answer is: don't do this

#### Mario Carneiro (Feb 09 2020 at 13:36):

in your real example it might be warranted, but in this example it's clearly a bad idea

#### Mario Carneiro (Feb 09 2020 at 13:41):

There is an easy `cases; refl`

proof in this case because `f`

and `g`

are the same function, but in real examples the proof would be harder

#### Markus Himmel (Feb 09 2020 at 14:29):

Thank you for the answer. I experimented with `eq.rec_on`

, and while I was able to prove the lemma that inspired this question, I ran into problems when trying to apply the lemma (as you predicted). However I am working with categories and found a solution using `eq_to_hom`

where all the instances of `eq_to_hom`

cancel out nicely.

#### Kevin Buzzard (Feb 09 2020 at 16:58):

Equality of types is a hairy thing. In your example you'd be better off knowing that if A=B then there's a map from A to B, and using this map instead of all these heq workarounds

#### Kevin Buzzard (Feb 09 2020 at 17:00):

At one point when doing basic group theory I had two equal normal subgroups of a group and I wanted to identify the quotients. I did it by writing down maps both ways between them instead of trying to use `=`

Last updated: May 08 2021 at 18:17 UTC