## Stream: new members

### Topic: ifinish

#### Michael Beeson (Sep 12 2020 at 06:56):

ifinish doesn't succeed with this simple proposition:

example: ∀ (A B:Prop), (A → B) → ((A ∧ B) ↔ A)


This is not a question, or even a complaint really, I'm just trying to get familiar enough with ifinish so as to know
whether to expect it to succeed or not. I thought it would do this one.

it does for me

#### Michael Beeson (Sep 12 2020 at 07:31):

lemma lemma11helper1: ∀ (A B:Prop), (A → B) → ((A ∧ B) ↔ A) :=
assume A B,
begin
ifinish,
end


produces

solve1 tactic failed, focused goal has not been solved
state:
A B : Prop,
a : A → B,
f : Prop,
a_1 : (A ∧ B ↔ A) → f
⊢ f


So please post your corresponding input and successful output.

#### Markus Himmel (Sep 12 2020 at 07:32):

It works with current Lean and mathlib:

https://leanprover-community.github.io/lean-web-editor/#code=import%20tactic%0A%0Alemma%20lemma11helper1%3A%20%E2%88%80%20%28A%20B%3AProp%29%2C%20%28A%20%E2%86%92%20B%29%20%E2%86%92%20%28%28A%20%E2%88%A7%20B%29%20%E2%86%94%20A%29%20%3A%3D%0A%20%20assume%20A%20B%2C%0A%20%20begin%0A%20%20%20%20ifinish%2C%0A%20%20end%0A

#### Michael Beeson (Sep 12 2020 at 07:35):

Oh. So I should update lean using leanproject, I guess. I'm worried that some of my nice proofs might break then.

Last updated: May 13 2021 at 19:20 UTC