norm_num extensions for GCD-adjacent functions

This module defines some norm_num extensions for functions such as Nat.gcd, Nat.lcm, Int.gcd, and Int.lcm.

Note that Nat.coprime is reducible and defined in terms of Nat.gcd, so the Nat.gcd extension also indirectly provides a Nat.coprime extension.

theorem Tactic.NormNum.int_gcd_helper' {d : ℕ} {x y : ℤ} (a b : ℤ) (h₁ : ↑d ∣ x) (h₂ : ↑d ∣ y) (h₃ : x * a + y * b = ↑d) : x.gcd y = d

theorem Tactic.NormNum.nat_gcd_helper_dvd_left (x y : ℕ) (h : y % x = 0) : x.gcd y = x

theorem Tactic.NormNum.nat_gcd_helper_dvd_right (x y : ℕ) (h : x % y = 0) : x.gcd y = y

theorem Tactic.NormNum.nat_gcd_helper_2 (d x y a b : ℕ) (hu : x % d = 0) (hv : y % d = 0) (h : x * a = y * b + d) : x.gcd y = d

theorem Tactic.NormNum.nat_gcd_helper_1 (d x y a b : ℕ) (hu : x % d = 0) (hv : y % d = 0) (h : y * b = x * a + d) : x.gcd y = d

theorem Tactic.NormNum.nat_gcd_helper_1' (x y a b : ℕ) (h : y * b = x * a + 1) : x.gcd y = 1

theorem Tactic.NormNum.nat_gcd_helper_2' (x y a b : ℕ) (h : x * a = y * b + 1) : x.gcd y = 1

theorem Tactic.NormNum.nat_lcm_helper (x y d m : ℕ) (hd : x.gcd y = d) (d0 : d.beq 0 = false) (dm : x * y = d * m) : x.lcm y = m

theorem Tactic.NormNum.int_gcd_helper {x y : ℤ} {x' y' d : ℕ} (hx : x.natAbs = x') (hy : y.natAbs = y') (h : x'.gcd y' = d) : x.gcd y = d

theorem Tactic.NormNum.int_lcm_helper {x y : ℤ} {x' y' d : ℕ} (hx : x.natAbs = x') (hy : y.natAbs = y') (h : x'.lcm y' = d) : x.lcm y = d

theorem Tactic.NormNum.isNat_gcd {x y nx ny z : ℕ} : Mathlib.Meta.NormNum.IsNat x nx → Mathlib.Meta.NormNum.IsNat y ny → nx.gcd ny = z → Mathlib.Meta.NormNum.IsNat (x.gcd y) z

theorem Tactic.NormNum.isNat_lcm {x y nx ny z : ℕ} : Mathlib.Meta.NormNum.IsNat x nx → Mathlib.Meta.NormNum.IsNat y ny → nx.lcm ny = z → Mathlib.Meta.NormNum.IsNat (x.lcm y) z

theorem Tactic.NormNum.isInt_gcd {x y nx ny : ℤ} {z : ℕ} : Mathlib.Meta.NormNum.IsInt x nx → Mathlib.Meta.NormNum.IsInt y ny → nx.gcd ny = z → Mathlib.Meta.NormNum.IsNat (x.gcd y) z

theorem Tactic.NormNum.isInt_lcm {x y nx ny : ℤ} {z : ℕ} : Mathlib.Meta.NormNum.IsInt x nx → Mathlib.Meta.NormNum.IsInt y ny → nx.lcm ny = z → Mathlib.Meta.NormNum.IsNat (x.lcm y) z

def Tactic.NormNum.proveNatGCD (ex ey : Q(ℕ)) : (ed : Q(ℕ)) × Q(«$ex».gcd «$ey» = «$ed»)

Given natural number literals ex and ey, return their GCD as a natural number literal and an equality proof. Panics if ex or ey aren't natural number literals.

def Tactic.NormNum.evalNatGCD : Mathlib.Meta.NormNum.NormNumExt

Evaluate the Nat.gcd function.

def Tactic.NormNum.proveNatLCM (ex ey : Q(ℕ)) : (ed : Q(ℕ)) × Q(«$ex».lcm «$ey» = «$ed»)

Given natural number literals ex and ey, return their LCM as a natural number literal and an equality proof. Panics if ex or ey aren't natural number literals.

def Tactic.NormNum.evalNatLCM : Mathlib.Meta.NormNum.NormNumExt

Evaluates the Nat.lcm function.

def Tactic.NormNum.proveIntGCD (ex ey : Q(ℤ)) : (ed : Q(ℕ)) × Q(«$ex».gcd «$ey» = «$ed»)

Given two integers, return their GCD and an equality proof. Panics if ex or ey aren't integer literals.

def Tactic.NormNum.evalIntGCD : Mathlib.Meta.NormNum.NormNumExt

Evaluates the Int.gcd function.

def Tactic.NormNum.proveIntLCM (ex ey : Q(ℤ)) : (ed : Q(ℕ)) × Q(«$ex».lcm «$ey» = «$ed»)

Given two integers, return their LCM and an equality proof. Panics if ex or ey aren't integer literals.

def Tactic.NormNum.evalIntLCM : Mathlib.Meta.NormNum.NormNumExt

Evaluates the Int.lcm function.

theorem Tactic.NormNum.isInt_ratNum {q : ℚ} {n : ℤ} {n' d : ℕ} : Mathlib.Meta.NormNum.IsRat q n d → n.natAbs = n' → n'.gcd d = 1 → Mathlib.Meta.NormNum.IsInt q.num n

theorem Tactic.NormNum.isNat_ratDen {q : ℚ} {n : ℤ} {n' d : ℕ} : Mathlib.Meta.NormNum.IsRat q n d → n.natAbs = n' → n'.gcd d = 1 → Mathlib.Meta.NormNum.IsNat q.den d

def Tactic.NormNum.evalRatNum : Mathlib.Meta.NormNum.NormNumExt

Evaluates the Rat.num function.

def Tactic.NormNum.evalRatDen : Mathlib.Meta.NormNum.NormNumExt

Evaluates the Rat.den function.