# Zulip Chat Archive

## Stream: new members

### Topic: lean4 structure equality

#### Arien Malec (Oct 24 2022 at 21:09):

What's the Lean4 approach for this proof (or even one direction of it?)

```
structure Foo where
mk :: (bar : Nat)
theorem eq_ext (a b: Foo) : a = b ↔ a.bar = b.bar := sorry
```

#### Arien Malec (Oct 24 2022 at 22:11):

should probably note that I've tried what I would consider the usual; `rfl`

, various flavors of trying to destructure, `rw`

etc.

#### Julian Berman (Oct 24 2022 at 22:16):

Possibly there's a clevererer way to do it (which I can't check because I can't update mathlib4 yet :/), but here's a simplistic way that seems to work:

```
structure Foo where
mk :: (bar : Nat)
theorem eq_ext (a b: Foo) : a = b ↔ a.bar = b.bar :=
⟨λ h => by rw [h],
λ h => by cases a; cases b; simp [h]⟩
```

seems to do it here at least.

#### Mario Carneiro (Oct 24 2022 at 22:18):

With the `ext`

tactic you get it for free:

```
import Std.Tactic.Ext
@[ext] structure Foo where
mk :: (bar : Nat)
theorem eq_ext : ∀ (a b: Foo), a = b ↔ a.bar = b.bar := Foo.ext_iff
```

#### Arien Malec (Oct 24 2022 at 22:28):

Julian Berman said:

Possibly there's a clevererer way to do it (which I can't check because I can't update mathlib4 yet :/), but here's a simplistic way that seems to work:

`structure Foo where mk :: (bar : Nat) theorem eq_ext (a b: Foo) : a = b ↔ a.bar = b.bar := ⟨λ h => by rw [h], λ h => by cases a; cases b; simp [h]⟩`

seems to do it here at least.

OK, I get the `mp`

direction, which seems obvious in retrospect. The `mpr`

direction seems like magic.

I go from

```
case mpr.mk.mk
bar✝¹bar✝: Nat
h: { bar := bar✝¹ }.bar = { bar := bar✝ }.bar
⊢ { bar := bar✝¹ } = { bar := bar✝ }
```

to :tada: via `simp [h]`

but it doesn't feel like there's anything to apply `simp`

to that isn't already in the premise...

#### Mario Carneiro (Oct 24 2022 at 22:37):

Here's another way to write the proof:

```
theorem eq_ext (a b: Foo) : a = b ↔ a.bar = b.bar :=
⟨λ h => by rw [h],
λ h => by
match a, b, h with
| ⟨a_bar⟩, ⟨b_bar⟩, (h : a_bar = b_bar) =>
rw [h]⟩
```

#### Mario Carneiro (Oct 24 2022 at 22:38):

The point is that after the two `cases`

, `h`

, which has the type `⟨a_bar⟩.bar = ⟨b_bar⟩.bar`

, is definitionally equal to `h : a_bar = b_bar`

and so we can use the same proof as the first half - we're just applying the `mk`

function to both sides to get equal values.

Last updated: Dec 20 2023 at 11:08 UTC