awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
b c : α
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
p : b ≤ c
a : α
ha : 0 ≤ a
⊢ b * a ≤ c * a

Tactic:
mul_le_mul_of_nonneg_right p ha

Premises used: mul_le_mul_of_nonneg_right
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
b c : α
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
p : b < c
a : α
ha : 0 < a
⊢ b * a < c * a

Tactic:
mul_lt_mul_of_pos_right p ha

Premises used: mul_lt_mul_of_pos_right
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
b c : α
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
p : b < c
a : α
ha : 0 ≤ a
⊢ b * a ≤ c * a

Tactic:
mul_le_mul_of_nonneg_right p.le ha

Premises used: LT.lt.le, mul_le_mul_of_nonneg_right
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
b c : α
inst : Mul α
p : b = c
a : α
⊢ a * b = a * c

Tactic:
p ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
b c : α
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
p : b ≤ c
a : α
ha : 0 ≤ a
⊢ a * b ≤ a * c

Tactic:
mul_le_mul_of_nonneg_left p ha

Premises used: mul_le_mul_of_nonneg_left
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
b c : α
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
p : b < c
a : α
ha : 0 < a
⊢ a * b < a * c

Tactic:
mul_lt_mul_of_pos_left p ha

Premises used: mul_lt_mul_of_pos_left
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
b c : α
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
p : b < c
a : α
ha : 0 ≤ a
⊢ a * b ≤ a * c

Tactic:
mul_le_mul_of_nonneg_left p.le ha

Premises used: LT.lt.le, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
K : Type u_2
t s : K
inst : SMul K α
p : t = s
c : α
⊢ t • c = s • c

Tactic:
p ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
K : Type u_2
t s : K
inst : Ring K
inst_1 : PartialOrder K
inst_2 : IsOrderedRing K
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
inst_6 : _root_.Module K α
inst_7 : IsOrderedModule K α
p : t ≤ s
a : α
ha : 0 ≤ a
⊢ t • a ≤ s • a

Tactic:
smul_le_smul_of_nonneg_right p ha

Premises used: smul_le_smul_of_nonneg_right
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
K : Type u_2
t s : K
inst : Ring K
inst_1 : PartialOrder K
inst_2 : IsOrderedRing K
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
inst_6 : _root_.Module K α
inst_7 : IsStrictOrderedModule K α
p : t < s
a : α
ha : 0 < a
⊢ t • a < s • a

Tactic:
smul_lt_smul_of_pos_right p ha

Premises used: smul_lt_smul_of_pos_right
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
K : Type u_2
t s : K
inst : Ring K
inst_1 : PartialOrder K
inst_2 : IsOrderedRing K
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
inst_6 : _root_.Module K α
inst_7 : IsStrictOrderedModule K α
p : t < s
a : α
ha : 0 ≤ a
⊢ t • a ≤ s • a

Tactic:
smul_le_smul_of_nonneg_right p.le ha

Premises used: smul_le_smul_of_nonneg_right, LT.lt.le
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
b c : α
K : Type u_2
inst : SMul K α
p : b = c
s : K
⊢ s • b = s • c

Tactic:
p ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
b c : α
K : Type u_2
inst : Semiring K
inst_1 : PartialOrder K
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : _root_.Module K α
inst_5 : PosSMulMono K α
p : b ≤ c
s : K
hs : 0 ≤ s
⊢ s • b ≤ s • c

Tactic:
smul_le_smul_of_nonneg_left p hs

Premises used: smul_le_smul_of_nonneg_left
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
b c : α
K : Type u_2
inst : Semiring K
inst_1 : PartialOrder K
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : _root_.Module K α
inst_5 : PosSMulStrictMono K α
p : b < c
s : K
hs : 0 < s
⊢ s • b < s • c

Tactic:
smul_lt_smul_of_pos_left p hs

Premises used: smul_lt_smul_of_pos_left
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
b c : α
K : Type u_2
inst : Semiring K
inst_1 : PartialOrder K
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : _root_.Module K α
inst_5 : PosSMulMono K α
p : b < c
s : K
hs : 0 ≤ s
⊢ s • b ≤ s • c

Tactic:
smul_le_smul_of_nonneg_left p.le hs

Premises used: LT.lt.le, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a b : α
inst : Div α
p : a = b
c : α
⊢ a / c = b / c

Tactic:
p ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
b c : α
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
p : b ≤ c
a : α
ha : 0 ≤ a
⊢ b / a ≤ c / a

Tactic:
div_le_div_of_nonneg_right p ha

Premises used: div_le_div_of_nonneg_right
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
b c : α
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
p : b < c
a : α
ha : 0 < a
⊢ b / a < c / a

Tactic:
div_lt_div_of_pos_right p ha

Premises used: div_lt_div_of_pos_right
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
b c : α
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
p : b < c
a : α
ha : 0 ≤ a
⊢ b / a ≤ c / a

Tactic:
div_le_div_of_nonneg_right p.le ha

Premises used: div_le_div_of_nonneg_right, LT.lt.le
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a a' b b' : α
inst : Add α
inst_1 : IsRightCancelAdd α
p : a = b
H : a' + b = b' + a
⊢ a' + b = b' + b

Tactic:
rw [p] at H
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a a' b b' : α
inst : Add α
inst_1 : IsRightCancelAdd α
p : a = b
H : a' + b = b' + b
⊢ a' = b'

Tactic:
add_right_cancel H

Premises used: add_right_cancel
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a a' b b' : α
inst : Add α
inst_1 : IsRightCancelAdd α
p : a = b
H : a' + b = b' + b
⊢ a' = b'

Tactic:
exact add_right_cancel H

Premises used: add_right_cancel
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a a' b b' : α
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
p : a ≤ b
H : a' + b ≤ b' + a
grw : a' + b ≤ b' + b
grw₁ : b' + a ≤ b' + b
grw₂ grw₃ : b' + b ≤ b' + b
⊢ a' ≤ b'

Tactic:
grw [← add_le_add_iff_right b, H, p]

Premises used: add_le_add_iff_right
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a a' b b' : α
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
p : a = b
H : a' + b ≤ b' + a
rwa : ∀ (H : a' + b ≤ b' + b), a' ≤ b'
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (H : a' ≤ b'), a' ≤ b'
⊢ a' ≤ b'

Tactic:
rwa [p, add_le_add_iff_right] at H

Premises used: add_le_add_iff_right
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a a' b b' : α
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
p : a < b
H : a' + b ≤ b' + a
⊢ a' ≤ b'

Tactic:
le_of_le p.le H

Premises used: LT.lt.le, Mathlib.Tactic.LinearCombination.le_of_le
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a a' b b' : α
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
p : a ≤ b
H : a' + b < b' + a
⊢ a' + b < b' + b

Tactic:
grw [p] at H
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a a' b b' : α
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
p : a ≤ b
H : a' + b < b' + b
⊢ a' < b'

Tactic:
simpa using H
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a a' b b' : α
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
p : a = b
H : a' + b < b' + a
rwa : ∀ (H : a' + b < b' + b), a' < b'
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (H : a' < b'), a' < b'
⊢ a' < b'

Tactic:
rwa [p, add_lt_add_iff_right] at H

Premises used: add_lt_add_iff_right
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a a' b b' : α
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
p : a < b
H : a' + b ≤ b' + a
grw : b' + a < b' + b
⊢ a' < b'

Tactic:
grw [← add_lt_add_iff_right b, H]

Premises used: add_lt_add_iff_right
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a a' b b' : α
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
p : a < b
H : a' + b ≤ b' + a
⊢ b' + a < b' + b

Tactic:
gcongr
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_3
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b : α
h : a - b ≤ 0
⊢ a ≤ b

Tactic:
sub_nonpos.mp h

Premises used: Iff.mp, sub_nonpos
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_3
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
a b : α
h : a - b < 0
⊢ a < b

Tactic:
sub_neg.mp h

Premises used: sub_neg, Iff.mp
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a a' b b' : α
inst : Ring α
inst_1 : NoZeroDivisors α
n : ℕ
p : a = b
H : (a' - b') ^ n - (a - b) = 0
rw : ∀ (p : a - b = 0) (H : (a' - b') ^ n - (a - b) = 0), a' - b' = 0
⊢ a' = b'

Tactic:
rw [← sub_eq_zero] at p ⊢

Premises used: sub_eq_zero
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a a' b b' : α
inst : Ring α
inst_1 : NoZeroDivisors α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n - (a - b) = 0
apply : (a' - b') ^ n = 0
⊢ a' - b' = 0

Tactic:
apply eq_zero_of_pow_eq_zero (n := n)

Premises used: eq_zero_of_pow_eq_zero
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a a' b b' : α
inst : Ring α
inst_1 : NoZeroDivisors α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n - (a - b) = 0
rwa : ∀ (H : (a' - b') ^ n = a - b), (a' - b') ^ n = 0
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (H : (a' - b') ^ n = 0), (a' - b') ^ n = 0
⊢ (a' - b') ^ n = 0

Tactic:
rwa [sub_eq_zero, p] at H

Premises used: sub_eq_zero
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
a b : α
inst : Add α
p : a = b
c : α
⊢ a + c = b + c

Tactic:
p ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
b c : α
inst : Add α
p : b = c
a : α
⊢ a + b = a + c

Tactic:
p ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
a₁ a₂ b₁ b₂ : α
inst : Add α
p₁ : a₁ = b₁
p₂ : a₂ = b₂
⊢ a₁ + a₂ = b₁ + b₂

Tactic:
p₁ ▸ p₂ ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
a b : α
inst : Sub α
p : a = b
c : α
⊢ a - c = b - c

Tactic:
p ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
b c : α
inst : Sub α
p : b = c
a : α
⊢ a - b = a - c

Tactic:
p ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
a₁ a₂ b₁ b₂ : α
inst : Sub α
p₁ : a₁ = b₁
p₂ : a₂ = b₂
⊢ a₁ - a₂ = b₁ - b₂

Tactic:
p₁ ▸ p₂ ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
a b : α
inst : Neg α
p : a = b
⊢ -a = -b

Tactic:
p ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
a b : α
inst : Mul α
p : a = b
c : α
⊢ a * c = b * c

Tactic:
p ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
b c : α
inst : Mul α
p : b = c
a : α
⊢ a * b = a * c

Tactic:
p ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
a₁ a₂ b₁ b₂ : α
inst : Mul α
p₁ : a₁ = b₁
p₂ : a₂ = b₂
⊢ a₁ * a₂ = b₁ * b₂

Tactic:
p₁ ▸ p₂ ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
a b : α
inst : Inv α
p : a = b
⊢ a⁻¹ = b⁻¹

Tactic:
p ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
a b : α
inst : Div α
p : a = b
c : α
⊢ a / c = b / c

Tactic:
p ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
b c : α
inst : Div α
p : b = c
a : α
⊢ a / b = a / c

Tactic:
p ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
a₁ a₂ b₁ b₂ : α
inst : Div α
p₁ : a₁ = b₁
p₂ : a₂ = b₂
⊢ a₁ / a₂ = b₁ / b₂

Tactic:
p₁ ▸ p₂ ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
a a' b b' : α
p : a = b
p₁ : a = a'
p₂ : b = b'
⊢ a' = b'

Tactic:
p₁ ▸ p₂ ▸ p

Premises used: Eq.rec
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
a a' b b' : α
inst : AddGroup α
p : a = b
H : a' - b' - (a - b) = 0
rw : ∀ (p : a - b = 0) (H : a' - b' - (a - b) = 0), a' - b' = 0
⊢ a' = b'

Tactic:
rw [← sub_eq_zero] at p ⊢

Premises used: sub_eq_zero
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
a a' b b' : α
inst : AddGroup α
p : a - b = 0
H : a' - b' - (a - b) = 0
rwa : ∀ (H : a' - b' = a - b), a' - b' = 0
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (H : a' - b' = 0), a' - b' = 0
⊢ a' - b' = 0

Tactic:
rwa [sub_eq_zero, p] at H

Premises used: sub_eq_zero
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
a a' b b' : α
inst : Ring α
inst_1 : NoZeroDivisors α
n : ℕ
p : a = b
H : (a' - b') ^ n - (a - b) = 0
rw : ∀ (p : a - b = 0) (H : (a' - b') ^ n - (a - b) = 0), a' - b' = 0
⊢ a' = b'

Tactic:
rw [← sub_eq_zero] at p ⊢

Premises used: sub_eq_zero
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
a a' b b' : α
inst : Ring α
inst_1 : NoZeroDivisors α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n - (a - b) = 0
apply : (a' - b') ^ n = 0
⊢ a' - b' = 0

Tactic:
apply eq_zero_of_pow_eq_zero (n := n)

Premises used: eq_zero_of_pow_eq_zero
-- Module: Mathlib.Tactic.LinearCombinationPrime
Goal:
α : Type u_1
a a' b b' : α
inst : Ring α
inst_1 : NoZeroDivisors α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n - (a - b) = 0
rwa : ∀ (H : (a' - b') ^ n = a - b), (a' - b') ^ n = 0
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (H : (a' - b') ^ n = 0), (a' - b') ^ n = 0
⊢ (a' - b') ^ n = 0

Tactic:
rwa [sub_eq_zero, p] at H

Premises used: sub_eq_zero
-- Module: Mathlib.Tactic.ModCases
Goal:
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ LT.lt (α := ℤ) 0 (↑n : ℤ)

Tactic:
have := natCast_pos.2 <| Nat.le_of_ble_eq_true hn
-- Module: Mathlib.Tactic.ModCases
Goal:
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : LT.lt (α := ℤ) 0 (↑n : ℤ)
⊢ 0 ≤ a % (↑n : ℤ)

Tactic:
have nonneg := emod_nonneg a <| Int.ne_of_gt this
-- Module: Mathlib.Tactic.ModCases
Goal:
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : LT.lt (α := ℤ) 0 (↑n : ℤ)
nonneg : 0 ≤ a % (↑n : ℤ)
⊢ 0 ≤ (a % (↑n : ℤ)).toNat ∧ (a % (↑n : ℤ)).toNat < n ∧ a ≡ (↑(a % (↑n : ℤ)).toNat : ℤ) [ZMOD (↑n : ℤ)]

Tactic:
⟨Nat.zero_le _, ?_, ?_⟩

Premises used: Nat.zero_le, And.intro
-- Module: Mathlib.Tactic.ModCases
Goal:
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : LT.lt (α := ℤ) 0 (↑n : ℤ)
nonneg : 0 ≤ a % (↑n : ℤ)
refine_1 : (a % (↑n : ℤ)).toNat < n
refine_2 : a ≡ (↑(a % (↑n : ℤ)).toNat : ℤ) [ZMOD (↑n : ℤ)]
⊢ 0 ≤ (a % (↑n : ℤ)).toNat ∧ (a % (↑n : ℤ)).toNat < n ∧ a ≡ (↑(a % (↑n : ℤ)).toNat : ℤ) [ZMOD (↑n : ℤ)]

Tactic:
refine ⟨Nat.zero_le _, ?_, ?_⟩
-- Module: Mathlib.Tactic.ModCases
Goal:
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : LT.lt (α := ℤ) 0 (↑n : ℤ)
nonneg : 0 ≤ a % (↑n : ℤ)
refine_1 : a % (↑n : ℤ) < (↑n : ℤ)
⊢ (a % (↑n : ℤ)).toNat < n

Tactic:
rw [Int.toNat_lt nonneg]

Premises used: Int.toNat_lt
-- Module: Mathlib.Tactic.ModCases
Goal:
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : LT.lt (α := ℤ) 0 (↑n : ℤ)
nonneg : 0 ≤ a % (↑n : ℤ)
⊢ a % (↑n : ℤ) < (↑n : ℤ)

Tactic:
Int.emod_lt_of_pos _ this

Premises used: Int.emod_lt_of_pos
-- Module: Mathlib.Tactic.ModCases
Goal:
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : LT.lt (α := ℤ) 0 (↑n : ℤ)
nonneg : 0 ≤ a % (↑n : ℤ)
⊢ a % (↑n : ℤ) < (↑n : ℤ)

Tactic:
exact Int.emod_lt_of_pos _ this

Premises used: Int.emod_lt_of_pos
-- Module: Mathlib.Tactic.ModCases
Goal:
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : LT.lt (α := ℤ) 0 (↑n : ℤ)
nonneg : 0 ≤ a % (↑n : ℤ)
refine_2 : a % (↑n : ℤ) = HMod.hMod (α := ℤ) (↑(a % (↑n : ℤ)).toNat : ℤ) (↑n : ℤ)
refine_2₁ : a % (↑n : ℤ) = a % (↑n : ℤ) % (↑n : ℤ)
refine_2₂ refine_2₃ : a % (↑n : ℤ) = a % (↑n : ℤ)
⊢ a ≡ (↑(a % (↑n : ℤ)).toNat : ℤ) [ZMOD (↑n : ℤ)]

Tactic:
rw [Int.ModEq, Int.toNat_of_nonneg nonneg, emod_emod]

Premises used: Int.toNat_of_nonneg, Int.ModEq, Int.emod_emod
-- Module: Mathlib.Tactic.ModCases
Goal:
p : Sort u_1
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ 0 ≤ a % n ∧ a % n < n ∧ a ≡ a % n [MOD n]

Tactic:
⟨Nat.zero_le _, ?_, ?_⟩

Premises used: Nat.zero_le, And.intro
-- Module: Mathlib.Tactic.ModCases
Goal:
p : Sort u_1
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
refine_1 : a % n < n
refine_2 : a ≡ a % n [MOD n]
⊢ 0 ≤ a % n ∧ a % n < n ∧ a ≡ a % n [MOD n]

Tactic:
refine ⟨Nat.zero_le _, ?_, ?_⟩
-- Module: Mathlib.Tactic.ModCases
Goal:
p : Sort u_1
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ a % n < n

Tactic:
Nat.mod_lt _ (Nat.le_of_ble_eq_true hn)

Premises used: Nat.le_of_ble_eq_true, Nat.mod_lt
-- Module: Mathlib.Tactic.ModCases
Goal:
p : Sort u_1
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ a % n < n

Tactic:
exact Nat.mod_lt _ (Nat.le_of_ble_eq_true hn)

Premises used: Nat.le_of_ble_eq_true, Nat.mod_lt
-- Module: Mathlib.Tactic.ModCases
Goal:
p : Sort u_1
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
refine_2 : a % n = a % n % n
refine_2₁ refine_2₂ : a % n = a % n
⊢ a ≡ a % n [MOD n]

Tactic:
rw [Nat.ModEq, Nat.mod_mod]

Premises used: Nat.mod_mod, Nat.ModEq
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : AddMonoid M
inst_1 : SMul R M
p : R × M
l : NF R M
⊢ (p ::ᵣ l).eval = p.1 • p.2 + l.eval

Tactic:
rfl
-- Module: Mathlib.Tactic.Module
Goal:
M : Type u_3
inst : AddMonoid M
x : M
⊢ x = eval (R := ℕ) [(1, x)]

Tactic:
simp [eval]

Premises used: Mathlib.Tactic.Module.NF.eval
-- Module: Mathlib.Tactic.Module
Goal:
M : Type u_3
inst : AddMonoid M
⊢ Eq.{u_3 + 1} (α := M) 0 (eval (R := ℕ) [])

Tactic:
rfl

Premises used: List.sum, Mathlib.Tactic.Module.NF.eval, List.foldr, rfl
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : AddMonoid M
inst_1 : SMul R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : l₁.eval + (a₂ ::ᵣ l₂).eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval + (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval

Tactic:
simp only [eval_cons, ← h, add_assoc]

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

Tactic:
simp only [← h, eval_cons, add_smul, add_assoc]

Premises used: add_assoc, add_smul, Mathlib.Tactic.Module.NF.eval_cons
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid 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 : Semiring R
inst_1 : AddCommMonoid 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 : Semiring R
inst_1 : AddCommMonoid 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 : Semiring R
inst_1 : AddCommMonoid 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 : Semiring R
inst_1 : AddCommMonoid 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₂ ::ᵣ l).eval

Tactic:
simp only [eval_cons, ← h]

Premises used: Mathlib.Tactic.Module.NF.eval_cons
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval + l₂.eval = l.eval
nth_rw : a₁.1 • a₁.2 + l₁.eval + (a₂.1 • a₂.2 + l₂.eval) = a₁.1 • a₁.2 + l₁.eval + 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 + l₁.eval + l₂.eval)

Tactic:
nth_rw 4 [add_comm]

Premises used: add_comm
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid 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 + (l₁.eval + (l₂.eval + a₂.1 • a₂.2))
⊢ a₁.1 • a₁.2 + l₁.eval + (a₂.1 • a₂.2 + l₂.eval) = a₁.1 • a₁.2 + l₁.eval + l₂.eval + a₂.1 • a₂.2

Tactic:
simp only [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid 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 = l₂.eval + a₂.1 • a₂.2
⊢ a₁.1 • a₁.2 + (l₁.eval + (a₂.1 • a₂.2 + l₂.eval)) = a₁.1 • a₁.2 + (l₁.eval + (l₂.eval + a₂.1 • a₂.2))

Tactic:
congr! 2
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid 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₁ h₂ : l₂.eval + a₂.1 • a₂.2 = l₂.eval + a₂.1 • a₂.2
⊢ a₂.1 • a₂.2 + l₂.eval = l₂.eval + a₂.1 • a₂.2

Tactic:
rw [add_comm]

Premises used: add_comm
-- 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₂ 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 = 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₄ rw₅ : l.eval = l.eval
⊢ x₁ + x₂ = l.eval

Tactic:
rw [hx₁, hx₂, ← h₁, ← h₂, h]
-- Module: Mathlib.Tactic.Module
Goal:
R : Type u_2
M : Type u_3
inst : SMul R M
inst_1 : AddGroup M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : l₁.eval - (a₂ ::ᵣ l₂).eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval - (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval

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

Premises used: add_assoc, sub_eq_add_neg, 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
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
simp : r₁ • x + (l₁.eval + (-(r₂ • x) + -l₂.eval)) = r₁ • x + (-(r₂ • x) + (l₁.eval + -l₂.eval))
⊢ ((r₁, x) ::ᵣ l₁).eval - ((r₂, x) ::ᵣ l₂).eval = ((r₁ - r₂, x) ::ᵣ l).eval

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

Premises used: neg_smul, add_assoc, sub_eq_add_neg, neg_add, add_smul, Mathlib.Tactic.Module.NF.eval_cons