awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
inl :
  ∀ (ha : a < 0),
    (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
inr :
  ∀ (ha : 0 < a),
    (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
⊢ (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)

Tactic:
rcases hna.lt_or_gt with ha | ha

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
inl :
  ∀ (hb : b < 0),
    (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
inl₁ :
  ∀ (hb : 0 < b),
    (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
⊢ (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)

Tactic:
rcases hnb.lt_or_gt with hb | hb

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
inr :
  ∀ (hb : b < 0),
    (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
inr₁ :
  ∀ (hb : 0 < b),
    (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)
⊢ (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)

Tactic:
rcases hnb.lt_or_gt with hb | hb

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
hb : b < 0
⊢ (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)

Tactic:
simp [Int.mul_nonneg_iff, ha.le, ha.not_ge, hb.le, hb.not_ge]

Premises used: Int.mul_nonneg_iff, LT.lt.le, LT.lt.not_ge
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
hb : 0 < b
⊢ (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)

Tactic:
simp [Int.mul_nonneg_iff, ha.le, ha.not_ge, hb.le, hb.not_ge]

Premises used: Int.mul_nonneg_iff, LT.lt.le, LT.lt.not_ge
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
hb : b < 0
⊢ (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)

Tactic:
simp [Int.mul_nonneg_iff, ha.le, ha.not_ge, hb.le, hb.not_ge]

Premises used: Int.mul_nonneg_iff, LT.lt.le, LT.lt.not_ge
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
hb : 0 < b
⊢ (if 0 ≤ a * b then 1 else -1) = HMul.hMul (α := ℤˣ) (if 0 ≤ a then 1 else -1) (if 0 ≤ b then 1 else -1)

Tactic:
simp [Int.mul_nonneg_iff, ha.le, ha.not_ge, hb.le, hb.not_ge]

Premises used: Int.mul_nonneg_iff, LT.lt.le, LT.lt.not_ge
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
u : ℤˣ
eq : u = -1
⊢ LT.lt (α := ℤ) (-1) 0

Tactic:
decide
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
z : ℤ
⊢ Eq (α := ℤˣ) (normUnit z) (if 0 ≤ z then 1 else -1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
z : ℤ
h : 0 ≤ z
rw : z * (↑(normUnit z) : ℤ) = z
rw₁ : z * (↑(if 0 ≤ z then 1 else -1) : ℤ) = z
rw₂ : z * (↑1 : ℤ) = z
rw₃ : z * 1 = z
rw₄ rw₅ : z = z
⊢ (normalize : (a : ℤ) → ℤ) z = z

Tactic:
rw [normalize_apply, normUnit_eq, if_pos h, Units.val_one, mul_one]

Premises used: Int.normUnit_eq, normalize_apply, if_pos, Units.val_one, mul_one
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
z : ℤ
h : z ≤ 0
inl : ∀ (h : LE.le (α := ℤ) 0 0), Eq (α := ℤ) ((normalize : (a : ℤ) → ℤ) 0 : ℤ) (-0 : ℤ)
inr : ∀ (h : z < 0), (normalize : (a : ℤ) → ℤ) z = -z
⊢ (normalize : (a : ℤ) → ℤ) z = -z

Tactic:
obtain rfl | h := h.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
h : LE.le (α := ℤ) 0 0
⊢ Eq (α := ℤ) ((normalize : (a : ℤ) → ℤ) 0 : ℤ) (-0 : ℤ)

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
z : ℤ
h_1 : z ≤ 0
h : z < 0
inr : z * (↑(normUnit z) : ℤ) = -z
inr₁ : z * (↑(if 0 ≤ z then 1 else -1) : ℤ) = -z
inr₂ : z * (↑(-1) : ℤ) = -z
inr₃ : z * -(↑1 : ℤ) = -z
inr₄ : z * -1 = -z
inr₅ inr₆ : -z = -z
⊢ (normalize : (a : ℤ) → ℤ) z = -z

Tactic:
rw [normalize_apply, normUnit_eq, if_neg (not_le_of_gt h), Units.val_neg, Units.val_one,
      mul_neg_one]

Premises used: Int.normUnit_eq, normalize_apply, Units.val_neg, Units.val_one, mul_neg_one, not_le_of_gt, if_neg
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
n : ℕ
⊢ Eq (α := ℤ) ((normalize : (a : ℤ) → ℤ) (↑n : ℤ) : ℤ) ((↑n : ℤ) : ℤ)

Tactic:
normalize_of_nonneg (ofNat_le_ofNat_of_le <| Nat.zero_le n)

Premises used: Nat.zero_le, Int.normalize_of_nonneg, Int.ofNat_le_ofNat_of_le
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
z : ℤ
inl : 0 ≤ z → |z| = (normalize : (a : ℤ) → ℤ) z
inr : z ≤ 0 → |z| = (normalize : (a : ℤ) → ℤ) z
⊢ |z| = (normalize : (a : ℤ) → ℤ) z

Tactic:
cases le_total 0 z

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
z : ℤ
h : 0 ≤ z
⊢ |z| = (normalize : (a : ℤ) → ℤ) z

Tactic:
simp [abs_of_nonneg, abs_of_nonpos, normalize_of_nonneg, normalize_of_nonpos, *]

Premises used: Int.normalize_of_nonneg, Int.normalize_of_nonpos, abs_of_nonpos, abs_of_nonneg
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
z : ℤ
h : z ≤ 0
⊢ |z| = (normalize : (a : ℤ) → ℤ) z

Tactic:
simp [abs_of_nonneg, abs_of_nonpos, normalize_of_nonneg, normalize_of_nonpos, *]

Premises used: Int.normalize_of_nonneg, Int.normalize_of_nonpos, abs_of_nonpos, abs_of_nonneg
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
z : ℤ
hz : (normalize : (a : ℤ) → ℤ) z = z
pos : ∀ (h : 0 ≤ z), 0 ≤ z
neg : ∀ (h : z < 0), 0 ≤ z
⊢ 0 ≤ z

Tactic:
by_cases! h : 0 ≤ z
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
z : ℤ
hz : (normalize : (a : ℤ) → ℤ) z = z
h : 0 ≤ z
⊢ 0 ≤ z

Tactic:
h
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
z : ℤ
hz : (normalize : (a : ℤ) → ℤ) z = z
h : 0 ≤ z
⊢ 0 ≤ z

Tactic:
exact h
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
z : ℤ
hz : (normalize : (a : ℤ) → ℤ) z = z
h : z < 0
⊢ -z = z

Tactic:
rw [normalize_of_nonpos h.le] at hz

Premises used: LT.lt.le, Int.normalize_of_nonpos
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
z : ℤ
hz : (normalize : (a : ℤ) → ℤ) z = z
h : z < 0
hz₁ : -z = z
⊢ z < 0

Tactic:
rw [normalize_of_nonpos h.le] at hz

Premises used: LT.lt.le, Int.normalize_of_nonpos
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
z : ℤ
hz : -z = z
h : z < 0
⊢ 0 ≤ z

Tactic:
lia
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
z : ℤ
⊢ (normalize : (a : ℤ) → ℤ) z = z ↔ 0 ≤ z

Tactic:
⟨nonneg_of_normalize_eq_self, normalize_of_nonneg⟩

Premises used: Int.normalize_of_nonneg, Int.nonneg_of_normalize_eq_self, Iff.intro
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℤ
h : Associated a b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a = b

Tactic:
dvd_antisymm_of_normalize_eq (normalize_of_nonneg ha) (normalize_of_nonneg hb) h.dvd h.symm.dvd

Premises used: Associated.dvd, Int.normalize_of_nonneg, dvd_antisymm_of_normalize_eq, Associated.symm
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℤ
rw : Associated ((normalize : (a : ℤ) → ℤ) (a * b)) (a * b)
⊢ Associated (HMul.hMul (α := ℤ) (↑(a.gcd b) : ℤ) (↑(a.lcm b) : ℤ)) (a * b)

Tactic:
rw [← Int.natCast_mul, gcd_mul_lcm, ← natAbs_mul, natCast_natAbs, abs_eq_normalize]

Premises used: Int.natAbs_mul, Int.natCast_mul, Int.gcd_mul_lcm, Int.abs_eq_normalize, Int.natCast_natAbs
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℤ
⊢ Associated ((normalize : (a : ℤ) → ℤ) (a * b)) (a * b)

Tactic:
normalize_associated (a * b)

Premises used: HMul.hMul, normalize_associated
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℤ
⊢ Associated ((normalize : (a : ℤ) → ℤ) (a * b)) (a * b)

Tactic:
exact normalize_associated (a * b)

Premises used: HMul.hMul, normalize_associated
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
i j : ℤ
⊢ (↑(i.gcd j) : ℤ) = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
i j : ℤ
⊢ (↑(i.lcm j) : ℤ) = @GCDMonoid.lcm _ CommSemiring.toCommMonoidWithZero _ i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
i j : ℤ
⊢ (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ i j).natAbs = i.gcd j

Tactic:
rfl

Premises used: Int.gcd, Int.natAbs, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
i j : ℤ
⊢ (@GCDMonoid.lcm _ CommSemiring.toCommMonoidWithZero _ i j).natAbs = i.lcm j

Tactic:
rfl

Premises used: Nat.lcm, Int.lcm, Int.natAbs, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
i j : ℤ
⊢ 0 ≤ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ i j

Tactic:
simp [← coe_gcd]

Premises used: Int.coe_gcd
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
i j : ℤ
⊢ 0 ≤ @GCDMonoid.lcm _ CommSemiring.toCommMonoidWithZero _ i j

Tactic:
simp [← coe_lcm]

Premises used: Int.coe_lcm
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a : ℤ
inl : ∀ (h : a = (↑a.natAbs : ℤ)), ∃ (u : ℤ), ∃ (x : IsUnit u), (↑a.natAbs : ℤ) = u * a
inr : ∀ (h : a = -(↑a.natAbs : ℤ)), ∃ (u : ℤ), ∃ (x : IsUnit u), (↑a.natAbs : ℤ) = u * a
⊢ ∃ (u : ℤ), ∃ (x : IsUnit u), (↑a.natAbs : ℤ) = u * a

Tactic:
rcases natAbs_eq a with h | h

Premises used: Int.natAbs_eq
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a : ℤ
h : a = (↑a.natAbs : ℤ)
h₁ : (↑a.natAbs : ℤ) = 1 * a
⊢ ∃ (u : ℤ), ∃ (x : IsUnit u), (↑a.natAbs : ℤ) = u * a

Tactic:
use 1, isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a : ℤ
h : a = (↑a.natAbs : ℤ)
h₁ : a = 1 * a
h₂ h₃ : a = a
⊢ (↑a.natAbs : ℤ) = 1 * a

Tactic:
rw [← h, one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a : ℤ
h : a = -(↑a.natAbs : ℤ)
h₁ : (↑a.natAbs : ℤ) = -1 * a
⊢ ∃ (u : ℤ), ∃ (x : IsUnit u), (↑a.natAbs : ℤ) = u * a

Tactic:
use -1, isUnit_one.neg

Premises used: isUnit_one, IsUnit.neg
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a : ℤ
h : a = -(↑a.natAbs : ℤ)
h₁ : -a = -1 * a
⊢ (↑a.natAbs : ℤ) = -1 * a

Tactic:
rw [← neg_eq_iff_eq_neg.mpr h]

Premises used: Iff.mpr, neg_eq_iff_eq_neg
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a : ℤ
h : a = -(↑a.natAbs : ℤ)
⊢ -a = -1 * a

Tactic:
simp only [neg_mul, one_mul]

Premises used: neg_mul, one_mul
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℤ
⊢ a.gcd b = a.natAbs.gcd b.natAbs

Tactic:
rfl

Premises used: Int.gcd, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
refine_1 : Function.LeftInverse (fun (x : ℕ) ↦ Associates.mk (↑x : ℤ)) fun (x : Associates ℤ) ↦ x.out.natAbs
refine_2 :
  ∀ (n : ℕ), (fun (x : Associates ℤ) ↦ x.out.natAbs) ((fun (x : ℕ) ↦ (Associates.mk (↑x : ℤ) : Associates ℤ)) n) = n
⊢ Associates ℤ ≃ ℕ

Tactic:
refine ⟨(·.out.natAbs), (Associates.mk ·), ?_, fun n ↦ ?_⟩
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
⊢ Function.LeftInverse (fun (x : ℕ) ↦ Associates.mk (↑x : ℤ)) fun (x : Associates ℤ) ↦ x.out.natAbs

Tactic:
Associates.forall_associated.2 fun a ↦ ?_

Premises used: Iff.mpr, Function.LeftInverse, Associates.forall_associated
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
refine_1 :
  ∀ (a : ℤ),
    Eq (α := Associates ℤ)
      ((fun (x : ℕ) ↦ (Associates.mk (↑x : ℤ) : Associates ℤ))
        ((fun (x : Associates ℤ) ↦ x.out.natAbs) (Associates.mk a)))
      (Associates.mk a)
⊢ Function.LeftInverse (fun (x : ℕ) ↦ Associates.mk (↑x : ℤ)) fun (x : Associates ℤ) ↦ x.out.natAbs

Tactic:
refine Associates.forall_associated.2 fun a ↦ ?_

Premises used: Iff.mpr, Associates.forall_associated
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a : ℤ
⊢ Eq (α := Associates ℤ)
    ((fun (x : ℕ) ↦ (Associates.mk (↑x : ℤ) : Associates ℤ))
      ((fun (x : Associates ℤ) ↦ x.out.natAbs) (Associates.mk a)))
    (Associates.mk a)

Tactic:
Associates.mk_eq_mk_iff_associated.2 <| Associated.symm <| ⟨normUnit a, ?_⟩

Premises used: Iff.mpr, Associates.mk_eq_mk_iff_associated, Associated.symm, Exists.intro, NormalizationMonoid.normUnit
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a : ℤ
refine_1 : a * (↑(normUnit a) : ℤ) = (↑((fun (x : Associates ℤ) ↦ x.out.natAbs) (Associates.mk a)) : ℤ)
⊢ Eq (α := Associates ℤ)
    ((fun (x : ℕ) ↦ (Associates.mk (↑x : ℤ) : Associates ℤ))
      ((fun (x : Associates ℤ) ↦ x.out.natAbs) (Associates.mk a)))
    (Associates.mk a)

Tactic:
refine Associates.mk_eq_mk_iff_associated.2 <| Associated.symm <| ⟨normUnit a, ?_⟩

Premises used: Iff.mpr, Associates.mk_eq_mk_iff_associated, Associated.symm
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a : ℤ
⊢ a * (↑(normUnit a) : ℤ) = (↑((fun (x : Associates ℤ) ↦ x.out.natAbs) (Associates.mk a)) : ℤ)

Tactic:
simp [Int.natCast_natAbs, Int.abs_eq_normalize, normalize_apply]

Premises used: normalize_apply, Int.abs_eq_normalize, Int.natCast_natAbs
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
n : ℕ
refine_2 : Int.natAbs |(↑n : ℤ)| = n
refine_2₁ : Int.natAbs (↑n : ℤ) = n
refine_2₂ refine_2₃ : n = n
⊢ Int.natAbs ((normalize : (a : ℤ) → ℤ) (↑n : ℤ)) = n

Tactic:
rw [← Int.abs_eq_normalize, Int.natAbs_abs, Int.natAbs_natCast]

Premises used: Int.natAbs_abs, Int.abs_eq_normalize, Int.natAbs_natCast
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
k : ℤ
⊢ Associated k (↑k.natAbs : ℤ)

Tactic:
associated_of_dvd_dvd (Int.dvd_natCast.mpr dvd_rfl) (Int.natAbs_dvd.mpr dvd_rfl)

Premises used: Iff.mpr, associated_of_dvd_dvd, Int.dvd_natCast, dvd_rfl, Int.natAbs_dvd
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℤ
rw : Associated a.natAbs b.natAbs ↔ a.natAbs = b.natAbs
⊢ Associated a b ↔ a.natAbs = b.natAbs

Tactic:
rw [← dvd_dvd_iff_associated, ← Int.natAbs_dvd_natAbs, ← Int.natAbs_dvd_natAbs,
    dvd_dvd_iff_associated]

Premises used: Int.natAbs_dvd_natAbs, dvd_dvd_iff_associated
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℤ
⊢ Associated a.natAbs b.natAbs ↔ a.natAbs = b.natAbs

Tactic:
associated_iff_eq

Premises used: associated_iff_eq
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℤ
⊢ Associated a.natAbs b.natAbs ↔ a.natAbs = b.natAbs

Tactic:
exact associated_iff_eq

Premises used: associated_iff_eq
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℤ
rw : a.natAbs = b.natAbs ↔ a = b ∨ a = -b
⊢ Associated a b ↔ a = b ∨ a = -b

Tactic:
rw [Int.associated_iff_natAbs]

Premises used: Int.associated_iff_natAbs
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a = b ∨ a = -b

Tactic:
Int.natAbs_eq_natAbs_iff

Premises used: Int.natAbs_eq_natAbs_iff
-- Module: Mathlib.Algebra.GCDMonoid.Nat
Goal:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a = b ∨ a = -b

Tactic:
exact Int.natAbs_eq_natAbs_iff

Premises used: Int.natAbs_eq_natAbs_iff
-- Module: Mathlib.Algebra.GCDMonoid.PUnit
Goal:
⊢ ∀ {a b : PUnit.{u_1 + 1}}, a ≠ 0 → b ≠ 0 → 1 = HMul.hMul (α := PUnit.{u_1 + 1}ˣ) 1 1

Tactic:
subsingleton
-- Module: Mathlib.Algebra.GCDMonoid.PUnit
Goal:
⊢ ∀ (u : PUnit.{u_1 + 1}ˣ), 1 = u⁻¹

Tactic:
subsingleton
-- Module: Mathlib.Algebra.GCDMonoid.PUnit
Goal:
x x_1 : PUnit.{u_1 + 1}
⊢ x = unit * unit

Tactic:
subsingleton
-- Module: Mathlib.Algebra.GCDMonoid.PUnit
Goal:
x x_1 : PUnit.{u_1 + 1}
⊢ x_1 = unit * unit

Tactic:
subsingleton
-- Module: Mathlib.Algebra.GCDMonoid.PUnit
Goal:
x x_1 x_2 : PUnit.{u_1 + 1}
h : x ∣ x_2
h_1 : x ∣ x_1
⊢ unit = x * unit

Tactic:
subsingleton
-- Module: Mathlib.Algebra.GCDMonoid.PUnit
Goal:
x x_1 : PUnit.{u_1 + 1}
⊢ unit * unit * (↑1 : PUnit.{u_1 + 1}) = x * x_1

Tactic:
subsingleton
-- Module: Mathlib.Algebra.GCDMonoid.PUnit
Goal:
⊢ ∀ (a : PUnit.{u_1 + 1}), unit = 0

Tactic:
subsingleton
-- Module: Mathlib.Algebra.GCDMonoid.PUnit
Goal:
⊢ ∀ (a b : PUnit.{u_1 + 1}), (normalize : (a : PUnit.{u_1 + 1}) → PUnit.{u_1 + 1}) unit = unit

Tactic:
subsingleton
-- Module: Mathlib.Algebra.GCDMonoid.PUnit
Goal:
x y : PUnit.{u_1 + 1}
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ x y = unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GCDMonoid.PUnit
Goal:
x y : PUnit.{u_1 + 1}
⊢ @lcm _ CommSemiring.toCommMonoidWithZero _ x y = unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GCDMonoid.PUnit
Goal:
x : PUnit.{u_1 + 1}
⊢ Eq (α := PUnit.{u_1 + 1}ˣ) (normUnit x) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
α : Type u_3
A : ι → Type u_2
inst : (i : ι) → SMul.{u_3, u_2} α (A i)
a : α
x : GradedMonoid A
⊢ (a • x).fst (β := A) = x.fst (β := A)

Tactic:
rfl

Premises used: GradedMonoid, rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
α : Type u_3
A : ι → Type u_2
inst : (i : ι) → SMul.{u_3, u_2} α (A i)
a : α
x : GradedMonoid A
⊢ (a • x).snd (β := A) = a • x.snd (β := A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
α : Type u_3
A : ι → Type u_2
inst : (i : ι) → SMul.{u_3, u_2} α (A i)
i : ι
c : α
a : A i
⊢ c • mk (A := A) i a = mk (A := A) i (c • a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
A : ι → Type u_2
inst : Zero ι
inst_1 : GOne A
⊢ Eq.{u_1 + 1} (α := ι) (Sigma.fst (β := A) 1) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
A : ι → Type u_2
inst : Zero ι
inst_1 : GOne A
⊢ Eq.{u_2 + 1} (α := A (Sigma.fst (β := A) 1)) (Sigma.snd (β := A) 1) (GOne.one (A := A))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
A : ι → Type u_2
inst : Add ι
inst_1 : GMul A
x y : GradedMonoid A
⊢ (x * y).fst (β := A) = x.fst (β := A) + y.fst (β := A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
A : ι → Type u_2
inst : Add ι
inst_1 : GMul A
x y : GradedMonoid A
⊢ (x * y).snd (β := A) = GMul.mul (A := A) (x.snd (β := A)) (y.snd (β := A))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
A : ι → Type u_2
inst : Add ι
inst_1 : GMul A
i j : ι
a : A i
b : A j
⊢ mk (A := A) i a * mk (A := A) j b = mk (A := A) (i + j) (GMul.mul (A := A) a b)

Tactic:
rfl

Premises used: rfl, GradedMonoid.mk
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
A : ι → Type u_2
inst : AddMonoid ι
inst_1 : GMul A
inst_2 : GOne A
a : GradedMonoid A
⊢ mk (A := A) (HSMul.hSMul (α := ℕ) 0 (a.fst (β := A))) (gnpowRec (A := A) 0 (a.snd (β := A))) = 1

Tactic:
Sigma.ext (zero_nsmul _) (heq_of_cast_eq _ rfl).symm

Premises used: HEq.symm, zero_nsmul, heq_of_cast_eq, GradedMonoid, Sigma.ext, rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
A : ι → Type u_2
inst : AddMonoid ι
inst_1 : GMul A
inst_2 : GOne A
n : ℕ
a : GradedMonoid A
⊢ mk (A := A) (n.succ • a.fst (β := A)) (gnpowRec (A := A) n.succ (a.snd (β := A))) =
    Sigma.mk (β := A) (n • a.fst (β := A)) (gnpowRec (A := A) n (a.snd (β := A))) * a

Tactic:
Sigma.ext (succ_nsmul _ _) (heq_of_cast_eq _ rfl).symm

Premises used: HEq.symm, heq_of_cast_eq, GradedMonoid, Sigma.ext, rfl, succ_nsmul
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
A : ι → Type u_2
inst : AddMonoid ι
inst_1 : GMonoid A
x : GradedMonoid A
n : ℕ
⊢ (x ^ n).fst (β := A) = n • x.fst (β := A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
A : ι → Type u_2
inst : AddMonoid ι
inst_1 : GMonoid A
x : GradedMonoid A
n : ℕ
⊢ (x ^ n).snd (β := A) = GMonoid.gnpow (A := A) n (x.snd (β := A))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
A : ι → Type u_2
inst : AddMonoid ι
inst_1 : GMonoid A
i : ι
a : A i
n : ℕ
⊢ mk (A := A) i a ^ n = mk (A := A) (n • i) (GMonoid.gnpow (A := A) n a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
A : ι → Type u_2
inst : AddZeroClass ι
inst_1 : GMul A
i : ι
a : A 0
b : A i
⊢ mk (A := A) i (a • b) = mk (A := A) 0 a * mk (A := A) i b

Tactic:
Sigma.ext (zero_add _).symm <| eqRec_heq _ _

Premises used: eqRec_heq, zero_add, GradedMonoid, Eq.symm, Sigma.ext
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
A : ι → Type u_2
inst : AddZeroClass ι
inst_1 : GMul A
a b : A 0
⊢ a • b = a * b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
A : ι → Type u_2
inst : AddMonoid ι
inst_1 : GMonoid A
a : A 0
n : ℕ
⊢ mk (A := A) 0 (a ^ n) = mk (A := A) 0 a ^ n

Tactic:
Sigma.ext (nsmul_zero n).symm <| eqRec_heq _ _

Premises used: eqRec_heq, nsmul_zero, GradedMonoid, Eq.symm, Sigma.ext
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
α : Type u_2
inst : AddMonoid ι
fι : α → ι
⊢ dProdIndex [] fι = 0

Tactic:
rfl

Premises used: List.dProdIndex, List.foldr, rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
α : Type u_2
inst : AddMonoid ι
a : α
l : List α
fι : α → ι
⊢ (a :: l).dProdIndex fι = fι a + l.dProdIndex fι

Tactic:
rfl

Premises used: List.dProdIndex, List.foldr, rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
α : Type u_2
inst : AddMonoid ι
l : List α
fι : α → ι
⊢ dProdIndex [] fι = (map fι []).sum

Tactic:
simp
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
α : Type u_2
inst : AddMonoid ι
l : List α
fι : α → ι
head : α
tail : List α
⊢ (head :: tail).dProdIndex fι = (map fι (head :: tail)).sum

Tactic:
simp [List.dProdIndex_eq_map_sum tail fι]
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
α : Type u_2
inst : AddMonoid ι
l : List α
fι : α → ι
⊢ l.dProdIndex fι = (map fι l).sum

Tactic:
match l with
  | [] => simp
  | head::tail => simp [List.dProdIndex_eq_map_sum tail fι]
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst : AddMonoid ι
inst_1 : GradedMonoid.GMonoid A
fι : α → ι
fA : (a : α) → A (fι a)
⊢ Eq (α := A (dProdIndex [] fι)) (dProd (A := A) [] fι fA) (GradedMonoid.GOne.one (A := A))

Tactic:
rfl

Premises used: List.foldrRecOn, List.dProd, rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst : AddMonoid ι
inst_1 : GradedMonoid.GMonoid A
fι : α → ι
fA : (a : α) → A (fι a)
a : α
l : List α
⊢ Eq (α := A ((a :: l).dProdIndex fι)) ((a :: l).dProd (A := A) fι fA)
    (GradedMonoid.GMul.mul (A := A) (fA a) (l.dProd (A := A) fι fA))

Tactic:
rfl

Premises used: List.dProdIndex, List.foldrRecOn, List.dProd, rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst : AddMonoid ι
inst_1 : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
simp : Eq (α := GradedMonoid A) (mk (A := A) 0 (GOne.one (A := A))) 1
⊢ mk (A := A) (List.dProdIndex [] fι) (List.dProd (A := A) [] fι fA) =
    List.prod (List.map (fun (a : α) ↦ mk (A := A) (fι a) (fA a)) [])

Tactic:
simp only [List.dProdIndex_nil, List.dProd_nil, List.map_nil, List.prod_nil]

Premises used: List.dProdIndex_nil, List.dProd_nil, List.prod_nil, List.map_nil
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst : AddMonoid ι
inst_1 : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ Eq (α := GradedMonoid A) (mk (A := A) 0 (GOne.one (A := A))) 1

Tactic:
rfl
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst : AddMonoid ι
inst_1 : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
⊢ mk (A := A) ((head :: tail).dProdIndex fι) ((head :: tail).dProd (A := A) fι fA) =
    List.prod (List.map (fun (a : α) ↦ mk (A := A) (fι a) (fA a)) (head :: tail))

Tactic:
simp [← GradedMonoid.mk_list_dProd tail _ _, GradedMonoid.mk_mul_mk, List.prod_cons]

Premises used: GradedMonoid.mk_mul_mk, List.prod_cons
-- Module: Mathlib.Algebra.GradedMonoid
Goal:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst : AddMonoid ι
inst_1 : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ mk (A := A) (l.dProdIndex fι) (l.dProd (A := A) fι fA) =
    List.prod (List.map (fun (a : α) ↦ mk (A := A) (fι a) (fA a)) l)

Tactic:
match l with
  | [] => simp only [List.dProdIndex_nil, List.dProd_nil, List.map_nil, List.prod_nil]; rfl
  | head::tail =>
    simp [← GradedMonoid.mk_list_dProd tail _ _, GradedMonoid.mk_mul_mk, List.prod_cons]