a b : ℤ
ha : a ≠ 0
⊢ IsLeast {n | 0 < n ∧ gcd a b ∣ n} (gcd a b)
a b : ℤ
ha : a ≠ 0
⊢ IsLeast {n | 0 < n ∧ ∃ x y, ↑n = a * x + b * y} (gcd a b)
simp_rw [← gcd_dvd_iff]
case left
a b : ℤ
ha : a ≠ 0
⊢ gcd a b ∈ {n | 0 < n ∧ gcd a b ∣ n}

case right
a b : ℤ
ha : a ≠ 0
⊢ gcd a b ∈ lowerBounds {n | 0 < n ∧ gcd a b ∣ n}
a b : ℤ
ha : a ≠ 0
⊢ IsLeast {n | 0 < n ∧ gcd a b ∣ n} (gcd a b)
constructor
no goals
case left
a b : ℤ
ha : a ≠ 0
⊢ gcd a b ∈ {n | 0 < n ∧ gcd a b ∣ n}
simpa [and_true_iff, dvd_refl, Set.mem_setOf_eq] using gcd_pos_of_ne_zero_left b ha
case right
a b : ℤ
ha : a ≠ 0
⊢ ∀ ⦃a_1 : ℕ⦄, 0 < a_1 → gcd a b ∣ a_1 → gcd a b ≤ a_1
case right
a b : ℤ
ha : a ≠ 0
⊢ gcd a b ∈ lowerBounds {n | 0 < n ∧ gcd a b ∣ n}
simp only [lowerBounds, and_imp, Set.mem_setOf_eq]
no goals
case right
a b : ℤ
ha : a ≠ 0
⊢ ∀ ⦃a_1 : ℕ⦄, 0 < a_1 → gcd a b ∣ a_1 → gcd a b ≤ a_1
exact fun n hn_pos hn => Nat.le_of_dvd hn_pos hn