# Zulip Chat Archive

## Stream: new members

### Topic: Simple arithmetic statements: 1...4 divide 12

#### Laurent Bartholdi (Jun 23 2023 at 08:28):

Could some kind soul explain to me how to optimize the following:

```
example : ∀i ∈ ({1,2,3,4} : finset ℕ), ∃j : ℕ, i*j=12 := begin
intros i ih,
use 12/i,
finish,
end
```

? It takes for ages, and I'd like a 1-liner avoiding heavy-hitters like `finish`

. I tried `ring`

and its variants, without success, and case-by-case also seems not to work smoothly

#### Damiano Testa (Jun 23 2023 at 08:52):

First of all, `rcases ih with rfl | rfl | rfl | rfl | ⟨⟨⟩⟩,`

helps! You can find out about it by using `rcases? ih`

.

#### Damiano Testa (Jun 23 2023 at 08:54):

After that, `norm_num`

works:

```
example : ∀i ∈ ({1,2,3,4} : finset ℕ), ∃j : ℕ, i*j=12 := begin
rintros i ih,
use 12/i,
rcases ih with rfl | rfl | rfl | rfl | ⟨⟨⟩⟩;
norm_num,
end
```

This is almost instant. Also the original version was not so bad, though...

#### Damiano Testa (Jun 23 2023 at 08:57):

Do you really need the ∃?

#### Damiano Testa (Jun 23 2023 at 08:57):

```
example : ∀i ∈ ({1,2,3,4} : finset ℕ), i*(12/i)=12 := by
rintros i (rfl | rfl | rfl | rfl | ⟨⟨⟩⟩); norm_num
```

#### Damiano Testa (Jun 23 2023 at 09:09):

Actually, with the last formulation, you can also prove it as: `example : ∀i ∈ ({1,2,3,4} : finset ℕ), i*(12/i)=12 := by norm_num`

.

#### Laurent Bartholdi (Jun 23 2023 at 09:09):

Thanks a lot! Yes, I wrote a M(N)WE, but I need to get hold of the `j`

. If you have improvement suggestions, here is where the code comes from:

```
variables {G : Type} [group G] (g : G) (foobar : G → set ℕ)
lemma l1 (j : ℕ) : foobar g ⊆ foobar (g^j) := sorry
lemma l2 : ∀i ∈ ({1,2,3,4} : finset ℕ), foobar (g^i) ⊆ foobar (g^12) := begin
intros i ih,
let j : ℕ := 12/i,
have div_12 : i*j = 12 := begin rcases ih with rfl | rfl | rfl | rfl | ⟨⟨⟩⟩; tauto end,
exact div_12 ▸ (pow_mul g i j).symm ▸ l1 (g^i) foobar j,
end
```

#### Anand Rao Tadipatri (Jun 23 2023 at 09:14):

Here is a (partial) solution using `decide`

(this code snippet is in Lean4):

```
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Nat.Basic
class DecideForAllMemMem (F : Type _ → Type _) [∀ α, Membership α (F α)] where
decideForAllMem {P : α → Prop} [DecidablePred P] (l : F α) : Decidable (∀ a : α, a ∈ l → P a)
instance : DecideForAllMemMem List where
decideForAllMem := sorry
instance : DecideForAllMemMem Multiset where
decideForAllMem := sorry
instance : DecideForAllMemMem Finset where
decideForAllMem := sorry
attribute [instance] DecideForAllMemMem.decideForAllMem
example : ∀ i ∈ ({1,2,3,4} : Finset ℕ), i ∣ 12 := by
sorry -- decide
```

Lean already knows that `a ∣ b`

is a decidable problem when `a b : ℕ`

, and consequently for any `l : Finset ℕ`

, the proposition `∀ i : ℕ, i ∈ l → i ∣ x`

should be decidable by enumeration. The code above is an (incomplete) attempt at getting Lean to perform decision by enumeration on `Finset`

s. When all the `sorry`

s are filled in, the proof should ideally just be `by decide`

.

#### Damiano Testa (Jun 23 2023 at 09:43):

I do not know if this is any better for your application, but I find that the `convert`

line let's me, as a human, know what is happening: we are applying `l1`

; after that, it is just a case-check.

```
lemma l2 : ∀i ∈ ({1,2,3,4} : finset ℕ), foobar (g^i) ⊆ foobar (g^12) := begin
intros i ih,
convert l1 (g ^ i) foobar (12 / i) using 2,
rw ← pow_mul,
fin_cases ih;
norm_num,
end
```

Maybe this is more show-casing some of the automation that can be used, though...

The more I use Lean, the more I prefer writing proofs for humans, over highly-compressed machine-parseable code.

#### Laurent Bartholdi (Jun 25 2023 at 22:45):

If I dare, a followup question: how do I convert inequalities to a finset, as in

```
example (a : ℕ) (h : 1 ≤ a) (k : a ≤ 4) : a ∈ ({1,2,3,4} : finset ℕ) := sorry
```

?

#### Heather Macbeth (Jun 25 2023 at 22:50):

`interval_cases a; tauto`

? (Untested)

#### Damiano Testa (Jun 25 2023 at 22:53):

```
example (a : ℕ) (h : 1 ≤ a) (k : a ≤ 4) : a ∈ ({1,2,3,4} : finset ℕ) :=
begin
rcases a with _ | _ | _ | _ | _ | a;
try {linarith <|> simp, done},
change a + 5 ≤ 4 at k,
linarith,
end
```

#### Damiano Testa (Jun 25 2023 at 22:56):

Heather's suggestion is better though, but using `simp`

instead of `tauto`

.

#### Yakov Pechersky (Jun 26 2023 at 10:32):

If you're converting inequalities to a finset, then you should use a construction like Finset.range instead of a manual construction as you have now that is via Finset.insert

Last updated: Dec 20 2023 at 11:08 UTC