understanding simp and interaction with iff and hypotheses

Stream: lean4

[Yakov Pechersky]

Consider the following example, pbind_eq_some_iff, which is a mwe of pbind_eq_some, in porting in Mathlib.Data.Option.Basic for mathlib4. Some questions: why is the only working proof here the one that is simp only ... <;> intro h <;> simp at h? Why does just simp not work? Does one need the new simp_intros? Why does the simp at * version not work? That issue is regardless of whether the intro-d hypothesis named or not:

@[simp] theorem not_exists {α : Sort _} {p : α → Prop} : (¬∃ x, p x) ↔ ∀ x, ¬p x := sorry

namespace Option

instance : Membership α (Option α) := ⟨fun a b => b = some a⟩

variable {x : Option α}

@[simp] theorem mem_def {a : α} {b : Option α} : a ∈ b ↔ b = some a := .rfl

@[simp]
def pbind : ∀ x : Option α, (∀ a : α, a ∈ x → Option β) → Option β
  | none, _ => none
  | some a, f => f a rfl

theorem pbind_eq_some_imp {f : ∀ a : α, a ∈ x → Option β} {y : β} :
    x.pbind f = some y → ∃ (z : α) (H : z ∈ x), f z H = some y := by
  cases x
  · simp
  · sorry

-- why does this not work when the `imp` version does?
theorem pbind_eq_some_iff {f : ∀ a : α, a ∈ x → Option β} {y : β} :
    x.pbind f = some y ↔ ∃ (z : α) (H : z ∈ x), f z H = some y := by
  cases x
  · simp -- doesn't work all the way
    sorry
  · sorry

theorem pbind_eq_some_iff' {f : ∀ a : α, a ∈ x → Option β} {y : β} :
    x.pbind f = some y ↔ ∃ (z : α) (H : z ∈ x), f z H = some y := by
  cases x
  · simp only [pbind, false_iff, not_exists]
    intro z h
    simp at h
  · sorry

-- why does this not work when the previous `intro h, simp at h` did?
theorem pbind_eq_some_iff'' {f : ∀ a : α, a ∈ x → Option β} {y : β} :
    x.pbind f = some y ↔ ∃ (z : α) (H : z ∈ x), f z H = some y := by
  cases x
  · simp only [pbind, false_iff, not_exists] -- also red line is here and not at `simp at *`
    intro z h
    simp at * -- doesn't work
  · sorry

end Option

[Kevin Buzzard]

In Lean 3 there was something like simp {something:=tt} which would do the intros for you

[Mario Carneiro]

you mean simp {contextual := tt}?

[Mario Carneiro]

that's spelled simp (config := {contextual := true}) now

[Kevin Buzzard]

I never really understood whether that was simp_intros or whether it just happened to do what simp_intros did

[Mario Carneiro]

Oh, simp_intros is something else

[Mario Carneiro]

maybe that's what you want here, I didn't read closely

[Mario Carneiro]

simp {contextual := tt} will make use of hypotheses that enter the context when it "rewrites under binders"

[Mario Carneiro]

so for example \forall (h : a = b), a + a = 1 will simp to \forall (h : a = b), b + b = 1