# Zulip Chat Archive

## Stream: general

### Topic: question

#### sedev627 (Nov 27 2022 at 11:27):

#### sedev627 (Nov 27 2022 at 11:28):

Can I get some advice....?

#### sedev627 (Nov 27 2022 at 11:29):

I posted the above question, but not answered yet...

#### Sebastien Gouezel (Nov 27 2022 at 11:30):

Can you post a #mwe, with #backticks?

#### sedev627 (Nov 27 2022 at 11:32):

```
import tactic
import init.default
import init.data.nat
def arith_sum : ℕ → ℕ
| 0 := 0
| (nat.succ n) := nat.succ n + arith_sum n
def arith_formula (n : ℕ) : ℕ := n * (n + 1) / 2
open nat
theorem arith_eq (n : ℕ) : arith_formula n = arith_sum n :=
begin
rw arith_formula,
induction n,
{
ring,
},
{
rw arith_sum,
rw ← n_ih,
rw ← add_one,
sorry,
},
end
```

#### sedev627 (Nov 27 2022 at 11:32):

Is it working...?

#### Patrick Johnson (Nov 27 2022 at 11:33):

That is not a #mwe.

#### sedev627 (Nov 27 2022 at 11:33):

Oh sorry... I'll fix it

#### sedev627 (Nov 27 2022 at 11:34):

Is it okay....?

#### sedev627 (Nov 27 2022 at 11:35):

(deleted)

#### sedev627 (Nov 27 2022 at 11:39):

Precisely... I stuck at "How to erase common constant 1/2 in equation....?".

#### sedev627 (Nov 27 2022 at 11:51):

Did I have some mistakes in above question...?

#### Patrick Johnson (Nov 27 2022 at 12:02):

```
lemma arith_eq {n : ℕ} : arith_formula n = arith_sum n :=
begin
rw arith_formula, induction n with n ih, { ring },
{ rw [arith_sum, ←ih, ←nat.add_one, ←nat.mul_left_inj (by linarith : 0 < 2),
add_mul _ _ 2, nat.div_mul_cancel, nat.div_mul_cancel], ring,
repeat { rw ←even_iff_two_dvd, apply nat.even_mul_succ_self }},
end
```

#### sedev627 (Nov 27 2022 at 12:11):

Thank you....!

#### sedev627 (Nov 27 2022 at 12:37):

Patrick Johnson said:

`lemma arith_eq {n : ℕ} : arith_formula n = arith_sum n := begin rw arith_formula, induction n with n ih, { ring }, { rw [arith_sum, ←ih, ←nat.add_one, ←nat.mul_left_inj (by linarith : 0 < 2), add_mul _ _ 2, nat.div_mul_cancel, nat.div_mul_cancel], ring, repeat { rw ←even_iff_two_dvd, apply nat.even_mul_succ_self }}, end`

It has error "unknown identifier 'nat.mul_left_inj'"... where is nat.mul_left_inj?

#### Patrick Johnson (Nov 27 2022 at 12:47):

I forgot to update my mathlib. Here is the fixed proof:

```
lemma arith_eq {n : ℕ} : arith_formula n = arith_sum n :=
begin
rw arith_formula, induction n with n ih, { ring },
{ rw [arith_sum, ←ih, ←nat.add_one, ←mul_right_cancel_iff_of_pos (by linarith : 0 < 2),
add_mul _ _ 2, nat.div_mul_cancel, nat.div_mul_cancel], ring,
all_goals { rw ←even_iff_two_dvd, apply nat.even_mul_succ_self }},
end
```

You also have to import `data.nat.parity`

#### sedev627 (Nov 27 2022 at 12:49):

It is working....!!!! Thank you!

#### Kyle Miller (Nov 28 2022 at 09:45):

@sedev627 You can also use the tactic#qify tactic, where you can give it information about whether something evenly divides, which lets it convert everything to rational arithmetic. Then `ring`

works.

```
import tactic
import init.default
import init.data.nat
import data.nat.parity
import tactic.qify
def arith_sum : ℕ → ℕ
| 0 := 0
| (nat.succ n) := nat.succ n + arith_sum n
def arith_formula (n : ℕ) : ℕ := n * (n + 1) / 2
open nat
lemma two_dvd_mul_succ_self (n : ℕ) : 2 ∣ n * (n + 1) :=
by { rw [← even_iff_two_dvd], exact nat.even_mul_succ_self n }
theorem arith_eq (n : ℕ) : arith_formula n = arith_sum n :=
begin
rw arith_formula,
induction n,
{
ring,
},
{
rw arith_sum,
rw ← n_ih,
rw ← add_one,
qify [two_dvd_mul_succ_self],
ring,
},
end
```

#### sedev627 (Nov 30 2022 at 02:21):

Can Type casting be do in lean prover?

#### sedev627 (Nov 30 2022 at 02:23):

Kyle Miller said:

sedev627 You can also use the tactic#qify tactic, where you can give it information about whether something evenly divides, which lets it convert everything to rational arithmetic. Then

`ring`

works.`import tactic import init.default import init.data.nat import data.nat.parity import tactic.qify def arith_sum : ℕ → ℕ | 0 := 0 | (nat.succ n) := nat.succ n + arith_sum n def arith_formula (n : ℕ) : ℕ := n * (n + 1) / 2 open nat lemma two_dvd_mul_succ_self (n : ℕ) : 2 ∣ n * (n + 1) := by { rw [← even_iff_two_dvd], exact nat.even_mul_succ_self n } theorem arith_eq (n : ℕ) : arith_formula n = arith_sum n := begin rw arith_formula, induction n, { ring, }, { rw arith_sum, rw ← n_ih, rw ← add_one, qify [two_dvd_mul_succ_self], ring, }, end`

Oh... I saw it just now... This is what I want.. thank you :)

#### sedev627 (Dec 26 2022 at 05:30):

Is there any examples using is_compact?

#### Bulhwi Cha (Dec 26 2022 at 09:58):

@sedev627 See https://leanprover-community.github.io/mathematics_in_lean/07_Topology.html#compactness.

#### sedev627 (Dec 28 2022 at 18:39):

```
import tactic
def id_ {α : Type} (a : α) : α :=
a
class has_mul_ (α : Type*) :=
(mul : α → α → α)
class semigroup_ (α : Type*) extends has_mul_ α :=
(mul_assoc : ∀ a b c : α, mul (mul a b) c = mul a (mul b c))
class has_one_ (α : Type*) :=
(one : α)
class monoid_ (α : Type*) extends semigroup_ α, has_one α :=
(one_mul : ∀ a : α , mul one a = a)
(mul_one : ∀ a : α , mul a one = a)
class has_inv_ (α : Type*) :=
(inv : α → α)
class group_ (α : Type*) extends monoid_ α, has_inv_ α :=
(mul_left_inv : ∀ a : α , mul (inv a) a = one)
class subgroup_ (α : Type*) [group_ α] (S : set α) : Prop :=
(mul_inv : ∀ {a b}, a ∈ S → b ∈ S → mul a (inv b) ∈ S)
```

I struggled to define subgroup. What's wrong?

#### Martin Dvořák (Dec 28 2022 at 18:44):

Seems you allow `S`

to be empty.

#### sedev627 (Dec 28 2022 at 18:47):

Martin Dvořák said:

Seems you allow

`S`

to be empty.

What should I do? I'm a beginner...

#### Martin Dvořák (Dec 28 2022 at 18:49):

What doesn't work that you want to do?

#### sedev627 (Dec 28 2022 at 18:51):

I want subgroup_ to be well defined. However, the code now has an error.

#### Martin Dvořák (Dec 28 2022 at 18:51):

Show us.

#### sedev627 (Dec 28 2022 at 18:52):

#### sedev627 (Dec 28 2022 at 18:53):

Can you see it...?

#### Mario Carneiro (Dec 28 2022 at 18:55):

`mul`

and `inv`

are functions in their respective namespaces `has_mul_`

and `has_inv_`

#### Mario Carneiro (Dec 28 2022 at 18:55):

so you should either `open`

them or write `has_mul_.mul`

(or make a notation for it)

#### sedev627 (Dec 28 2022 at 18:56):

Thank you!!!

#### Mario Carneiro (Dec 28 2022 at 18:56):

the reason you don't need to do that when you use `extends`

is because they are actually local variables in that case (you can see them in the context in the goal view)

#### Martin Dvořák (Dec 28 2022 at 19:17):

Now when your code is syntactically correct, let's turn to the semantics. Do you want the empty set to be a subgroup?

#### Riccardo Brasca (Dec 28 2022 at 19:20):

Unless you want to really change the mathematical definition, the empty set is not a subgroup...

Last updated: Dec 20 2023 at 11:08 UTC