How to understand this "=" in "h = h₂"?

Stream: new members

[chenjulang]

lemma foo1 (s : Set ι) (i : ι) (h h₂ : i ∈ s) : h = h₂ := by
  rfl
#print foo1

theorem foo2 : ∀ {ι : Type u_1} (s : Set ι) (i : ι) (h h₂ : i ∈ s), h = h₂ :=
  fun {ι} s i h h₂ ↦ Eq.refl h

[chenjulang]

Waiting......

[Yongyi Chen]

It's proof irrelevance! i ∈ s is a Prop and any two terms of the same Prop are definitionally equal.

[chenjulang]

Oh

[chenjulang]

@Yongyi Chen Can I change it into the following theorem?

theorem foo3 : ∀ {ι : Type u_1} (s : Set ι) (i : ι) (h h₂ :Prop := i ∈ s), h = h₂ := by
  intros h1 h2 h3 h4 h5
  refine (Iff.to_eq ?h).symm
  constructor
  intro  h6

[chenjulang]

But I cannot prove it......

[Yongyi Chen]

After some digging, I have found that the syntax (h h₂ : Prop := i ∈ s) means that h and h₂ are optional parameters of type Prop with default values i ∈ s. Of course this means the user of the theorem can set h and h₂ to whatever Props they like, and so h = h₂ cannot be proved.

[chenjulang]

like this , Right?

variable (h1 : 0<1) (h2 : 0<1)
#check h1 -- h1 : 0 < 1
#check h2 -- h2 : 0 < 1
theorem foo2:  h1 = h2 := by
  exact rfl

[Yongyi Chen]

I don't know what you mean by "like this."

[chenjulang]

If h1 and h2 has the same "type" , they are equal

[chenjulang]

But these h1 and h2 is not equal.
Seems like self-defined type such as "0 < 1" would work,
But System-defined type such as "N" cannot work.

variable (h1 : ℕ ) (h2 : ℕ )
#check h1 -- h1 : ℕ
#check h2 -- h2 : ℕ
theorem foo3:  h1 = h2 := by

[Ruben Van de Velde]

You may benefit from reading this chapter of #tpil: https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html

[chenjulang]

Alright