Lean displaying _ in local context

Stream: new members

[Keefer Rowan]

I can't come up with a simpler example of this phenomenon, so I can only give you a slightly convoluted one. A complicated function I defined has one of its equations printed by Lean (by the #print command) as

set.subset_of_sts_all_less_than_finite_func.equations._eqn_2 : ∀ {n : ℕ} (m : ℕ) (A : set (all_less_than n).set_to_subtype)
(h : A.subset_of_sts_all_less_than_finite_size_of = m.succ) (x_val : (all_less_than n).set_to_subtype)
(x_property : x_val ∈ A),
  subset_of_sts_all_less_than_finite_func h ⟨x_val, x_property⟩ =
    dite (x_val = classical.some _) (λ (hyp : x_val = classical.some _), ⟨m, _⟩)
      (λ (hyp : ¬x_val = classical.some _), ⟨(subset_of_sts_all_less_than_finite_func _ ⟨x_val, _⟩).val, _⟩)

Note the _. These terms are fairly complicated and it doesn't seem like they can be inferred from the local context, so I'm confused as to why Lean represents them with _. Is this a a printing option?

My problem is that these _'s propagate when trying to prove stuff about my definition, making it hard to complete proofs as an important part of the definition is just given as _.

[Keefer Rowan]

As an example of the problem I'm having, I have this in my local context,

h : ⟨m, _⟩ = ⟨(subset_of_sts_all_less_than_finite_func _ ⟨y_val, _⟩).val, _⟩

but rw subtype.mk.inj_eq at h, fails as rewrite tactic failed, did not find instance of the pattern in the target expression ⟨?m_3, ?m_4⟩ = ⟨?m_5, ?m_6⟩, which doesn't make any sense, but I'm assuming it has something to do with the _'s.

[Anas Himmi]

try putting

set_option pp.implicit  true

it may show you what's wrong

[Alex J. Best]

It's because they are proofs (so terms whose type is a Prop) so any two proofs of the same prop are equal, hence sometimes not that relevant to see them all the time, this can be controlled with set_option pp.proofs true

[Alex J. Best]

set_option pp.proofs true
noncomputable theory
lemma t : classical.some (⟨1, dec_trivial⟩: ∃ p, 0 < p) = 2 := sorry
#print t

[Keefer Rowan]

Any idea why rw subtype.mk.inj_eq at h isn't working?

[Alex J. Best]

Not without a #mwe ;)