awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * nb = (↑k : ℤ) * nc
h₂_1 : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
h₁ : HMul.hMul (α := α) (↑na : α) (↑nb : α) = HMul.hMul (α := α) (↑k : α) (↑nc : α)
h₂ :
  HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _) =
    HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) *
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
rw :
  HMul.hMul (α := α) (↑nc : α) (↑k : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ =
    HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) *
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
⊢ HMul.hMul (α := α) (↑k : α) (↑nc : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ =
    HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _)

Tactic:
rw [h₂, Nat.cast_commute]

Premises used: Nat.cast_commute
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁_1 : na * nb = (↑k : ℤ) * nc
h₂_1 : da * db = k * dc
this_1 : Invertible (α := α) (↑(da * db) : α)
this : Invertible (α := α) (↑dc : α)
H :
  ∀ (a : α),
    a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ =
      a * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑db : α) _ *
        @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _
h₁ : HMul.hMul (α := α) (↑na : α) (↑nb : α) = HMul.hMul (α := α) (↑k : α) (↑nc : α)
h₂ :
  HMul.hMul (α := α) (↑nc : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _) =
    HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) *
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _
⊢ HMul.hMul (α := α) (↑nc : α) (↑k : α) * @Invertible.invOf _ MulOne.toMul MulOne.toOne (↑da : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ =
    HMul.hMul (α := α) (↑nc : α) (↑k : α) * (↑dc : α) *
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _ *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _ *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑dc : α) _

Tactic:
simp only [mul_invOf_cancel_right,
    (Nat.cast_commute (α := α) da dc).invOf_left.invOf_right.right_comm,
    (Nat.cast_commute (α := α) db dc).invOf_left.invOf_right.right_comm]

Premises used: Commute.invOf_right, mul_invOf_cancel_right, Nat.cast, Commute.invOf_left, Commute.right_comm, Nat.cast_commute
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
«$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$inst» : Semiring «$α»
«$na» «$nb» : ℕ
⊢ AddMonoidWithOne «$α»

Tactic:
apply AddCommMonoidWithOne.toAddMonoidWithOne

Premises used: AddCommMonoidWithOne.toAddMonoidWithOne
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u
inst : DivisionSemiring α
x x_1 : α
x_2 x_3 : ℕ
h : IsNNRat (x * x_1⁻¹) x_2 x_3
⊢ IsNNRat (x / x_1) x_2 x_3

Tactic:
simpa [div_eq_mul_inv] using h

Premises used: div_eq_mul_inv
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u
inst : DivisionRing α
x x_1 : α
x_2 : ℤ
x_3 : ℕ
h : IsRat (x * x_1⁻¹) x_2 x_3
⊢ IsRat (x / x_1) x_2 x_3

Tactic:
simpa [div_eq_mul_inv] using h

Premises used: div_eq_mul_inv
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
x y : ℕ
rw : x.ble y = false ↔ ¬x ≤ y
rw₁ : ¬x.ble y = true ↔ ¬x ≤ y
rw₂ rw₃ : ¬x ≤ y ↔ ¬x ≤ y
⊢ x.ble y = false ↔ y < x

Tactic:
rw [← Nat.not_le, ← Bool.not_eq_true, Nat.ble_eq]

Premises used: Nat.ble_eq, Bool.not_eq_true, Nat.not_le
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u
inst : Semiring α
num denom : ℕ
inv inv_1 : Invertible (α := α) (↑denom : α)
e_a : inv = inv_1
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _) =
    HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)

Tactic:
congr
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u
inst : Semiring α
num denom : ℕ
inv inv_1 : Invertible (α := α) (↑denom : α)
⊢ inv = inv_1

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u
inst : Ring α
num : ℤ
denom : ℕ
inv inv_1 : Invertible (α := α) (↑denom : α)
e_a : inv = inv_1
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _) =
    HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)

Tactic:
congr
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u
inst : Ring α
num : ℤ
denom : ℕ
inv inv_1 : Invertible (α := α) (↑denom : α)
⊢ inv = inv_1

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
a b : Prop
ha : a
hb : b
⊢ a = b

Tactic:
propext (iff_of_true ha hb)

Premises used: iff_of_true, propext
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
a b : Prop
ha : ¬a
hb : b
⊢ a ≠ b

Tactic:
mt (· ▸ hb) ha

Premises used: mt
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
a b : Prop
ha : a
hb : ¬b
⊢ a ≠ b

Tactic:
mt (· ▸ ha) hb

Premises used: mt
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
a b : Prop
ha : ¬a
hb : ¬b
⊢ a = b

Tactic:
propext (iff_of_false ha hb)

Premises used: iff_of_false, propext
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
n : ℕ
⊢ Nat.succ (↑n : ℕ) = (↑n.succ : ℕ)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
n n_1 : ℕ
⊢ HSub.hSub (α := ℕ) (↑n : ℕ) (↑n_1 : ℕ) = (↑(n.sub n_1) : ℕ)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
n n_1 : ℕ
⊢ HMod.hMod (α := ℕ) (↑n : ℕ) (↑n_1 : ℕ) = (↑(n.mod n_1) : ℕ)

Tactic:
aesop
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
n n_1 : ℕ
⊢ HDiv.hDiv (α := ℕ) (↑n : ℕ) (↑n_1 : ℕ) = (↑(n.div n_1) : ℕ)

Tactic:
aesop
-- Module: Mathlib.Tactic.NormNum.BigOperators
Goal:
n : ℕ
pn : NormNum.IsNat n 0
rw : List.range (↑0 : ℕ) = []
rw₁ : List.range 0 = []
rw₂ rw₃ : Eq (α := List ℕ) [] []
⊢ List.range n = []

Tactic:
rw [pn.out, Nat.cast_zero, List.range_zero]

Premises used: Nat.cast_zero, Mathlib.Meta.NormNum.IsNat.out, List.range_zero
-- Module: Mathlib.Tactic.NormNum.BigOperators
Goal:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
rw : List.range (↑nn : ℕ) = 0 :: List.map Nat.succ (List.range n')
rw₁ : List.range nn = 0 :: List.map Nat.succ (List.range n')
rw₂ : List.range n'.succ = 0 :: List.map Nat.succ (List.range n')
rw₃ rw₄ : 0 :: List.map Nat.succ (List.range n') = 0 :: List.map Nat.succ (List.range n')
⊢ List.range n = 0 :: List.map Nat.succ (List.range n')

Tactic:
rw [pn.out, Nat.cast_id, pn', List.range_succ_eq_map]

Premises used: Nat.cast_id, List.range_succ_eq_map, Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.NormNum.BigOperators
Goal:
α : Type u_1
a : α
s : Multiset α
⊢ insert a s = a ::ₘ s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Tactic.NormNum.BigOperators
Goal:
n : ℕ
pn : NormNum.IsNat n 0
rw : Multiset.range (↑0 : ℕ) = 0
rw₁ : Multiset.range 0 = 0
rw₂ rw₃ : Eq (α := Multiset ℕ) 0 0
⊢ Multiset.range n = 0

Tactic:
rw [pn.out, Nat.cast_zero, Multiset.range_zero]

Premises used: Nat.cast_zero, Mathlib.Meta.NormNum.IsNat.out, Multiset.range_zero
-- Module: Mathlib.Tactic.NormNum.BigOperators
Goal:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
rw : Multiset.range (↑nn : ℕ) = n' ::ₘ Multiset.range n'
rw₁ : Multiset.range nn = n' ::ₘ Multiset.range n'
rw₂ : Multiset.range n'.succ = n' ::ₘ Multiset.range n'
rw₃ rw₄ : n' ::ₘ Multiset.range n' = n' ::ₘ Multiset.range n'
⊢ Multiset.range n = n' ::ₘ Multiset.range n'

Tactic:
rw [pn.out, Nat.cast_id, pn', Multiset.range_succ]

Premises used: Nat.cast_id, Mathlib.Meta.NormNum.IsNat.out, Multiset.range_succ
-- Module: Mathlib.Tactic.NormNum.BigOperators
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ insert a s = Finset.cons a s h

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.BigOperators
Goal:
n : ℕ
pn : NormNum.IsNat n 0
rw : Finset.range (↑0 : ℕ) = ∅
rw₁ : Finset.range 0 = ∅
rw₂ rw₃ : Eq (α := Finset ℕ) ∅ ∅
⊢ Finset.range n = ∅

Tactic:
rw [pn.out, Nat.cast_zero, Finset.range_zero]

Premises used: Nat.cast_zero, Mathlib.Meta.NormNum.IsNat.out, Finset.range_zero
-- Module: Mathlib.Tactic.NormNum.BigOperators
Goal:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
rw : Finset.range (↑nn : ℕ) = Finset.cons n' (Finset.range n') ⋯
rw₁ : Finset.range nn = Finset.cons n' (Finset.range n') ⋯
rw₂ : Finset.range n'.succ = Finset.cons n' (Finset.range n') ⋯
rw₃ : insert n' (Finset.range n') = Finset.cons n' (Finset.range n') ⋯
rw₄ : Finset.cons n' (Finset.range n') ⋯ = Finset.cons n' (Finset.range n') ⋯
h : n' ∉ Finset.range n'
rw₅ : Finset.cons n' (Finset.range n') ⋯ = Finset.cons n' (Finset.range n') ⋯
h₁ : n' ∉ Finset.range n'
⊢ Finset.range n = Finset.cons n' (Finset.range n') ⋯

Tactic:
rw [pn.out, Nat.cast_id, pn', Finset.range_add_one, Finset.insert_eq_cons]

Premises used: Nat.cast_id, Mathlib.Meta.Finset.insert_eq_cons, Finset.range_add_one, Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.NormNum.BigOperators
Goal:
α : Type u_1
inst : Fintype α
elems : Finset α
complete : ∀ (x : α), x ∈ elems
h : ∀ (x : α), Membership.mem (γ := Finset α) Finset.univ x ↔ x ∈ elems
⊢ Finset.univ = elems

Tactic:
ext x
-- Module: Mathlib.Tactic.NormNum.BigOperators
Goal:
α : Type u_1
inst : Fintype α
elems : Finset α
complete : ∀ (x : α), x ∈ elems
x : α
⊢ Membership.mem (γ := Finset α) Finset.univ x ↔ x ∈ elems

Tactic:
simpa using complete x
-- Module: Mathlib.Tactic.NormNum.BigOperators
Goal:
β : Type u_1
α : Type u_2
inst : CommSemiring β
f : α → β
⊢ Finset.sum ∅ f = (↑0 : β)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.BigOperators
Goal:
β : Type u_1
α : Type u_2
inst : CommSemiring β
f : α → β
⊢ Finset.prod ∅ f = (↑1 : β)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
n : ℤ
⊢ HDiv.hDiv (α := ℤ) (↑n : ℤ) (↑0 : ℤ) = (↑0 : ℤ)

Tactic:
simp [Int.ediv_zero]

Premises used: Int.ediv_zero
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
a b q m a' : ℤ
b' r : ℕ
ha : IsInt a a'
hb : IsNat b b'
hm : q * (↑b' : ℤ) = m
h : (↑r : ℤ) + m = a'
h₂ : r.blt b' = true
obtain : ∀ (h : (↑r : ℤ) + m = a), a / (↑b' : ℤ) = (↑q : ℤ)
⊢ a / b = (↑q : ℤ)

Tactic:
obtain ⟨⟨rfl⟩, ⟨rfl⟩⟩ := ha, hb

Premises used: rfl
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h₂ : r.blt b' = true
h : (↑r : ℤ) + m = a
⊢ r < b'

Tactic:
simp only [Nat.blt_eq] at h₂

Premises used: Nat.blt_eq
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h : (↑r : ℤ) + m = a
h₂ : r < b'
simp : ((↑r : ℤ) + q * (↑b' : ℤ)) / (↑b' : ℤ) = q
⊢ a / (↑b' : ℤ) = (↑q : ℤ)

Tactic:
simp only [← h, ← hm, Int.cast_id]

Premises used: Int.cast_id
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h : (↑r : ℤ) + m = a
h₂ : r < b'
rw : HDiv.hDiv (α := ℤ) (↑r : ℤ) (↑b' : ℤ) + q = q
⊢ ((↑r : ℤ) + q * (↑b' : ℤ)) / (↑b' : ℤ) = q

Tactic:
rw [Int.add_mul_ediv_right _ _ (Int.ofNat_ne_zero.2 ((Nat.zero_le ..).trans_lt h₂).ne')]

Premises used: Iff.mpr, Nat.zero_le, Int.ofNat_ne_zero, LT.lt.ne', LE.le.trans_lt, Int.add_mul_ediv_right
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h : (↑r : ℤ) + m = a
h₂ : r < b'
H1 : LE.le (α := ℤ) 0 (↑r : ℤ)
H2 : LT.lt (α := ℤ) (↑r : ℤ) (↑b' : ℤ)
⊢ HDiv.hDiv (α := ℤ) (↑r : ℤ) (↑b' : ℤ) + q = q

Tactic:
rw [Int.ediv_eq_zero_of_lt, zero_add]

Premises used: zero_add, Int.ediv_eq_zero_of_lt
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h : (↑r : ℤ) + m = a
h₂ : r < b'
⊢ LE.le (α := ℤ) 0 (↑r : ℤ)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h : (↑r : ℤ) + m = a
h₂ : r < b'
⊢ LT.lt (α := ℤ) (↑r : ℤ) (↑b' : ℤ)

Tactic:
simpa using h₂
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h : (↑r : ℤ) + m = a
h₂ : r < b'
rw : 0 + q = q
H1 : LE.le (α := ℤ) 0 (↑r : ℤ)
H2 : LT.lt (α := ℤ) (↑r : ℤ) (↑b' : ℤ)
rw₁ : q = q
H1₁ : LE.le (α := ℤ) 0 (↑r : ℤ)
H2₁ : LT.lt (α := ℤ) (↑r : ℤ) (↑b' : ℤ)
rw₂ : q = q
H1₂ : LE.le (α := ℤ) 0 (↑r : ℤ)
H2₂ : LT.lt (α := ℤ) (↑r : ℤ) (↑b' : ℤ)
H1₃ : LE.le (α := ℤ) 0 (↑r : ℤ)
H2₃ : LT.lt (α := ℤ) (↑r : ℤ) (↑b' : ℤ)
H1₄ : LE.le (α := ℤ) 0 (↑r : ℤ)
H2₄ : LT.lt (α := ℤ) (↑r : ℤ) (↑b' : ℤ)
⊢ HDiv.hDiv (α := ℤ) (↑r : ℤ) (↑b' : ℤ) + q = q

Tactic:
rw [Int.ediv_eq_zero_of_lt, zero_add] <;> [simp; simpa using h₂]

Premises used: zero_add, Int.ediv_eq_zero_of_lt
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
a b q q' : ℤ
h : IsInt (a / -b) q
hq : -q = q'
rw : a / b = q'
rw₁ : a / b = -q
rw₂ : a / b = -(↑q : ℤ)
rw₃ : a / b = -(a / -b)
rw₄ : a / b = a / - -b
rw₅ rw₆ : a / b = a / b
⊢ a / b = (↑q' : ℤ)

Tactic:
rw [Int.cast_id, ← hq, ← @Int.cast_id q, ← h.out, ← Int.ediv_neg, Int.neg_neg]

Premises used: Int.ediv_neg, Int.cast_id, Int.neg_neg, Mathlib.Meta.NormNum.IsInt.out
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
a : ℤ
b : ℕ
h : IsInt a (Int.negOfNat b)
⊢ -a = (↑b : ℤ)

Tactic:
simp [h.out]

Premises used: Mathlib.Meta.NormNum.IsInt.out
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
x x_1 : ℤ
e : IsInt x x_1
⊢ IsInt (x % (↑0 : ℤ)) x_1

Tactic:
simp [e]
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
a b q m a' : ℤ
b' r : ℕ
ha : IsInt a a'
hb : IsNat b b'
hm : q * (↑b' : ℤ) = m
h : (↑r : ℤ) + m = a'
h₂ : r.blt b' = true
obtain : ∀ (h : (↑r : ℤ) + m = a), a % (↑b' : ℤ) = (↑r : ℤ)
⊢ a % b = (↑r : ℤ)

Tactic:
obtain ⟨⟨rfl⟩, ⟨rfl⟩⟩ := ha, hb

Premises used: rfl
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h₂ : r.blt b' = true
h : (↑r : ℤ) + m = a
simp : HMod.hMod (α := ℤ) (↑r : ℤ) (↑b' : ℤ) = (↑r : ℤ)
⊢ a % (↑b' : ℤ) = (↑r : ℤ)

Tactic:
simp only [← h, ← hm, Int.add_mul_emod_self_right]

Premises used: Int.add_mul_emod_self_right
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h₂ : r.blt b' = true
h : (↑r : ℤ) + m = a
H1 : LE.le (α := ℤ) 0 (↑r : ℤ)
H2 : LT.lt (α := ℤ) (↑r : ℤ) (↑b' : ℤ)
⊢ HMod.hMod (α := ℤ) (↑r : ℤ) (↑b' : ℤ) = (↑r : ℤ)

Tactic:
rw [Int.emod_eq_of_lt]

Premises used: Int.emod_eq_of_lt
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h₂ : r.blt b' = true
h : (↑r : ℤ) + m = a
⊢ LE.le (α := ℤ) 0 (↑r : ℤ)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h₂ : r.blt b' = true
h : (↑r : ℤ) + m = a
⊢ LT.lt (α := ℤ) (↑r : ℤ) (↑b' : ℤ)

Tactic:
simpa using h₂
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h₂ : r.blt b' = true
h : (↑r : ℤ) + m = a
rw : Eq (α := ℤ) (↑r : ℤ) (↑r : ℤ)
H1 : LE.le (α := ℤ) 0 (↑r : ℤ)
H2 : LT.lt (α := ℤ) (↑r : ℤ) (↑b' : ℤ)
rw₁ : Eq (α := ℤ) (↑r : ℤ) (↑r : ℤ)
H1₁ : LE.le (α := ℤ) 0 (↑r : ℤ)
H2₁ : LT.lt (α := ℤ) (↑r : ℤ) (↑b' : ℤ)
H1₂ : LE.le (α := ℤ) 0 (↑r : ℤ)
H2₂ : LT.lt (α := ℤ) (↑r : ℤ) (↑b' : ℤ)
H1₃ : LE.le (α := ℤ) 0 (↑r : ℤ)
H2₃ : LT.lt (α := ℤ) (↑r : ℤ) (↑b' : ℤ)
⊢ HMod.hMod (α := ℤ) (↑r : ℤ) (↑b' : ℤ) = (↑r : ℤ)

Tactic:
rw [Int.emod_eq_of_lt] <;> [simp; simpa using h₂]

Premises used: Int.emod_eq_of_lt
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
a b : ℤ
r : ℕ
h : IsNat (a % -b) r
rw : a % -b = (↑r : ℤ)
rw₁ rw₂ : Eq (α := ℤ) (↑r : ℤ) (↑r : ℤ)
⊢ a % b = (↑r : ℤ)

Tactic:
rw [← Int.emod_neg, h.out]

Premises used: Int.emod_neg, Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.NormNum.DivMod
Goal:
n n_1 : ℤ
e : (n_1.emod n != 0) = true
⊢ ¬HMod.hMod (α := ℤ) (↑n_1 : ℤ) (↑n : ℤ) = 0

Tactic:
simpa using e
-- Module: Mathlib.Tactic.NormNum.Eq
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : CharZero α
n n_1 : ℕ
h : n.beq n_1 = false
⊢ ¬Eq.{u_1 + 1} (α := α) (↑n : α) (↑n_1 : α)

Tactic:
simpa using Nat.ne_of_beq_eq_false h

Premises used: Nat.ne_of_beq_eq_false
-- Module: Mathlib.Tactic.NormNum.Eq
Goal:
α : Type u_1
inst : Ring α
inst_1 : CharZero α
n n_1 : ℤ
h : decide (n = n_1) = false
⊢ ¬Eq.{u_1 + 1} (α := α) (↑n : α) (↑n_1 : α)

Tactic:
simpa using of_decide_eq_false h

Premises used: of_decide_eq_false
-- Module: Mathlib.Tactic.NormNum.Eq
Goal:
α : Type u_1
inst : Semiring α
n₁ n₂ : ℕ
a₁ a₂ : α
inst_1 : Invertible a₁
inst_2 : Invertible a₂
rw :
  (↑n₁ : α) = (↑n₂ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ * a₁ ↔
    (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
rw₁ :
  (↑n₁ : α) = @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ * (↑n₂ : α) * a₁ ↔
    (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
rw₂ :
  (↑n₁ : α) = @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ * ((↑n₂ : α) * a₁) ↔
    (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
rw₃ : a₂ * (↑n₁ : α) = (↑n₂ : α) * a₁ ↔ (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
rw₄ rw₅ : (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁ ↔ (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
⊢ (↑n₁ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₁ _ =
      (↑n₂ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ ↔
    (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁

Tactic:
rw [mul_invOf_eq_iff_eq_mul_right, ← Nat.commute_cast, mul_assoc,
    ← mul_left_eq_iff_eq_invOf_mul, Nat.commute_cast]

Premises used: Nat.commute_cast, mul_left_eq_iff_eq_invOf_mul, mul_assoc, mul_invOf_eq_iff_eq_mul_right
-- Module: Mathlib.Tactic.NormNum.Eq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : CharZero α
num num_1 denom denom_1 : ℕ
inv : Invertible (α := α) (↑denom : α)
inv_1 : Invertible (α := α) (↑denom_1 : α)
h : decide (num.mul denom_1 = num_1.mul denom) = false
rw : ¬HMul.hMul (α := α) (↑num : α) (↑denom_1 : α) = HMul.hMul (α := α) (↑num_1 : α) (↑denom : α)
⊢ ¬HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _) =
      HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom_1 : α) _)

Tactic:
rw [NNRat.invOf_denom_swap]

Premises used: Mathlib.Meta.NormNum.NNRat.invOf_denom_swap
-- Module: Mathlib.Tactic.NormNum.Eq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : CharZero α
num num_1 denom denom_1 : ℕ
inv : Invertible (α := α) (↑denom : α)
inv_1 : Invertible (α := α) (↑denom_1 : α)
h : decide (num.mul denom_1 = num_1.mul denom) = false
⊢ ¬HMul.hMul (α := α) (↑num : α) (↑denom_1 : α) = HMul.hMul (α := α) (↑num_1 : α) (↑denom : α)

Tactic:
mod_cast of_decide_eq_false h

Premises used: Nat.cast_mul._simp_1, congrArg, cast, congr, Nat.cast_inj._simp_1, Eq.symm, Eq, Not, Eq.trans, of_decide_eq_false
-- Module: Mathlib.Tactic.NormNum.Eq
Goal:
α : Type u_1
inst : Semiring α
inst_1 : CharZero α
num num_1 denom denom_1 : ℕ
inv : Invertible (α := α) (↑denom : α)
inv_1 : Invertible (α := α) (↑denom_1 : α)
h : decide (num.mul denom_1 = num_1.mul denom) = false
⊢ ¬HMul.hMul (α := α) (↑num : α) (↑denom_1 : α) = HMul.hMul (α := α) (↑num_1 : α) (↑denom : α)

Tactic:
exact mod_cast of_decide_eq_false h

Premises used: of_decide_eq_false
-- Module: Mathlib.Tactic.NormNum.Eq
Goal:
α : Type u_1
inst : Ring α
n₁ n₂ : ℤ
a₁ a₂ : α
inst_1 : Invertible a₁
inst_2 : Invertible a₂
rw :
  (↑n₁ : α) = (↑n₂ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ * a₁ ↔
    (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
rw₁ :
  (↑n₁ : α) = @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ * (↑n₂ : α) * a₁ ↔
    (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
rw₂ :
  (↑n₁ : α) = @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ * ((↑n₂ : α) * a₁) ↔
    (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
rw₃ : a₂ * (↑n₁ : α) = (↑n₂ : α) * a₁ ↔ (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
rw₄ rw₅ : (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁ ↔ (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
⊢ (↑n₁ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₁ _ =
      (↑n₂ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ ↔
    (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁

Tactic:
rw [mul_invOf_eq_iff_eq_mul_right, ← Int.commute_cast, mul_assoc,
    ← mul_left_eq_iff_eq_invOf_mul, Int.commute_cast]

Premises used: mul_left_eq_iff_eq_invOf_mul, mul_assoc, Int.commute_cast, mul_invOf_eq_iff_eq_mul_right
-- Module: Mathlib.Tactic.NormNum.Eq
Goal:
α : Type u_1
inst : Ring α
inst_1 : CharZero α
num num_1 : ℤ
denom denom_1 : ℕ
inv : Invertible (α := α) (↑denom : α)
inv_1 : Invertible (α := α) (↑denom_1 : α)
h : decide (num.mul (Int.ofNat denom_1) = num_1.mul (Int.ofNat denom)) = false
rw : ¬HMul.hMul (α := α) (↑num : α) (↑denom_1 : α) = HMul.hMul (α := α) (↑num_1 : α) (↑denom : α)
⊢ ¬HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _) =
      HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom_1 : α) _)

Tactic:
rw [Rat.invOf_denom_swap]

Premises used: Mathlib.Meta.NormNum.Rat.invOf_denom_swap
-- Module: Mathlib.Tactic.NormNum.Eq
Goal:
α : Type u_1
inst : Ring α
inst_1 : CharZero α
num num_1 : ℤ
denom denom_1 : ℕ
inv : Invertible (α := α) (↑denom : α)
inv_1 : Invertible (α := α) (↑denom_1 : α)
h : decide (num.mul (Int.ofNat denom_1) = num_1.mul (Int.ofNat denom)) = false
⊢ ¬HMul.hMul (α := α) (↑num : α) (↑denom_1 : α) = HMul.hMul (α := α) (↑num_1 : α) (↑denom : α)

Tactic:
mod_cast of_decide_eq_false h

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, cast, Nat.cast, Int.cast_inj._simp_1, Int.cast_mul._simp_1, congr, Eq.symm, Eq, Not, Eq.trans, of_decide_eq_false
-- Module: Mathlib.Tactic.NormNum.Eq
Goal:
α : Type u_1
inst : Ring α
inst_1 : CharZero α
num num_1 : ℤ
denom denom_1 : ℕ
inv : Invertible (α := α) (↑denom : α)
inv_1 : Invertible (α := α) (↑denom_1 : α)
h : decide (num.mul (Int.ofNat denom_1) = num_1.mul (Int.ofNat denom)) = false
⊢ ¬HMul.hMul (α := α) (↑num : α) (↑denom_1 : α) = HMul.hMul (α := α) (↑num_1 : α) (↑denom : α)

Tactic:
exact mod_cast of_decide_eq_false h

Premises used: of_decide_eq_false
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
d : ℕ
x y a b : ℤ
h₁ : (↑d : ℤ) ∣ x
h₂ : (↑d : ℤ) ∣ y
h₃ : x * a + y * b = (↑d : ℤ)
⊢ x.gcd y = d

Tactic:
Nat.dvd_antisymm ?_ (Int.natCast_dvd_natCast.1 (Int.dvd_coe_gcd h₁ h₂))

Premises used: Int.dvd_coe_gcd, Iff.mp, Nat.dvd_antisymm, Int.natCast_dvd_natCast
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
d : ℕ
x y a b : ℤ
h₁ : (↑d : ℤ) ∣ x
h₂ : (↑d : ℤ) ∣ y
h₃ : x * a + y * b = (↑d : ℤ)
refine : x.gcd y ∣ d
⊢ x.gcd y = d

Tactic:
refine Nat.dvd_antisymm ?_ (Int.natCast_dvd_natCast.1 (Int.dvd_coe_gcd h₁ h₂))

Premises used: Int.dvd_coe_gcd, Iff.mp, Nat.dvd_antisymm, Int.natCast_dvd_natCast
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
d : ℕ
x y a b : ℤ
h₁ : (↑d : ℤ) ∣ x
h₂ : (↑d : ℤ) ∣ y
h₃ : x * a + y * b = (↑d : ℤ)
rw : (↑(x.gcd y) : ℤ) ∣ x * a + y * b
⊢ x.gcd y ∣ d

Tactic:
rw [← Int.natCast_dvd_natCast, ← h₃]

Premises used: Int.natCast_dvd_natCast
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
d : ℕ
x y a b : ℤ
h₁ : (↑d : ℤ) ∣ x
h₂ : (↑d : ℤ) ∣ y
h₃ : x * a + y * b = (↑d : ℤ)
h₄ : (↑(x.gcd y) : ℤ) ∣ x * a
h₅ : (↑(x.gcd y) : ℤ) ∣ y * b
⊢ (↑(x.gcd y) : ℤ) ∣ x * a + y * b

Tactic:
apply dvd_add

Premises used: dvd_add
-- Module: Mathlib.Tactic.NormNum.GCD
Goal:
d : ℕ
x y a b : ℤ
h₁ : (↑d : ℤ) ∣ x
h₂ : (↑d : ℤ) ∣ y
h₃ : x * a + y * b = (↑d : ℤ)
⊢ (↑(x.gcd y) : ℤ) ∣ x * a

Tactic:
(Int.gcd_dvd_left ..).mul_right _

Premises used: Dvd.dvd.mul_right, Int.gcd_dvd_left