no goals
R : Type u_1
inst✝ : MonoidWithZero R
⊢ ↑1 1 = 1
simp
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : coprime m n
⊢ ↑1 (m * n) = ↑1 m * ↑1 n
R : Type u_1
inst✝ : MonoidWithZero R
⊢ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → coprime m n → ↑1 (m * n) = ↑1 m * ↑1 n
intro m n hm _hn hmn
case inl
R : Type u_1
inst✝ : MonoidWithZero R
n : ℕ
_hn : n ≠ 0
hm : 1 ≠ 0
hmn : coprime 1 n
⊢ ↑1 (1 * n) = ↑1 1 * ↑1 n

case inr
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : coprime m n
hm' : m ≠ 1
⊢ ↑1 (m * n) = ↑1 m * ↑1 n
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : coprime m n
⊢ ↑1 (m * n) = ↑1 m * ↑1 n
rcases eq_or_ne m 1 with (rfl | hm')
case inr
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : coprime m n
hm' : m ≠ 1
⊢ m * n ≠ 1
case inr
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : coprime m n
hm' : m ≠ 1
⊢ ↑1 (m * n) = ↑1 m * ↑1 n
rw [one_apply_ne, one_apply_ne hm', MulZeroClass.zero_mul]
case inr
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : coprime m n
hm' : m ≠ 1
⊢ ¬m = 1 ∨ ¬n = 1
case inr
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : coprime m n
hm' : m ≠ 1
⊢ m * n ≠ 1
rw [Ne.def, mul_eq_one, not_and_or]
no goals
case inr
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : coprime m n
hm' : m ≠ 1
⊢ ¬m = 1 ∨ ¬n = 1
exact Or.inl hm'
no goals
case inl
R : Type u_1
inst✝ : MonoidWithZero R
n : ℕ
_hn : n ≠ 0
hm : 1 ≠ 0
hmn : coprime 1 n
⊢ ↑1 (1 * n) = ↑1 1 * ↑1 n
simp