K : Type u
inst✝ : Field K
x y : RatFunc K
hxy : x + y ≠ 0
h_zero : num x * denom y + denom x * num y = 0
⊢ False
K : Type u
inst✝ : Field K
x y : RatFunc K
hxy : x + y ≠ 0
⊢ num x * denom y + denom x * num y ≠ 0
intro h_zero
K : Type u
inst✝ : Field K
x y : RatFunc K
hxy : x + y ≠ 0
h_zero : num x * denom y + denom x * num y = 0
h : num (x + y) * (denom x * denom y) = (num x * denom y + denom x * num y) * denom (x + y)
⊢ False
K : Type u
inst✝ : Field K
x y : RatFunc K
hxy : x + y ≠ 0
h_zero : num x * denom y + denom x * num y = 0
⊢ False
have h := num_denom_add x y
K : Type u
inst✝ : Field K
x y : RatFunc K
hxy : x + y ≠ 0
h_zero : num x * denom y + denom x * num y = 0
h : num (x + y) * (denom x * denom y) = 0
⊢ False
K : Type u
inst✝ : Field K
x y : RatFunc K
hxy : x + y ≠ 0
h_zero : num x * denom y + denom x * num y = 0
h : num (x + y) * (denom x * denom y) = (num x * denom y + denom x * num y) * denom (x + y)
⊢ False
rw [h_zero, MulZeroClass.zero_mul] at h
no goals
K : Type u
inst✝ : Field K
x y : RatFunc K
hxy : x + y ≠ 0
h_zero : num x * denom y + denom x * num y = 0
h : num (x + y) * (denom x * denom y) = 0
⊢ False
exact (mul_ne_zero (num_ne_zero hxy) (mul_ne_zero x.denom_ne_zero y.denom_ne_zero)) h