awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst : Ring A
inst_1 : LinearOrder A
inst_2 : IsStrictOrderedRing A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (n < 0) = true
pos_invOf_d : LT.lt.{u_1} (α := A) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
neg_n : LT.lt.{u_1} (α := A) (↑n : A) 0
neg : HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _) < 0
⊢ HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _) ≠ 0

Tactic:
ne_iff_lt_or_gt.2 (Or.inl neg)

Premises used: Iff.mpr, ne_iff_lt_or_gt, Or.inl
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst : Ring A
inst_1 : LinearOrder A
inst_2 : IsStrictOrderedRing A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (n < 0) = true
pos_invOf_d : LT.lt.{u_1} (α := A) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
neg_n : LT.lt.{u_1} (α := A) (↑n : A) 0
neg : HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _) < 0
⊢ HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _) ≠ 0

Tactic:
exact ne_iff_lt_or_gt.2 (Or.inl neg)

Premises used: Iff.mpr, ne_iff_lt_or_gt, Or.inl
-- Module: Mathlib.Tactic.Positivity.Finset
Goal:
α : Type u_1
s : Finset α
⊢ 0 ≤ #s

Tactic:
positivity
-- Module: Mathlib.Tactic.Positivity.Finset
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ 0 < #s

Tactic:
positivity
-- Module: Mathlib.Tactic.Positivity.Finset
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
⊢ 0 ≤ Fintype.card α

Tactic:
positivity
-- Module: Mathlib.Tactic.Positivity.Finset
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
⊢ 0 ≤ s.dens

Tactic:
positivity
-- Module: Mathlib.Tactic.Positivity.Finset
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
hs : s.Nonempty
⊢ 0 < s.dens

Tactic:
positivity
-- Module: Mathlib.Tactic.Positivity.Finset
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
hs : s.Nonempty
⊢ s.dens ≠ 0

Tactic:
positivity
-- Module: Mathlib.Tactic.Positivity.Finset
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : Nonempty α
⊢ 0 < card.{u_1} (α := α) univ

Tactic:
positivity
-- Module: Mathlib.Tactic.Positivity.Finset
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : Nonempty α
⊢ 0 < Fintype.card α

Tactic:
positivity
-- Module: Mathlib.Tactic.Positivity.Finset
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : Nonempty α
⊢ 0 < dens.{u_1} (α := α) univ

Tactic:
positivity
-- Module: Mathlib.Tactic.Positivity.Finset
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : Nonempty α
⊢ dens.{u_1} (α := α) univ ≠ 0

Tactic:
positivity
-- Module: Mathlib.Tactic.Positivity.Finset
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
G : Type u_2
A : Finset G
f : G → ℕ := fun (x : G) ↦ 1
h : ∀ (s : G), HPow.hPow (β := ℕ) (f s) 2 = 1
⊢ 0 ≤ #A

Tactic:
positivity
-- Module: Mathlib.Tactic.Push
Goal:
p q : Prop
rw : ¬p ∧ q ∨ p ∧ ¬q ↔ p ∧ ¬q ∨ ¬p ∧ q
rw₁ rw₂ : p ∧ ¬q ∨ ¬p ∧ q ↔ p ∧ ¬q ∨ ¬p ∧ q
⊢ ¬p ∧ q ∨ ¬¬p ∧ ¬q ↔ p ∧ ¬q ∨ ¬p ∧ q

Tactic:
rw [not_not, or_comm]

Premises used: Classical.not_not, or_comm
-- Module: Mathlib.Tactic.Push
Goal:
α : Sort u_1
s : α → Prop
⊢ ¬Exists s ↔ ∀ (x : α), binderNameHint x s ¬s x

Tactic:
_root_.not_exists

Premises used: not_exists, binderNameHint
-- Module: Mathlib.Tactic.Push
Goal:
p q : Prop
⊢ (¬(p ∧ q)) = (p → ¬q)

Tactic:
propext not_and

Premises used: propext, not_and
-- Module: Mathlib.Tactic.Push
Goal:
p q : Prop
⊢ (¬(p ∧ q)) = (¬p ∨ ¬q)

Tactic:
propext not_and_or

Premises used: not_and_or, propext
-- Module: Mathlib.Tactic.Push
Goal:
α : Sort u_1
s : α → Prop
⊢ (¬∀ (x : α), s x) = ∃ (x : α), ¬s x

Tactic:
propext not_forall

Premises used: propext, Classical.not_forall
-- Module: Mathlib.Tactic.Qify
Goal:
a b : ℤ
⊢ a = b ↔ Eq (α := ℚ) (↑a : ℚ) (↑b : ℚ)

Tactic:
simp only [Int.cast_inj]

Premises used: Int.cast_inj
-- Module: Mathlib.Tactic.Qify
Goal:
a b : ℤ
⊢ a ≤ b ↔ LE.le (α := ℚ) (↑a : ℚ) (↑b : ℚ)

Tactic:
Int.cast_le.symm

Premises used: Int.cast_le, Iff.symm
-- Module: Mathlib.Tactic.Qify
Goal:
a b : ℤ
⊢ a < b ↔ LT.lt (α := ℚ) (↑a : ℚ) (↑b : ℚ)

Tactic:
Int.cast_lt.symm

Premises used: Int.cast_lt, Iff.symm
-- Module: Mathlib.Tactic.Qify
Goal:
a b : ℤ
⊢ a ≠ b ↔ Ne (α := ℚ) (↑a : ℚ) (↑b : ℚ)

Tactic:
simp only [ne_eq, Int.cast_inj]

Premises used: Int.cast_inj, ne_eq
-- Module: Mathlib.Tactic.ReduceModChar
Goal:
e' r : ℤ
α : Type u_1
inst_1 : Ring α
n n' : ℕ
inst : CharP α n
e : α
he : IsInt e e'
hn : IsNat n n'
h₂ : IsInt (e' % (↑n' : ℤ)) r
rw : Eq.{u_1 + 1} (α := α) (↑e' : α) (↑r : α)
rw₁ : Eq.{u_1 + 1} (α := α) (↑(e' % (↑n : ℤ)) : α) (↑r : α)
rw₂ : Eq.{u_1 + 1} (α := α) (↑(e' % (↑n' : ℤ)) : α) (↑r : α)
rw₃ : Eq.{u_1 + 1} (α := α) (↑(↑r : ℤ) : α) (↑r : α)
rw₄ rw₅ : Eq.{u_1 + 1} (α := α) (↑r : α) (↑r : α)
⊢ e = (↑r : α)

Tactic:
rw [he.out, CharP.intCast_eq_intCast_mod α n, show n = n' from hn.out, h₂.out, Int.cast_id]

Premises used: Int.cast_id, Mathlib.Meta.NormNum.IsNat.out, CharP.intCast_eq_intCast_mod, Mathlib.Meta.NormNum.IsInt.out
-- Module: Mathlib.Tactic.ReduceModChar
Goal:
α : Type u_1
inst : Semiring α
a_1 : α
a b n : ℕ
h_1 : CharP α (↑n : ℕ)
h : a_1 = (↑a : α)
rw : Eq.{u_1 + 1} (α := α) (↑(a ^ b % n) : α) (↑((a ^ b).mod n) : α)
⊢ HPow.hPow (β := ℕ) a_1 (↑b : ℕ) = (↑((a.pow b).mod n) : α)

Tactic:
rw [h, Nat.cast_id, Nat.pow_eq, ← Nat.cast_pow, CharP.natCast_eq_natCast_mod α n]

Premises used: Nat.pow_eq, CharP.natCast_eq_natCast_mod, Nat.cast_id, Nat.cast_pow
-- Module: Mathlib.Tactic.ReduceModChar
Goal:
α : Type u_1
inst : Semiring α
a_1 : α
a b n : ℕ
h_1 : CharP α (↑n : ℕ)
h : a_1 = (↑a : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(a ^ b % n) : α) (↑((a ^ b).mod n) : α)

Tactic:
rfl
-- Module: Mathlib.Tactic.ReduceModChar
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
k : ℤ
⊢ Eq.{u_1 + 1} (α := R) (↑k : R) (↑(k % (↑p : ℤ)) : R)

Tactic:
CharP.intCast_eq_intCast_mod R p

Premises used: CharP.intCast_eq_intCast_mod
-- Module: Mathlib.Tactic.ReduceModChar
Goal:
α : Type u_1
inst_1 : Ring α
n : ℕ
inst : CharP α n
b : α
a : ℕ
a' : α
p : IsNat (HSub.hSub (α := α) (↑n : α) 1) a
pa : (↑a : α) = a'
rw : -1 * b = HSub.hSub (α := α) (↑n : α) 1 * b
⊢ -b = a' * b

Tactic:
rw [← pa, ← p.out, ← neg_one_mul]

Premises used: neg_one_mul, Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.ReduceModChar
Goal:
α : Type u_1
inst_1 : Ring α
n : ℕ
inst : CharP α n
b : α
a : ℕ
a' : α
p : IsNat (HSub.hSub (α := α) (↑n : α) 1) a
pa : (↑a : α) = a'
⊢ -1 * b = HSub.hSub (α := α) (↑n : α) 1 * b

Tactic:
simp
-- Module: Mathlib.Tactic.ReduceModChar
Goal:
α : Type u_1
inst_1 : Ring α
n : ℕ
inst : CharP α n
a b : α
na : ℕ
na' : α
p : IsNat (HSub.hSub (α := α) (↑n : α) 1 * a) na
pa : (↑na : α) = na'
rw : -1 * (a * b) = HSub.hSub (α := α) (↑n : α) 1 * a * b
⊢ -(a * b) = na' * b

Tactic:
rw [← pa, ← p.out, ← neg_one_mul]

Premises used: neg_one_mul, Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.ReduceModChar
Goal:
α : Type u_1
inst_1 : Ring α
n : ℕ
inst : CharP α n
a b : α
na : ℕ
na' : α
p : IsNat (HSub.hSub (α := α) (↑n : α) 1 * a) na
pa : (↑na : α) = na'
⊢ -1 * (a * b) = HSub.hSub (α := α) (↑n : α) 1 * a * b

Tactic:
simp
-- Module: Mathlib.Tactic.Rify
Goal:
a b : ℚ
⊢ a = b ↔ Eq (α := ℝ) (↑a : ℝ) (↑b : ℝ)

Tactic:
simp
-- Module: Mathlib.Tactic.Rify
Goal:
a b : ℚ
⊢ a ≤ b ↔ LE.le (α := ℝ) (↑a : ℝ) (↑b : ℝ)

Tactic:
simp
-- Module: Mathlib.Tactic.Rify
Goal:
a b : ℚ
⊢ a < b ↔ LT.lt (α := ℝ) (↑a : ℝ) (↑b : ℝ)

Tactic:
simp
-- Module: Mathlib.Tactic.Rify
Goal:
a b : ℚ
⊢ a ≠ b ↔ Ne (α := ℝ) (↑a : ℝ) (↑b : ℝ)

Tactic:
simp
-- Module: Mathlib.Tactic.Rify
Goal:
a : ℕ
inst : a.AtLeastTwo
⊢ Eq (α := ℝ) (↑(OfNat.ofNat a) : ℝ) (OfNat.ofNat a)

Tactic:
rfl

Premises used: CauSeq.Completion.ofRat, rfl
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a : R
n : ℕ
e : a = (↑n : R)
⊢ a = HAdd.hAdd (α := R) n.rawCast 0

Tactic:
simp [e]
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a : R
e : a = (↑0 : R)
⊢ a = 0

Tactic:
simp [e]
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
n : ℕ
R : Type u_2
inst : Ring R
a : R
e : a = (↑(Int.negOfNat n) : R)
⊢ a = HAdd.hAdd (α := R) (Int.negOfNat n).rawCast 0

Tactic:
simp [e]
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
n d : ℕ
R : Type u_2
inst : DivisionSemiring R
a : R
inv : Invertible (α := R) (↑d : R)
e : a = HMul.hMul (α := R) (↑n : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _)
⊢ a = HAdd.hAdd (α := R) (NNRat.rawCast n d) 0

Tactic:
simp [e, div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
n : ℤ
d : ℕ
R : Type u_2
inst : DivisionRing R
a : R
inv : Invertible (α := R) (↑d : R)
e : a = HMul.hMul (α := R) (↑n : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : R) _)
⊢ a = HAdd.hAdd (α := R) (Rat.rawCast n d) 0

Tactic:
simp [e, div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑n.rawCast : R) n.rawCast

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_1
inst : CommSemiring R
b₁ b₃ : R
a₁ a₃ a₂ : ℕ
h : (↑a₁ : R) = b₁
h_1 : (↑a₃ : R) = b₃
subst_vars : (↑(a₁ ^ a₂ * a₃) : R) = HPow.hPow (α := R) (↑a₁ : R) a₂ * (↑a₃ : R)
⊢ (↑(a₁ ^ a₂ * a₃) : R) = b₁ ^ a₂ * b₃

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a₁ a₃ a₂ : ℕ
⊢ (↑(a₁ ^ a₂ * a₃) : R) = HPow.hPow (α := R) (↑a₁ : R) a₂ * (↑a₃ : R)

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := R) (↑0 : R) 0

Tactic:
Nat.cast_zero

Premises used: Nat.cast_zero
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_1
inst : CommSemiring R
b₁ b₂ : R
a₁ a₂ : ℕ
h : (↑a₁ : R) = b₁
h_1 : (↑a₂ : R) = b₂
subst_vars : (↑(a₁ + a₂) : R) = HAdd.hAdd (α := R) (↑a₁ : R) (↑a₂ : R)
⊢ (↑(a₁ + a₂) : R) = b₁ + b₂

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a₁ a₂ : ℕ
⊢ (↑(a₁ + a₂) : R) = HAdd.hAdd (α := R) (↑a₁ : R) (↑a₂ : R)

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_2
inst : CommRing R
n : ℕ
⊢ Eq.{u_2 + 1} (α := R) (↑n.rawCast : R) n.rawCast

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_2
inst : CommRing R
n : ℕ
⊢ Eq.{u_2 + 1} (α := R) (↑(Int.negOfNat n).rawCast : R) (Int.negOfNat n).rawCast

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_2
inst : CommRing R
b₁ b₃ : R
a₁ a₃ : ℤ
a₂ : ℕ
h : (↑a₁ : R) = b₁
h_1 : (↑a₃ : R) = b₃
subst_vars : (↑(a₁ ^ a₂ * a₃) : R) = HPow.hPow (α := R) (↑a₁ : R) a₂ * (↑a₃ : R)
⊢ (↑(a₁ ^ a₂ * a₃) : R) = b₁ ^ a₂ * b₃

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_2
inst : CommRing R
a₁ a₃ : ℤ
a₂ : ℕ
⊢ (↑(a₁ ^ a₂ * a₃) : R) = HPow.hPow (α := R) (↑a₁ : R) a₂ * (↑a₃ : R)

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_2
inst : CommRing R
⊢ Eq.{u_2 + 1} (α := R) (↑0 : R) 0

Tactic:
Int.cast_zero

Premises used: Int.cast_zero
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_2
inst : CommRing R
b₁ b₂ : R
a₁ a₂ : ℤ
h : (↑a₁ : R) = b₁
h_1 : (↑a₂ : R) = b₂
subst_vars : (↑(a₁ + a₂) : R) = HAdd.hAdd (α := R) (↑a₁ : R) (↑a₂ : R)
⊢ (↑(a₁ + a₂) : R) = b₁ + b₂

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_2
inst : CommRing R
a₁ a₂ : ℤ
⊢ (↑(a₁ + a₂) : R) = HAdd.hAdd (α := R) (↑a₁ : R) (↑a₂ : R)

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
α : Type u_2
inst : Mul α
a a' : α
h : a = a'
b : α
subst : a • b = a * b
⊢ a • b = a' * b

Tactic:
subst h
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
α : Type u_2
inst : Mul α
a b : α
⊢ a • b = a * b

Tactic:
rfl
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_1
inst : CommSemiring R
n n' : ℕ
r : R
hr : (↑n : R) = r
hn : n' = n
a : R
subst_vars : n' • a = (↑n' : R) * a
⊢ n' • a = r * a

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_1
inst : CommSemiring R
n' : ℕ
a : R
⊢ n' • a = (↑n' : R) * a

Tactic:
simp only [nsmul_eq_mul]

Premises used: nsmul_eq_mul
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_2
n n' : ℤ
r : R
inst : CommRing R
hr : (↑n : R) = r
hn : n' = n
a : R
subst_vars : n' • a = (↑n' : R) * a
⊢ n' • a = r * a

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
R : Type u_2
n' : ℤ
inst : CommRing R
a : R
⊢ n' • a = (↑n' : R) * a

Tactic:
simp only [zsmul_eq_mul]

Premises used: zsmul_eq_mul
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
u : Lean.Level
α_1 : Q(Type u)
sα : Q(CommSemiring «$α_1»)
R : Type u_1
inst : CommSemiring R
n a₁ a₂ a₃ : ℕ
b₁ b₂ b₃ : R
α β : Type u_2
inst_1 : CSLift α β
a : α
⊢ CSLiftVal a (CSLift.lift a)

Tactic:
⟨rfl⟩

Premises used: Mathlib.Tactic.Ring.CSLiftVal.mk, rfl
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
α β : Type u_2
inst : CSLift α β
a b : α
a' b' : β
h1 : CSLiftVal a a'
h2 : CSLiftVal b b'
h : a' = b'
rwa : a' = CSLift.lift b
rwa₁ rwa₂ rwa₃ rwa₄ : a' = b'
⊢ CSLift.lift a = CSLift.lift b

Tactic:
rwa [← h1.1, ← h2.1]

Premises used: Mathlib.Tactic.Ring.CSLiftVal.eq
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
α : Sort u_2
a b c : α
h : a = c
h_1 : b = c
subst_vars : c = c
⊢ a = b

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Basic
Goal:
α : Sort u_2
c : α
⊢ c = c

Tactic:
rfl
-- Module: Mathlib.Tactic.Ring.Common
Goal:
u_1 u : Lean.Level
α : Q(Type u)
BaseType : Q(«$α») → Type
inst : ∀ (e : Q(«$α»)), Nonempty (BaseType e)
sα : Q(CommSemiring «$α»)
⊢ Nonempty (RingCompute BaseType sα)

Tactic:
⟨{
  eq := default
  compare := default
  add := default
  mul := default
  cast _ _ _ _ _ _ := do return ⟨_, .zero (BaseType := BaseType) (sα := sα), default⟩
  neg := default
  pow := default
  inv := default
  derive := default
  isOne := default
  one :=
    have (e : Q($α)) : Inhabited (BaseType e) := Classical.inhabited_of_nonempty'
    default
}⟩

Premises used: Pure.pure, Inhabited.default, Mathlib.Tactic.Ring.Common.RingCompute.mk, Mathlib.Tactic.Ring.Common.RingCompare.mk, Lean.Expr.const, Classical.inhabited_of_nonempty', Prod.mk, Nonempty.intro, List.cons, Lean.Literal.natVal, Mathlib.Tactic.Ring.Common.ExSum.zero, Lean.Name.mkStr2, Lean.Expr.app, Sigma.mk, Lean.Name.mkStr1, Lean.Expr.lit, List.nil
-- Module: Mathlib.Tactic.Ring.Common
Goal:
«$u_1» «$u» : Lean.Level
«$α» : Type u
«$sα» : CommSemiring «$α»
«$a» : «$α»
«$b» : ℕ
«$expr» : «$α»
«$pf» : Nat.rawCast 1 = «$expr»
rw rw₁ : «$a» ^ «$b» * Nat.rawCast 1 = «$a» ^ «$b» * Nat.rawCast 1
⊢ «$a» ^ «$b» * Nat.rawCast 1 = «$a» ^ «$b» * «$expr»

Tactic:
rw [← $pf]
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a b c x : R
e : ℕ
pq_pf : a + b = c
subst_vars : x ^ e * a + x ^ e * b = x ^ e * (a + b)
⊢ x ^ e * a + x ^ e * b = x ^ e * c

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a b x : R
e : ℕ
⊢ x ^ e * a + x ^ e * b = x ^ e * (a + b)

Tactic:
simp [mul_add]

Premises used: mul_add
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a b x : R
e : ℕ
h : a + b = (↑0 : R)
⊢ x ^ e * a + x ^ e * b = (↑0 : R)

Tactic:
simp [h, ← mul_add]

Premises used: mul_add
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
b : R
⊢ 0 + b = b

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a : R
⊢ a + 0 = a

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a₁ a₂ b₁ b₂ c₁ c₂ : R
h : a₁ + b₁ = c₁
h_1 : a₂ + b₂ = c₂
subst_vars : a₁ + a₂ + (b₁ + b₂) = a₁ + b₁ + (a₂ + b₂)
⊢ a₁ + a₂ + (b₁ + b₂) = c₁ + c₂

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a₁ a₂ b₁ b₂ : R
⊢ a₁ + a₂ + (b₁ + b₂) = a₁ + b₁ + (a₂ + b₂)

Tactic:
simp [add_assoc, add_left_comm]

Premises used: add_left_comm, add_assoc
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a₁ a₂ b₁ b₂ c : R
h : IsNat (a₁ + b₁) 0
h₄ : a₂ + b₂ = c
subst_vars : a₁ + a₂ + (b₁ + b₂) = a₂ + b₂
⊢ a₁ + a₂ + (b₁ + b₂) = c

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a₁ a₂ b₁ b₂ : R
h : IsNat (a₁ + b₁) 0
rw : a₁ + b₁ + (a₂ + b₂) = a₂ + b₂
rw₁ : (↑0 : R) + (a₂ + b₂) = a₂ + b₂
rw₂ : 0 + (a₂ + b₂) = a₂ + b₂
rw₃ rw₄ : a₂ + b₂ = a₂ + b₂
⊢ a₁ + a₂ + (b₁ + b₂) = a₂ + b₂

Tactic:
rw [add_add_add_comm, h.1, Nat.cast_zero, add_pf_zero_add]

Premises used: add_add_add_comm, Nat.cast_zero, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a₂ b c a₁ : R
h : a₂ + b = c
⊢ a₁ + a₂ + b = a₁ + c

Tactic:
simp [*, add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a b₂ c b₁ : R
h : a + b₂ = c
subst_vars : a + (b₁ + b₂) = b₁ + (a + b₂)
⊢ a + (b₁ + b₂) = b₁ + c

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a b₂ b₁ : R
⊢ a + (b₁ + b₂) = b₁ + (a + b₂)

Tactic:
simp [add_left_comm]

Premises used: add_left_comm
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a : R
⊢ Nat.rawCast 1 * a = a

Tactic:
simp [Nat.rawCast]

Premises used: Nat.rawCast
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a : R
⊢ a * Nat.rawCast 1 = a

Tactic:
simp [Nat.rawCast]

Premises used: Nat.rawCast
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a₃ b c a₁ : R
a₂ : ℕ
h : a₃ * b = c
subst_vars : a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * (a₃ * b)
⊢ a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * c

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a₃ b a₁ : R
a₂ : ℕ
rw rw₁ : a₁ ^ a₂ * (a₃ * b) = a₁ ^ a₂ * (a₃ * b)
⊢ a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * (a₃ * b)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a b₃ c b₁ : R
b₂ : ℕ
h : a * b₃ = c
subst_vars : a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * (a * b₃)
⊢ a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * c

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a b₃ b₁ : R
b₂ : ℕ
rw rw₁ : b₁ ^ b₂ * (a * b₃) = b₁ ^ b₂ * (a * b₃)
⊢ a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * (a * b₃)

Tactic:
rw [mul_left_comm]

Premises used: mul_left_comm
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a₂ b₂ c : R
ea eb e : ℕ
x : R
h : ea + eb = e
h_1 : a₂ * b₂ = c
subst_vars : x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂)
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * c

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a₂ b₂ : R
ea eb : ℕ
x : R
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂)

Tactic:
simp [pow_add, mul_mul_mul_comm]

Premises used: mul_mul_mul_comm, pow_add
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a : R
⊢ a * 0 = 0

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a b₁ b₂ c₁ c₂ d : R
h : a * b₁ = c₁
h_1 : a * b₂ = c₂
h_2 : c₁ + 0 + c₂ = d
subst_vars : a * (b₁ + b₂) = a * b₁ + 0 + a * b₂
⊢ a * (b₁ + b₂) = d

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a b₁ b₂ : R
⊢ a * (b₁ + b₂) = a * b₁ + 0 + a * b₂

Tactic:
simp [_root_.mul_add]

Premises used: mul_add
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
b : R
⊢ 0 * b = 0

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a₁ a₂ b c₁ c₂ d : R
h : a₁ * b = c₁
h_1 : a₂ * b = c₂
h_2 : c₁ + c₂ = d
subst_vars : (a₁ + a₂) * b = a₁ * b + a₂ * b
⊢ (a₁ + a₂) * b = d

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a₁ a₂ b : R
⊢ (a₁ + a₂) * b = a₁ * b + a₂ * b

Tactic:
simp [_root_.add_mul]

Premises used: add_mul
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : CommRing R
a b : R
h : -1 * a = b
subst_vars : -a = -1 * a
⊢ -a = b

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : CommRing R
a : R
⊢ -a = -1 * a

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : CommRing R
a₁ : R
a₂ : ℕ
a₃ b : R
h : -a₃ = b
subst_vars : -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * -a₃
⊢ -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * b

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : CommRing R
a₁ : R
a₂ : ℕ
a₃ : R
⊢ -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * -a₃

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : CommRing R
⊢ Eq.{u_2 + 1} (α := R) (-0) 0

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : CommRing R
a₁ a₂ b₁ b₂ : R
h : -a₁ = b₁
h_1 : -a₂ = b₂
subst_vars : -(a₁ + a₂) = -a₁ + -a₂
⊢ -(a₁ + a₂) = b₁ + b₂

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : CommRing R
a₁ a₂ : R
⊢ -(a₁ + a₂) = -a₁ + -a₂

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : CommRing R
a b c d : R
h : -b = c
h_1 : a + c = d
subst_vars : a - b = a + -b
⊢ a - b = d

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : CommRing R
a b : R
⊢ a - b = a + -b

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a : R
b : ℕ
e : R
h : (a + 0) ^ b * Nat.rawCast 1 = e
⊢ a ^ b = e

Tactic:
simp [← h]
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a : R
b : ℕ
e : R
h : a ^ b * Nat.rawCast 1 = e
⊢ a ^ b = e + 0

Tactic:
simp [← h]
-- Module: Mathlib.Tactic.Ring.Common
Goal:
n : ℕ
h : Nat.ble 1 n = true
⊢ LT.lt (α := ℕ) 0 n.rawCast

Tactic:
Nat.le_of_ble_eq_true h

Premises used: Nat.le_of_ble_eq_true, Nat.lt
-- Module: Mathlib.Tactic.Ring.Common
Goal:
a₁ a₂ n : ℕ
h₁ : 0 < a₁
h₂ : 0 < a₂
⊢ 0 < a₁ ^ n * a₂

Tactic:
Nat.mul_pos (Nat.pow_pos h₁) h₂

Premises used: Nat.mul_pos, Nat.pow_pos
-- Module: Mathlib.Tactic.Ring.Common
Goal:
a₁ a₂ : ℕ
h : 0 < a₁
⊢ 0 < a₁ + a₂

Tactic:
Nat.lt_of_lt_of_le h (Nat.le_add_right ..)

Premises used: Nat.le_add_right, Nat.lt_of_lt_of_le
-- Module: Mathlib.Tactic.Ring.Common
Goal:
a₂ a₁ : ℕ
h : 0 < a₂
⊢ 0 < a₁ + a₂

Tactic:
Nat.lt_of_lt_of_le h (Nat.le_add_left ..)

Premises used: Nat.le_add_left, Nat.lt_of_lt_of_le
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a : R
⊢ a ^ 1 = a

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a b c : R
k : ℕ
h : a ^ k = b
h_1 : b * b = c
subst_vars : a ^ Nat.mul 2 k = a ^ k * a ^ k
⊢ a ^ Nat.mul 2 k = c

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a : R
k : ℕ
⊢ a ^ Nat.mul 2 k = a ^ k * a ^ k

Tactic:
simp [Nat.succ_mul, pow_add]

Premises used: pow_add, Nat.succ_mul
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a b c : R
k : ℕ
d : R
h : a ^ k = b
h_1 : b * b = c
h_2 : c * a = d
subst_vars : a ^ (Nat.mul 2 k).add 1 = a ^ k * a ^ k * a
⊢ a ^ (Nat.mul 2 k).add 1 = d

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a : R
k : ℕ
⊢ a ^ (Nat.mul 2 k).add 1 = a ^ k * a ^ k * a

Tactic:
simp [Nat.succ_mul, pow_add]

Premises used: pow_add, Nat.succ_mul
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a : R
b : ℕ
ha : IsNat a 1
⊢ a ^ b = a

Tactic:
simp [ha.out]

Premises used: Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a₂ c₂ : R
ea₁ b c₁ : ℕ
xa₁ : R
h : ea₁ * b = c₁
h_1 : a₂ ^ b = c₂
subst_vars : (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * a₂ ^ b
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ c₁ * c₂

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a₂ : R
ea₁ b : ℕ
xa₁ : R
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * a₂ ^ b

Tactic:
simp [_root_.mul_pow, pow_mul]

Premises used: pow_mul, mul_pow