a*a = b*c -> gcd a b = min a b

Stream: maths

[Rick Love]

I'm trying to prove the following, but I am stuck. I'm not sure how to proceed.

A proof in words would be something like:

• get all prime factors for both sides
• the prime factors must match
• the union of all factors in a * a = b * c
• the common factors a,b + common factors a,c = all factors
• common factors a,b = min a,b

However, I don't know how to break the equality into it's factors and prove their intersection in lean

-- 4 * 4 = 2 * 8  -> gcd a b = 2 gcd a c = 4
-- 6 * 6 = 4 * 9  -> gcd a b = 2 gcd a c = 3
-- 6 * 6 = 1 * 36 -> gcd a b = 1 gcd a c = 6
theorem multiple_factors_then_gcd (a b c k : nat):
    a*a = b*c ->
    gcd a b = min a b :=
begin
    intros,

    cases eq_or_not a b with ab_eq ab_neq,
    -- case a = b
    {
        rw ab_eq,
        rw min_self,
        apply gcd_eq_left,
        refl,
    },

    cases le_or_gt a b with ab_le ab_gt,
    -- case a < b
    {
        have haltb : a < b, {apply le_and_ne_then_lt, split, apply ab_le, apply ab_neq,},
        rw min_eq_left ab_le,
        apply gcd_eq_left,
        apply dvd.intro k,

        -- revert a_1,
        -- contrapose,
        -- intros,
        -- rw a_1,

        -- rw nat.div,
        sorry,
    },

    -- case a > b
    have hageb : a >= b, {apply le_of_lt ab_gt},
    rw min_eq_right hageb,
    apply gcd_eq_right,
    sorry,

    -- case a > b

    -- split,
    -- apply dvd.intro a,
    -- cc,

    -- split,
    -- apply dvd.intro d,
    -- cc,

    -- apply dvd.intro c,
    -- cc,
end

[Rick Love]

Actually starting to make progress now that I had to think about how to do that in words:

-- 4 * 4 = 2 * 8  -> gcd a b = 2 gcd a c = 4
-- 6 * 6 = 4 * 9  -> gcd a b = 2 gcd a c = 3
-- 6 * 6 = 1 * 36 -> gcd a b = 1 gcd a c = 6
theorem multiple_factors_then_gcd (a b c k : nat):
    a*a = b*c ->
    gcd a b = min a b :=
begin
    intros h,

    let faa := factors (a*a),
    let fbc := factors (b*c),
    have h_faa_fbc : faa = fbc := by { dsimp [faa, fbc], rw h,},


    -- have
end

[Kevin Buzzard]

How about 12^2=9*16?

[Kevin Buzzard]

Or even 6^2=9*4?