# Zulip Chat Archive

## Stream: new members

### Topic: How to understand this "=" in "h = h₂"?

#### chenjulang (Dec 04 2023 at 06:16):

```
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 (Dec 04 2023 at 06:17):

Waiting......

#### Yongyi Chen (Dec 04 2023 at 06:18):

It's proof irrelevance! `i ∈ s`

is a `Prop`

and any two terms of the same `Prop`

are definitionally equal.

#### chenjulang (Dec 04 2023 at 06:18):

Oh

#### chenjulang (Dec 04 2023 at 06:32):

@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 (Dec 04 2023 at 06:33):

But I cannot prove it......

#### Yongyi Chen (Dec 04 2023 at 06:58):

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 `Prop`

s they like, and so `h = h₂`

cannot be proved.

#### chenjulang (Dec 04 2023 at 07:11):

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 (Dec 04 2023 at 07:12):

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

#### chenjulang (Dec 04 2023 at 07:12):

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

#### chenjulang (Dec 04 2023 at 07:21):

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 (Dec 04 2023 at 07:52):

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

#### chenjulang (Dec 04 2023 at 08:04):

Alright

Last updated: Dec 20 2023 at 11:08 UTC