Coercions Disappear

Stream: new members

[Colin Jones ⚛️]

I have a problem trying to prove this statement:

import Mathlib.Data.Real.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real

variable {x y z : ℝ}
example (h : x ≠ 0) : x ^ ((x * y/x) + 1) = x*x^y := by
  have hxy : (x * y)/x  = (y * x)/x := by ring
  rw [hxy];
  rw [mul_div_cancel y h]; have hx : x * x^y = x^1 * x^y := by simp;
  have hx_C : x ≠ 0 → (x:ℂ) ≠ (0:ℂ) := by simp
  rw [hx, mul_comm]
  have h' := by apply Complex.cpow_add y 1 (hx_C h)
  by_contra hcontra
  push_neg at hcontra
  have conc : x ^ (y + 1) ≠ x ^ y * x ^ 1 → ↑x ^ (↑y + 1) ≠ ↑x ^ ↑y * ↑x ^ 1 := by simp
  have h'' : ↑x ^ (↑y + 1) ≠ ↑x ^ ↑y * ↑x ^ 1 := by apply (conc hcontra)
  contradiction

h'' should be the opposite of h' but the coercions disappear in the h'' statement. How do I force them to stay?

[Colin Jones ⚛️]

Also I would like to keep x y z as Real numbers. I recognize it would be easier to convert them at the start, but I would like to see where this path leads.

[Julian Berman]

I think what's happening has to do with your have conc line. Specifically, you have have conc : x ^ (y + 1) ≠ x ^ y * x ^ 1 → ↑x ^ (↑y + 1) ≠ ↑x ^ ↑y * ↑x ^ 1 := by simp -- the up arrow is telling Lean "coerce x to make this thing type check", but Lean doesn't know where you mean for x to live -- it is perfectly happy for x to stay in \R, because your equation then still type checks. So your conc ends up being some trivial statement.

[Alex J. Best]

If you want to manually insert coercions, you should use a type ascription (↑x : ℂ) as well as an arrow (actually you don't even need the arrow even most of the time when you do that).

[Julian Berman]

If you change to:

import Mathlib.Data.Real.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real

variable {x y z : ℝ}
example (h : x ≠ 0) : x ^ ((x * y/x) + 1) = x*x^y := by
  have hxy : (x * y)/x  = (y * x)/x := by ring
  rw [hxy];
  rw [mul_div_cancel y h]; have hx : x * x^y = x^1 * x^y := by simp;
  have hx_C : x ≠ 0 → (x:ℂ) ≠ (0:ℂ) := by simp
  rw [hx, mul_comm]
  have h' := by apply Complex.cpow_add y 1 (hx_C h)
  by_contra hcontra
  push_neg at hcontra
  have conc : x ^ (y + 1) ≠ x ^ y * x ^ 1 → (x : ℂ) ^ ((y : ℂ) + 1) ≠ x ^ y * x ^ 1 := sorry
  have h'' : (x : ℂ) ^ ((y : ℂ) + (1 : ℂ)) ≠ x ^ y * x ^ 1 := conc hcontra
  contradiction

now the contradiction will indeed close your goal -- and you're left indeed with trying to now prove conc really holds for lifting that from R to C

[Yongyi Chen]

If you use Real.rpow_add_one, you don't need to go into complex numbers at all:

example (h : x ≠ 0) : x ^ ((x * y / x) + 1) = x * x ^ y := by
  rw [mul_comm, mul_div_cancel _ h, Real.rpow_add_one h, mul_comm]