strange [ ]'s in my goal

Stream: general

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I was using delta :-)

[Keeley Hoek]

Is that something unfold_projs can fix

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

They are a dead end for me.

[Keeley Hoek]

ok :'(

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

I assume rfl doesn't work?

[Mario Carneiro]

you can always use change to say what the zero is

[Kevin Buzzard]

I assume rfl doesn't work?

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

[Kevin Buzzard]

The zero is some gigantic term when I unfold it.