How to get hold of subterms deep inside a Prop?

[htzh]

I would like to prove the following:

import data.set
namespace function
section
open set
variables {A B : Type}
definition bijective (f : A → B) := injective f ∧ surjective f
lemma injective_eq_inj_on_univ (f : A → B) : injective f = inj_on f univ :=
  begin
    esimp [injective, inj_on, univ, mem],
  end
end
end function

After esimp the goal is now:

⊢ (∀ (a₁ a₂ : A), f a₁ = f a₂ → a₁ = a₂) = ∀ ⦃x1 x2 : A⦄,
    true → true → f x1 = f x2 → x1 = x2

I can use true_imp

theorem true_imp (a : Prop) : (true → a) ↔ a

Is there a way to do it without manually breaking down the structure (with propext, iff.intro, assume ......)?

[htzh]

This works:

lemma injective_eq_inj_on_univ (f : A → B) : injective f = inj_on f univ :=
  begin
    esimp [injective, inj_on, univ, mem],
    apply propext,
    apply iff.intro,
      intro Pl a1 a2,
        rewrite *(propext !true_imp),
        exact Pl a1 a2,
      intro Pr a1 a2,
        assert Ptrue : true, apply true.intro,
        exact Pr Ptrue Ptrue
  end
end

I am wondering if there is a better way.

[leodemoura]

Here is a smaller one:

lemma injective_eq_inj_on_univ₃ (f : A → B) : injective f = inj_on f univ :=
  begin
    esimp [injective, inj_on, univ, mem],
    apply propext,
    repeat (apply forall_congr; intros),
    rewrite *(propext !true_imp)
  end

BTW, I've just implemented an extension that uses propext automatically in the rewrite tactic. That is, it will allow us to write rewrite true_imp instead of rewrite (propext !true_imp). I will push as soon as I finish testing it.

This kind of problem will be perfect for the bottom-up simplifier that will have in Lean. This simplifier automatically applies forall_congr and funext to go inside of binders.

[leodemoura]

I pushed the new feature. Here is the new version for the lemma above https://github.com/leanprover/lean/blob/master/tests/lean/run/tut_104.lean#L41-L48

[htzh]

Great! Good to learn repeat (apply forall_congr; intros) too. Thanks!