Specializing weak implicit arguments

Stream: new members

[Li Yao'an]

I'm trying to work with the inductive definition in mathlib. If I didn't misinterpret the notation, it uses weak implicit arguments in the forall quantifier, which I am having trouble trying to specialize, since unlike normal arguments, h a does not specialize the hypothesis with argument a. The exact example I'm trying to do is below. How does one deal with these weak implicit arguments?

def bijective' {α β} (f : α → β) : Prop :=
    ∃ f' : β → α, (∀ a : α, f' (f a) = a) ∧ (∀ b : β, f (f' b) = b)

theorem bijective_iff_bijective' {α β} (f : α → β) : bijective f ↔ bijective' f :=
begin
    dunfold bijective bijective' surjective injective, split,
        {intro h, cases h with h1 h2, existsi λ b, classical.some (h2 b), simp, split,
            {intro a, have h3 := some_spec (h2 (f a)), sorry}, -- How to resolve this?
            {sorry}},
        {sorry},
    done
end

[Mario Carneiro]

You don't really need to in this case, you can just fill the sorry with exact h1 h3

[Mario Carneiro]

but you can apply a weak implicit using @h1 (some _) a

[Kevin Buzzard]

Note also the choose tactic:

import tactic.interactive

open function

def bijective' {α β} (f : α → β) : Prop :=
    ∃ f' : β → α, (∀ a : α, f' (f a) = a) ∧ (∀ b : β, f (f' b) = b)

theorem bijective_iff_bijective' {α β} (f : α → β) : bijective f ↔ bijective' f :=
begin
  split,
  { intro h,
    choose f' h' using h.2,
    use f',
    split,
      sorry,
    exact h',
  },
  sorry
end