# Zulip Chat Archive

## Stream: new members

### Topic: using quotient.map2

#### Yakov Pechersky (Feb 10 2022 at 09:18):

In this example, why do I have to reprove the property of my function lifted into the quotient? I would have thought that `map2_mk`

is able to retrieve it from the function itself. The lemma docs#quotient.map₂_mk is tagged `@[simp]`

where it is defined.

```
import algebra.order.group
import algebra.order.with_zero
variables {S : Type*} [comm_semigroup S]
lemma cancel_left {a b c : S} (h : a * b = a * c) : b = c := sorry
variables (S)
-- we twist the multiplication to simplify refl and symm proofs
-- the definition is equivalent to `(a, a') ≈ (b, b') <-> a * b' = a' * b` due to the commutativity assumption
def mul_pair_setoid : setoid (S × S) :=
{ r := λ p q, p.1 * q.2 = q.1 * p.2,
iseqv := begin
refine ⟨λ _, rfl, λ _ _, eq.symm, _⟩,
intros p q r h h',
have := congr_arg ((*) p.snd) h',
rw [mul_left_comm, ←mul_assoc, ←h, mul_comm _ q.snd, mul_comm _ q.snd, ←mul_left_comm,
mul_assoc] at this,
rw [cancel_left this, mul_comm],
end }
variables {S}
local attribute [instance] mul_pair_setoid
@[simp] lemma mul_pair_equiv_iff (p q : S × S) : p ≈ q ↔ p.1 * q.2 = q.1 * p.2 := iff.rfl
lemma mul_pair_left_eq (p : S × S) (x : S) : ⟦(x * p.1, x * p.2)⟧ = ⟦p⟧ :=
by simp only [quotient.eq, mul_pair_equiv_iff, mul_assoc, mul_comm, mul_left_comm]
namespace mul_pair_quotient
local notation `G` := quotient (mul_pair_setoid S)
def mul : G → G → G :=
quotient.map₂ (λ (p q : S × S), (p.1 * q.1, p.2 * q.2)) begin
rintro ⟨a, a'⟩ ⟨c, c'⟩ hac ⟨b, b'⟩ ⟨d, d'⟩ hbd,
simp only [mul_pair_equiv_iff, quotient.eq] at hac hbd ⊢,
rw [mul_left_comm, ←mul_assoc, ←mul_assoc, mul_assoc, hbd, mul_comm c', hac],
simp [mul_left_comm, mul_assoc, mul_comm]
end
instance : has_mul G := ⟨mul⟩
-- why do I have to provide the proof again?
@[simp] lemma mk_mul : ∀ (p q : S × S), ⟦p⟧ * ⟦q⟧ = ⟦(p.1 * q.1, p.2 * q.2)⟧ :=
quotient.map₂_mk _ begin
rintro ⟨a, a'⟩ ⟨c, c'⟩ hac ⟨b, b'⟩ ⟨d, d'⟩ hbd,
simp only [mul_pair_equiv_iff, quotient.eq] at hac hbd ⊢,
rw [mul_left_comm, ←mul_assoc, ←mul_assoc, mul_assoc, hbd, mul_comm c', hac],
simp [mul_left_comm, mul_assoc, mul_comm]
end
end mul_pair_quotient
```

#### Eric Wieser (Feb 10 2022 at 09:34):

This works:

```
@[simp] lemma mk_mul : ∀ (p q : S × S), ⟦p⟧ * ⟦q⟧ = ⟦(p.1 * q.1, p.2 * q.2)⟧ :=
begin
change (∀ p q, mul ⟦p⟧ ⟦q⟧ = _),
refine quotient.map₂_mk _ _,
end
```

#### Yakov Pechersky (Feb 10 2022 at 09:35):

All of those are "term-like" tactics, so why doesn't just the `refine`

step work?

#### Eric Wieser (Feb 10 2022 at 09:37):

This also works:

```
@[simp] lemma mk_mul : ∀ (p q : S × S), ⟦p⟧ * ⟦q⟧ = ⟦(p.1 * q.1, p.2 * q.2)⟧ :=
begin
dunfold has_mul.mul,
refine quotient.map₂_mk _ _,
end
```

#### Eric Wieser (Feb 10 2022 at 09:37):

The elaborator can't infer the implicit arguments correctly for you unless you unfold things in the right order for it, it seems

#### Yakov Pechersky (Feb 10 2022 at 09:38):

Thanks. This is helpful for the API I am building, but I still don't grok what's "wrong"

#### Eric Wieser (Feb 10 2022 at 09:38):

(as an aside, note that `(λ (p q : S × S), (p.1 * q.1, p.2 * q.2))`

is just `(*)`

)

#### Alex J. Best (Feb 10 2022 at 09:39):

And if you really want term mode:

```
@[simp] lemma mk_mul' : ∀ (p q : S × S), ⟦p⟧ * ⟦q⟧ = ⟦(p.1 * q.1, p.2 * q.2)⟧ :=
assume p q,
show mul ⟦p⟧ ⟦q⟧ = _, from quotient.map₂_mk _ _ p q
```

#### Yakov Pechersky (Feb 10 2022 at 09:40):

Term mode or tactic mode, I don't understand why `show _, from _`

is necessary for the unification(?) to occur

#### Eric Wieser (Feb 10 2022 at 09:42):

My guess is that it unfolds things in the wrong order

#### Eric Wieser (Feb 10 2022 at 09:42):

Here's a version without `show`

:

```
@[simp] lemma mk_mul : ∀ (p q : S × S), ⟦p⟧ * ⟦q⟧ = ⟦(p.1 * q.1, p.2 * q.2)⟧ :=
(quotient.map₂_mk _ _ : ∀ p q : S × S, mul ⟦p⟧ ⟦q⟧ = _)
```

Last updated: Dec 20 2023 at 11:08 UTC