# Zulip Chat Archive

## Stream: new members

### Topic: gyro_mul_left_inj

#### James Arthur (Aug 13 2020 at 09:45):

I'm trying to create a `mul_left_inj`

for a new group that I'm formalising and developing. Heres basically as far as I have got:

```
import tactic
noncomputable theory
open_locale classical
universe u
class has_gyrop (α : Type u) := (gyrop : α → α → α)
class has_subgyrop (α : Type u) := (subgyrop : α → α → α)
class has_neggyrop (α : Type u) := (neggyrop : α → α)
class has_cogyrop (α : Type u) := (cogyrop : α → α → α)
class has_subcogyrop (α : Type u) := (subcogyrop : α → α → α)
class has_negcogyrop (α : Type u) := (negcogyrop : α → α)
infix `⊙`:75 := has_gyrop.gyrop
infix `⊝`:75 := has_subgyrop.subgyrop
prefix `⊝`:65 := has_neggyrop.neggyrop
infix `⊞`:80 := has_cogyrop.cogyrop
infix `⊟`:80 := has_subcogyrop.subcogyrop -- what a long name
infix `⊟`:85 := has_negcogyrop.negcogyrop
/-?
A gyrogroup (G, ⊕) is gyrocommutative if its binary operation obeys the gyrocommutative law
(G6) a ⊕ b = gyr[a, b](b ⊕ a) for all a, b ∈ G.
-/
class gyrocomm_gyrogroup (C : Type) extends has_gyrop C, has_subgyrop C, has_neggyrop C, has_zero C :=
-- axiom 1: 0 ⊕ a = a
(zero_gyro : ∀ (a : C), 0 ⊙ a = a)
-- axiom 2: ⊖a⊕a = 0
(gyr_add_left_neg : ∀ (a : C), ⊝a ⊙ a = 0)
(gyr : C → C → C → C) -- gyr a b c is gyr[a, b]c in the notation from the Wiki
-- axiom 3: ∀ a b c ∈ G, a + (b + c) = (a + b) + gyr a b c
(add_gyr_assoc : ∀ a b c, a ⊙ (b ⊙ c) = (a ⊙ b) ⊙ gyr a b c)
(add_gyr_assoc' : ∀ a b c d, a ⊙ (b ⊙ c) = (a ⊙ b) ⊙ d → d = gyr a b c) -- uniqueness
-- axiom 5: gyr a b = gyr (a + b) b
(gyr_loop : ∀ a b, gyr a b = gyr (a ⊙ b) b)
--axiom 6: a ⊕ b = gyr[a, b](b ⊕ a) for all a, b ∈ G
(gyro_comm: ∀ (a b : C), a ⊙ b = gyr a b (b ⊙ a))
variables (C : Type) [gyrocomm_gyrogroup C]
variables (a b c d : C)
namespace gyrocomm_gyrogroup
axiom gyr_a_b_zero : gyr a b 0 = 0
axiom gyr_distrib : gyr a b (c ⊙ d) = gyr a b c ⊙ gyr a b d
end gyrocomm_gyrogroup
lemma gyrocomm_equal : a ⊙ b = a ⊙ c ↔ b = c :=
begin
split,
{intros fabc,
sorry},
{ intros fbc,
rw fbc,}
end
```

(I think thats all is needed to get it to work. I have too many files. The full code can be found here)

Basically, my goal is at

```
C : Type,
_inst_1 : gyrocomm_gyrogroup C,
a b c : C,
fabc : a⊙b = a⊙c
⊢ b = c
```

and I want to do ` refine congr rfl _ at fabc`

, but lean disagrees with me throwing many errors all saying that I have given it a wrong command. So how to I apply something like this command to `fabc`

?

#### Scott Morrison (Aug 13 2020 at 09:52):

It seems you're asking for magic. Why couldn't there be some other reason that they are equal? What is the maths proof here?

#### Mario Carneiro (Aug 13 2020 at 12:56):

At first I thought those axioms were for the sake of the #mwe but they are also in your actual project. That's a really weird thing to do; you almost certainly either want them to be `theorem ... := sorry`

if they should be provable, or fields of the structure if they are not

Last updated: May 13 2021 at 18:26 UTC