Multiply by a constant

Stream: new members

[Steven Herbert]

As a new lean user, I came across this: https://leanprover-community.github.io/archive/stream/113489-new-members/topic/Multiplying.20both.20sides.20of.20an.20expression.20by.20a.20constant.html

Which almost exactly answers what I am looking for except:

1. I believe its for an earlier version of Lean

2. I want to multiply through by a general constant, c.
   ```(h : a + c = 1) : a * b + c * b = b

I think this should be straightforward, but I'm finding it a bit tricky. Any ideas?

[Ruben Van de Velde]

What code have you written so far?

[Steven Herbert]

I've basically derived a hypothesis h : a + c = 1, and a * b + c * b = b is the final goal

[Ruben Van de Velde]

Sorry I was unclear

[Ruben Van de Velde]

Please show the code you've written so far

[Steven Herbert]

example {p a : ℤ }(h1: ∃ r t : ℤ , p * r + a * t = 1):
    ∀ b : ℤ , ∃ x y : ℤ, p * x * b + a * y * b = b := by
    intro b
    cases' h1 with r hr
    cases' hr with t ht
    use r
    use t

[Steven Herbert]

So what I'm left with is equivalent to what I asked above

[Aaron Liu]

Try apply_fun (· * b) at ht

[Riccardo Brasca]

You are almost there. You can work in the goal to make it (p * r + a * t) * b = b and the use your ht.

[Riccardo Brasca]

Or work on ht, but this is indeed slightly trickier (we have a tactic for that, apply_fun).

[Riccardo Brasca]

Anyway at some point you need distributivity.

[Steven Herbert]

Thanks everybody! With much trial and error I've now picked my way through it

[Steven Herbert]

example {p a : ℤ }(h1: ∃ r t : ℤ , p * r + a * t = 1):
    ∀ b : ℤ , ∃ x y : ℤ, p * x * b + a * y * b = b := by
    intro b
    cases' h1 with r hr
    cases' hr with t ht
    use r
    use t
    apply_fun (· * b) at ht
    rw [mul_comm] at ht
    rw [Distrib.left_distrib] at ht
    rw [mul_comm] at ht
    rw [mul_comm b (a*t)] at ht
    rw [one_mul] at ht
    exact ht

[Steven Herbert]

(Not necessarily the most efficient way, but a way that does work!

[Riccardo Brasca]

Wow, that really looks over complicated, why not

import Mathlib

example {p a : ℤ }(h1: ∃ r t : ℤ , p * r + a * t = 1):
    ∀ b : ℤ , ∃ x y : ℤ, p * x * b + a * y * b = b := by
    intro b
    cases' h1 with r hr
    cases' hr with t ht
    use r
    use t
    apply_fun (· * b) at ht
    rw [add_mul, one_mul] at ht
    exact ht

[Steven Herbert]

The clue is in the 'new user'. Once I get a bit better I'm sure I'll do something like that. (But thanks for posting a better solution -- for those who stumble on this in future I'm sure they'll prefer yours to mine!)

[Riccardo Brasca]

Sorry, I didn't want to criticize, just noting that the order of the factors in the multiplications is the good one, so no need to change it.

[Steven Herbert]

Not taken as criticism! Thanks for pointing out a better way

[Riccardo Brasca]

ah, because you used left distributivity! We also have right distributivity :)