How to substitute a number in a hypothesis?

Stream: new members

[Arshak Parsa]

Hi, I want to substitute 2 for m :

example {n m : ℕ} : n+m = n*m → n+2 = n*2 := by
  intro h1
  let m := 2
  sorry -- doesn't work :/

any idea?
By the way I'm trying to proof this lemma :

lemma sum_eq_mul_imp_exp_real {f : ℝ → ℝ} {x y z : ℝ} (fcont : Continuous f) :
   (f (x+y)) = (f x) * (f y) → (f z) = (f 1)^z := by
  intro h1
  have h2 : (f 2) = (f 1)*(f 1) := by sorry
  sorry

Has anyone seen a similar lemma in mathlib ? I didn't find anything

[Yaël Dillies]

Use set instead of let

[Yaël Dillies]

@Mantas Baksys and I have a proof of the Cauchy functional equation, but it's not yet in mathlib

[Arshak Parsa]

@Yaël Dillies
So add it to mathlib as soon as you can :)

[Yaël Dillies]

I'm currently sailing, but if you're willing to wait two weeks then I'm yours!

[Arshak Parsa]

I can't figure out how to use set.
I did it in a weird way but I'm not sure if it's the right way to do this :

def prop1 (n : ℕ) (m : ℕ) := n+m = n*m

lemma lem1 (h : ∀ n m, prop1 n m) : n+2 = n*2 := by
  rw [← prop1]
  simp [h]
  done

#print axioms lem1

#check propext

I wish there was an easier way to do this.
And I found out that simp used an axiom called propext.

[Damiano Testa]

apply h works. And you can also remove by and use simply h ...

[Dan Velleman]

@Arshak Parsa , I think you may be confused about how free variables work in theorems. They are implicitly universally quantified. Your first example was:

example {n m : ℕ} : n+m = n*m → n+2 = n*2

This means ∀ {n m : ℕ}, n + m = n * m → n + 2 = n * 2. This statement is false. For example, if n = m = 0 then n + m = n * m is true but n + 2 = n * 2 is false. Similarly, you say that the lemma you want to prove is:

lemma sum_eq_mul_imp_exp_real {f : ℝ → ℝ} {x y z : ℝ} (fcont : Continuous f) :
   (f (x+y)) = (f x) * (f y) → (f z) = (f 1)^z

This is also false. Suppose f is the function x => x + 1, x = 0, y = 1, and z = 2. Then f (x+y) = 2 = 1 * 2 = (f x) * (f y), but f z = 3 and (f 1)^z = 2 ^ 2 = 4. Perhaps the lemma you meant to state is:

lemma sum_eq_mul_imp_exp_real {f : ℝ → ℝ} (fcont : Continuous f) :
   (∀ (x y : ℝ), f (x+y) = (f x) * (f y)) → ∀ (z : ℝ), (f z) = (f 1)^z

[Kevin Buzzard]

Note that this lemma is false because 0^0=1:

import Mathlib

-- assume the lemma
lemma sum_eq_mul_imp_exp_real {f : ℝ → ℝ} (fcont : Continuous f) :
   (∀ (x y : ℝ), f (x+y) = (f x) * (f y)) → ∀ (z : ℝ), (f z) = (f 1)^z := sorry

-- get a contradiction
example : False := by
  have foo := sum_eq_mul_imp_exp_real (f := fun x ↦ 0) (by continuity)
    (by simp (config := {contextual := true})) 0
  norm_num at foo

[Dan Velleman]

Thanks @Kevin Buzzard . I think if you add the assumption that f 1 ≠ 0 then it's true.

[Kevin Buzzard]

Yes I should think so

[Arshak Parsa]

I finally figured out that it matters where you put the ∀. I added parenthesis and now everything is working.
I didn't know that it makes such a big difference! :sweat_smile: By the way I proved a weaker version of this lemma :

lemma sum_eq_mul_imp_exp_nat {f : ℕ → ℕ} (hf_one : f 1 ≠ 0):
   (∀ x y : ℕ , (f (x+y)) = (f x) * (f y)) → (∀ z, (f z) = (f 1)^z ) := by
  intro h1
  have h2 : f 1 = (f 1) * (f 0) := by
    exact h1 1 0
  have h3 {m : ℕ} : f (m+1) = (f m) * (f 1) := by
    exact h1 m 1
  intro z
  induction z with
    | zero =>
      simp
      exact (Nat.mul_eq_left hf_one).mp (id (Eq.symm h2))
      done
    | succ n ih =>
      rw [h3]
      exact congrFun (congrArg HMul.hMul ih) (f 1)
  done

Thank you :heart: @Kevin Buzzard @Dan Velleman