awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
h₁ : l₁.eval + (-(r₂ • x) + -l₂.eval) = -(r₂ • x) + (l₁.eval + -l₂.eval)
⊢ r₁ • x + (l₁.eval + (-(r₂ • x) + -l₂.eval)) = r₁ • x + (-(r₂ • x) + (l₁.eval + -l₂.eval))

Tactic:
congr! 1
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
h₁ : l₁.eval + -(r₂ • x) + -l₂.eval = -(r₂ • x) + l₁.eval + -l₂.eval
⊢ l₁.eval + (-(r₂ • x) + -l₂.eval) = -(r₂ • x) + (l₁.eval + -l₂.eval)

Tactic:
simp only [← add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
h₁ : l₁.eval + -(r₂ • x) = -(r₂ • x) + l₁.eval
⊢ l₁.eval + -(r₂ • x) + -l₂.eval = -(r₂ • x) + l₁.eval + -l₂.eval

Tactic:
congr! 1
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
h₁ h₂ : -(r₂ • x) + l₁.eval = -(r₂ • x) + l₁.eval
⊢ l₁.eval + -(r₂ • x) = -(r₂ • x) + l₁.eval

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval
simp : a₁.1 • a₁.2 + l₁.eval + -(a₂.1 • a₂.2) + -l₂.eval = -(a₂.1 • a₂.2) + a₁.1 • a₁.2 + l₁.eval + -l₂.eval
⊢ (a₁ ::ᵣ l₁).eval - (a₂ ::ᵣ l₂).eval = ((-a₂.1, a₂.2) ::ᵣ l).eval

Tactic:
simp only [eval_cons, neg_smul, neg_add, sub_eq_add_neg, ← h, ← add_assoc]

Premises used: neg_smul, add_assoc, sub_eq_add_neg, neg_add, Mathlib.Tactic.Module.NF.eval_cons
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval
h₁ : a₁.1 • a₁.2 + l₁.eval + -(a₂.1 • a₂.2) = -(a₂.1 • a₂.2) + a₁.1 • a₁.2 + l₁.eval
⊢ a₁.1 • a₁.2 + l₁.eval + -(a₂.1 • a₂.2) + -l₂.eval = -(a₂.1 • a₂.2) + a₁.1 • a₁.2 + l₁.eval + -l₂.eval

Tactic:
congr! 1
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval
h₁ : -(a₂.1 • a₂.2) + (a₁.1 • a₁.2 + l₁.eval) = -(a₂.1 • a₂.2) + a₁.1 • a₁.2 + l₁.eval
h₂ h₃ : -(a₂.1 • a₂.2) + (a₁.1 • a₁.2 + l₁.eval) = -(a₂.1 • a₂.2) + (a₁.1 • a₁.2 + l₁.eval)
⊢ a₁.1 • a₁.2 + l₁.eval + -(a₂.1 • a₂.2) = -(a₂.1 • a₂.2) + a₁.1 • a₁.2 + l₁.eval

Tactic:
rw [add_comm, add_assoc]

Premises used: add_assoc, add_comm
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
S₁ : Type u_6
S₂ : Type u_7
inst : AddCommGroup M
inst_1 : Ring R
inst_2 : Module R M
inst_3 : Semiring R₁
inst_4 : Module R₁ M
inst_5 : Semiring R₂
inst_6 : Module R₂ M
inst_7 : Semiring S₁
inst_8 : Module S₁ M
inst_9 : Semiring S₂
inst_10 : Module S₂ M
l₁ l₂ l : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
l₁'' : NF S₁ M
l₂'' : NF S₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁''.eval
hx₂ : x₂ = l₂''.eval
h₁' : l₁'.eval = l₁''.eval
h₂' : l₂'.eval = l₂''.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval - l₂.eval = l.eval
rw : l₁''.eval - x₂ = l.eval
rw₁ : l₁''.eval - l₂''.eval = l.eval
rw₂ : l₁'.eval - l₂''.eval = l.eval
rw₃ : l₁'.eval - l₂'.eval = l.eval
rw₄ : l₁.eval - l₂'.eval = l.eval
rw₅ : l₁.eval - l₂.eval = l.eval
rw₆ rw₇ : l.eval = l.eval
⊢ x₁ - x₂ = l.eval

Tactic:
rw [hx₁, hx₂, ← h₁', ← h₂', ← h₁, ← h₂, h]
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : AddCommGroup M
inst_1 : Ring R
inst_2 : Module R M
l : NF R M
simp :
  Eq.{u_3 + 1} (α := M) (sum (map ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (-x.1, x.2)) l))
    (sum (map ((fun (x : M) ↦ -x) ∘ fun (x : R × M) ↦ x.1 • x.2) l))
⊢ (-l).eval = -l.eval

Tactic:
simp +instances only [NF.eval, List.map_map, List.sum_neg, NF.instNeg]

Premises used: List.map_map, List.sum_neg, Mathlib.Tactic.Module.NF.eval, Mathlib.Tactic.Module.NF.instNeg
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : AddCommGroup M
inst_1 : Ring R
inst_2 : Module R M
l : NF R M
e_a :
  Eq (α := R × M → M) ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (-x.1, x.2))
    ((fun (x : M) ↦ -x) ∘ fun (x : R × M) ↦ x.1 • x.2)
⊢ Eq.{u_3 + 1} (α := M) (sum (map ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (-x.1, x.2)) l))
    (sum (map ((fun (x : M) ↦ -x) ∘ fun (x : R × M) ↦ x.1 • x.2) l))

Tactic:
congr
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : AddCommGroup M
inst_1 : Ring R
inst_2 : Module R M
l : NF R M
e_a :
  ∀ (p : R × M),
    Eq.{u_3 + 1} (α := M) (((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (-x.1, x.2)) p)
      (((fun (x : M) ↦ -x) ∘ fun (x : R × M) ↦ x.1 • x.2) p)
⊢ Eq (α := R × M → M) ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (-x.1, x.2))
    ((fun (x : M) ↦ -x) ∘ fun (x : R × M) ↦ x.1 • x.2)

Tactic:
ext p
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : AddCommGroup M
inst_1 : Ring R
inst_2 : Module R M
l : NF R M
p : R × M
⊢ Eq.{u_3 + 1} (α := M) (((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (-x.1, x.2)) p)
    (((fun (x : M) ↦ -x) ∘ fun (x : R × M) ↦ x.1 • x.2) p)

Tactic:
simp
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : AddCommGroup M
inst_1 : Ring R
inst_2 : Module R M
l : NF R M
⊢ 0 - l.eval = (-l).eval

Tactic:
simp [eval_neg]

Premises used: Mathlib.Tactic.Module.NF.eval_neg
-- Module: Mathlib.Tactic.Module
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : AddCommGroup M
inst_1 : Semiring S
inst_2 : Module S M
inst_3 : Ring R
inst_4 : Module R M
l : NF R M
l₀ : NF S M
hl : l.eval = l₀.eval
x : M
h : x = l₀.eval
rw : -l₀.eval = (-l).eval
rw₁ : -l.eval = (-l).eval
rw₂ rw₃ : -l.eval = -l.eval
⊢ -x = (-l).eval

Tactic:
rw [h, ← hl, eval_neg]

Premises used: Mathlib.Tactic.Module.NF.eval_neg
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : Mul R
r : R
l : NF R M
⊢ r • l =
    map
      (fun (x : R × M) ↦
        match (motive := R × M → R × M) x with
        | (a, x) => (r * a, x))
      l

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
l : NF R M
x : M
h :
  x =
    sum
      (map
        (fun (x : R × M) ↦
          match (motive := R × M → M) x with
          | (r, x) => r • x)
        l)
r : R
simp :
  Eq.{u_3 + 1} (α := M) (sum (map ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (r * x.1, x.2)) l))
    (sum (map ((fun (x : M) ↦ r • x) ∘ fun (x : R × M) ↦ x.1 • x.2) l))
⊢ sum
      (map
        (fun (x : R × M) ↦
          match (motive := R × M → M) x with
          | (r, x) => r • x)
        (r • l)) =
    r • x

Tactic:
simp only [h, smul_sum, map_map, NF.smul_apply]

Premises used: List.map_map, Mathlib.Tactic.Module.NF.smul_apply, List.smul_sum
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
l : NF R M
x : M
h :
  x =
    sum
      (map
        (fun (x : R × M) ↦
          match (motive := R × M → M) x with
          | (r, x) => r • x)
        l)
r : R
e_a :
  Eq (α := R × M → M) ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (r * x.1, x.2))
    ((fun (x : M) ↦ r • x) ∘ fun (x : R × M) ↦ x.1 • x.2)
⊢ Eq.{u_3 + 1} (α := M) (sum (map ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (r * x.1, x.2)) l))
    (sum (map ((fun (x : M) ↦ r • x) ∘ fun (x : R × M) ↦ x.1 • x.2) l))

Tactic:
congr
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
l : NF R M
x : M
h :
  x =
    sum
      (map
        (fun (x : R × M) ↦
          match (motive := R × M → M) x with
          | (r, x) => r • x)
        l)
r : R
e_a :
  ∀ (p : R × M),
    Eq.{u_3 + 1} (α := M) (((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (r * x.1, x.2)) p)
      (((fun (x : M) ↦ r • x) ∘ fun (x : R × M) ↦ x.1 • x.2) p)
⊢ Eq (α := R × M → M) ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (r * x.1, x.2))
    ((fun (x : M) ↦ r • x) ∘ fun (x : R × M) ↦ x.1 • x.2)

Tactic:
ext p
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
l : NF R M
x : M
h :
  x =
    sum
      (map
        (fun (x : R × M) ↦
          match (motive := R × M → M) x with
          | (r, x) => r • x)
        l)
r : R
p : R × M
⊢ Eq.{u_3 + 1} (α := M) (((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : R × M) ↦ (r * x.1, x.2)) p)
    (((fun (x : M) ↦ r • x) ∘ fun (x : R × M) ↦ x.1 • x.2) p)

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Tactic.Module
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : Semiring R₀
inst_4 : Module R₀ M
inst_5 : Semiring S
inst_6 : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
h : l.eval = l.eval
⊢ s • x = (r • l).eval

Tactic:
rw [← hs, hx, ← hl, eval_smul]

Premises used: Mathlib.Tactic.Module.NF.eval_smul
-- Module: Mathlib.Tactic.Module
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : Semiring R₀
inst_4 : Module R₀ M
inst_5 : Semiring S
inst_6 : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ l.eval = l.eval

Tactic:
rfl
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : AddMonoid M
inst_1 : SMul R M
r₁ r₂ : R
m : M
l₁ l₂ : NF R M
h1 : r₁ = r₂
h2 : l₁.eval = l₂.eval
⊢ ((r₁, m) ::ᵣ l₁).eval = ((r₂, m) ::ᵣ l₂).eval

Tactic:
simp [h1, h2]
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
r : R
m n : M
l : NF R M
h1 : r = 0
h2 : l.eval = n
⊢ ((r, m) ::ᵣ l).eval = n

Tactic:
simp [h1, h2]
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
r : R
m n : M
l : NF R M
h1 : 0 = r
h2 : n = l.eval
⊢ n = ((r, m) ::ᵣ l).eval

Tactic:
simp [← h1, h2]
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
inst_3 : Semiring R₁
inst_4 : Module R₁ M
inst_5 : Semiring R₂
inst_6 : Module R₂ M
l₁ l₂ : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁'.eval
hx₂ : x₂ = l₂'.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval = l₂.eval
rw : l₁'.eval = x₂
rw₁ : l₁'.eval = l₂'.eval
rw₂ : l₁.eval = l₂'.eval
rw₃ : l₁.eval = l₂.eval
rw₄ rw₅ : l₂.eval = l₂.eval
⊢ x₁ = x₂

Tactic:
rw [hx₁, hx₂, ← h₁, ← h₂, h]
-- Module: Mathlib.Tactic.Module
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : Algebra S R
inst_3 : AddMonoid M
inst_4 : SMul S M
inst_5 : MulAction R M
inst_6 : IsScalarTower S R M
l : NF S M
simp :
  Eq.{u_3 + 1} (α := M)
    (sum (map ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : S × M) ↦ ((Algebra.algebraMap S R : (a : S) → R) x.1, x.2)) l))
    (sum (map (fun (x : S × M) ↦ x.1 • x.2) l))
⊢ (algebraMap R l).eval = l.eval

Tactic:
simp only [NF.eval, algebraMap, map_map]

Premises used: List.map_map, Mathlib.Tactic.Module.NF.algebraMap, Mathlib.Tactic.Module.NF.eval
-- Module: Mathlib.Tactic.Module
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : Algebra S R
inst_3 : AddMonoid M
inst_4 : SMul S M
inst_5 : MulAction R M
inst_6 : IsScalarTower S R M
l : NF S M
e_a :
  Eq (α := S × M → M)
    ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : S × M) ↦ ((Algebra.algebraMap S R : (a : S) → R) x.1, x.2))
    fun (x : S × M) ↦ x.1 • x.2
⊢ Eq.{u_3 + 1} (α := M)
    (sum (map ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : S × M) ↦ ((Algebra.algebraMap S R : (a : S) → R) x.1, x.2)) l))
    (sum (map (fun (x : S × M) ↦ x.1 • x.2) l))

Tactic:
congr
-- Module: Mathlib.Tactic.Module
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : Algebra S R
inst_3 : AddMonoid M
inst_4 : SMul S M
inst_5 : MulAction R M
inst_6 : IsScalarTower S R M
l : NF S M
e_a :
  ∀ (x : S × M),
    ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : S × M) ↦ ((Algebra.algebraMap S R : (a : S) → R) x.1, x.2)) x = x.1 • x.2
⊢ Eq (α := S × M → M)
    ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : S × M) ↦ ((Algebra.algebraMap S R : (a : S) → R) x.1, x.2))
    fun (x : S × M) ↦ x.1 • x.2

Tactic:
ext
-- Module: Mathlib.Tactic.Module
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : Algebra S R
inst_3 : AddMonoid M
inst_4 : SMul S M
inst_5 : MulAction R M
inst_6 : IsScalarTower S R M
l : NF S M
x : S × M
⊢ ((fun (x : R × M) ↦ x.1 • x.2) ∘ fun (x : S × M) ↦ ((Algebra.algebraMap S R : (a : S) → R) x.1, x.2)) x = x.1 • x.2

Tactic:
simp [IsScalarTower.algebraMap_smul]

Premises used: IsScalarTower.algebraMap_smul
-- Module: Mathlib.Tactic.NoncommRing
Goal:
R : Type u_1
inst : NonAssocSemiring R
r : R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ OfNat.ofNat n * r = HSMul.hSMul (α := ℕ) (OfNat.ofNat n) r

Tactic:
simp only [nsmul_eq_mul, Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, nsmul_eq_mul
-- Module: Mathlib.Tactic.NoncommRing
Goal:
R : Type u_1
inst : NonAssocSemiring R
r : R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ r * OfNat.ofNat n = HSMul.hSMul (α := ℕ) (OfNat.ofNat n) r

Tactic:
simp only [nsmul_eq_mul', Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, nsmul_eq_mul'
-- Module: Mathlib.Tactic.Nontriviality.Core
Goal:
p : Prop
α : Type u
h₁ : Subsingleton α → p
h₂ : Nontrivial α → p
⊢ p

Tactic:
(subsingleton_or_nontrivial α).elim @h₁ @h₂

Premises used: subsingleton_or_nontrivial, Or.elim
-- Module: Mathlib.Tactic.NormNum.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : Lattice α
inst_2 : IsOrderedRing α
a : α
na : ℕ
pa : IsNat a na
rw : IsNat.{u_1} (α := α) (↑na : α) na
⊢ IsNat |a| na

Tactic:
rw [pa.out, Nat.abs_cast]

Premises used: Nat.abs_cast, Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.NormNum.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : Lattice α
inst_2 : IsOrderedRing α
a : α
na : ℕ
pa : IsNat a na
out : Eq.{u_1 + 1} (α := α) (↑na : α) (↑na : α)
⊢ IsNat.{u_1} (α := α) (↑na : α) na

Tactic:
constructor
-- Module: Mathlib.Tactic.NormNum.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : Lattice α
inst_2 : IsOrderedRing α
a : α
na : ℕ
pa : IsNat a na
⊢ Eq.{u_1 + 1} (α := α) (↑na : α) (↑na : α)

Tactic:
rfl
-- Module: Mathlib.Tactic.NormNum.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : Lattice α
inst_2 : IsOrderedRing α
a : α
na : ℕ
pa : IsInt a (Int.negOfNat na)
rw : IsNat.{u_1} (α := α) |(↑(Int.negOfNat na) : α)| na
⊢ IsNat |a| na

Tactic:
rw [pa.out]

Premises used: Mathlib.Meta.NormNum.IsInt.out
-- Module: Mathlib.Tactic.NormNum.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : Lattice α
inst_2 : IsOrderedRing α
a : α
na : ℕ
pa : IsInt a (Int.negOfNat na)
out : Eq.{u_1 + 1} (α := α) |(↑(Int.negOfNat na) : α)| (↑na : α)
⊢ IsNat.{u_1} (α := α) |(↑(Int.negOfNat na) : α)| na

Tactic:
constructor
-- Module: Mathlib.Tactic.NormNum.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : Lattice α
inst_2 : IsOrderedRing α
a : α
na : ℕ
pa : IsInt a (Int.negOfNat na)
⊢ Eq.{u_1 + 1} (α := α) |(↑(Int.negOfNat na) : α)| (↑na : α)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Abs
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
num den : ℕ
ra : IsNNRat a num den
obtain :
  ∀ (ha1 : Invertible (α := α) (↑den : α)),
    IsNNRat |HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)| num
      den
⊢ IsNNRat |a| num den

Tactic:
obtain ⟨ha1, rfl⟩ := ra

Premises used: rfl
-- Module: Mathlib.Tactic.NormNum.Abs
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible (α := α) (↑den : α)
⊢ IsNNRat |HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)| num
    den

Tactic:
⟨ha1, abs_of_nonneg ?_⟩

Premises used: Mathlib.Meta.NormNum.IsNNRat.mk, abs_of_nonneg
-- Module: Mathlib.Tactic.NormNum.Abs
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible (α := α) (↑den : α)
refine : 0 ≤ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)
⊢ IsNNRat |HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)| num
    den

Tactic:
refine ⟨ha1, abs_of_nonneg ?_⟩
-- Module: Mathlib.Tactic.NormNum.Abs
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible (α := α) (↑den : α)
ha : LE.le.{u_1} (α := α) 0 (↑num : α)
hb : LE.le.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)
⊢ 0 ≤ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)

Tactic:
apply mul_nonneg

Premises used: mul_nonneg
-- Module: Mathlib.Tactic.NormNum.Abs
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible (α := α) (↑den : α)
⊢ LE.le.{u_1} (α := α) 0 (↑num : α)

Tactic:
Nat.cast_nonneg' num

Premises used: Nat.cast_nonneg'
-- Module: Mathlib.Tactic.NormNum.Abs
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible (α := α) (↑den : α)
⊢ LE.le.{u_1} (α := α) 0 (↑num : α)

Tactic:
exact Nat.cast_nonneg' num

Premises used: Nat.cast_nonneg'
-- Module: Mathlib.Tactic.NormNum.Abs
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible (α := α) (↑den : α)
⊢ LE.le.{u_1} (α := α) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)

Tactic:
simp only [invOf_eq_inv, inv_nonneg, Nat.cast_nonneg]

Premises used: Nat.cast_nonneg, inv_nonneg, invOf_eq_inv
-- Module: Mathlib.Tactic.NormNum.Abs
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
num den : ℕ
ra : IsRat a (Int.negOfNat num) den
obtain :
  ∀ (ha1 : Invertible (α := α) (↑den : α)),
    IsNNRat
      |HMul.hMul (α := α) (↑(Int.negOfNat num) : α)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)|
      num den
⊢ IsNNRat |a| num den

Tactic:
obtain ⟨ha1, rfl⟩ := ra

Premises used: rfl
-- Module: Mathlib.Tactic.NormNum.Abs
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible (α := α) (↑den : α)
simp :
  IsNNRat |HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)| num
    den
⊢ IsNNRat
    |HMul.hMul (α := α) (↑(Int.negOfNat num) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑den : α) _)|
    num den

Tactic:
simp only [Int.cast_negOfNat, neg_mul, abs_neg]

Premises used: abs_neg, neg_mul, Int.cast_negOfNat
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Semiring α
k : ℕ
b c : α
hc1 : c * ((↑k : α) * b) = 1
hc2 : (↑k : α) * b * c = 1
⊢ c * (↑k : α) * b = 1

Tactic:
rw [← mul_assoc] at hc1

Premises used: mul_assoc
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Semiring α
k : ℕ
b c : α
hc1 : c * ((↑k : α) * b) = 1
hc2 : (↑k : α) * b * c = 1
hc1₁ : c * (↑k : α) * b = 1
⊢ (↑k : α) * b * c = 1

Tactic:
rw [← mul_assoc] at hc1

Premises used: mul_assoc
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Semiring α
k : ℕ
b c : α
hc1 : c * (↑k : α) * b = 1
hc2 : (↑k : α) * b * c = 1
⊢ b * (c * (↑k : α)) = 1

Tactic:
rw [Nat.cast_commute k, mul_assoc, Nat.cast_commute k] at hc2

Premises used: mul_assoc, Nat.cast_commute
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Semiring α
k : ℕ
b c : α
hc1 : c * (↑k : α) * b = 1
hc2 : b * (c * (↑k : α)) = 1
⊢ Invertible b

Tactic:
exact ⟨_, hc1, hc2⟩
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Semiring α
a k b : ℕ
inst_1 : Invertible (α := α) (↑a : α)
h : a = k * b
⊢ (↑a : α) = HMul.hMul (α := α) (↑k : α) (↑b : α)

Tactic:
simp [h]
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
n : ℤ
⊢ IsInt n n

Tactic:
⟨rfl⟩

Premises used: Mathlib.Meta.NormNum.IsInt.mk, rfl
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
⊢ IsNat.{u_1} (α := α) Zero.zero 0

Tactic:
⟨Nat.cast_zero.symm⟩

Premises used: Mathlib.Meta.NormNum.IsNat.mk, Nat.cast_zero, Eq.symm
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
⊢ IsNat.{u_1} (α := α) One.one 1

Tactic:
⟨Nat.cast_one.symm⟩

Premises used: Mathlib.Meta.NormNum.IsNat.mk, Eq.symm, Nat.cast_one
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u
inst : AddMonoidWithOne α
a : α
n : ℕ
h : (↑n : α) = a
⊢ IsNat a n

Tactic:
⟨h.symm⟩

Premises used: Mathlib.Meta.NormNum.IsNat.mk, Eq.symm
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
m n : ℕ
h : IsNat m n
⊢ IsInt (Int.negOfNat m) (Int.negOfNat n)

Tactic:
⟨congr_arg Int.negOfNat h.1⟩

Premises used: congr_arg, Mathlib.Meta.NormNum.IsInt.mk, Mathlib.Meta.NormNum.IsNat.out, Int.negOfNat
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
a : ℕ
⊢ Int.natAbs (↑(Int.negOfNat a) : ℤ) = (↑a : ℕ)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
m : ℕ
⊢ IsNat.{u_1} (α := R) (↑(↑m : ℕ) : R) m

Tactic:
⟨rfl⟩

Premises used: Mathlib.Meta.NormNum.IsNat.mk, rfl
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
m : ℕ
⊢ IsNat.{u_1} (α := R) (↑(↑m : ℕ) : R) m

Tactic:
exact ⟨rfl⟩
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑(↑m : ℤ) : R) (↑m : R)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℕ
⊢ IsNat.{u_1} (α := R) (↑(↑m : ℤ) : R) m

Tactic:
exact ⟨by simp⟩
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℤ
⊢ IsInt.{u_1} (α := R) (↑(↑m : ℤ) : R) m

Tactic:
⟨rfl⟩

Premises used: Mathlib.Meta.NormNum.IsInt.mk, rfl
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
R : Type u_1
inst : Ring R
m : ℤ
⊢ IsInt.{u_1} (α := R) (↑(↑m : ℤ) : R) m

Tactic:
exact ⟨rfl⟩
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * db + nb * da = k * nc
h₂ : da * db = k * dc
⊢ Invertible (α := α) (↑(da * db) : α)

Tactic:
simpa using invertibleMul (da:α) db

Premises used: Nat.cast, invertibleMul
-- Module: Mathlib.Tactic.NormNum.Basic
Goal:
α : Type u_1
inst : Semiring α
na nb nc da db dc k : ℕ
inv : Invertible (α := α) (↑da : α)
inv_1 : Invertible (α := α) (↑db : α)
h₁ : na * db + nb * da = k * nc
h₂ : da * db = k * dc
have :
  ∀ (this : Invertible (α := α) (↑(da * db) : α)),
    IsNNRat
      (HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) +
        HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
      nc dc
⊢ IsNNRat
    (HMul.hMul (α := α) (↑na : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑da : α) _) +
      HMul.hMul (α := α) (↑nb : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑db : α) _))
    nc dc

Tactic:
have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da:α) db