How to refer to unnamed proofs in term mode?

Stream: lean4

[Mario Weitzer]

This is a very basic question but how can I avoid using tactic mode in a proof like this one:

lemma l1 (n : Nat) (_ : n = 0) : n = 0 := by
  assumption

lemma l2 (n : Nat) (_ : n = 0) : n = 0 := by
  expose_names
  exact h

lemma l3 (n : Nat) (_ : n = 0) : n = 0 := by
  revert n
  exact fun n h => h

#print l1
-- theorem l1 : ∀ (n : Nat), n = 0 → n = 0 := fun n x ↦ x
#print l2
-- theorem l2 : ∀ (n : Nat), n = 0 → n = 0 := fun n x ↦ x
#print l3
-- theorem l3 : ∀ (n : Nat), n = 0 → n = 0 := fun n x ↦ x

lemma l4 (n : Nat) (_ : n = 0) : n = 0 := fun n x ↦ x
-- Doesn't work for obvious reasons, even though it's just a copy of what #print claims to be the proof term of l1, l2, and l3.

[Michael Rothgang]

If you want to refer to the hypothesis on n, you should give it a name (not just an underscore).

[Michael Rothgang]

#print doesn't say "it's unnamed", by the way (it wouldn't print names for named arguments either, but prints the type of the statement).

[Mario Weitzer]

Michael Rothgang said:

#print doesn't say "it's unnamed", by the way (it wouldn't print names for named arguments either, but prints the type of the statement).

I know that giving it a name would solve the problem but this is just a minimal example of an artificial situation in which I don't have a name, which can occur in some situations. For example, it's not common to give names to type class instances (even though I'm aware that it is possible to name them as well)

lemma l5 (n : Nat) [Fact (n = 0)] : n = 0 := by
  exact Fact.elim (by assumption)

#print l5
-- l5 : ∀ (n : Nat) [Fact (n = 0)], n = 0 := fun n [inst : Fact (n = 0)] ↦ Fact.elim inst

There must be a way to complete these proofs without going into tactic mode, isn't there?

[Damiano Testa]

Would using exact?% be a solution? :upside_down:

[Jovan Gerbscheid]

Here are some of the ways you might do this:

import Mathlib

example (n : Nat) [Fact (n = 0)] : n = 0 := by
  exact Fact.elim ‹Fact (n = 0)›

example (n : Nat) [Fact (n = 0)] : n = 0 := by
  exact Fact.elim inferInstance

example (n : Nat) [Fact (n = 0)] : n = 0 := by
  expose_names
  exact Fact.elim inst

example (n : Nat) [Fact (n = 0)] : n = 0 := by
  rename_i bla
  exact Fact.elim bla

[Mario Weitzer]

Jovan Gerbscheid said:

Here are some of the ways you might do this:

import Mathlib

example (n : Nat) [Fact (n = 0)] : n = 0 := by
  exact Fact.elim ‹Fact (n = 0)›

example (n : Nat) [Fact (n = 0)] : n = 0 := by
  exact Fact.elim inferInstance

example (n : Nat) [Fact (n = 0)] : n = 0 := by
  expose_names
  exact Fact.elim inst

example (n : Nat) [Fact (n = 0)] : n = 0 := by
  rename_i bla
  exact Fact.elim bla

Yes, but all of these use tactics. I want to prove it without going into tactic mode (so no "by" anywhere).

[Yaël Dillies]

The exact term mode equivalent of assumption is ‹_›

[Jovan Gerbscheid]

The first two options work in term mode

[Yaël Dillies]

In general, ‹Foo› is the same as (by assumption : Foo)

[Mario Weitzer]

Yaël Dillies said:

The exact term mode equivalent of assumption is ‹_›

I see, thanks! (to all of you)

[Ruben Van de Velde]

But also the solution is usually "don't get into this situation" (i.e., name the hypothesis when you have the chance)

[Damiano Testa]

Isn't ‹_› a macro for by assumption, though? Does that really count as "not using tactic mode"?