awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
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') ⋯
⊢ Finset.range n = Finset.cons n' (Finset.range n') ⋯
have h : n' ∉ Finset.range n'
Tactic: rw [pn.out, Nat.cast_id, pn', Finset.range_add_one, Finset.insert_eq_cons]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.BigOperators (goal)
Goal:
α : Type u_1
inst : Fintype α
elems : Finset α
complete : ∀ (x : α), x ∈ elems
⊢ Finset.univ = elems
have h : ∀ (x : α), Membership.mem (γ := Finset α) Finset.univ x ↔ x ∈ elems
Tactic: ext x
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
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
⊢ a / b = (↑q : ℤ)
have obtain : ∀ (h : (↑r : ℤ) + m = a), a / (↑b' : ℤ) = (↑q : ℤ)
Tactic: obtain ⟨⟨rfl⟩, ⟨rfl⟩⟩ := ha, hb
Cleared hypotheses: b, a', ha, hb, h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (hypothesis)
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h₂ : r.blt b' = true
h : (↑r : ℤ) + m = a
⊢ a / (↑b' : ℤ) = (↑q : ℤ)
have h₃ : r < b'
Tactic: simp only [Nat.blt_eq] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h : (↑r : ℤ) + m = a
h₂ : r < b'
⊢ a / (↑b' : ℤ) = (↑q : ℤ)
have simp : ((↑r : ℤ) + q * (↑b' : ℤ)) / (↑b' : ℤ) = q
Tactic: simp only [← h, ← hm, Int.cast_id]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h : (↑r : ℤ) + m = a
h₂ : r < b'
⊢ ((↑r : ℤ) + q * (↑b' : ℤ)) / (↑b' : ℤ) = q
have rw : HDiv.hDiv (α := ℤ) (↑r : ℤ) (↑b' : ℤ) + q = q
Tactic: rw [Int.add_mul_ediv_right _ _ (Int.ofNat_ne_zero.2 ((Nat.zero_le ..).trans_lt h₂).ne')]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h : (↑r : ℤ) + m = a
h₂ : r < b'
⊢ HDiv.hDiv (α := ℤ) (↑r : ℤ) (↑b' : ℤ) + q = q
have H1 : LE.le (α := ℤ) 0 (↑r : ℤ)
Tactic: rw [Int.ediv_eq_zero_of_lt, zero_add]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h : (↑r : ℤ) + m = a
h₂ : r < b'
H1 : LE.le (α := ℤ) 0 (↑r : ℤ)
⊢ HDiv.hDiv (α := ℤ) (↑r : ℤ) (↑b' : ℤ) + q = q
have H2 : LT.lt (α := ℤ) (↑r : ℤ) (↑b' : ℤ)
Tactic: rw [Int.ediv_eq_zero_of_lt, zero_add]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h : (↑r : ℤ) + m = a
h₂ : r < b'
⊢ HDiv.hDiv (α := ℤ) (↑r : ℤ) (↑b' : ℤ) + q = q
have rw : 0 + q = q
Tactic: rw [Int.ediv_eq_zero_of_lt, zero_add] <;> [simp; simpa using h₂]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h : (↑r : ℤ) + m = a
h₂ : r < b'
rw : 0 + q = q
⊢ HDiv.hDiv (α := ℤ) (↑r : ℤ) (↑b' : ℤ) + q = q
have H1 : LE.le (α := ℤ) 0 (↑r : ℤ)
Tactic: rw [Int.ediv_eq_zero_of_lt, zero_add] <;> [simp; simpa using h₂]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
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 : ℤ)
⊢ HDiv.hDiv (α := ℤ) (↑r : ℤ) (↑b' : ℤ) + q = q
have H2 : LT.lt (α := ℤ) (↑r : ℤ) (↑b' : ℤ)
Tactic: rw [Int.ediv_eq_zero_of_lt, zero_add] <;> [simp; simpa using h₂]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
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' : ℤ)
⊢ HDiv.hDiv (α := ℤ) (↑r : ℤ) (↑b' : ℤ) + q = q
have rw₁ : q = q
Tactic: rw [Int.ediv_eq_zero_of_lt, zero_add] <;> [simp; simpa using h₂]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
Goal:
a b q q' : ℤ
h : IsInt (a / -b) q
hq : -q = q'
⊢ a / b = (↑q' : ℤ)
have rw : a / b = q'
Tactic: rw [Int.cast_id, ← hq, ← @Int.cast_id q, ← h.out, ← Int.ediv_neg, Int.neg_neg]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
Goal:
a b q q' : ℤ
h : IsInt (a / -b) q
hq : -q = q'
rw : a / b = q'
⊢ a / b = (↑q' : ℤ)
have rw₁ : a / b = -q
Tactic: rw [Int.cast_id, ← hq, ← @Int.cast_id q, ← h.out, ← Int.ediv_neg, Int.neg_neg]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
Goal:
a b q q' : ℤ
h : IsInt (a / -b) q
hq : -q = q'
rw : a / b = q'
rw₁ : a / b = -q
⊢ a / b = (↑q' : ℤ)
have rw₂ : a / b = -(↑q : ℤ)
Tactic: rw [Int.cast_id, ← hq, ← @Int.cast_id q, ← h.out, ← Int.ediv_neg, Int.neg_neg]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
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 : ℤ)
⊢ a / b = (↑q' : ℤ)
have rw₃ : a / b = -(a / -b)
Tactic: rw [Int.cast_id, ← hq, ← @Int.cast_id q, ← h.out, ← Int.ediv_neg, Int.neg_neg]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
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)
⊢ a / b = (↑q' : ℤ)
have rw₄ : a / b = a / - -b
Tactic: rw [Int.cast_id, ← hq, ← @Int.cast_id q, ← h.out, ← Int.ediv_neg, Int.neg_neg]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
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
⊢ a / b = (↑q' : ℤ)
have rw₅ : a / b = a / b
Tactic: rw [Int.cast_id, ← hq, ← @Int.cast_id q, ← h.out, ← Int.ediv_neg, Int.neg_neg]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
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
⊢ a % b = (↑r : ℤ)
have obtain : ∀ (h : (↑r : ℤ) + m = a), a % (↑b' : ℤ) = (↑r : ℤ)
Tactic: obtain ⟨⟨rfl⟩, ⟨rfl⟩⟩ := ha, hb
Cleared hypotheses: b, a', ha, hb, h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h₂ : r.blt b' = true
h : (↑r : ℤ) + m = a
⊢ a % (↑b' : ℤ) = (↑r : ℤ)
have simp : HMod.hMod (α := ℤ) (↑r : ℤ) (↑b' : ℤ) = (↑r : ℤ)
Tactic: simp only [← h, ← hm, Int.add_mul_emod_self_right]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h₂ : r.blt b' = true
h : (↑r : ℤ) + m = a
⊢ HMod.hMod (α := ℤ) (↑r : ℤ) (↑b' : ℤ) = (↑r : ℤ)
have H1 : LE.le (α := ℤ) 0 (↑r : ℤ)
Tactic: rw [Int.emod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h₂ : r.blt b' = true
h : (↑r : ℤ) + m = a
H1 : LE.le (α := ℤ) 0 (↑r : ℤ)
⊢ HMod.hMod (α := ℤ) (↑r : ℤ) (↑b' : ℤ) = (↑r : ℤ)
have H2 : LT.lt (α := ℤ) (↑r : ℤ) (↑b' : ℤ)
Tactic: rw [Int.emod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h₂ : r.blt b' = true
h : (↑r : ℤ) + m = a
⊢ HMod.hMod (α := ℤ) (↑r : ℤ) (↑b' : ℤ) = (↑r : ℤ)
have rw : Eq (α := ℤ) (↑r : ℤ) (↑r : ℤ)
Tactic: rw [Int.emod_eq_of_lt] <;> [simp; simpa using h₂]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
Goal:
a q m : ℤ
b' r : ℕ
hm : q * (↑b' : ℤ) = m
h₂ : r.blt b' = true
h : (↑r : ℤ) + m = a
rw : Eq (α := ℤ) (↑r : ℤ) (↑r : ℤ)
⊢ HMod.hMod (α := ℤ) (↑r : ℤ) (↑b' : ℤ) = (↑r : ℤ)
have H1 : LE.le (α := ℤ) 0 (↑r : ℤ)
Tactic: rw [Int.emod_eq_of_lt] <;> [simp; simpa using h₂]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
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 : ℤ)
⊢ HMod.hMod (α := ℤ) (↑r : ℤ) (↑b' : ℤ) = (↑r : ℤ)
have H2 : LT.lt (α := ℤ) (↑r : ℤ) (↑b' : ℤ)
Tactic: rw [Int.emod_eq_of_lt] <;> [simp; simpa using h₂]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
Goal:
a b : ℤ
r : ℕ
h : IsNat (a % -b) r
⊢ a % b = (↑r : ℤ)
have rw : a % -b = (↑r : ℤ)
Tactic: rw [← Int.emod_neg, h.out]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.DivMod (goal)
Goal:
a b : ℤ
r : ℕ
h : IsNat (a % -b) r
rw : a % -b = (↑r : ℤ)
⊢ a % b = (↑r : ℤ)
have rw₁ : Eq (α := ℤ) (↑r : ℤ) (↑r : ℤ)
Tactic: rw [← Int.emod_neg, h.out]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Eq (goal)
Goal:
α : Type u_1
inst : Semiring α
n₁ n₂ : ℕ
a₁ a₂ : α
inst_1 : Invertible a₁
inst_2 : Invertible a₂
⊢ (↑n₁ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₁ _ =
      (↑n₂ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ ↔
    (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
have rw : (↑n₁ : α) = (↑n₂ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ * 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Eq (goal)
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₁
⊢ (↑n₁ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₁ _ =
      (↑n₂ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ ↔
    (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
have rw₁ : (↑n₁ : α) = @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ * (↑n₂ : α) * 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Eq (goal)
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₁
⊢ (↑n₁ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₁ _ =
      (↑n₂ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ ↔
    (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
have rw₂ : (↑n₁ : α) = @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ * ((↑n₂ : α) * 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Eq (goal)
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₁
⊢ (↑n₁ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₁ _ =
      (↑n₂ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ ↔
    (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
have rw₃ : a₂ * (↑n₁ : α) = (↑n₂ : α) * 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Eq (goal)
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₁
⊢ (↑n₁ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₁ _ =
      (↑n₂ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ ↔
    (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
have rw₄ : (↑n₁ : α) * a₂ = (↑n₂ : α) * 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Eq (goal)
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 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _) =
      HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom_1 : α) _)
have rw : ¬HMul.hMul (α := α) (↑num : α) (↑denom_1 : α) = HMul.hMul (α := α) (↑num_1 : α) (↑denom : α)
Tactic: rw [NNRat.invOf_denom_swap]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Eq (goal)
Goal:
α : Type u_1
inst : Ring α
n₁ n₂ : ℤ
a₁ a₂ : α
inst_1 : Invertible a₁
inst_2 : Invertible a₂
⊢ (↑n₁ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₁ _ =
      (↑n₂ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ ↔
    (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
have rw : (↑n₁ : α) = (↑n₂ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ * 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Eq (goal)
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₁
⊢ (↑n₁ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₁ _ =
      (↑n₂ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ ↔
    (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
have rw₁ : (↑n₁ : α) = @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ * (↑n₂ : α) * 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Eq (goal)
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₁
⊢ (↑n₁ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₁ _ =
      (↑n₂ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ ↔
    (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
have rw₂ : (↑n₁ : α) = @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ * ((↑n₂ : α) * 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Eq (goal)
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₁
⊢ (↑n₁ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₁ _ =
      (↑n₂ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ ↔
    (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
have rw₃ : a₂ * (↑n₁ : α) = (↑n₂ : α) * 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Eq (goal)
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₁
⊢ (↑n₁ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₁ _ =
      (↑n₂ : α) * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a₂ _ ↔
    (↑n₁ : α) * a₂ = (↑n₂ : α) * a₁
have rw₄ : (↑n₁ : α) * a₂ = (↑n₂ : α) * 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Eq (goal)
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 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _) =
      HMul.hMul (α := α) (↑num_1 : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom_1 : α) _)
have rw : ¬HMul.hMul (α := α) (↑num : α) (↑denom_1 : α) = HMul.hMul (α := α) (↑num_1 : α) (↑denom : α)
Tactic: rw [Rat.invOf_denom_swap]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
Goal:
d : ℕ
x y a b : ℤ
h₁ : (↑d : ℤ) ∣ x
h₂ : (↑d : ℤ) ∣ y
h₃ : x * a + y * b = (↑d : ℤ)
⊢ x.gcd y = d
have refine : x.gcd y ∣ d
Tactic: refine Nat.dvd_antisymm ?_ (Int.natCast_dvd_natCast.1 (Int.dvd_coe_gcd h₁ h₂))
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
Goal:
d : ℕ
x y a b : ℤ
h₁ : (↑d : ℤ) ∣ x
h₂ : (↑d : ℤ) ∣ y
h₃ : x * a + y * b = (↑d : ℤ)
⊢ x.gcd y ∣ d
have rw : (↑(x.gcd y) : ℤ) ∣ x * a + y * b
Tactic: rw [← Int.natCast_dvd_natCast, ← h₃]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
Goal:
d : ℕ
x y a b : ℤ
h₁ : (↑d : ℤ) ∣ x
h₂ : (↑d : ℤ) ∣ y
h₃ : x * a + y * b = (↑d : ℤ)
⊢ (↑(x.gcd y) : ℤ) ∣ x * a + y * b
have h₄ : (↑(x.gcd y) : ℤ) ∣ x * a
Tactic: apply dvd_add
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
Goal:
d : ℕ
x y a b : ℤ
h₁ : (↑d : ℤ) ∣ x
h₂ : (↑d : ℤ) ∣ y
h₃ : x * a + y * b = (↑d : ℤ)
h₄ : (↑(x.gcd y) : ℤ) ∣ x * a
⊢ (↑(x.gcd y) : ℤ) ∣ x * a + y * b
have h₅ : (↑(x.gcd y) : ℤ) ∣ y * b
Tactic: apply dvd_add
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
Goal:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ x.gcd y = d
have rw : Int.gcd (↑x : ℤ) (↑y : ℤ) = d
Tactic: rw [← Int.gcd_natCast_natCast]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
Goal:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ Int.gcd (↑x : ℤ) (↑y : ℤ) = d
have apply : HMul.hMul (α := ℤ) (↑x : ℤ) (↑a : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (-(↑b : ℤ)) = (↑d : ℤ)
Tactic: apply int_gcd_helper' a (-b)
    (Int.natCast_dvd_natCast.mpr (Nat.dvd_of_mod_eq_zero hu))
    (Int.natCast_dvd_natCast.mpr (Nat.dvd_of_mod_eq_zero hv))
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
Goal:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ HMul.hMul (α := ℤ) (↑x : ℤ) (↑a : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (-(↑b : ℤ)) = (↑d : ℤ)
have rw : HMul.hMul (α := ℤ) (↑x : ℤ) (↑a : ℤ) = HMul.hMul (α := ℤ) (↑y : ℤ) (↑b : ℤ) + (↑d : ℤ)
Tactic: rw [mul_neg, ← sub_eq_add_neg, sub_eq_iff_eq_add']
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
Goal:
x y d m : ℕ
hd : x.gcd y = d
d0 : d.beq 0 = false
dm : x * y = d * m
⊢ d * x.lcm y = d * m
have rw : d * x.lcm y = x * y
Tactic: rw [← dm, ← hd, Nat.gcd_mul_lcm]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
Goal:
x y d m : ℕ
hd : x.gcd y = d
d0 : d.beq 0 = false
dm : x * y = d * m
rw : d * x.lcm y = x * y
⊢ d * x.lcm y = d * m
have rw₁ : x.gcd y * x.lcm y = x * y
Tactic: rw [← dm, ← hd, Nat.gcd_mul_lcm]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
Goal:
x y d m : ℕ
hd : x.gcd y = d
d0 : d.beq 0 = false
dm : x * y = d * m
rw : d * x.lcm y = x * y
rw₁ : x.gcd y * x.lcm y = x * y
⊢ d * x.lcm y = d * m
have rw₂ : x * y = x * y
Tactic: rw [← dm, ← hd, Nat.gcd_mul_lcm]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
Goal:
x y : ℤ
x' y' d : ℕ
hx : x.natAbs = x'
hy : y.natAbs = y'
h : x'.gcd y' = d
⊢ x.gcd y = d
have subst_vars : x.gcd y = x.natAbs.gcd y.natAbs
Tactic: subst_vars
Cleared hypotheses: x', y', d, hx, hy, h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
Goal:
x y : ℤ
⊢ x.gcd y = x.natAbs.gcd y.natAbs
have rw : x.natAbs.gcd y.natAbs = x.natAbs.gcd y.natAbs
Tactic: rw [Int.gcd_def]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
Goal:
x y : ℤ
x' y' d : ℕ
hx : x.natAbs = x'
hy : y.natAbs = y'
h : x'.lcm y' = d
⊢ x.lcm y = d
have subst_vars : x.lcm y = x.natAbs.lcm y.natAbs
Tactic: subst_vars
Cleared hypotheses: x', y', d, hx, hy, h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
Goal:
x y : ℤ
⊢ x.lcm y = x.natAbs.lcm y.natAbs
have rw : x.natAbs.lcm y.natAbs = x.natAbs.lcm y.natAbs
Tactic: rw [Int.lcm_def]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
Goal:
n : ℤ
d : ℕ
hi : Invertible (α := ℚ) (↑d : ℚ)
h : n.natAbs.gcd d = 1
⊢ IsInt (HMul.hMul (α := ℚ) (↑n : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).num n
have out : (HMul.hMul (α := ℚ) (↑n : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).num = (↑n : ℤ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (hypothesis)
Goal:
n : ℤ
d : ℕ
hi : Invertible (α := ℚ) (↑d : ℚ)
h : n.natAbs.gcd d = 1
⊢ (HMul.hMul (α := ℚ) (↑n : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).num = (↑n : ℤ)
have this : 0 < d
Tactic: have : 0 < d := Nat.pos_iff_ne_zero.mpr <| by simpa using hi.ne_zero
-- Lean 4 proof step from Mathlib.Tactic.NormNum.GCD (goal)
Goal:
n : ℤ
d : ℕ
hi : Invertible (α := ℚ) (↑d : ℚ)
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ (HMul.hMul (α := ℚ) (↑n : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).num = (↑n : ℤ)
have out : Rat.num (↑n : ℚ) * Rat.num (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _) /
    (↑((Rat.num (↑n : ℚ) * Rat.num (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _)).natAbs.gcd
          (Rat.den (↑n : ℚ) * Rat.den (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℚ) _))) :
      ℤ) =
  (↑n : ℤ)
Tactic: simp_rw [Rat.mul_num, Rat.den_intCast, invOf_eq_inv,
      Rat.inv_natCast_den_of_pos this, Rat.inv_natCast_num_of_pos this,
      Rat.num_intCast, one_mul, mul_one, h, Nat.cast_one, Int.ediv_one, Int.cast_id]