internlm/Lean-Github huggingface dataset:
Theorem: FreeModule.elem_distrib
Proof state before:
case h.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
⊢ scmul a (s₁ ++ s₂) ≈ scmul a s₁ ++ scmul a s₂
Tactic:
apply funext
Proof state after:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
⊢ ∀ (x : X), coords (scmul a (s₁ ++ s₂)) x = coords (scmul a s₁ ++ scmul a s₂) x
Theorem: FreeModule.elem_distrib
Proof state before:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
⊢ ∀ (x : X), coords (scmul a (s₁ ++ s₂)) x = coords (scmul a s₁ ++ scmul a s₂) x
Tactic:
intro x₀
Proof state after:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
⊢ coords (scmul a (s₁ ++ s₂)) x₀ = coords (scmul a s₁ ++ scmul a s₂) x₀
Theorem: FreeModule.elem_distrib
Proof state before:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
⊢ coords (scmul a (s₁ ++ s₂)) x₀ = coords (scmul a s₁ ++ scmul a s₂) x₀
Tactic:
rw [← scmul_coords]
Proof state after:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
⊢ a * coords (s₁ ++ s₂) x₀ = coords (scmul a s₁ ++ scmul a s₂) x₀
Theorem: FreeModule.elem_distrib
Proof state before:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
⊢ a * coords (s₁ ++ s₂) x₀ = coords (scmul a s₁ ++ scmul a s₂) x₀
Tactic:
rw [← append_coords]
Proof state after:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
⊢ a * (coords s₁ x₀ + coords s₂ x₀) = coords (scmul a s₁ ++ scmul a s₂) x₀
Theorem: FreeModule.elem_distrib
Proof state before:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
⊢ a * (coords s₁ x₀ + coords s₂ x₀) = coords (scmul a s₁ ++ scmul a s₂) x₀
Tactic:
rw [← append_coords]
Proof state after:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
⊢ a * (coords s₁ x₀ + coords s₂ x₀) = coords (scmul a s₁) x₀ + coords (scmul a s₂) x₀
Theorem: FreeModule.elem_distrib
Proof state before:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
⊢ a * (coords s₁ x₀ + coords s₂ x₀) = coords (scmul a s₁) x₀ + coords (scmul a s₂) x₀
Tactic:
rw [← scmul_coords]
Proof state after:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
⊢ a * (coords s₁ x₀ + coords s₂ x₀) = a * coords s₁ x₀ + coords (scmul a s₂) x₀
Theorem: FreeModule.elem_distrib
Proof state before:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
⊢ a * (coords s₁ x₀ + coords s₂ x₀) = a * coords s₁ x₀ + coords (scmul a s₂) x₀
Tactic:
rw [← scmul_coords]
Proof state after:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
⊢ a * (coords s₁ x₀ + coords s₂ x₀) = a * coords s₁ x₀ + a * coords s₂ x₀
Theorem: FreeModule.elem_distrib
Proof state before:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
⊢ a * (coords s₁ x₀ + coords s₂ x₀) = a * coords s₁ x₀ + a * coords s₂ x₀
Tactic:
simp [left_distrib]
Proof state after:
no goals
Theorem: FreeModule.coeffs_distrib
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
x : R[X]
⊢ a • x + b • x = (a + b) • x
Tactic:
apply @Quotient.ind (motive := fun x : R[X] => 
  a • x + b • x = (a + b) • x)
Proof state after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
x : R[X]
⊢ ∀ (a_1 : FormalSum R X),
    a • Quotient.mk (formalSumSetoid R X) a_1 + b • Quotient.mk (formalSumSetoid R X) a_1 =
      (a + b) • Quotient.mk (formalSumSetoid R X) a_1
Theorem: FreeModule.coeffs_distrib
Proof state before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
x : R[X]
⊢ ∀ (a_1 : FormalSum R X),
    a • Quotient.mk (formalSumSetoid R X) a_1 + b • Quotient.mk (formalSumSetoid R X) a_1 =
      (a + b) • Quotient.mk (formalSumSetoid R X) a_1
Tactic:
intro s
Proof state after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
x : R[X]
s : FormalSum R X
⊢ a • Quotient.mk (formalSumSetoid R X) s + b • Quotient.mk (formalSumSetoid R X) s =
    (a + b) • Quotient.mk (formalSumSetoid R X) s
Theorem: FreeModule.coeffs_distrib
Proof state before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
x : R[X]
s : FormalSum R X
⊢ a • Quotient.mk (formalSumSetoid R X) s + b • Quotient.mk (formalSumSetoid R X) s =
    (a + b) • Quotient.mk (formalSumSetoid R X) s
Tactic:
apply Quotient.sound
Proof state after:
case a.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
x : R[X]
s : FormalSum R X
⊢ scmul a s ++ scmul b s ≈ scmul (a + b) s
Theorem: FreeModule.coeffs_distrib
Proof state before:
case a.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
x : R[X]
s : FormalSum R X
⊢ scmul a s ++ scmul b s ≈ scmul (a + b) s
Tactic:
apply funext
Proof state after:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
x : R[X]
s : FormalSum R X
⊢ ∀ (x : X), coords (scmul a s ++ scmul b s) x = coords (scmul (a + b) s) x
Theorem: FreeModule.coeffs_distrib
Proof state before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
x : R[X]
s : FormalSum R X
⊢ ∀ (x : X), coords (scmul a s ++ scmul b s) x = coords (scmul (a + b) s) x
Tactic:
intro x₀
Proof state after:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
x : R[X]
s : FormalSum R X
x₀ : X
⊢ coords (scmul a s ++ scmul b s) x₀ = coords (scmul (a + b) s) x₀
Theorem: FreeModule.coeffs_distrib
Proof state before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
x : R[X]
s : FormalSum R X
x₀ : X
⊢ coords (scmul a s ++ scmul b s) x₀ = coords (scmul (a + b) s) x₀
Tactic:
let l := act_sum a b s
Proof state after:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
x : R[X]
s : FormalSum R X
x₀ : X
l : scmul a s ++ scmul b s ≈ scmul (a + b) s := act_sum a b s
⊢ coords (scmul a s ++ scmul b s) x₀ = coords (scmul (a + b) s) x₀
Theorem: FreeModule.coeffs_distrib
Proof state before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
x : R[X]
s : FormalSum R X
x₀ : X
l : scmul a s ++ scmul b s ≈ scmul (a + b) s := act_sum a b s
⊢ coords (scmul a s ++ scmul b s) x₀ = coords (scmul (a + b) s) x₀
Tactic:
let l'' := congrFun l x₀
Proof state after:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
x : R[X]
s : FormalSum R X
x₀ : X
l : scmul a s ++ scmul b s ≈ scmul (a + b) s := act_sum a b s
l'' : coords (scmul a s ++ scmul b s) x₀ = coords (scmul (a + b) s) x₀ := congrFun l x₀
⊢ coords (scmul a s ++ scmul b s) x₀ = coords (scmul (a + b) s) x₀
Theorem: FreeModule.coeffs_distrib
Proof state before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
x : R[X]
s : FormalSum R X
x₀ : X
l : scmul a s ++ scmul b s ≈ scmul (a + b) s := act_sum a b s
l'' : coords (scmul a s ++ scmul b s) x₀ = coords (scmul (a + b) s) x₀ := congrFun l x₀
⊢ coords (scmul a s ++ scmul b s) x₀ = coords (scmul (a + b) s) x₀
Tactic:
exact l''
Proof state after:
no goals
Theorem: FreeModule.unit_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
⊢ 1 • x = x
Tactic:
apply @Quotient.ind (motive := fun x : R[X] => 
  (1 : R) • x =  x)
Proof state after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
⊢ ∀ (a : FormalSum R X), 1 • Quotient.mk (formalSumSetoid R X) a = Quotient.mk (formalSumSetoid R X) a
Theorem: FreeModule.unit_coeffs
Proof state before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
⊢ ∀ (a : FormalSum R X), 1 • Quotient.mk (formalSumSetoid R X) a = Quotient.mk (formalSumSetoid R X) a
Tactic:
intro s
Proof state after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
⊢ 1 • Quotient.mk (formalSumSetoid R X) s = Quotient.mk (formalSumSetoid R X) s
Theorem: FreeModule.unit_coeffs
Proof state before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
⊢ 1 • Quotient.mk (formalSumSetoid R X) s = Quotient.mk (formalSumSetoid R X) s
Tactic:
apply Quotient.sound
Proof state after:
case a.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
⊢ scmul 1 s ≈ s
Theorem: FreeModule.unit_coeffs
Proof state before:
case a.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
⊢ scmul 1 s ≈ s
Tactic:
apply funext
Proof state after:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
⊢ ∀ (x : X), coords (scmul 1 s) x = coords s x
Theorem: FreeModule.unit_coeffs
Proof state before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
⊢ ∀ (x : X), coords (scmul 1 s) x = coords s x
Tactic:
intro x₀
Proof state after:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
x₀ : X
⊢ coords (scmul 1 s) x₀ = coords s x₀
Theorem: FreeModule.unit_coeffs
Proof state before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
x₀ : X
⊢ coords (scmul 1 s) x₀ = coords s x₀
Tactic:
let l := scmul_coords 1 s x₀
Proof state after:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
x₀ : X
l : 1 * coords s x₀ = coords (scmul 1 s) x₀ := scmul_coords 1 s x₀
⊢ coords (scmul 1 s) x₀ = coords s x₀
Theorem: FreeModule.unit_coeffs
Proof state before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
x₀ : X
l : 1 * coords s x₀ = coords (scmul 1 s) x₀ := scmul_coords 1 s x₀
⊢ coords (scmul 1 s) x₀ = coords s x₀
Tactic:
rw [← l]
Proof state after:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
x₀ : X
l : 1 * coords s x₀ = coords (scmul 1 s) x₀ := scmul_coords 1 s x₀
⊢ 1 * coords s x₀ = coords s x₀
Theorem: FreeModule.unit_coeffs
Proof state before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
x₀ : X
l : 1 * coords s x₀ = coords (scmul 1 s) x₀ := scmul_coords 1 s x₀
⊢ 1 * coords s x₀ = coords s x₀
Tactic:
simp
Proof state after:
no goals
Theorem: FreeModule.zero_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
⊢ 0 • x = Quotient.mk (formalSumSetoid R X) []
Tactic:
apply @Quotient.ind (motive := fun x : R[X] => 
  (0 : R) • x =  ⟦ [] ⟧)
Proof state after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
⊢ ∀ (a : FormalSum R X), 0 • Quotient.mk (formalSumSetoid R X) a = Quotient.mk (formalSumSetoid R X) []
Theorem: FreeModule.zero_coeffs
Proof state before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
⊢ ∀ (a : FormalSum R X), 0 • Quotient.mk (formalSumSetoid R X) a = Quotient.mk (formalSumSetoid R X) []
Tactic:
intro s
Proof state after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
⊢ 0 • Quotient.mk (formalSumSetoid R X) s = Quotient.mk (formalSumSetoid R X) []
Theorem: FreeModule.zero_coeffs
Proof state before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
⊢ 0 • Quotient.mk (formalSumSetoid R X) s = Quotient.mk (formalSumSetoid R X) []
Tactic:
apply Quotient.sound
Proof state after:
case a.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
⊢ scmul 0 s ≈ []
Theorem: FreeModule.zero_coeffs
Proof state before:
case a.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
⊢ scmul 0 s ≈ []
Tactic:
apply funext
Proof state after:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
⊢ ∀ (x : X), coords (scmul 0 s) x = coords [] x
Theorem: FreeModule.zero_coeffs
Proof state before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
⊢ ∀ (x : X), coords (scmul 0 s) x = coords [] x
Tactic:
intro x₀
Proof state after:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
x₀ : X
⊢ coords (scmul 0 s) x₀ = coords [] x₀
Theorem: FreeModule.zero_coeffs
Proof state before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
x₀ : X
⊢ coords (scmul 0 s) x₀ = coords [] x₀
Tactic:
let l := scmul_coords 0 s x₀
Proof state after:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
x₀ : X
l : 0 * coords s x₀ = coords (scmul 0 s) x₀ := scmul_coords 0 s x₀
⊢ coords (scmul 0 s) x₀ = coords [] x₀
Theorem: FreeModule.zero_coeffs
Proof state before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
x₀ : X
l : 0 * coords s x₀ = coords (scmul 0 s) x₀ := scmul_coords 0 s x₀
⊢ coords (scmul 0 s) x₀ = coords [] x₀
Tactic:
rw [← l]
Proof state after:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
x₀ : X
l : 0 * coords s x₀ = coords (scmul 0 s) x₀ := scmul_coords 0 s x₀
⊢ 0 * coords s x₀ = coords [] x₀
Theorem: FreeModule.zero_coeffs
Proof state before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
x₀ : X
l : 0 * coords s x₀ = coords (scmul 0 s) x₀ := scmul_coords 0 s x₀
⊢ 0 * coords s x₀ = coords [] x₀
Tactic:
simp [coords]
Proof state after:
no goals
Theorem: FormalSum.coords_move_invariant
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
s₁ s₂ : FormalSum R X
h : ElementaryMove R X s₁ s₂
⊢ coords s₁ x₀ = coords s₂ x₀
Tactic:
induction h with
| zeroCoeff tail x a hyp =>
  simp [coords, hyp, monom_coords_at_zero]
| addCoeffs a b x tail =>
  simp [coords, monom_coords_at_zero, ← add_assoc, monom_coords_hom]
| cons a x s₁ s₂ _ step =>
  simp [coords, step]
| swap a₁ a₂ x₁ x₂ tail =>
  simp [coords, ← add_assoc, add_comm]
Proof state after:
no goals
Theorem: FormalSum.coords_move_invariant
Proof state before:
case zeroCoeff
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
s₁ s₂ tail : FormalSum R X
x : X
a : R
hyp : a = 0
⊢ coords ((a, x) :: tail) x₀ = coords tail x₀
Tactic:
simp [coords, hyp, monom_coords_at_zero]
Proof state after:
no goals
Theorem: FormalSum.coords_move_invariant
Proof state before:
case addCoeffs
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
s₁ s₂ : FormalSum R X
a b : R
x : X
tail : FormalSum R X
⊢ coords ((a, x) :: (b, x) :: tail) x₀ = coords ((a + b, x) :: tail) x₀
Tactic:
simp [coords, monom_coords_at_zero, ← add_assoc, monom_coords_hom]
Proof state after:
no goals
Theorem: FormalSum.coords_move_invariant
Proof state before:
case cons
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
s₁✝ s₂✝ : FormalSum R X
a : R
x : X
s₁ s₂ : FormalSum R X
a✝ : ElementaryMove R X s₁ s₂
step : coords s₁ x₀ = coords s₂ x₀
⊢ coords ((a, x) :: s₁) x₀ = coords ((a, x) :: s₂) x₀
Tactic:
simp [coords, step]
Proof state after:
no goals
Theorem: FormalSum.coords_move_invariant
Proof state before:
case swap
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
s₁ s₂ : FormalSum R X
a₁ a₂ : R
x₁ x₂ : X
tail : FormalSum R X
⊢ coords ((a₁, x₁) :: (a₂, x₂) :: tail) x₀ = coords ((a₂, x₂) :: (a₁, x₁) :: tail) x₀
Tactic:
simp [coords, ← add_assoc, add_comm]
Proof state after:
no goals
Theorem: FormalSum.coeff_factors
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s : FormalSum R X
⊢ FreeModuleAux.coeff x (sum s) = coords s x
Tactic:
simp [FreeModuleAux.coeff]
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s : FormalSum R X
⊢ Quot.lift (fun s => coords s x) (_ : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → coords s₁ x = coords s₂ x)
      (sum s) =
    coords s x
Theorem: FormalSum.coeff_factors
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s : FormalSum R X
⊢ Quot.lift (fun s => coords s x) (_ : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → coords s₁ x = coords s₂ x)
      (sum s) =
    coords s x
Tactic:
apply @Quot.liftBeta (r := ElementaryMove R X) (f := fun s => s.coords x)
Proof state after:
case c
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s : FormalSum R X
⊢ ∀ (a b : FormalSum R X), ElementaryMove R X a b → coords a x = coords b x
Theorem: FormalSum.coeff_factors
Proof state before:
case c
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s : FormalSum R X
⊢ ∀ (a b : FormalSum R X), ElementaryMove R X a b → coords a x = coords b x
Tactic:
apply coords_move_invariant
Proof state after:
no goals
Theorem: FormalSum.coords_well_defined
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
⊢ s₁ ≃ s₂ → coords s₁ x = coords s₂ x
Tactic:
intro hyp
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
hyp : s₁ ≃ s₂
⊢ coords s₁ x = coords s₂ x
Theorem: FormalSum.coords_well_defined
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
hyp : s₁ ≃ s₂
⊢ coords s₁ x = coords s₂ x
Tactic:
have l : FreeModuleAux.coeff x (sum s₂) = s₂.coords x := by
  simp [coeff_factors, hyp]
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
hyp : s₁ ≃ s₂
l : FreeModuleAux.coeff x (sum s₂) = coords s₂ x
⊢ coords s₁ x = coords s₂ x
Theorem: FormalSum.coords_well_defined
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
hyp : s₁ ≃ s₂
l : FreeModuleAux.coeff x (sum s₂) = coords s₂ x
⊢ coords s₁ x = coords s₂ x
Tactic:
rw [← l]
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
hyp : s₁ ≃ s₂
l : FreeModuleAux.coeff x (sum s₂) = coords s₂ x
⊢ coords s₁ x = FreeModuleAux.coeff x (sum s₂)
Theorem: FormalSum.coords_well_defined
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
hyp : s₁ ≃ s₂
l : FreeModuleAux.coeff x (sum s₂) = coords s₂ x
⊢ coords s₁ x = FreeModuleAux.coeff x (sum s₂)
Tactic:
rw [← coeff_factors]
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
hyp : s₁ ≃ s₂
l : FreeModuleAux.coeff x (sum s₂) = coords s₂ x
⊢ FreeModuleAux.coeff x (sum s₁) = FreeModuleAux.coeff x (sum s₂)
Theorem: FormalSum.coords_well_defined
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
hyp : s₁ ≃ s₂
l : FreeModuleAux.coeff x (sum s₂) = coords s₂ x
⊢ FreeModuleAux.coeff x (sum s₁) = FreeModuleAux.coeff x (sum s₂)
Tactic:
rw [hyp]
Proof state after:
no goals
Theorem: FormalSum.coords_well_defined
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : X
s₁ s₂ : FormalSum R X
hyp : s₁ ≃ s₂
⊢ FreeModuleAux.coeff x (sum s₂) = coords s₂ x
Tactic:
simp [coeff_factors, hyp]
Proof state after:
no goals
Theorem: FormalSum.cons_equiv_of_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
a : R
x : X
⊢ s₁ ≃ s₂ → (a, x) :: s₁ ≃ (a, x) :: s₂
Tactic:
intro h
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
a : R
x : X
h : s₁ ≃ s₂
⊢ (a, x) :: s₁ ≃ (a, x) :: s₂
Theorem: FormalSum.cons_equiv_of_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
a : R
x : X
h : s₁ ≃ s₂
⊢ (a, x) :: s₁ ≃ (a, x) :: s₂
Tactic:
let f : FormalSum R X → FreeModuleAux R X := fun s => sum <| (a, x) :: s
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
a : R
x : X
h : s₁ ≃ s₂
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
⊢ (a, x) :: s₁ ≃ (a, x) :: s₂
Theorem: FormalSum.cons_equiv_of_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
a : R
x : X
h : s₁ ≃ s₂
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
⊢ (a, x) :: s₁ ≃ (a, x) :: s₂
Tactic:
let wit : (s₁ s₂ : FormalSum R X) → (ElementaryMove R X s₁ s₂) → f s₁ = f s₂ := by
  intro s₁ s₂ hyp
  apply Quot.sound
  apply ElementaryMove.cons
  assumption
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
a : R
x : X
h : s₁ ≃ s₂
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
wit : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂ :=
  fun s₁ s₂ hyp => Quot.sound (ElementaryMove.cons a x s₁ s₂ hyp)
⊢ (a, x) :: s₁ ≃ (a, x) :: s₂
Theorem: FormalSum.cons_equiv_of_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
a : R
x : X
h : s₁ ≃ s₂
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
wit : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂ :=
  fun s₁ s₂ hyp => Quot.sound (ElementaryMove.cons a x s₁ s₂ hyp)
⊢ (a, x) :: s₁ ≃ (a, x) :: s₂
Tactic:
let g := Quot.lift f wit
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
a : R
x : X
h : s₁ ≃ s₂
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
wit : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂ :=
  fun s₁ s₂ hyp => Quot.sound (ElementaryMove.cons a x s₁ s₂ hyp)
g : (Quot fun a b => ElementaryMove R X a b) → FreeModuleAux R X := Quot.lift f wit
⊢ (a, x) :: s₁ ≃ (a, x) :: s₂