Tactic to avoid `classical.some`

Stream: general

[Kevin Buzzard]

My goal was this:

⊢ comm_ring.zero (ring_completion (valuation_field (out (⟨⟨v, _⟩, _⟩.val)))) =
    domain.zero (ring_completion (valuation_field (out (⟨⟨v, _⟩, _⟩.val))))

and I tried dunfold out. This took me to the following slightly scary goal:

⊢ comm_ring.zero (ring_completion (valuation_field (classical.some _))) =
    domain.zero (ring_completion (valuation_field (classical.some _)))

I don't like classical.somes in my term. They come with a corresponding very helpful classical.some_spec which is hard to keep track of if you have proof terms turned off. Was dunfold out an incorrect move? How can I get the correct some_specs into my context somehow?

[Mario Carneiro]

what about generalize : (out (⟨⟨v, _⟩, _⟩.val)) = k?

[Mario Carneiro]

A tactic like split_ifs for classical.some would be nice

[Simon Hudon]

I think you will find such a tactic here: https://github.com/unitb/lean-lib/blob/master/src/util/classical.lean

[Simon Hudon]

I can PR it tomorrow. Or if you need it urgently, feel free to take it

[Kevin Buzzard]

I can't get it to work :-/

generalize tactic failed, result is not type correct
nested exception message:
check failed, application type mismatch (use 'set_option trace.check true' for additional details)
state:
4 goals
A : Huber_pair,
v : ↥A → ↥A → Prop,
Γ : Type u_1,
_inst_2 : linear_ordered_comm_group Γ,
v₀ : valuation ↥A Γ,
h : ∀ (r s : ↥A), ⇑v₀ r ≤ ⇑v₀ s ↔ v r s,
h1 : is_continuous ⟨v, _⟩,
h2 : ∀ (r : ↥A), r ∈ (λ (A : Huber_pair), A.Rplus) A → ⇑⟨v, _⟩ r ≤ 1
⊢ comm_ring.zero (ring_completion (valuation_field (classical.some _))) =
    domain.zero (ring_completion (valuation_field (classical.some _)))

Should I be applying the tactic before or after the state looks like this? I just dunfolded something and they all appeared.