## Stream: new members

### Topic: Specializing weak implicit arguments

#### Li Yao'an (Nov 21 2019 at 09:36):

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 (Nov 21 2019 at 11:55):

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

#### Mario Carneiro (Nov 21 2019 at 11:56):

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

#### Kevin Buzzard (Nov 21 2019 at 13:35):

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


Last updated: May 08 2021 at 17:33 UTC