rewriting `forall m in S`

Stream: new members

[Ralf Stephan]

What do I need to know, in order to understand why the first example below works, but not the second?

import Mathlib

open Nat

example (P : Prop) (S T : Set ℕ) (h' : ∀ m ∈ S, P)
    (h : S = T) : ∀ m ∈ T, P := by
  rw [←h]
  exact h'

example (P : Prop) (S : Set ℕ) (L : List ℕ) (h' : ∀ m ∈ S, P)
    (h : m ∈ S ↔ m ∈ L) : ∀ m ∈ L, P := by
  rw [←h]
  exact h'

[Yaël Dillies]

Write set_option autoImplicit false before the examples

[Ralf Stephan]

So, (m : ℕ) is missing but it still doesn't work.

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  m ∈ L
P: Prop
m: ℕ
S: Set ℕ
L: List ℕ
h': ∀ m ∈ S, P
h: m ∈ S ↔ m ∈ L
⊢ ∀ m ∈ L, P

[Riccardo Brasca]

What do you think your h : m ∈ S ↔ m ∈ L mean? What is m?

[Yaël Dillies]

Let me rewrite your new statement a bit:

example (P : Prop) (S : Set ℕ) (L : List ℕ) (m : ℕ) (h' : ∀ l ∈ S, P)
    (h : m ∈ S ↔ m ∈ L) : ∀ l ∈ L, P :=

[Yaël Dillies]

Do you see the issue?

[Ralf Stephan]

m is a variable? The statement is a bi-implication?

[Yaël Dillies]

Yes, but does it have anything to do with the l in your ∀ l ∈ L binder?

[Ralf Stephan]

Giving m via `rw [←h m] also doesn't work.

[Riccardo Brasca]

Do you want ∀ m, m ∈ S ↔ m ∈ L?

[Ralf Stephan]

isn't that implicit?

[Riccardo Brasca]

No, if you look at the infoview for

example (P : Prop) (S : Set ℕ) (L : List ℕ) (h' : ∀ m ∈ S, P)
    (h : m ∈ S ↔ m ∈ L) : ∀ m ∈ L, P := by

you see that Lean created a natural number called m to make sense of h : m ∈ S ↔ m ∈ L.

[Riccardo Brasca]

But this m is fixed

[Ralf Stephan]

It looks to me that ∀ m, m ∈ S ↔ m ∈ L behaves like m ∈ S ↔ m ∈ L. Do you say that the goal cannot be matched, and the rewrite not be done?

[Riccardo Brasca]

If you dont write the ∀ binder, Lean just assumes that this double implication holds for one specific number. This is exactly the same difference between ∀ m, m ∈ S ↔ m ∈ L and 37 ∈ S ↔ 37 ∈ L.

[Riccardo Brasca]

Your goal at the beginning is ∀ m ∈ L, P. The natural strategy here is to start with intro x. Now the goal is x ∈ L → P, so we do another intro hx. Now you have to prove P, and you have a number x such that x ∈ L. You want to use that m ∈ S ↔ m ∈ L to obtain that x ∈ s, but x and m are completely unrelated.

[Ralf Stephan]

I keep forgetting that intro splits off conditions also from forall statements. Thanks. That is embarrassing.

[Ralf Stephan]

hint wouldn't suggest intro either. Wouldn't that be useful?

[Riccardo Brasca]

I don't understand the question, hint suggests intro for me.

[Ralf Stephan]

In the original code, agreed. Not here, though:

import Mathlib
set_option autoImplicit false

example (P : Prop) (S : Set ℕ) (L : List ℕ) (h' : ∀ m ∈ S, P)
    (h : ∀ m, m ∈ S ↔ m ∈ L) : ∀ m ∈ L, P := by
  hint