## Stream: general

### Topic: What does "apply_instance" do?

#### Bernd Losert (Jan 10 2022 at 17:11):

I'm looking at https://leanprover-community.github.io/mathlib_docs/order/filter/ultrafilter.html#ultrafilter.unique and it has an argument (hne : g.ne_bot . "apply_instance"). What exactly is this doing?

#### Eric Wieser (Jan 10 2022 at 17:11):

tactic#apply_instance

#### Adam Topaz (Jan 10 2022 at 17:12):

it will try to apply the tactic apply_instance if you dont provide a term for that variable.

#### Eric Wieser (Jan 10 2022 at 17:12):

But I suspect your question is actually "what does some_type . "some_tactic" mean", which is syntax for docs#auto_param

#### Bernd Losert (Jan 10 2022 at 17:17):

So if I don't supply the theorem a hne, it's going to try to get one via instance search?

yep

I see.

#### Adam Topaz (Jan 10 2022 at 17:18):

auto_params are heavily used in the category theory library with the tactic obviously (which is essentially tidy) to automatically prove that simple diagrams commute. It's very useful.

#### Bernd Losert (Jan 10 2022 at 17:20):

I think I've seen it used to supply some default proofs that the composition in a category is associative and that the identity works as expected.

#### Bernd Losert (Jan 10 2022 at 17:21):

Yep: (f ≫ g) ≫ h = f ≫ g ≫ h) . "obviously"

#### Adam Topaz (Jan 10 2022 at 17:22):

right, so if you omit that field, then lean will try to use prove associativity by itself using the tactic obviously

#### Bernd Losert (Jan 10 2022 at 17:23):

Yeah, that's pretty cool.

#### Eric Wieser (Jan 10 2022 at 18:25):

(hne : g.ne_bot . "apply_instance") is particularly unusual though since [hne : g.ne_bot] means almost the same thing

Last updated: Dec 20 2023 at 11:08 UTC