internlm/Lean-Github huggingface dataset:
Theorem: FormalSum.act_sum
Proof state before:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
il₁ : coords (scmul a t) x₀ + coords (scmul b t) x₀ = coords (scmul (a + b) t) x₀
⊢ monomCoeff R X x₀ (a * h.1, h.2) + coords (scmul a t) x₀ +
      (monomCoeff R X x₀ (b * h.1, h.2) + coords (scmul b t) x₀) =
    monomCoeff R X x₀ (a * h.1, h.2) + monomCoeff R X x₀ (b * h.1, h.2) +
      (coords (scmul a t) x₀ + coords (scmul b t) x₀)
Tactic:
conv =>
  lhs
  rw [add_assoc]
  arg 2
  rw [← add_assoc]
  arg 1
  rw [add_comm]
Proof state after:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
il₁ : coords (scmul a t) x₀ + coords (scmul b t) x₀ = coords (scmul (a + b) t) x₀
⊢ monomCoeff R X x₀ (a * h.1, h.2) +
      (monomCoeff R X x₀ (b * h.1, h.2) + coords (scmul a t) x₀ + coords (scmul b t) x₀) =
    monomCoeff R X x₀ (a * h.1, h.2) + monomCoeff R X x₀ (b * h.1, h.2) +
      (coords (scmul a t) x₀ + coords (scmul b t) x₀)
Theorem: FormalSum.act_sum
Proof state before:
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
il₁ : coords (scmul a t) x₀ + coords (scmul b t) x₀ = coords (scmul (a + b) t) x₀
⊢ monomCoeff R X x₀ (a * h.1, h.2) +
      (monomCoeff R X x₀ (b * h.1, h.2) + coords (scmul a t) x₀ + coords (scmul b t) x₀) =
    monomCoeff R X x₀ (a * h.1, h.2) + monomCoeff R X x₀ (b * h.1, h.2) +
      (coords (scmul a t) x₀ + coords (scmul b t) x₀)
Tactic:
conv =>
  lhs
  rw [add_assoc]
  rw [← add_assoc]
Proof state after:
no goals
Theorem: FreeModule.module_action
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
x : R[X]
⊢ a • b • x = (a * b) • x
Tactic:
apply @Quotient.ind (motive := fun x : R[X] => a • (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 • b • Quotient.mk (formalSumSetoid R X) a_1 = (a * b) • Quotient.mk (formalSumSetoid R X) a_1
Theorem: FreeModule.module_action
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 • 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 • b • Quotient.mk (formalSumSetoid R X) s = (a * b) • Quotient.mk (formalSumSetoid R X) s
Theorem: FreeModule.module_action
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 • 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 (scmul b s) ≈ scmul (a * b) s
Theorem: FreeModule.module_action
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 (scmul b s) ≈ scmul (a * b) s
Tactic:
rw [FormalSum.action]
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 * b) s ≈ scmul (a * b) s
Theorem: FreeModule.module_action
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 * b) s ≈ scmul (a * b) s
Tactic:
apply eqlCoords.refl
Proof state after:
no goals
Theorem: FreeModule.addn_comm
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ : R[X]
⊢ x₁ + x₂ = x₂ + x₁
Tactic:
apply @Quotient.ind₂ (motive := fun x₁ x₂ : R[X] => x₁ + x₂ = x₂ + x₁)
Proof state after:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ : R[X]
⊢ ∀ (a b : FormalSum R X),
    Quotient.mk (formalSumSetoid R X) a + Quotient.mk (formalSumSetoid R X) b =
      Quotient.mk (formalSumSetoid R X) b + Quotient.mk (formalSumSetoid R X) a
Theorem: FreeModule.addn_comm
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ : R[X]
⊢ ∀ (a b : FormalSum R X),
    Quotient.mk (formalSumSetoid R X) a + Quotient.mk (formalSumSetoid R X) b =
      Quotient.mk (formalSumSetoid R X) b + Quotient.mk (formalSumSetoid R X) a
Tactic:
intro s₁ s₂
Proof state after:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
⊢ Quotient.mk (formalSumSetoid R X) s₁ + Quotient.mk (formalSumSetoid R X) s₂ =
    Quotient.mk (formalSumSetoid R X) s₂ + Quotient.mk (formalSumSetoid R X) s₁
Theorem: FreeModule.addn_comm
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
⊢ Quotient.mk (formalSumSetoid R X) s₁ + Quotient.mk (formalSumSetoid R X) s₂ =
    Quotient.mk (formalSumSetoid R X) s₂ + Quotient.mk (formalSumSetoid R X) s₁
Tactic:
apply Quotient.sound
Proof state after:
case h.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
⊢ s₁ ++ s₂ ≈ s₂ ++ s₁
Theorem: FreeModule.addn_comm
Proof state before:
case h.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
⊢ s₁ ++ s₂ ≈ s₂ ++ s₁
Tactic:
apply funext
Proof state after:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
⊢ ∀ (x : X), coords (s₁ ++ s₂) x = coords (s₂ ++ s₁) x
Theorem: FreeModule.addn_comm
Proof state before:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
⊢ ∀ (x : X), coords (s₁ ++ s₂) x = coords (s₂ ++ 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
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
⊢ coords (s₁ ++ s₂) x₀ = coords (s₂ ++ s₁) x₀
Theorem: FreeModule.addn_comm
Proof state before:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
⊢ coords (s₁ ++ s₂) x₀ = coords (s₂ ++ s₁) x₀
Tactic:
let lm₁ := append_coords s₁ s₂ x₀
Proof state after:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
lm₁ : coords s₁ x₀ + coords s₂ x₀ = coords (s₁ ++ s₂) x₀ := append_coords s₁ s₂ x₀
⊢ coords (s₁ ++ s₂) x₀ = coords (s₂ ++ s₁) x₀
Theorem: FreeModule.addn_comm
Proof state before:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
lm₁ : coords s₁ x₀ + coords s₂ x₀ = coords (s₁ ++ s₂) x₀ := append_coords s₁ s₂ x₀
⊢ coords (s₁ ++ s₂) x₀ = coords (s₂ ++ s₁) x₀
Tactic:
let lm₂ := append_coords s₂ s₁ x₀
Proof state after:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
lm₁ : coords s₁ x₀ + coords s₂ x₀ = coords (s₁ ++ s₂) x₀ := append_coords s₁ s₂ x₀
lm₂ : coords s₂ x₀ + coords s₁ x₀ = coords (s₂ ++ s₁) x₀ := append_coords s₂ s₁ x₀
⊢ coords (s₁ ++ s₂) x₀ = coords (s₂ ++ s₁) x₀
Theorem: FreeModule.addn_comm
Proof state before:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
lm₁ : coords s₁ x₀ + coords s₂ x₀ = coords (s₁ ++ s₂) x₀ := append_coords s₁ s₂ x₀
lm₂ : coords s₂ x₀ + coords s₁ x₀ = coords (s₂ ++ s₁) x₀ := append_coords s₂ s₁ x₀
⊢ coords (s₁ ++ s₂) x₀ = coords (s₂ ++ s₁) x₀
Tactic:
rw [← lm₁, ← lm₂]
Proof state after:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
lm₁ : coords s₁ x₀ + coords s₂ x₀ = coords (s₁ ++ s₂) x₀ := append_coords s₁ s₂ x₀
lm₂ : coords s₂ x₀ + coords s₁ x₀ = coords (s₂ ++ s₁) x₀ := append_coords s₂ s₁ x₀
⊢ coords s₁ x₀ + coords s₂ x₀ = coords s₂ x₀ + coords s₁ x₀
Theorem: FreeModule.addn_comm
Proof state before:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
lm₁ : coords s₁ x₀ + coords s₂ x₀ = coords (s₁ ++ s₂) x₀ := append_coords s₁ s₂ x₀
lm₂ : coords s₂ x₀ + coords s₁ x₀ = coords (s₂ ++ s₁) x₀ := append_coords s₂ s₁ x₀
⊢ coords s₁ x₀ + coords s₂ x₀ = coords s₂ x₀ + coords s₁ x₀
Tactic:
simp [add_comm]
Proof state after:
no goals
Theorem: FreeModule.add_assoc_aux
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ : FormalSum R X
x₂ x₃ : R[X]
⊢ Quotient.mk (formalSumSetoid R X) s₁ + x₂ + x₃ = Quotient.mk (formalSumSetoid R X) s₁ + (x₂ + x₃)
Tactic:
apply @Quotient.ind₂ (motive := fun x₂ x₃ : R[X] => (⟦s₁⟧ + x₂) + x₃ = ⟦s₁⟧ + (x₂ + x₃))
Proof state after:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ : FormalSum R X
x₂ x₃ : R[X]
⊢ ∀ (a b : FormalSum R X),
    Quotient.mk (formalSumSetoid R X) s₁ + Quotient.mk (formalSumSetoid R X) a + Quotient.mk (formalSumSetoid R X) b =
      Quotient.mk (formalSumSetoid R X) s₁ + (Quotient.mk (formalSumSetoid R X) a + Quotient.mk (formalSumSetoid R X) b)
Theorem: FreeModule.add_assoc_aux
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ : FormalSum R X
x₂ x₃ : R[X]
⊢ ∀ (a b : FormalSum R X),
    Quotient.mk (formalSumSetoid R X) s₁ + Quotient.mk (formalSumSetoid R X) a + Quotient.mk (formalSumSetoid R X) b =
      Quotient.mk (formalSumSetoid R X) s₁ + (Quotient.mk (formalSumSetoid R X) a + Quotient.mk (formalSumSetoid R X) b)
Tactic:
intro x₂ x₃
Proof state after:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ : FormalSum R X
x₂✝ x₃✝ : R[X]
x₂ x₃ : FormalSum R X
⊢ Quotient.mk (formalSumSetoid R X) s₁ + Quotient.mk (formalSumSetoid R X) x₂ + Quotient.mk (formalSumSetoid R X) x₃ =
    Quotient.mk (formalSumSetoid R X) s₁ + (Quotient.mk (formalSumSetoid R X) x₂ + Quotient.mk (formalSumSetoid R X) x₃)
Theorem: FreeModule.add_assoc_aux
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ : FormalSum R X
x₂✝ x₃✝ : R[X]
x₂ x₃ : FormalSum R X
⊢ Quotient.mk (formalSumSetoid R X) s₁ + Quotient.mk (formalSumSetoid R X) x₂ + Quotient.mk (formalSumSetoid R X) x₃ =
    Quotient.mk (formalSumSetoid R X) s₁ + (Quotient.mk (formalSumSetoid R X) x₂ + Quotient.mk (formalSumSetoid R X) x₃)
Tactic:
apply Quotient.sound
Proof state after:
case h.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ : FormalSum R X
x₂✝ x₃✝ : R[X]
x₂ x₃ : FormalSum R X
⊢ s₁ ++ x₂ ++ x₃ ≈ s₁ ++ (x₂ ++ x₃)
Theorem: FreeModule.add_assoc_aux
Proof state before:
case h.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ : FormalSum R X
x₂✝ x₃✝ : R[X]
x₂ x₃ : FormalSum R X
⊢ s₁ ++ x₂ ++ x₃ ≈ s₁ ++ (x₂ ++ x₃)
Tactic:
apply funext
Proof state after:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ : FormalSum R X
x₂✝ x₃✝ : R[X]
x₂ x₃ : FormalSum R X
⊢ ∀ (x : X), coords (s₁ ++ x₂ ++ x₃) x = coords (s₁ ++ (x₂ ++ x₃)) x
Theorem: FreeModule.add_assoc_aux
Proof state before:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ : FormalSum R X
x₂✝ x₃✝ : R[X]
x₂ x₃ : FormalSum R X
⊢ ∀ (x : X), coords (s₁ ++ x₂ ++ x₃) x = coords (s₁ ++ (x₂ ++ x₃)) x
Tactic:
intro x₀
Proof state after:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ : FormalSum R X
x₂✝ x₃✝ : R[X]
x₂ x₃ : FormalSum R X
x₀ : X
⊢ coords (s₁ ++ x₂ ++ x₃) x₀ = coords (s₁ ++ (x₂ ++ x₃)) x₀
Theorem: FreeModule.add_assoc_aux
Proof state before:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ : FormalSum R X
x₂✝ x₃✝ : R[X]
x₂ x₃ : FormalSum R X
x₀ : X
⊢ coords (s₁ ++ x₂ ++ x₃) x₀ = coords (s₁ ++ (x₂ ++ x₃)) 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
s₁ : FormalSum R X
x₂✝ x₃✝ : R[X]
x₂ x₃ : FormalSum R X
x₀ : X
⊢ coords (s₁ ++ x₂) x₀ + coords x₃ x₀ = coords (s₁ ++ (x₂ ++ x₃)) x₀
Theorem: FreeModule.add_assoc_aux
Proof state before:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ : FormalSum R X
x₂✝ x₃✝ : R[X]
x₂ x₃ : FormalSum R X
x₀ : X
⊢ coords (s₁ ++ x₂) x₀ + coords x₃ x₀ = coords (s₁ ++ (x₂ ++ x₃)) 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
s₁ : FormalSum R X
x₂✝ x₃✝ : R[X]
x₂ x₃ : FormalSum R X
x₀ : X
⊢ coords s₁ x₀ + coords x₂ x₀ + coords x₃ x₀ = coords (s₁ ++ (x₂ ++ x₃)) x₀
Theorem: FreeModule.add_assoc_aux
Proof state before:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ : FormalSum R X
x₂✝ x₃✝ : R[X]
x₂ x₃ : FormalSum R X
x₀ : X
⊢ coords s₁ x₀ + coords x₂ x₀ + coords x₃ x₀ = coords (s₁ ++ (x₂ ++ x₃)) 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
s₁ : FormalSum R X
x₂✝ x₃✝ : R[X]
x₂ x₃ : FormalSum R X
x₀ : X
⊢ coords s₁ x₀ + coords x₂ x₀ + coords x₃ x₀ = coords s₁ x₀ + coords (x₂ ++ x₃) x₀
Theorem: FreeModule.add_assoc_aux
Proof state before:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ : FormalSum R X
x₂✝ x₃✝ : R[X]
x₂ x₃ : FormalSum R X
x₀ : X
⊢ coords s₁ x₀ + coords x₂ x₀ + coords x₃ x₀ = coords s₁ x₀ + coords (x₂ ++ x₃) 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
s₁ : FormalSum R X
x₂✝ x₃✝ : R[X]
x₂ x₃ : FormalSum R X
x₀ : X
⊢ coords s₁ x₀ + coords x₂ x₀ + coords x₃ x₀ = coords s₁ x₀ + (coords x₂ x₀ + coords x₃ x₀)
Theorem: FreeModule.add_assoc_aux
Proof state before:
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ : FormalSum R X
x₂✝ x₃✝ : R[X]
x₂ x₃ : FormalSum R X
x₀ : X
⊢ coords s₁ x₀ + coords x₂ x₀ + coords x₃ x₀ = coords s₁ x₀ + (coords x₂ x₀ + coords x₃ x₀)
Tactic:
simp [add_assoc]
Proof state after:
no goals
Theorem: FreeModule.addn_assoc
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ x₃ : R[X]
⊢ x₁ + x₂ + x₃ = x₁ + (x₂ + x₃)
Tactic:
apply @Quotient.ind (motive := fun x₁ : R[X] => (x₁ + x₂) + x₃ = x₁ + (x₂ + x₃))
Proof state after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ x₃ : R[X]
⊢ ∀ (a : FormalSum R X), Quotient.mk (formalSumSetoid R X) a + x₂ + x₃ = Quotient.mk (formalSumSetoid R X) a + (x₂ + x₃)
Theorem: FreeModule.addn_assoc
Proof state before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁ x₂ x₃ : R[X]
⊢ ∀ (a : FormalSum R X), Quotient.mk (formalSumSetoid R X) a + x₂ + x₃ = Quotient.mk (formalSumSetoid R X) a + (x₂ + x₃)
Tactic:
intro x₁
Proof state after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁✝ x₂ x₃ : R[X]
x₁ : FormalSum R X
⊢ Quotient.mk (formalSumSetoid R X) x₁ + x₂ + x₃ = Quotient.mk (formalSumSetoid R X) x₁ + (x₂ + x₃)
Theorem: FreeModule.addn_assoc
Proof state before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₁✝ x₂ x₃ : R[X]
x₁ : FormalSum R X
⊢ Quotient.mk (formalSumSetoid R X) x₁ + x₂ + x₃ = Quotient.mk (formalSumSetoid R X) x₁ + (x₂ + x₃)
Tactic:
apply add_assoc_aux
Proof state after:
no goals
Theorem: FreeModule.addn_zero
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
⊢ x + zero = x
Tactic:
apply @Quotient.ind (motive := fun x : R[X] => x + zero = 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), Quotient.mk (formalSumSetoid R X) a + zero = Quotient.mk (formalSumSetoid R X) a
Theorem: FreeModule.addn_zero
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), Quotient.mk (formalSumSetoid R X) a + zero = Quotient.mk (formalSumSetoid R X) a
Tactic:
intro x
Proof state after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
⊢ Quotient.mk (formalSumSetoid R X) x + zero = Quotient.mk (formalSumSetoid R X) x
Theorem: FreeModule.addn_zero
Proof state before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
⊢ Quotient.mk (formalSumSetoid R X) x + zero = Quotient.mk (formalSumSetoid R X) 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]
x : FormalSum R X
⊢ x ++ [] ≈ x
Theorem: FreeModule.addn_zero
Proof state before:
case a.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
⊢ x ++ [] ≈ x
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]
x : FormalSum R X
⊢ ∀ (x_1 : X), coords (x ++ []) x_1 = coords x x_1
Theorem: FreeModule.addn_zero
Proof state before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
⊢ ∀ (x_1 : X), coords (x ++ []) x_1 = coords x x_1
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]
x : FormalSum R X
x₀ : X
⊢ coords (x ++ []) x₀ = coords x x₀
Theorem: FreeModule.addn_zero
Proof state before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
x₀ : X
⊢ coords (x ++ []) x₀ = coords x x₀
Tactic:
rw [← append_coords]
Proof state after:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
x₀ : X
⊢ coords x x₀ + coords [] x₀ = coords x x₀
Theorem: FreeModule.addn_zero
Proof state before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
x₀ : X
⊢ coords x x₀ + coords [] x₀ = coords x x₀
Tactic:
simp [add_zero, coords]
Proof state after:
no goals
Theorem: FreeModule.zero_addn
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
⊢ zero + x = x
Tactic:
apply @Quotient.ind (motive := fun x : R[X] => zero + 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), zero + Quotient.mk (formalSumSetoid R X) a = Quotient.mk (formalSumSetoid R X) a
Theorem: FreeModule.zero_addn
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), zero + Quotient.mk (formalSumSetoid R X) a = Quotient.mk (formalSumSetoid R X) a
Tactic:
intro x
Proof state after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
⊢ zero + Quotient.mk (formalSumSetoid R X) x = Quotient.mk (formalSumSetoid R X) x
Theorem: FreeModule.zero_addn
Proof state before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
⊢ zero + Quotient.mk (formalSumSetoid R X) x = Quotient.mk (formalSumSetoid R X) 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]
x : FormalSum R X
⊢ [] ++ x ≈ x
Theorem: FreeModule.zero_addn
Proof state before:
case a.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
⊢ [] ++ x ≈ x
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]
x : FormalSum R X
⊢ ∀ (x_1 : X), coords ([] ++ x) x_1 = coords x x_1
Theorem: FreeModule.zero_addn
Proof state before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
⊢ ∀ (x_1 : X), coords ([] ++ x) x_1 = coords x x_1
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]
x : FormalSum R X
x₀ : X
⊢ coords ([] ++ x) x₀ = coords x x₀
Theorem: FreeModule.zero_addn
Proof state before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
x₀ : X
⊢ coords ([] ++ x) x₀ = coords x x₀
Tactic:
rw [← append_coords]
Proof state after:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
x₀ : X
⊢ coords [] x₀ + coords x x₀ = coords x x₀
Theorem: FreeModule.zero_addn
Proof state before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
x₀ : X
⊢ coords [] x₀ + coords x x₀ = coords x x₀
Tactic:
simp [add_zero, coords]
Proof state after:
no goals
Theorem: FreeModule.elem_distrib
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
⊢ a • (x₁ + x₂) = a • x₁ + a • x₂
Tactic:
apply @Quotient.ind₂ (motive := fun x₁ x₂ : R[X] => a • (x₁ + x₂) = a • x₁ + a • x₂)
Proof state after:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
⊢ ∀ (a_1 b : FormalSum R X),
    a • (Quotient.mk (formalSumSetoid R X) a_1 + Quotient.mk (formalSumSetoid R X) b) =
      a • Quotient.mk (formalSumSetoid R X) a_1 + a • Quotient.mk (formalSumSetoid R X) b
Theorem: FreeModule.elem_distrib
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
⊢ ∀ (a_1 b : FormalSum R X),
    a • (Quotient.mk (formalSumSetoid R X) a_1 + Quotient.mk (formalSumSetoid R X) b) =
      a • Quotient.mk (formalSumSetoid R X) a_1 + a • Quotient.mk (formalSumSetoid R X) b
Tactic:
intro s₁ s₂
Proof state after:
case 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
⊢ a • (Quotient.mk (formalSumSetoid R X) s₁ + Quotient.mk (formalSumSetoid R X) s₂) =
    a • Quotient.mk (formalSumSetoid R X) s₁ + a • Quotient.mk (formalSumSetoid R X) s₂
Theorem: FreeModule.elem_distrib
Proof state before:
case 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
⊢ a • (Quotient.mk (formalSumSetoid R X) s₁ + Quotient.mk (formalSumSetoid R X) s₂) =
    a • Quotient.mk (formalSumSetoid R X) s₁ + a • Quotient.mk (formalSumSetoid R X) s₂
Tactic:
apply Quotient.sound
Proof state after:
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₂