awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.LinearCombination.Lemmas (goal)
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'
⊢ a' ≤ b'
have rwa₁ : ∀ (H : a' ≤ b'), a' ≤ b'
Tactic: rwa [p, add_le_add_iff_right] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Tactic.LinearCombination.Lemmas (hypothesis)
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'
have H₁ : a' + b < b' + b
Tactic: grw [p] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Tactic.LinearCombination.Lemmas (goal)
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'
have rwa : ∀ (H : a' + b < b' + b), a' < b'
Tactic: rwa [p, add_lt_add_iff_right] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Tactic.LinearCombination.Lemmas (goal)
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'
⊢ a' < b'
have rwa₁ : ∀ (H : a' < b'), a' < b'
Tactic: rwa [p, add_lt_add_iff_right] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Tactic.LinearCombination.Lemmas (goal)
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'
have grw : b' + a < b' + b
Tactic: grw [← add_lt_add_iff_right b, H]
-- Lean 4 proof step from Mathlib.Tactic.LinearCombination.Lemmas (goal)
Goal:
α : Type u_1
a a' b b' : α
inst : Ring α
inst_1 : NoZeroDivisors α
n : ℕ
p : a = b
H : (a' - b') ^ n - (a - b) = 0
⊢ a' = b'
have rw : ∀ (p : a - b = 0) (H : (a' - b') ^ n - (a - b) = 0), a' - b' = 0
Tactic: rw [← sub_eq_zero] at p ⊢
Cleared hypotheses: p, H
-- Lean 4 proof step from Mathlib.Tactic.LinearCombination.Lemmas (goal)
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
⊢ a' - b' = 0
have apply : (a' - b') ^ n = 0
Tactic: apply eq_zero_of_pow_eq_zero (n := n)
-- Lean 4 proof step from Mathlib.Tactic.LinearCombination.Lemmas (goal)
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
⊢ (a' - b') ^ n = 0
have rwa : ∀ (H : (a' - b') ^ n = a - b), (a' - b') ^ n = 0
Tactic: rwa [sub_eq_zero, p] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Tactic.LinearCombination.Lemmas (goal)
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
⊢ (a' - b') ^ n = 0
have rwa₁ : ∀ (H : (a' - b') ^ n = 0), (a' - b') ^ n = 0
Tactic: rwa [sub_eq_zero, p] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Tactic.LinearCombinationPrime (goal)
Goal:
α : Type u_1
a a' b b' : α
inst : AddGroup α
p : a = b
H : a' - b' - (a - b) = 0
⊢ a' = b'
have rw : ∀ (p : a - b = 0) (H : a' - b' - (a - b) = 0), a' - b' = 0
Tactic: rw [← sub_eq_zero] at p ⊢
Cleared hypotheses: p, H
-- Lean 4 proof step from Mathlib.Tactic.LinearCombinationPrime (goal)
Goal:
α : Type u_1
a a' b b' : α
inst : AddGroup α
p : a - b = 0
H : a' - b' - (a - b) = 0
⊢ a' - b' = 0
have rwa : ∀ (H : a' - b' = a - b), a' - b' = 0
Tactic: rwa [sub_eq_zero, p] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Tactic.LinearCombinationPrime (goal)
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
⊢ a' - b' = 0
have rwa₁ : ∀ (H : a' - b' = 0), a' - b' = 0
Tactic: rwa [sub_eq_zero, p] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Tactic.LinearCombinationPrime (goal)
Goal:
α : Type u_1
a a' b b' : α
inst : Ring α
inst_1 : NoZeroDivisors α
n : ℕ
p : a = b
H : (a' - b') ^ n - (a - b) = 0
⊢ a' = b'
have rw : ∀ (p : a - b = 0) (H : (a' - b') ^ n - (a - b) = 0), a' - b' = 0
Tactic: rw [← sub_eq_zero] at p ⊢
Cleared hypotheses: p, H
-- Lean 4 proof step from Mathlib.Tactic.LinearCombinationPrime (goal)
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
⊢ a' - b' = 0
have apply : (a' - b') ^ n = 0
Tactic: apply eq_zero_of_pow_eq_zero (n := n)
-- Lean 4 proof step from Mathlib.Tactic.LinearCombinationPrime (goal)
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
⊢ (a' - b') ^ n = 0
have rwa : ∀ (H : (a' - b') ^ n = a - b), (a' - b') ^ n = 0
Tactic: rwa [sub_eq_zero, p] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Tactic.LinearCombinationPrime (goal)
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
⊢ (a' - b') ^ n = 0
have rwa₁ : ∀ (H : (a' - b') ^ n = 0), (a' - b') ^ n = 0
Tactic: rwa [sub_eq_zero, p] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Tactic.ModCases (hypothesis)
Goal:
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ 0 ≤ (a % (↑n : ℤ)).toNat ∧ (a % (↑n : ℤ)).toNat < n ∧ a ≡ (↑(a % (↑n : ℤ)).toNat : ℤ) [ZMOD (↑n : ℤ)]
have this : LT.lt (α := ℤ) 0 (↑n : ℤ)
Tactic: have := natCast_pos.2 <| Nat.le_of_ble_eq_true hn
-- Lean 4 proof step from Mathlib.Tactic.ModCases (hypothesis)
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 : ℤ)).toNat ∧ (a % (↑n : ℤ)).toNat < n ∧ a ≡ (↑(a % (↑n : ℤ)).toNat : ℤ) [ZMOD (↑n : ℤ)]
have nonneg : 0 ≤ a % (↑n : ℤ)
Tactic: have nonneg := emod_nonneg a <| Int.ne_of_gt this
-- Lean 4 proof step from Mathlib.Tactic.ModCases (goal)
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 : ℤ)]
have refine_1 : (a % (↑n : ℤ)).toNat < n
Tactic: refine ⟨Nat.zero_le _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Tactic.ModCases (goal)
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
⊢ 0 ≤ (a % (↑n : ℤ)).toNat ∧ (a % (↑n : ℤ)).toNat < n ∧ a ≡ (↑(a % (↑n : ℤ)).toNat : ℤ) [ZMOD (↑n : ℤ)]
have refine_2 : a ≡ (↑(a % (↑n : ℤ)).toNat : ℤ) [ZMOD (↑n : ℤ)]
Tactic: refine ⟨Nat.zero_le _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Tactic.ModCases (goal)
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 : ℤ)).toNat < n
have refine_1 : a % (↑n : ℤ) < (↑n : ℤ)
Tactic: rw [Int.toNat_lt nonneg]
-- Lean 4 proof step from Mathlib.Tactic.ModCases (goal)
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 ≡ (↑(a % (↑n : ℤ)).toNat : ℤ) [ZMOD (↑n : ℤ)]
have refine_2 : a % (↑n : ℤ) = HMod.hMod (α := ℤ) (↑(a % (↑n : ℤ)).toNat : ℤ) (↑n : ℤ)
Tactic: rw [Int.ModEq, Int.toNat_of_nonneg nonneg, emod_emod]
-- Lean 4 proof step from Mathlib.Tactic.ModCases (goal)
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 : ℤ)
⊢ a ≡ (↑(a % (↑n : ℤ)).toNat : ℤ) [ZMOD (↑n : ℤ)]
have refine_2₁ : a % (↑n : ℤ) = a % (↑n : ℤ) % (↑n : ℤ)
Tactic: rw [Int.ModEq, Int.toNat_of_nonneg nonneg, emod_emod]
-- Lean 4 proof step from Mathlib.Tactic.ModCases (goal)
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 : ℤ)
⊢ a ≡ (↑(a % (↑n : ℤ)).toNat : ℤ) [ZMOD (↑n : ℤ)]
have refine_2₂ : a % (↑n : ℤ) = a % (↑n : ℤ)
Tactic: rw [Int.ModEq, Int.toNat_of_nonneg nonneg, emod_emod]
-- Lean 4 proof step from Mathlib.Tactic.ModCases (goal)
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]
have refine_1 : a % n < n
Tactic: refine ⟨Nat.zero_le _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Tactic.ModCases (goal)
Goal:
p : Sort u_1
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
refine_1 : a % n < n
⊢ 0 ≤ a % n ∧ a % n < n ∧ a ≡ a % n [MOD n]
have refine_2 : a ≡ a % n [MOD n]
Tactic: refine ⟨Nat.zero_le _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Tactic.ModCases (goal)
Goal:
p : Sort u_1
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ a ≡ a % n [MOD n]
have refine_2 : a % n = a % n % n
Tactic: rw [Nat.ModEq, Nat.mod_mod]
-- Lean 4 proof step from Mathlib.Tactic.ModCases (goal)
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
⊢ a ≡ a % n [MOD n]
have refine_2₁ : a % n = a % n
Tactic: rw [Nat.ModEq, Nat.mod_mod]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ ((r₁, x) ::ᵣ l₁).eval + ((r₂, x) ::ᵣ l₂).eval = ((r₁ + r₂, x) ::ᵣ l).eval
have simp : r₁ • x + (l₁.eval + (r₂ • x + l₂.eval)) = r₁ • x + (r₂ • x + (l₁.eval + l₂.eval))
Tactic: simp only [← h, eval_cons, add_smul, add_assoc]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ r₁ • x + (l₁.eval + (r₂ • x + l₂.eval)) = r₁ • x + (r₂ • x + (l₁.eval + l₂.eval))
have h₁ : l₁.eval + (r₂ • x + l₂.eval) = r₂ • x + (l₁.eval + l₂.eval)
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ l₁.eval + (r₂ • x + l₂.eval) = r₂ • x + (l₁.eval + l₂.eval)
have h₁ : l₁.eval + r₂ • x + l₂.eval = r₂ • x + l₁.eval + l₂.eval
Tactic: simp only [← add_assoc]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ l₁.eval + r₂ • x + l₂.eval = r₂ • x + l₁.eval + l₂.eval
have h₁ : l₁.eval + r₂ • x = r₂ • x + l₁.eval
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ l₁.eval + r₂ • x = r₂ • x + l₁.eval
have h₁ : r₂ • x + l₁.eval = r₂ • x + l₁.eval
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ (a₁ ::ᵣ l₁).eval + (a₂ ::ᵣ l₂).eval = (a₂ ::ᵣ l).eval
have 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)
Tactic: simp only [eval_cons, ← h]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ a₁.1 • a₁.2 + l₁.eval + (a₂.1 • a₂.2 + l₂.eval) = a₂.1 • a₂.2 + (a₁.1 • a₁.2 + l₁.eval + l₂.eval)
have 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
Tactic: nth_rw 4 [add_comm]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ a₁.1 • a₁.2 + l₁.eval + (a₂.1 • a₂.2 + l₂.eval) = a₁.1 • a₁.2 + l₁.eval + l₂.eval + a₂.1 • a₂.2
have 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))
Tactic: simp only [add_assoc]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ a₁.1 • a₁.2 + (l₁.eval + (a₂.1 • a₂.2 + l₂.eval)) = a₁.1 • a₁.2 + (l₁.eval + (l₂.eval + a₂.1 • a₂.2))
have h₁ : a₂.1 • a₂.2 + l₂.eval = l₂.eval + a₂.1 • a₂.2
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ a₂.1 • a₂.2 + l₂.eval = l₂.eval + a₂.1 • a₂.2
have h₁ : l₂.eval + a₂.1 • a₂.2 = l₂.eval + a₂.1 • a₂.2
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ x₁ + x₂ = l.eval
have rw : l₁'.eval + x₂ = l.eval
Tactic: rw [hx₁, hx₂, ← h₁, ← h₂, h]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ x₁ + x₂ = l.eval
have rw₁ : l₁'.eval + l₂'.eval = l.eval
Tactic: rw [hx₁, hx₂, ← h₁, ← h₂, h]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ x₁ + x₂ = l.eval
have rw₂ : l₁.eval + l₂'.eval = l.eval
Tactic: rw [hx₁, hx₂, ← h₁, ← h₂, h]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ x₁ + x₂ = l.eval
have rw₄ : l.eval = l.eval
Tactic: rw [hx₁, hx₂, ← h₁, ← h₂, h]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ ((r₁, x) ::ᵣ l₁).eval - ((r₂, x) ::ᵣ l₂).eval = ((r₁ - r₂, x) ::ᵣ l).eval
have simp : r₁ • x + (l₁.eval + (-(r₂ • x) + -l₂.eval)) = r₁ • x + (-(r₂ • x) + (l₁.eval + -l₂.eval))
Tactic: simp only [← h, eval_cons, sub_eq_add_neg, neg_add, add_smul, neg_smul, add_assoc]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ r₁ • x + (l₁.eval + (-(r₂ • x) + -l₂.eval)) = r₁ • x + (-(r₂ • x) + (l₁.eval + -l₂.eval))
have h₁ : l₁.eval + (-(r₂ • x) + -l₂.eval) = -(r₂ • x) + (l₁.eval + -l₂.eval)
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ l₁.eval + (-(r₂ • x) + -l₂.eval) = -(r₂ • x) + (l₁.eval + -l₂.eval)
have h₁ : l₁.eval + -(r₂ • x) + -l₂.eval = -(r₂ • x) + l₁.eval + -l₂.eval
Tactic: simp only [← add_assoc]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ l₁.eval + -(r₂ • x) + -l₂.eval = -(r₂ • x) + l₁.eval + -l₂.eval
have h₁ : l₁.eval + -(r₂ • x) = -(r₂ • x) + l₁.eval
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ l₁.eval + -(r₂ • x) = -(r₂ • x) + l₁.eval
have h₁ : -(r₂ • x) + l₁.eval = -(r₂ • x) + l₁.eval
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ (a₁ ::ᵣ l₁).eval - (a₂ ::ᵣ l₂).eval = ((-a₂.1, a₂.2) ::ᵣ l).eval
have 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
Tactic: simp only [eval_cons, neg_smul, neg_add, sub_eq_add_neg, ← h, ← add_assoc]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ a₁.1 • a₁.2 + l₁.eval + -(a₂.1 • a₂.2) + -l₂.eval = -(a₂.1 • a₂.2) + a₁.1 • a₁.2 + l₁.eval + -l₂.eval
have h₁ : a₁.1 • a₁.2 + l₁.eval + -(a₂.1 • a₂.2) = -(a₂.1 • a₂.2) + a₁.1 • a₁.2 + l₁.eval
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ a₁.1 • a₁.2 + l₁.eval + -(a₂.1 • a₂.2) = -(a₂.1 • a₂.2) + a₁.1 • a₁.2 + l₁.eval
have h₁ : -(a₂.1 • a₂.2) + (a₁.1 • a₁.2 + l₁.eval) = -(a₂.1 • a₂.2) + a₁.1 • a₁.2 + l₁.eval
Tactic: rw [add_comm, add_assoc]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ a₁.1 • a₁.2 + l₁.eval + -(a₂.1 • a₂.2) = -(a₂.1 • a₂.2) + a₁.1 • a₁.2 + l₁.eval
have h₂ : -(a₂.1 • a₂.2) + (a₁.1 • a₁.2 + l₁.eval) = -(a₂.1 • a₂.2) + (a₁.1 • a₁.2 + l₁.eval)
Tactic: rw [add_comm, add_assoc]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ x₁ - x₂ = l.eval
have rw : l₁''.eval - x₂ = l.eval
Tactic: rw [hx₁, hx₂, ← h₁', ← h₂', ← h₁, ← h₂, h]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ x₁ - x₂ = l.eval
have rw₁ : l₁''.eval - l₂''.eval = l.eval
Tactic: rw [hx₁, hx₂, ← h₁', ← h₂', ← h₁, ← h₂, h]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ x₁ - x₂ = l.eval
have rw₂ : l₁'.eval - l₂''.eval = l.eval
Tactic: rw [hx₁, hx₂, ← h₁', ← h₂', ← h₁, ← h₂, h]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ x₁ - x₂ = l.eval
have rw₃ : l₁'.eval - l₂'.eval = l.eval
Tactic: rw [hx₁, hx₂, ← h₁', ← h₂', ← h₁, ← h₂, h]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ x₁ - x₂ = l.eval
have rw₄ : l₁.eval - l₂'.eval = l.eval
Tactic: rw [hx₁, hx₂, ← h₁', ← h₂', ← h₁, ← h₂, h]
-- Lean 4 proof step from Mathlib.Tactic.Module (goal)
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
⊢ x₁ - x₂ = l.eval
have rw₆ : l.eval = l.eval
Tactic: rw [hx₁, hx₂, ← h₁', ← h₂', ← h₁, ← h₂, h]