u v : PrimeMultiset
n : ℕ+ := prod u
⊢ prod (u ⊓ v) = PNat.gcd (prod u) (prod v)
u v : PrimeMultiset
⊢ prod (u ⊓ v) = PNat.gcd (prod u) (prod v)
let n := u.prod
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
⊢ prod (u ⊓ v) = PNat.gcd (prod u) (prod v)
u v : PrimeMultiset
n : ℕ+ := prod u
⊢ prod (u ⊓ v) = PNat.gcd (prod u) (prod v)
let m := v.prod
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
⊢ prod (u ⊓ v) = PNat.gcd n m
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
⊢ prod (u ⊓ v) = PNat.gcd (prod u) (prod v)
change (u ⊓ v).prod = PNat.gcd n m
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this : u = PNat.factorMultiset n
⊢ prod (u ⊓ v) = PNat.gcd n m
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
⊢ prod (u ⊓ v) = PNat.gcd n m
have : u = n.factorMultiset := u.factorMultiset_prod.symm
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this : u = PNat.factorMultiset n
⊢ prod (PNat.factorMultiset n ⊓ v) = PNat.gcd n m
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this : u = PNat.factorMultiset n
⊢ prod (u ⊓ v) = PNat.gcd n m
rw [this]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this✝ : u = PNat.factorMultiset n
this : v = PNat.factorMultiset m
⊢ prod (PNat.factorMultiset n ⊓ v) = PNat.gcd n m
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this : u = PNat.factorMultiset n
⊢ prod (PNat.factorMultiset n ⊓ v) = PNat.gcd n m
have : v = m.factorMultiset := v.factorMultiset_prod.symm
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this✝ : u = PNat.factorMultiset n
this : v = PNat.factorMultiset m
⊢ prod (PNat.factorMultiset n ⊓ PNat.factorMultiset m) = PNat.gcd n m
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this✝ : u = PNat.factorMultiset n
this : v = PNat.factorMultiset m
⊢ prod (PNat.factorMultiset n ⊓ v) = PNat.gcd n m
rw [this]
no goals
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this✝ : u = PNat.factorMultiset n
this : v = PNat.factorMultiset m
⊢ prod (PNat.factorMultiset n ⊓ PNat.factorMultiset m) = PNat.gcd n m
rw [← PNat.factorMultiset_gcd n m, PNat.prod_factorMultiset]