## Stream: new members

### Topic: Using tfae theorem

#### Paul Rowe (Aug 14 2020 at 14:48):

I'm having trouble finding a simple explanation of how to use a tfae theorem. I have a theorem that basically looks like this

theorem thm1 : tfae [ a b c ] := sorry


(I have completed the proof.) I now need to use the fact that b -> c in the proof of another theorem. How do I access this fact from thm1?

I have run across some discussion of tfae.out but I can't immediately figure out how it works.

#### Mario Carneiro (Aug 14 2020 at 15:00):

I think tfae.out thm1 1 2 should be a proof of b -> c

#### Paul Rowe (Aug 14 2020 at 15:05):

That's what I tried first, but I get an error.

exact tactic failed, type mismatch, given expression has type
true
but is expected to have type
as_true (1 < [church_rosser ?m_2, confluent ?m_2, semiconfluent ?m_2].length)


(In this case, my a, b, c correspond to the properties church_rosser, confluent, semiconfluent.)

#### Mario Carneiro (Aug 14 2020 at 15:07):

namespace list
theorem tfae.out' {l} (h : tfae l) (n₁ n₂) {a b}
(h₁ : list.nth l n₁ = some a . control_laws_tac)
(h₂ : list.nth l n₂ = some b . control_laws_tac) :
a ↔ b :=
h _ (list.nth_mem h₁) _ (list.nth_mem h₂)
end list

example {a b c} (h : [a, b, c].tfae) : true :=
begin
have := h.out' 1 2,
end


#### Mario Carneiro (Aug 14 2020 at 15:08):

that error is a bit odd. You might have to specify ?m_2 (it should probably be an explicit argument to the theorem) but it should reduce even without that

#### Paul Rowe (Aug 14 2020 at 15:13):

Sorry. I'm still a newbie. How do I use that new version? Is that included in some library? If not, I am having trouble putting it into my file to use.

#### Mario Carneiro (Aug 14 2020 at 15:14):

I wrote it just now. You should just be able to put it at the top of your file

#### Mario Carneiro (Aug 14 2020 at 15:14):

make sure it's not in a namespace of yours

#### Paul Rowe (Aug 14 2020 at 15:23):

That works! I did end up having to make the implicit variable an explicit argument to the theorem. It didn't work otherwise. But that makes sense to me in my context. Thanks for the help!

Last updated: May 16 2021 at 21:11 UTC