Can't synthesize argument

Stream: new members

[Nir Paz]

I have a proof with a few assumptions (as variables) that are used in all the lemmas, and I can't get to a point where I don't have to explicitely write them every time I use something I proved. I thought something like this would work (so for example I wouldn't have to add h as an argument everywhere I use t):

import Mathlib

variable {α : Type*} {a : α} {P : α → Prop} {h : P a}

theorem t : ∃ x : α, P x := ⟨a, h⟩

theorem t' : ∃ x : α, P x := t -- fails

but it doesn't. Even if I replace the last line with

theorem t : ∃ x : α, P x := @t α a P _

it fails, with the funny looking context:

h : P a
⊢ P a

Why doesn't this work? And is there a better way to add some variables as hypotheses throughtout a section and not have to ever pass them as arguments explicitly?

[Kyle Miller]

The issue is that it can't infer the proof of P a using only unification. If you change it like so, you can pass h in:

variable {α : Type*} {a : α} {P : α → Prop} (h : P a)

theorem t : ∃ x : α, P x := ⟨a, h⟩

theorem t' : ∃ x : α, P x := t h

[Kyle Miller]

This is likely not a good idea, but you can configure the h argument to have a tactic it tries to run to fill itself in.

variable {α : Type*} {a : α} {P : α → Prop} (h : P a := by assumption)

theorem t : ∃ x : α, P x := ⟨a, h⟩

theorem t' : ∃ x : α, P x := t

[Kyle Miller]

(For both of these, make sure to check out the type of t to see what's going on.)

[Nir Paz]

I didn't know about running tactics like this, that's really cool! It seems to not work in more complicated cases when it's not the last argument to a theorem.

I might post the full code on another stream, but basically I do some constructions on a linear order that satisfies a condition h, so I make variables for a type, a linear order on it, and the assumption h about it. If I make h is explicit, I have to write it every time I use a previous construction when defining the next one (defining it with a tactic like this doesn't work because there are other arguments) which ends up being dozens of times. And defining it implicitly just doesn't work.