# Zulip Chat Archive

## Stream: new members

### Topic: Distributing ↑ over (v + 0)

#### Martin C. Martin (Nov 06 2023 at 18:49):

As an exercise, I'm defining vector spaces in Lean. However, I'm having trouble proving v + 0 = v in a subspace.

`intro v; ext`

reduces the goal to ↑(v + 0) = ↑v, and next I'm hoping for something to distribute the ↑ on the left hand side. In Lean 3, `simp`

would do that, but in Lean 4, `simp`

just undoes the `ext`

. I want to get to where I can use `rw [AddCommGroup.add_zero]`

to finish the proof.

Here's my #mwe, sorry it's so long:

```
import Mathlib.Algebra.Field.Basic
import Mathlib.Data.SetLike.Basic
namespace LADR
@[ext]
class AddCommGroup (V : Type _) extends Add V, Zero V, Neg V where
add_comm : ∀ u v : V, u + v = v + u
add_assoc : ∀ u v w : V, u + v + w = u + (v + w)
add_zero : ∀ v : V, v + 0 = v
add_right_inv : ∀ v : V, v + -v = 0
@[ext]
class VectorSpace (F : Type _) (V : Type _) [Field F] [AddCommGroup V] extends SMul F V where
smul_assoc : ∀ a b : F, ∀ v : V, (a * b) • v = a • b • v
mul_ident : ∀ v : V, (1 : F) • v = v
left_distrib : ∀ a : F, ∀ u v : V, a • (u + v) = a • u + a • v
right_distrib : ∀ a b : F, ∀ v : V, (a + b) • v = a • v + b • v
variable {F : Type _} [field_f: Field F]
namespace VectorSpace
variable {V : Type _} [AddCommGroup V] [VectorSpace F V]
theorem neg_one_smul_is_neg {v : V} : (-1 : F) • v = -v := sorry
end VectorSpace
structure AddCommSubgroup (V : Type _) [AddCommGroup V] where
carrier : Set V
add_mem' : ∀ {u v : V}, u ∈ carrier → v ∈ carrier → u + v ∈ carrier
zero_mem' : (0 : V) ∈ carrier
namespace AddCommSubgroup
variable {V : Type _} [AddCommGroup V] {v : V}
instance : SetLike (AddCommSubgroup V) V :=
⟨AddCommSubgroup.carrier, fun p q h => by cases p ; cases q ; congr⟩
@[simp]
theorem mem_carrier {p : AddCommSubgroup V} : v ∈ p.carrier ↔ v ∈ (p : Set V) :=
Iff.rfl
@[ext]
theorem ext {p q : AddCommSubgroup V} (h : ∀ v, v ∈ p ↔ v ∈ q) : p = q :=
SetLike.ext h
end AddCommSubgroup
-- Because this is a structure rather than a class, it's ok to extend add_comm_subgroup
structure Subspace (F : Type _) (V : Type _) [Field F] [AddCommGroup V] [VectorSpace F V] extends
AddCommSubgroup V where
smul_mem' : ∀ (c : F) {v : V}, v ∈ carrier → c • v ∈ carrier
namespace Subspace
variable {F : Type _} {V : Type _} [Field F] [AddCommGroup V] [VectorSpace F V]
variable {v : V}
instance : SetLike (Subspace F V) V where
coe s := s.carrier
coe_injective' p q h := by cases p; cases q; congr; exact SetLike.coe_injective' h
@[simp]
theorem mem_carrier {p : Subspace F V} : v ∈ p.carrier ↔ v ∈ (p : Set V) :=
Iff.rfl
@[ext]
theorem ext {p q : Subspace F V} (h : ∀ v, v ∈ p ↔ v ∈ q) : p = q :=
SetLike.ext h
variable (p : Subspace F V)
instance foo : AddCommGroup p
where
add u v := ⟨u.1 + v.1, by apply p.add_mem'; simp; simp⟩
zero := ⟨0, p.zero_mem'⟩
neg v := ⟨-v.1, by rw [← @VectorSpace.neg_one_smul_is_neg F _ V]; apply p.smul_mem'; simp⟩
add_comm := by intros; ext; apply AddCommGroup.add_comm
add_assoc := by intros; ext; apply AddCommGroup.add_assoc
add_zero := by intro v; ext; rw [AddCommGroup.add_zero] -- <-- This fails.
add_right_inv := by intros; ext; rw [AddCommGroup.add_right_inv] -- <-- This also fails.
end Subspace
end LADR
```

#### Eric Wieser (Nov 06 2023 at 18:51):

(note that Lean comments are `--`

not `#`

)

#### Jireh Loreaux (Nov 06 2023 at 18:52):

Note:

```
add_zero := by intro v; ext; exact AddCommGroup.add_zero _ -- This works.
```

#### Jireh Loreaux (Nov 06 2023 at 18:53):

The issue is that you are defining addition on the subspace at the same time as you are proving properties about it. If you define the addition first, then you can have a `coe_add`

lemma (proved by `rfl`

) which you can then rewrite with when you create the `AddCommGroup`

instance for subspaces.

#### Eric Wieser (Nov 06 2023 at 18:55):

Which would look like:

```
instance : Add p where
add u v := ⟨u.1 + v.1, by apply p.add_mem'; simp; simp⟩
@[simp] theorem val_add (a b : p) : (a + b).val = a.val + b.val := rfl
instance foo : AddCommGroup p where
add_zero := by intro v; ext; rw [val_add] -- this makes more progress
-- other fields,except `add`, as before
```

#### Martin C. Martin (Nov 06 2023 at 19:35):

Thanks to both of you! It's odd that `exact`

works but `apply`

and `rw`

did not. Is this related to using an underscore with `exact`

, but not with `apply`

or `rw`

?

#### Eric Wieser (Nov 06 2023 at 19:39):

I'm surprised it didn't work with `apply`

, but it wouldn't work with `rw`

because `rw`

refuses to unfold definitions

#### Martin C. Martin (Nov 06 2023 at 19:40):

In general, I do struggle to understand when to use `simp`

vs `dsimp`

vs `rw`

vs `apply`

vs `exact`

. I always thought anything that works with `exact`

would also work with `apply`

, that `apply`

is a kind of recursive `exact`

, but I guess that's not right.

#### Martin C. Martin (Nov 06 2023 at 19:42):

Actually, it does work with `apply`

. I swore I tried that a few weeks ago and it didn't work. You can see I used it on the earlier ones. Maybe I still had the `simp`

in there? Definitely doesn't work if you use `simp`

before the `apply`

.

#### Martin C. Martin (Nov 06 2023 at 19:43):

It seems odd that `simp`

is undoing `ext`

, but there's certainly a sense in which that's simpler. Still, I expect `simp`

to unfold definitions, rather than the opposite.

#### Jireh Loreaux (Nov 06 2023 at 21:27):

I would *not* expect `simp`

to unfold definitions in general (unless you pass them explicitly to the `simp`

call). Often that would defeat the purpose of having the definition, which is to hide some object behind the default semireducible transparency.

Last updated: Dec 20 2023 at 11:08 UTC