awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
⊢ map (Embedding.subtype fun (n : ℕ) ↦ 0 < n) (Ioc a b) = Ioc (↑a : ℕ) (↑b : ℕ)

Tactic:
Finset.map_subtype_embedding_Ioc _ _ _ fun _c _ _x hx _ hc _ => hc.trans_le hx

Premises used: PNat.val, Finset.map_subtype_embedding_Ioc, LT.lt.trans_le, PNat
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
⊢ map (Embedding.subtype fun (n : ℕ) ↦ 0 < n) (Ioo a b) = Ioo (↑a : ℕ) (↑b : ℕ)

Tactic:
Finset.map_subtype_embedding_Ioo _ _ _ fun _c _ _x hx _ hc _ => hc.trans_le hx

Premises used: PNat.val, LT.lt.trans_le, Finset.map_subtype_embedding_Ioo, PNat
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
⊢ map (Embedding.subtype fun (n : ℕ) ↦ 0 < n) (uIcc a b) = uIcc (↑a : ℕ) (↑b : ℕ)

Tactic:
map_subtype_embedding_Icc _ _

Premises used: PNat.val, PNat.map_subtype_embedding_Icc, Finset.uIcc
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
rw : #(Icc a b) = #(Icc (↑a : ℕ) (↑b : ℕ))
rw₁ : #(Icc a b) = #(map (Embedding.subtype fun (n : ℕ) ↦ 0 < n) (Icc a b))
rw₂ rw₃ : #(Icc a b) = #(Icc a b)
⊢ #(Icc a b) = (↑b : ℕ) + 1 - (↑a : ℕ)

Tactic:
rw [← Nat.card_Icc, ← map_subtype_embedding_Icc, card_map]

Premises used: Finset.card_map, PNat.map_subtype_embedding_Icc, Nat.card_Icc
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
rw : #(Ico a b) = #(Ico (↑a : ℕ) (↑b : ℕ))
rw₁ : #(Ico a b) = #(map (Embedding.subtype fun (n : ℕ) ↦ 0 < n) (Ico a b))
rw₂ rw₃ : #(Ico a b) = #(Ico a b)
⊢ #(Ico a b) = (↑b : ℕ) - (↑a : ℕ)

Tactic:
rw [← Nat.card_Ico, ← map_subtype_embedding_Ico, card_map]

Premises used: PNat.map_subtype_embedding_Ico, Finset.card_map, Nat.card_Ico
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
rw : #(Ioc a b) = #(Ioc (↑a : ℕ) (↑b : ℕ))
rw₁ : #(Ioc a b) = #(map (Embedding.subtype fun (n : ℕ) ↦ 0 < n) (Ioc a b))
rw₂ rw₃ : #(Ioc a b) = #(Ioc a b)
⊢ #(Ioc a b) = (↑b : ℕ) - (↑a : ℕ)

Tactic:
rw [← Nat.card_Ioc, ← map_subtype_embedding_Ioc, card_map]

Premises used: Finset.card_map, Nat.card_Ioc, PNat.map_subtype_embedding_Ioc
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
rw : #(uIcc a b) = #(uIcc (↑a : ℕ) (↑b : ℕ))
rw₁ : #(uIcc a b) = #(map (Embedding.subtype fun (n : ℕ) ↦ 0 < n) (uIcc a b))
rw₂ rw₃ : #(uIcc a b) = #(uIcc a b)
⊢ #(uIcc a b) = (HSub.hSub (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ)).natAbs + 1

Tactic:
rw [← Nat.card_uIcc, ← map_subtype_embedding_uIcc, card_map]

Premises used: Finset.card_map, PNat.map_subtype_embedding_uIcc, Nat.card_uIcc
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
rw : Fintype.card (↑(Set.Icc a b) : Type) = #(Icc a b)
rw₁ rw₂ : #(Icc a b) = #(Icc a b)
⊢ Fintype.card (↑(Set.Icc a b) : Type) = (↑b : ℕ) + 1 - (↑a : ℕ)

Tactic:
rw [← card_Icc, Fintype.card_ofFinset]

Premises used: Fintype.card_ofFinset, PNat.card_Icc
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
rw : Fintype.card (↑(Set.Ico a b) : Type) = #(Ico a b)
rw₁ rw₂ : #(Ico a b) = #(Ico a b)
⊢ Fintype.card (↑(Set.Ico a b) : Type) = (↑b : ℕ) - (↑a : ℕ)

Tactic:
rw [← card_Ico, Fintype.card_ofFinset]

Premises used: Fintype.card_ofFinset, PNat.card_Ico
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
rw : Fintype.card (↑(Set.Ioc a b) : Type) = #(Ioc a b)
rw₁ rw₂ : #(Ioc a b) = #(Ioc a b)
⊢ Fintype.card (↑(Set.Ioc a b) : Type) = (↑b : ℕ) - (↑a : ℕ)

Tactic:
rw [← card_Ioc, Fintype.card_ofFinset]

Premises used: Fintype.card_ofFinset, PNat.card_Ioc
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
rw : Fintype.card (↑(Set.Ioo a b) : Type) = #(Ioo a b)
rw₁ rw₂ : #(Ioo a b) = #(Ioo a b)
⊢ Fintype.card (↑(Set.Ioo a b) : Type) = (↑b : ℕ) - (↑a : ℕ) - 1

Tactic:
rw [← card_Ioo, Fintype.card_ofFinset]

Premises used: Fintype.card_ofFinset, PNat.card_Ioo
-- Module: Mathlib.Data.PNat.Interval
Goal:
a b : ℕ+
rw : Fintype.card (↑(Set.uIcc a b) : Type) = #(uIcc a b)
rw₁ rw₂ : #(uIcc a b) = #(uIcc a b)
⊢ Fintype.card (↑(Set.uIcc a b) : Type) = (HSub.hSub (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ)).natAbs + 1

Tactic:
rw [← card_uIcc, Fintype.card_ofFinset]

Premises used: Fintype.card_ofFinset, PNat.card_uIcc
-- Module: Mathlib.Data.PNat.Order
Goal:
n : ℕ+
⊢ Order.succ n = n + 1

Tactic:
rfl

Premises used: Order.succ, rfl
-- Module: Mathlib.Data.PNat.Prime
Goal:
p : Primes
⊢ (↑(↑p : ℕ+) : ℕ) = (↑p : ℕ)

Tactic:
rfl

Premises used: PNat.val, Nat.Prime, Nat.Primes, Nat.lt, rfl
-- Module: Mathlib.Data.PNat.Prime
Goal:
p q : Primes
h : (↑p : ℕ+) = (↑q : ℕ+)
⊢ (↑p : ℕ) = (↑q : ℕ)

Tactic:
injection h
-- Module: Mathlib.Data.PNat.Prime
Goal:
p q : Primes
⊢ (↑p : ℕ+) = (↑q : ℕ+) ↔ p = q

Tactic:
coe_pnat_injective.eq_iff

Premises used: Nat.Primes.coe_pnat_injective, Function.Injective.eq_iff
-- Module: Mathlib.Data.PNat.Prime
Goal:
n m : ℕ+
h : 0 < (↑n : ℕ) * (↑m : ℕ) := ⋯
⊢ 0 < (↑n : ℕ).lcm (↑m : ℕ) * (↑n : ℕ).gcd (↑m : ℕ)

Tactic:
rw [← gcd_mul_lcm (n : ℕ) (m : ℕ), mul_comm] at h

Premises used: PNat.val, Nat.gcd_mul_lcm, mul_comm
-- Module: Mathlib.Data.PNat.Prime
Goal:
n m : ℕ+
h : 0 < (↑n : ℕ).lcm (↑m : ℕ) * (↑n : ℕ).gcd (↑m : ℕ)
⊢ 0 < (↑n : ℕ).lcm (↑m : ℕ)

Tactic:
pos_of_dvd_of_pos (Dvd.intro (Nat.gcd (n : ℕ) (m : ℕ)) rfl) h

Premises used: Nat.gcd, PNat.val, Dvd.intro, Nat.pos_of_dvd_of_pos, rfl
-- Module: Mathlib.Data.PNat.Prime
Goal:
n m : ℕ+
h : 0 < (↑n : ℕ).lcm (↑m : ℕ) * (↑n : ℕ).gcd (↑m : ℕ)
⊢ 0 < (↑n : ℕ).lcm (↑m : ℕ)

Tactic:
exact pos_of_dvd_of_pos (Dvd.intro (Nat.gcd (n : ℕ) (m : ℕ)) rfl) h

Premises used: Nat.gcd, PNat.val, Dvd.intro, Nat.pos_of_dvd_of_pos, rfl
-- Module: Mathlib.Data.PNat.Prime
Goal:
n m : ℕ+
⊢ (↑(n.gcd m) : ℕ) = (↑n : ℕ).gcd (↑m : ℕ)

Tactic:
rfl

Premises used: PNat.val, rfl
-- Module: Mathlib.Data.PNat.Prime
Goal:
n m : ℕ+
⊢ (↑(n.lcm m) : ℕ) = (↑n : ℕ).lcm (↑m : ℕ)

Tactic:
rfl

Premises used: Nat.lcm, PNat.val, rfl
-- Module: Mathlib.Data.PNat.Prime
Goal:
n m : ℕ+
⊢ n.gcd m ∣ n

Tactic:
dvd_iff.2 (Nat.gcd_dvd_left (n : ℕ) (m : ℕ))

Premises used: PNat.val, Iff.mpr, Nat.gcd_dvd_left, PNat.dvd_iff
-- Module: Mathlib.Data.PNat.Prime
Goal:
n m : ℕ+
⊢ n.gcd m ∣ m

Tactic:
dvd_iff.2 (Nat.gcd_dvd_right (n : ℕ) (m : ℕ))

Premises used: PNat.val, Iff.mpr, PNat.dvd_iff, Nat.gcd_dvd_right
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n k : ℕ+
hm : k ∣ m
hn : k ∣ n
⊢ k ∣ m.gcd n

Tactic:
dvd_iff.2 (Nat.dvd_gcd (dvd_iff.1 hm) (dvd_iff.1 hn))

Premises used: Iff.mpr, PNat.dvd_iff, Nat.dvd_gcd, Iff.mp
-- Module: Mathlib.Data.PNat.Prime
Goal:
n m : ℕ+
⊢ n ∣ n.lcm m

Tactic:
dvd_iff.2 (Nat.dvd_lcm_left (n : ℕ) (m : ℕ))

Premises used: PNat.val, Iff.mpr, Nat.dvd_lcm_left, PNat.dvd_iff
-- Module: Mathlib.Data.PNat.Prime
Goal:
n m : ℕ+
⊢ m ∣ n.lcm m

Tactic:
dvd_iff.2 (Nat.dvd_lcm_right (n : ℕ) (m : ℕ))

Premises used: PNat.val, Iff.mpr, PNat.dvd_iff, Nat.dvd_lcm_right
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n k : ℕ+
hm : m ∣ k
hn : n ∣ k
⊢ m.lcm n ∣ k

Tactic:
dvd_iff.2 (@Nat.lcm_dvd (m : ℕ) (n : ℕ) (k : ℕ) (dvd_iff.1 hm) (dvd_iff.1 hn))

Premises used: Iff.mpr, PNat.dvd_iff, Nat.lcm_dvd, Iff.mp
-- Module: Mathlib.Data.PNat.Prime
Goal:
n m : ℕ+
⊢ n.gcd m * n.lcm m = n * m

Tactic:
Subtype.ext (Nat.gcd_mul_lcm (n : ℕ) (m : ℕ))

Premises used: PNat.val, Nat.gcd_mul_lcm, Subtype.ext, PNat
-- Module: Mathlib.Data.PNat.Prime
Goal:
n : ℕ+
rw : n = 1 → n = 1
⊢ n < HAdd.hAdd (α := ℕ+) 1 1 → n = 1

Tactic:
rw [lt_add_one_iff, le_one_iff_eq_one]

Premises used: le_one_iff_eq_one, PNat.lt_add_one_iff
-- Module: Mathlib.Data.PNat.Prime
Goal:
n : ℕ+
⊢ n = 1 → n = 1

Tactic:
id

Premises used: id
-- Module: Mathlib.Data.PNat.Prime
Goal:
n : ℕ+
⊢ n = 1 → n = 1

Tactic:
exact id

Premises used: id
-- Module: Mathlib.Data.PNat.Prime
Goal:
p : ℕ+
⊢ p.Prime → 1 < p

Tactic:
Nat.Prime.one_lt

Premises used: PNat.val, Nat.Prime.one_lt, PNat.Prime
-- Module: Mathlib.Data.PNat.Prime
Goal:
⊢ Prime 2

Tactic:
Nat.prime_two

Premises used: PNat.val, Nat.prime_two, PNat.Prime
-- Module: Mathlib.Data.PNat.Prime
Goal:
p : ℕ+
h : Fact p.Prime
⊢ Fact (Nat.Prime (↑p : ℕ))

Tactic:
h

Premises used: PNat.Prime
-- Module: Mathlib.Data.PNat.Prime
Goal:
⊢ Fact (Prime 2)

Tactic:
⟨prime_two⟩

Premises used: Fact.mk, PNat.prime_two
-- Module: Mathlib.Data.PNat.Prime
Goal:
⊢ Prime 3

Tactic:
Nat.prime_three

Premises used: PNat.val, Nat.prime_three, PNat.Prime
-- Module: Mathlib.Data.PNat.Prime
Goal:
⊢ Fact (Prime 3)

Tactic:
⟨prime_three⟩

Premises used: Fact.mk, PNat.prime_three
-- Module: Mathlib.Data.PNat.Prime
Goal:
⊢ Prime 5

Tactic:
Nat.prime_five

Premises used: PNat.val, Nat.prime_five, PNat.Prime
-- Module: Mathlib.Data.PNat.Prime
Goal:
⊢ Fact (Prime 5)

Tactic:
⟨prime_five⟩

Premises used: PNat.prime_five, Fact.mk
-- Module: Mathlib.Data.PNat.Prime
Goal:
p m : ℕ+
pp : p.Prime
rw : (↑m : ℕ) ∣ (↑p : ℕ) ↔ m = 1 ∨ m = p
⊢ m ∣ p ↔ m = 1 ∨ m = p

Tactic:
rw [PNat.dvd_iff]

Premises used: PNat.dvd_iff
-- Module: Mathlib.Data.PNat.Prime
Goal:
p m : ℕ+
pp : p.Prime
rw : (↑m : ℕ) = 1 ∨ (↑m : ℕ) = (↑p : ℕ) ↔ m = 1 ∨ m = p
⊢ (↑m : ℕ) ∣ (↑p : ℕ) ↔ m = 1 ∨ m = p

Tactic:
rw [Nat.dvd_prime pp]

Premises used: Nat.dvd_prime
-- Module: Mathlib.Data.PNat.Prime
Goal:
p m : ℕ+
pp : p.Prime
⊢ (↑m : ℕ) = 1 ∨ (↑m : ℕ) = (↑p : ℕ) ↔ m = 1 ∨ m = p

Tactic:
simp
-- Module: Mathlib.Data.PNat.Prime
Goal:
p : ℕ+
pp : p.Prime
contra : p = 1
apply : (↑p : ℕ) = 1
⊢ False

Tactic:
apply Nat.Prime.ne_one pp

Premises used: Nat.Prime.ne_one
-- Module: Mathlib.Data.PNat.Prime
Goal:
p : ℕ+
pp : p.Prime
contra rw : p = 1
⊢ (↑p : ℕ) = 1

Tactic:
rw [PNat.coe_eq_one_iff]

Premises used: PNat.coe_eq_one_iff
-- Module: Mathlib.Data.PNat.Prime
Goal:
p : ℕ+
pp : p.Prime
contra : p = 1
⊢ p = 1

Tactic:
apply contra
-- Module: Mathlib.Data.PNat.Prime
Goal:
⊢ ¬Prime 1

Tactic:
Nat.not_prime_one

Premises used: PNat.val, Nat.not_prime_one, PNat.Prime
-- Module: Mathlib.Data.PNat.Prime
Goal:
p : ℕ+
pp : p.Prime
rw : ¬(↑p : ℕ) ∣ (↑1 : ℕ)
⊢ ¬p ∣ 1

Tactic:
rw [dvd_iff]

Premises used: PNat.dvd_iff
-- Module: Mathlib.Data.PNat.Prime
Goal:
p : ℕ+
pp : p.Prime
⊢ ¬(↑p : ℕ) ∣ (↑1 : ℕ)

Tactic:
apply Nat.Prime.not_dvd_one pp

Premises used: Nat.Prime.not_dvd_one
-- Module: Mathlib.Data.PNat.Prime
Goal:
n : ℕ+
hn : n ≠ 1
obtain : ∀ (p : ℕ) (hp : Nat.Prime p ∧ p ∣ (↑n : ℕ)), ∃ (p : ℕ+), p.Prime ∧ p ∣ n
⊢ ∃ (p : ℕ+), p.Prime ∧ p ∣ n

Tactic:
obtain ⟨p, hp⟩ := Nat.exists_prime_and_dvd (mt coe_eq_one_iff.mp hn)

Premises used: PNat.coe_eq_one_iff, mt, Nat.exists_prime_and_dvd, Iff.mp
-- Module: Mathlib.Data.PNat.Prime
Goal:
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ (↑n : ℕ)
exists : Prime (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p ⋯) ∧ Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p ⋯ ∣ n
⊢ ∃ (p : ℕ+), p.Prime ∧ p ∣ n

Tactic:
exists (⟨p, Nat.Prime.pos hp.left⟩ : ℕ+)

Premises used: Nat.Prime.pos, Subtype.mk, And.left
-- Module: Mathlib.Data.PNat.Prime
Goal:
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ (↑n : ℕ)
rw : Prime (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p ⋯) ∧ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p ⋯) : ℕ) ∣ (↑n : ℕ)
⊢ Prime (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p ⋯) ∧ Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p ⋯ ∣ n

Tactic:
rw [dvd_iff]

Premises used: PNat.dvd_iff
-- Module: Mathlib.Data.PNat.Prime
Goal:
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ (↑n : ℕ)
⊢ Prime (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p ⋯) ∧ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p ⋯) : ℕ) ∣ (↑n : ℕ)

Tactic:
apply hp
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n : ℕ+
rw : (↑m : ℕ).gcd (↑n : ℕ) = 1 ↔ (↑(m.gcd n) : ℕ) = (↑1 : ℕ)
⊢ (↑m : ℕ).gcd (↑n : ℕ) = 1 ↔ m.gcd n = 1

Tactic:
rw [← coe_inj]

Premises used: PNat.coe_inj
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n : ℕ+
⊢ (↑m : ℕ).gcd (↑n : ℕ) = 1 ↔ (↑(m.gcd n) : ℕ) = (↑1 : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.PNat.Prime
Goal:
k m n : ℕ+
rw : (↑m : ℕ).Coprime (↑k : ℕ) → n.Coprime k → (m * n).Coprime k
⊢ m.Coprime k → n.Coprime k → (m * n).Coprime k

Tactic:
rw [← coprime_coe]

Premises used: PNat.coprime_coe
-- Module: Mathlib.Data.PNat.Prime
Goal:
k m n : ℕ+
rw : (↑m : ℕ).Coprime (↑k : ℕ) → (↑n : ℕ).Coprime (↑k : ℕ) → (m * n).Coprime k
⊢ (↑m : ℕ).Coprime (↑k : ℕ) → n.Coprime k → (m * n).Coprime k

Tactic:
rw [← coprime_coe]

Premises used: PNat.coprime_coe
-- Module: Mathlib.Data.PNat.Prime
Goal:
k m n : ℕ+
rw : (↑m : ℕ).Coprime (↑k : ℕ) → (↑n : ℕ).Coprime (↑k : ℕ) → (↑(m * n) : ℕ).Coprime (↑k : ℕ)
⊢ (↑m : ℕ).Coprime (↑k : ℕ) → (↑n : ℕ).Coprime (↑k : ℕ) → (m * n).Coprime k

Tactic:
rw [← coprime_coe]

Premises used: PNat.coprime_coe
-- Module: Mathlib.Data.PNat.Prime
Goal:
k m n : ℕ+
repeat : (↑m : ℕ).Coprime (↑k : ℕ) → (↑n : ℕ).Coprime (↑k : ℕ) → (↑(m * n) : ℕ).Coprime (↑k : ℕ)
⊢ m.Coprime k → n.Coprime k → (m * n).Coprime k

Tactic:
repeat rw [← coprime_coe]

Premises used: PNat.coprime_coe
-- Module: Mathlib.Data.PNat.Prime
Goal:
k m n : ℕ+
⊢ (↑m : ℕ).Coprime (↑k : ℕ) → (↑n : ℕ).Coprime (↑k : ℕ) → ((↑m : ℕ) * (↑n : ℕ)).Coprime (↑k : ℕ)

Tactic:
apply Nat.Coprime.mul_left

Premises used: Nat.Coprime.mul_left
-- Module: Mathlib.Data.PNat.Prime
Goal:
k m n : ℕ+
rw : (↑k : ℕ).Coprime (↑m : ℕ) → k.Coprime n → k.Coprime (m * n)
⊢ k.Coprime m → k.Coprime n → k.Coprime (m * n)

Tactic:
rw [← coprime_coe]

Premises used: PNat.coprime_coe
-- Module: Mathlib.Data.PNat.Prime
Goal:
k m n : ℕ+
rw : (↑k : ℕ).Coprime (↑m : ℕ) → (↑k : ℕ).Coprime (↑n : ℕ) → k.Coprime (m * n)
⊢ (↑k : ℕ).Coprime (↑m : ℕ) → k.Coprime n → k.Coprime (m * n)

Tactic:
rw [← coprime_coe]

Premises used: PNat.coprime_coe
-- Module: Mathlib.Data.PNat.Prime
Goal:
k m n : ℕ+
rw : (↑k : ℕ).Coprime (↑m : ℕ) → (↑k : ℕ).Coprime (↑n : ℕ) → (↑k : ℕ).Coprime (↑(m * n) : ℕ)
⊢ (↑k : ℕ).Coprime (↑m : ℕ) → (↑k : ℕ).Coprime (↑n : ℕ) → k.Coprime (m * n)

Tactic:
rw [← coprime_coe]

Premises used: PNat.coprime_coe
-- Module: Mathlib.Data.PNat.Prime
Goal:
k m n : ℕ+
repeat : (↑k : ℕ).Coprime (↑m : ℕ) → (↑k : ℕ).Coprime (↑n : ℕ) → (↑k : ℕ).Coprime (↑(m * n) : ℕ)
⊢ k.Coprime m → k.Coprime n → k.Coprime (m * n)

Tactic:
repeat rw [← coprime_coe]

Premises used: PNat.coprime_coe
-- Module: Mathlib.Data.PNat.Prime
Goal:
k m n : ℕ+
⊢ (↑k : ℕ).Coprime (↑m : ℕ) → (↑k : ℕ).Coprime (↑n : ℕ) → (↑k : ℕ).Coprime ((↑m : ℕ) * (↑n : ℕ))

Tactic:
apply Nat.Coprime.mul_right

Premises used: Nat.Coprime.mul_right
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n : ℕ+
a : (↑(m.gcd n) : ℕ) = (↑(n.gcd m) : ℕ)
⊢ m.gcd n = n.gcd m

Tactic:
apply eq

Premises used: PNat.eq
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n : ℕ+
⊢ (↑m : ℕ).gcd (↑n : ℕ) = (↑n : ℕ).gcd (↑m : ℕ)

Tactic:
apply Nat.gcd_comm

Premises used: Nat.gcd_comm
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n : ℕ+
rw : (↑(m.gcd n) : ℕ) = (↑m : ℕ) ↔ (↑m : ℕ).gcd (↑n : ℕ) = (↑m : ℕ)
⊢ m.gcd n = m ↔ m ∣ n

Tactic:
rw [dvd_iff, ← Nat.gcd_eq_left_iff_dvd, ← coe_inj]

Premises used: PNat.dvd_iff, Nat.gcd_eq_left_iff_dvd, PNat.coe_inj
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n : ℕ+
⊢ (↑(m.gcd n) : ℕ) = (↑m : ℕ) ↔ (↑m : ℕ).gcd (↑n : ℕ) = (↑m : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n : ℕ+
rw : m.gcd n = m ↔ m ∣ n
⊢ n.gcd m = m ↔ m ∣ n

Tactic:
rw [gcd_comm]

Premises used: PNat.gcd_comm
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n : ℕ+
⊢ m.gcd n = m ↔ m ∣ n

Tactic:
apply gcd_eq_left_iff_dvd

Premises used: PNat.gcd_eq_left_iff_dvd
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n k : ℕ+
h : k.Coprime n
a : (↑((k * m).gcd n) : ℕ) = (↑(m.gcd n) : ℕ)
⊢ (k * m).gcd n = m.gcd n

Tactic:
apply eq

Premises used: PNat.eq
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n k : ℕ+
h : k.Coprime n
a : (↑k : ℕ).Coprime (↑n : ℕ)
⊢ ((↑k : ℕ) * (↑m : ℕ)).gcd (↑n : ℕ) = (↑m : ℕ).gcd (↑n : ℕ)

Tactic:
apply Nat.Coprime.gcd_mul_left_cancel

Premises used: Nat.Coprime.gcd_mul_left_cancel
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n k : ℕ+
h : k.Coprime n
⊢ (↑k : ℕ).Coprime (↑n : ℕ)

Tactic:
simpa
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n k : ℕ+
rw : k.Coprime n → (k * m).gcd n = m.gcd n
⊢ k.Coprime n → (m * k).gcd n = m.gcd n

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n k : ℕ+
⊢ k.Coprime n → (k * m).gcd n = m.gcd n

Tactic:
apply Coprime.gcd_mul_left_cancel

Premises used: PNat.Coprime.gcd_mul_left_cancel
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n k : ℕ+
h : k.Coprime m
rw : (k * n).gcd m = m.gcd n
⊢ m.gcd (k * n) = m.gcd n

Tactic:
rw [gcd_comm]

Premises used: PNat.gcd_comm
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n k : ℕ+
h : k.Coprime m
symm : m.gcd n = (k * n).gcd m
⊢ (k * n).gcd m = m.gcd n

Tactic:
symm
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n k : ℕ+
h : k.Coprime m
rw : n.gcd m = (k * n).gcd m
⊢ m.gcd n = (k * n).gcd m

Tactic:
rw [gcd_comm]

Premises used: PNat.gcd_comm
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n k : ℕ+
h : k.Coprime m
symm : (k * n).gcd m = n.gcd m
⊢ n.gcd m = (k * n).gcd m

Tactic:
symm
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n k : ℕ+
h : k.Coprime m
iterate : (k * n).gcd m = n.gcd m
⊢ m.gcd (k * n) = m.gcd n

Tactic:
iterate 2 rw [gcd_comm]; symm

Premises used: PNat.gcd_comm
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n k : ℕ+
h : k.Coprime m
⊢ (k * n).gcd m = n.gcd m

Tactic:
apply Coprime.gcd_mul_left_cancel _ h

Premises used: PNat.Coprime.gcd_mul_left_cancel
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n k : ℕ+
rw : k.Coprime m → m.gcd (k * n) = m.gcd n
⊢ k.Coprime m → m.gcd (n * k) = m.gcd n

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n k : ℕ+
⊢ k.Coprime m → m.gcd (k * n) = m.gcd n

Tactic:
apply Coprime.gcd_mul_left_cancel_right

Premises used: PNat.Coprime.gcd_mul_left_cancel_right
-- Module: Mathlib.Data.PNat.Prime
Goal:
n : ℕ+
rw : 1 ∣ n
⊢ gcd 1 n = 1

Tactic:
rw [gcd_eq_left_iff_dvd]

Premises used: PNat.gcd_eq_left_iff_dvd
-- Module: Mathlib.Data.PNat.Prime
Goal:
n : ℕ+
⊢ 1 ∣ n

Tactic:
apply one_dvd

Premises used: one_dvd
-- Module: Mathlib.Data.PNat.Prime
Goal:
n : ℕ+
rw : gcd 1 n = 1
⊢ n.gcd 1 = 1

Tactic:
rw [gcd_comm]

Premises used: PNat.gcd_comm
-- Module: Mathlib.Data.PNat.Prime
Goal:
n : ℕ+
⊢ gcd 1 n = 1

Tactic:
apply one_gcd

Premises used: PNat.one_gcd
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n : ℕ+
rw : n.gcd m = 1 → n.gcd m = 1
⊢ m.gcd n = 1 → n.gcd m = 1

Tactic:
rw [gcd_comm]

Premises used: PNat.gcd_comm
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n : ℕ+
⊢ n.gcd m = 1 → n.gcd m = 1

Tactic:
simp
-- Module: Mathlib.Data.PNat.Prime
Goal:
n : ℕ+
⊢ Coprime 1 n

Tactic:
one_gcd

Premises used: PNat.Coprime, PNat.one_gcd
-- Module: Mathlib.Data.PNat.Prime
Goal:
n : ℕ+
⊢ n.Coprime 1

Tactic:
Coprime.symm one_coprime

Premises used: PNat.Coprime.symm, PNat.one_coprime
-- Module: Mathlib.Data.PNat.Prime
Goal:
m k n : ℕ+
rw : (↑m : ℕ) ∣ (↑k : ℕ) → k.Coprime n → m.Coprime n
⊢ m ∣ k → k.Coprime n → m.Coprime n

Tactic:
rw [dvd_iff]

Premises used: PNat.dvd_iff
-- Module: Mathlib.Data.PNat.Prime
Goal:
m k n : ℕ+
rw : (↑m : ℕ) ∣ (↑k : ℕ) → (↑k : ℕ).Coprime (↑n : ℕ) → m.Coprime n
⊢ (↑m : ℕ) ∣ (↑k : ℕ) → k.Coprime n → m.Coprime n

Tactic:
rw [← coprime_coe]

Premises used: PNat.coprime_coe
-- Module: Mathlib.Data.PNat.Prime
Goal:
m k n : ℕ+
rw : (↑m : ℕ) ∣ (↑k : ℕ) → (↑k : ℕ).Coprime (↑n : ℕ) → (↑m : ℕ).Coprime (↑n : ℕ)
⊢ (↑m : ℕ) ∣ (↑k : ℕ) → (↑k : ℕ).Coprime (↑n : ℕ) → m.Coprime n

Tactic:
rw [← coprime_coe]

Premises used: PNat.coprime_coe
-- Module: Mathlib.Data.PNat.Prime
Goal:
m k n : ℕ+
repeat : (↑m : ℕ) ∣ (↑k : ℕ) → (↑k : ℕ).Coprime (↑n : ℕ) → (↑m : ℕ).Coprime (↑n : ℕ)
⊢ (↑m : ℕ) ∣ (↑k : ℕ) → k.Coprime n → m.Coprime n

Tactic:
repeat rw [← coprime_coe]

Premises used: PNat.coprime_coe
-- Module: Mathlib.Data.PNat.Prime
Goal:
m k n : ℕ+
⊢ (↑m : ℕ) ∣ (↑k : ℕ) → (↑k : ℕ).Coprime (↑n : ℕ) → (↑m : ℕ).Coprime (↑n : ℕ)

Tactic:
apply Nat.Coprime.coprime_dvd_left

Premises used: Nat.Coprime.coprime_dvd_left
-- Module: Mathlib.Data.PNat.Prime
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a.gcd m = a

Tactic:
rw [← gcd_eq_left_iff_dvd] at am

Premises used: PNat.gcd_eq_left_iff_dvd
-- Module: Mathlib.Data.PNat.Prime
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
am₁ : a.gcd m = a
⊢ b ∣ n

Tactic:
rw [← gcd_eq_left_iff_dvd] at am

Premises used: PNat.gcd_eq_left_iff_dvd
-- Module: Mathlib.Data.PNat.Prime
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
rw : a.gcd m
| a

Tactic:
rw [← am]
-- Module: Mathlib.Data.PNat.Prime
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
conv_lhs : a.gcd m = (a * b).gcd m
⊢ a = (a * b).gcd m

Tactic:
conv_lhs => rw [← am]
-- Module: Mathlib.Data.PNat.Prime
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
rw : (a * b).gcd m = a.gcd m
⊢ a.gcd m = (a * b).gcd m

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.PNat.Prime
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
apply : b.Coprime m
⊢ (a * b).gcd m = a.gcd m

Tactic:
apply Coprime.gcd_mul_right_cancel a

Premises used: PNat.Coprime.gcd_mul_right_cancel
-- Module: Mathlib.Data.PNat.Prime
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ b.Coprime m

Tactic:
apply Coprime.coprime_dvd_left bn cop.symm

Premises used: PNat.Coprime.coprime_dvd_left, PNat.Coprime.symm
-- Module: Mathlib.Data.PNat.Prime
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
rw : a = (a * b).gcd m
⊢ a = (b * a).gcd m

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.PNat.Prime
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (a * b).gcd m

Tactic:
apply Coprime.factor_eq_gcd_left cop am bn

Premises used: PNat.Coprime.factor_eq_gcd_left
-- Module: Mathlib.Data.PNat.Prime
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
rw : a = (a * b).gcd m
⊢ a = m.gcd (a * b)

Tactic:
rw [gcd_comm]

Premises used: PNat.gcd_comm
-- Module: Mathlib.Data.PNat.Prime
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
rw : a = (b * a).gcd m
⊢ a = m.gcd (b * a)

Tactic:
rw [gcd_comm]

Premises used: PNat.gcd_comm
-- Module: Mathlib.Data.PNat.Prime
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (b * a).gcd m

Tactic:
apply Coprime.factor_eq_gcd_right cop am bn

Premises used: PNat.Coprime.factor_eq_gcd_right
-- Module: Mathlib.Data.PNat.Prime
Goal:
k m n : ℕ+
h : m.Coprime n
⊢ (↑m : ℕ).Coprime (↑n : ℕ)

Tactic:
rw [← coprime_coe] at h

Premises used: PNat.coprime_coe
-- Module: Mathlib.Data.PNat.Prime
Goal:
k m n : ℕ+
h : (↑m : ℕ).Coprime (↑n : ℕ)
a : (↑(k.gcd (m * n)) : ℕ) = (↑(k.gcd m * k.gcd n) : ℕ)
⊢ k.gcd (m * n) = k.gcd m * k.gcd n

Tactic:
apply eq

Premises used: PNat.eq
-- Module: Mathlib.Data.PNat.Prime
Goal:
k m n : ℕ+
h : (↑m : ℕ).Coprime (↑n : ℕ)
⊢ (↑k : ℕ).gcd ((↑m : ℕ) * (↑n : ℕ)) = (↑k : ℕ).gcd (↑m : ℕ) * (↑k : ℕ).gcd (↑n : ℕ)

Tactic:
apply Nat.Coprime.gcd_mul k h

Premises used: PNat.val, Nat.Coprime.gcd_mul
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n : ℕ+
k l : ℕ
h : m.Coprime n
⊢ (↑m : ℕ).Coprime (↑n : ℕ)

Tactic:
rw [← coprime_coe] at *

Premises used: PNat.coprime_coe
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n : ℕ+
k l : ℕ
h H1 : (↑m : ℕ).Coprime (↑n : ℕ)
⊢ ((↑m : ℕ) ^ k).Coprime ((↑n : ℕ) ^ l)

Tactic:
apply Nat.Coprime.pow

Premises used: Nat.Coprime.pow
-- Module: Mathlib.Data.PNat.Prime
Goal:
m n : ℕ+
k l : ℕ
h : (↑m : ℕ).Coprime (↑n : ℕ)
⊢ (↑m : ℕ).Coprime (↑n : ℕ)

Tactic:
apply h
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
fst : u.v.1 = (succ₂ u.vp).1
snd : u.v.2 = (succ₂ u.vp).2
⊢ u.v = succ₂ u.vp

Tactic:
ext
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
⊢ (u.wp + 1) * (u.ap + 1) + u.x * (u.bp + 1) = u.wp + u.x + u.ap + u.wp * u.ap + u.x * u.bp + 1

Tactic:
ring_nf
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
⊢ u.y * (u.ap + 1) + (u.zp + 1) * (u.bp + 1) = u.y + u.zp + u.bp + u.y * u.ap + u.zp * u.bp + 1

Tactic:
ring_nf