Proving if rhs is `some a` lhs must be `some`

Stream: mathlib4

[Arien Malec]

I have

h : (match f b with
  | Sum.inl a => some a
  | Sum.inr val => none) =
  some a'

that I'd like to reduce to some a = some a'

but I haven't found the lemmata that get me there...

[Kevin Buzzard]

Do cases on f b

[Kevin Buzzard]

Or maybe try cases on h

[Sebastian Ullrich]

split at h should work too

[Arien Malec]

Hmm. I have an f b in both hypothesis and goal -- is there a way to make Lean 4 recognize that in the cases or splits? Otherwise, I get the goal and hypothesis with different names and run into a corner...

[David Renshaw]

maybe (generalizing := true) would help? https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Reusing.20knowledge.20from.20a.20pattern.20match/near/242485680

[Kevin Buzzard]

#mwe ?

[Arien Malec]

Indeed -- I'm working on hacking it out from the middle of the proof.

[Kevin Buzzard]

For a question such as this, any working example should be fine.

[Arien Malec]

I think this does it:

import Mathlib.Data.Sum.Basic

def foo (f : β → Sum α β) : Sum α β → Option α × Sum α β
  | Sum.inl a => (some a, Sum.inl a)
  | Sum.inr b =>
    (match f b with
      | Sum.inl a => some a
      | Sum.inr _ => none,
      f b)

theorem bar (h: (foo f (Sum.inr b)).fst = some a') :
      (foo f (foo f (Sum.inr b)).snd).fst = some a' := by
    dsimp [foo] at *
    sorry

[Arien Malec]

Tactic state is:

α: Type u
β: Type v
γ: Type w
β✝: Type u_1
α✝: Type u_2
f: β✝ → α✝ ⊕ β✝
b: β✝
a': α✝
h: (match f b with
  | Sum.inl a => some a
  | Sum.inr val => none) =
  some a'
⊢ (match f b with
    | Sum.inl a => (some a, Sum.inl a)
    | Sum.inr b =>
      (match f b with
        | Sum.inl a => some a
        | Sum.inr val => none,
        f b)).fst =
  some a'

Most of the moves I try get me to corners where I have the goal as some a_dagger = none where it logically should only be in that state if h is a contradiction.

[Sebastian Ullrich]

That doesn't look solvable, the inner f b uses a different b

[Arien Malec]

When I hover over the goal state, they are all f : β✝ → α✝ ⊕ β✝

[Arien Malec]

and b : β✝

[Arien Malec]

Everything right up to this point is straight out of the mathport output....

[Arien Malec]

What does appear odd is that the as are different between Sum.inl a and some a but again I haven't changed anything here out of the port.

[Arien Malec]

got it...

import Mathlib.Data.Sum.Basic

def foo (f : β → Sum α β) : Sum α β → Option α × Sum α β
  | Sum.inl a => (some a, Sum.inl a)
  | Sum.inr b =>
    (match f b with
      | Sum.inl a => some a
      | Sum.inr _ => none,
      f b)

theorem bar (h: (foo f (Sum.inr b)).fst = some a') :
      (foo f (foo f (Sum.inr b)).snd).fst = some a' := by
    dsimp [foo] at *
    revert h
    cases' f b with a b' <;> dsimp <;> intro h
    · rw [← h]
    · contradiction

[Sebastian Ullrich]

Oh I guess I misread the goal

    unfold foo at *
    split <;> simp_all

[Arien Malec]

Cool - is there a deep reason why I had to revert to use cases properly above, but split works fine?

Also: any reason to prefer unfold foo at * vs dsimp [foo] at *?

[Sebastian Ullrich]

split introduces an extra hypothesis, the same works with cases as well

by
    cases h' : f b <;> simp_all!

[Sebastian Ullrich]

Arien Malec said:

Also: any reason to prefer unfold foo at * vs dsimp [foo] at *?

It's one character shorter :)