auto_param

Stream: general

[Patrick Massot]

I have a really dumb-sounding question: how can I get Lean to automatically use auto_params? I have a lemma with assumption (hconj : ∀ x₀ : α, tendsto (λ x: α, x₀*x*x₀⁻¹) 𝓝 1 𝓝 1 . prove_conj) where prove_conj tries to prove the assumption using commutativity of multiplication. My idea was that would succeed when the relevant multiplication is commutative, and leave the hypothesis to prove otherwise. But clearly I misunderstood how this all works. I can only use it by writing by apply_auto_param where wants a proof of hconj.

[Rob Lewis]

That is how it works in general, with the exception that the goal left when the tactic fails is kind of ugly. Do you have a MWE?

def my_fun {α} (a b : α) (h : a = b . tactic.interactive.reflexivity) : a = b := h

example : 1 = 1 := my_fun _ _

example : 1 = 1 := by apply my_fun

example : 1 = 2 :=
begin
  apply my_fun,
  dsimp, -- 1 = 2
end

[Patrick Massot]

I think I'm starting to understand. The magic argument has to come last, right?

[Patrick Massot]

This fails:

lemma my_fun {α} (a b : α) (h : a = b . tactic.interactive.reflexivity) (h' : 0 = 0) : a = b := h

example : 1 = 1 := my_fun 1 1 (rfl : 0 = 0)

[Patrick Massot]

which makes sense. But I was hoping to write:

lemma my_fun {α} (a b : α) (h : a = b . tactic.interactive.reflexivity) (h' : 0 = 0) : a = b := h

example : 1 = 1 := my_fun 1 1 _ (rfl : 0 = 0)

which also fails