## Stream: general

### Topic: strange [ ]'s in my goal

#### Kevin Buzzard (Apr 21 2019 at 04:49):

1 goal
A : Huber_pair,
v : Spv ↥A,
hv : v ∈ Spa A
⊢ [comm_ring.zero (ring_completion.comm_ring (valuation_field (out (⟨v, hv⟩.val))))] =
[domain.zero division_ring.to_domain]


Where did those square brackets come from? They're there whether or not I have notation on.

#### Mario Carneiro (Apr 21 2019 at 04:50):

That's the projection macro, you probably unfolded something you shouldn't have

#### Kevin Buzzard (Apr 21 2019 at 04:52):

Yeah, I was trying to get to the bottom of things.

#### Kevin Buzzard (Apr 21 2019 at 04:52):

I was using delta :-)

#### Keeley Hoek (Apr 21 2019 at 04:53):

Is that something unfold_projs can fix

#### Kevin Buzzard (Apr 21 2019 at 04:59):

I decided to take a different route. I'll go back and take a look.

#### Kevin Buzzard (Apr 21 2019 at 05:01):

unfold_projs failed to simplify
state:
A : Huber_pair,
v : Spv ↥A,
h1 : is_continuous v,
h2 : ∀ (r : ↥A), r ∈ (λ (A : Huber_pair), A.Rplus) A → ⇑v r ≤ 1
⊢ [comm_ring.zero (ring_completion.comm_ring (valuation_field (out v)))] =
[discrete_field.zero (completable_top_field.discrete_field (valuation_field (out v)))]


#### Kevin Buzzard (Apr 21 2019 at 05:01):

They are a dead end for me.

ok :'(

#### Kevin Buzzard (Apr 21 2019 at 05:02):

Is it likely that, if what I'm trying to prove is provable (possibly noncomputably), then there will be a proof which avoids those weird square brackets? Do I ever have to deal with them as an end user?

#### Mario Carneiro (Apr 21 2019 at 05:05):

It is possible to unfold them to a comm_ring.rec application, but it's a sign that you are unfolding things that you shouldn't

#### Mario Carneiro (Apr 21 2019 at 05:05):

you should not ever have to see them as an end user

#### Mario Carneiro (Apr 21 2019 at 05:06):

I assume rfl doesn't work?

#### Mario Carneiro (Apr 21 2019 at 05:07):

you can always use change to say what the zero is

#### Kevin Buzzard (Apr 21 2019 at 05:07):

I assume rfl doesn't work?

That's right -- that's what I'm trying to debug.

#### Kevin Buzzard (Apr 21 2019 at 05:07):

The zero is some gigantic term when I unfold it.

Last updated: May 11 2021 at 00:31 UTC