case mp
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℤ
⊢ IsCoprime m n → gcd m n = 1

case mpr
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℤ
⊢ gcd m n = 1 → IsCoprime m n
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℤ
⊢ IsCoprime m n ↔ gcd m n = 1
constructor
case mp.intro.intro
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n a b : ℤ
h : a * m + b * n = 1
⊢ gcd m n = 1
case mp
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℤ
⊢ IsCoprime m n → gcd m n = 1
rintro ⟨a, b, h⟩
case mp.intro.intro
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n a b : ℤ
h : a * m + b * n = 1
this : 1 = m * a + n * b
⊢ gcd m n = 1
case mp.intro.intro
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n a b : ℤ
h : a * m + b * n = 1
⊢ gcd m n = 1
have : 1 = m * a + n * b := by rwa [mul_comm m, mul_comm n, eq_comm]
no goals
case mp.intro.intro
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n a b : ℤ
h : a * m + b * n = 1
this : 1 = m * a + n * b
⊢ gcd m n = 1
exact Nat.dvd_one.mp (Int.gcd_dvd_iff.mpr ⟨a, b, this⟩)
no goals
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n a b : ℤ
h : a * m + b * n = 1
⊢ 1 = m * a + n * b
rwa [mul_comm m, mul_comm n, eq_comm]
case mpr
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℤ
⊢ gcdA m n * m + gcdB m n * n = 1 → ∃ a b, a * m + b * n = 1
case mpr
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℤ
⊢ gcd m n = 1 → IsCoprime m n
rw [← Int.ofNat_inj, IsCoprime, Int.gcd_eq_gcd_ab, mul_comm m, mul_comm n, Nat.cast_one]
case mpr
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℤ
h : gcdA m n * m + gcdB m n * n = 1
⊢ ∃ a b, a * m + b * n = 1
case mpr
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℤ
⊢ gcdA m n * m + gcdB m n * n = 1 → ∃ a b, a * m + b * n = 1
intro h
no goals
case mpr
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℤ
h : gcdA m n * m + gcdB m n * n = 1
⊢ ∃ a b, a * m + b * n = 1
exact ⟨_, _, h⟩