# Zulip Chat Archive

## Stream: new members

### Topic: Lean displaying _ in local context

#### Keefer Rowan (May 20 2020 at 22:08):

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 (May 20 2020 at 22:13):

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 (May 20 2020 at 22:14):

try putting

```
set_option pp.implicit true
```

it may show you what's wrong

#### Alex J. Best (May 20 2020 at 22:14):

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 (May 20 2020 at 22:14):

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

#### Keefer Rowan (May 20 2020 at 22:20):

Any idea why `rw subtype.mk.inj_eq at h`

isn't working?

#### Alex J. Best (May 20 2020 at 22:24):

Not without a #mwe ;)

Last updated: May 06 2021 at 21:09 UTC