this : ∀ (a b : Num), natSize (a * b) ≤ natSize a + natSize b
⊢ ∀ (a b : Num), ↑(gcd a b) = Nat.gcd ↑a ↑b
⊢ ∀ (a b : Num), ↑(gcd a b) = Nat.gcd ↑a ↑b
have : ∀ a b : Num, (a * b).natSize ≤ a.natSize + b.natSize := by
  intros
  simp [natSize_to_nat]
  rw [Nat.size_le, pow_add]
  exact mul_lt_mul'' (Nat.lt_size_self _) (Nat.lt_size_self _) (Nat.zero_le _) (Nat.zero_le _)
this : ∀ (a b : Num), natSize (a * b) ≤ natSize a + natSize b
a✝ b✝ : Num
⊢ ↑(gcd a✝ b✝) = Nat.gcd ↑a✝ ↑b✝
this : ∀ (a b : Num), natSize (a * b) ≤ natSize a + natSize b
⊢ ∀ (a b : Num), ↑(gcd a b) = Nat.gcd ↑a ↑b
intros
this : ∀ (a b : Num), natSize (a * b) ≤ natSize a + natSize b
a✝ b✝ : Num
⊢ ↑(if a✝ ≤ b✝ then gcdAux (natSize a✝ + natSize b✝) a✝ b✝ else gcdAux (natSize b✝ + natSize a✝) b✝ a✝) =
    Nat.gcd ↑a✝ ↑b✝
this : ∀ (a b : Num), natSize (a * b) ≤ natSize a + natSize b
a✝ b✝ : Num
⊢ ↑(gcd a✝ b✝) = Nat.gcd ↑a✝ ↑b✝
unfold gcd
case inl
this : ∀ (a b : Num), natSize (a * b) ≤ natSize a + natSize b
a✝ b✝ : Num
h : a✝ ≤ b✝
⊢ ↑(gcdAux (natSize a✝ + natSize b✝) a✝ b✝) = Nat.gcd ↑a✝ ↑b✝

case inr
this : ∀ (a b : Num), natSize (a * b) ≤ natSize a + natSize b
a✝ b✝ : Num
h : ¬a✝ ≤ b✝
⊢ ↑(gcdAux (natSize b✝ + natSize a✝) b✝ a✝) = Nat.gcd ↑a✝ ↑b✝
this : ∀ (a b : Num), natSize (a * b) ≤ natSize a + natSize b
a✝ b✝ : Num
⊢ ↑(if a✝ ≤ b✝ then gcdAux (natSize a✝ + natSize b✝) a✝ b✝ else gcdAux (natSize b✝ + natSize a✝) b✝ a✝) =
    Nat.gcd ↑a✝ ↑b✝
split_ifs with h
a✝ b✝ : Num
⊢ natSize (a✝ * b✝) ≤ natSize a✝ + natSize b✝
⊢ ∀ (a b : Num), natSize (a * b) ≤ natSize a + natSize b
intros
a✝ b✝ : Num
⊢ Nat.size (↑a✝ * ↑b✝) ≤ Nat.size ↑a✝ + Nat.size ↑b✝
a✝ b✝ : Num
⊢ natSize (a✝ * b✝) ≤ natSize a✝ + natSize b✝
simp [natSize_to_nat]
a✝ b✝ : Num
⊢ ↑a✝ * ↑b✝ < 2 ^ Nat.size ↑a✝ * 2 ^ Nat.size ↑b✝
a✝ b✝ : Num
⊢ Nat.size (↑a✝ * ↑b✝) ≤ Nat.size ↑a✝ + Nat.size ↑b✝
rw [Nat.size_le, pow_add]
no goals
a✝ b✝ : Num
⊢ ↑a✝ * ↑b✝ < 2 ^ Nat.size ↑a✝ * 2 ^ Nat.size ↑b✝
exact mul_lt_mul'' (Nat.lt_size_self _) (Nat.lt_size_self _) (Nat.zero_le _) (Nat.zero_le _)
no goals
case inl
this : ∀ (a b : Num), natSize (a * b) ≤ natSize a + natSize b
a✝ b✝ : Num
h : a✝ ≤ b✝
⊢ ↑(gcdAux (natSize a✝ + natSize b✝) a✝ b✝) = Nat.gcd ↑a✝ ↑b✝
exact gcd_to_nat_aux h (this _ _)
case inr
this : ∀ (a b : Num), natSize (a * b) ≤ natSize a + natSize b
a✝ b✝ : Num
h : ¬a✝ ≤ b✝
⊢ ↑(gcdAux (natSize b✝ + natSize a✝) b✝ a✝) = Nat.gcd ↑b✝ ↑a✝
case inr
this : ∀ (a b : Num), natSize (a * b) ≤ natSize a + natSize b
a✝ b✝ : Num
h : ¬a✝ ≤ b✝
⊢ ↑(gcdAux (natSize b✝ + natSize a✝) b✝ a✝) = Nat.gcd ↑a✝ ↑b✝
rw [Nat.gcd_comm]
no goals
case inr
this : ∀ (a b : Num), natSize (a * b) ≤ natSize a + natSize b
a✝ b✝ : Num
h : ¬a✝ ≤ b✝
⊢ ↑(gcdAux (natSize b✝ + natSize a✝) b✝ a✝) = Nat.gcd ↑b✝ ↑a✝
exact gcd_to_nat_aux (le_of_not_le h) (this _ _)