internlm/Lean-Github huggingface dataset:
Theorem: FreeModule.eqlquot_of_beq_support
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : ¬0 = FormalSum.coords s₁ x
lem : x ∈ FormalSum.support s₁
lem' : FormalSum.coords s₁ x = FormalSum.coords s₂ x :=
  eq_mem_of_equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) x lem ch₁
⊢ FormalSum.coords s₁ x = FormalSum.coords s₂ x
Tactic:
exact lem'
Proof state after:
no goals
Theorem: FreeModule.eqlquot_of_beq_support
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : ¬0 = FormalSum.coords s₁ x
⊢ x ∈ FormalSum.support s₁
Tactic:
apply nonzero_coord_in_support
Proof state after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : ¬0 = FormalSum.coords s₁ x
⊢ 0 ≠ FormalSum.coords s₁ x
Theorem: FreeModule.eqlquot_of_beq_support
Proof state before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : ¬0 = FormalSum.coords s₁ x
⊢ 0 ≠ FormalSum.coords s₁ x
Tactic:
assumption
Proof state after:
no goals
Theorem: FreeModule.eq_of_beq_true
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
⊢ ∀ (x₁ x₂ : R[X]), beq_quot x₁ x₂ = true → x₁ = x₂
Tactic:
apply Quotient.ind₂ (motive := fun (x₁ x₂ : R[X]) => x₁.beq_quot x₂ = true → x₁ = x₂)
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
⊢ ∀ (a b : FormalSum R X),
    beq_quot (Quotient.mk (formalSumSetoid R X) a) (Quotient.mk (formalSumSetoid R X) b) = true →
      Quotient.mk (formalSumSetoid R X) a = Quotient.mk (formalSumSetoid R X) b
Theorem: FreeModule.eq_of_beq_true
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
⊢ ∀ (a b : FormalSum R X),
    beq_quot (Quotient.mk (formalSumSetoid R X) a) (Quotient.mk (formalSumSetoid R X) b) = true →
      Quotient.mk (formalSumSetoid R X) a = Quotient.mk (formalSumSetoid R X) b
Tactic:
intro s₁ s₂ eqv
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
eqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = true
⊢ Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂
Theorem: FreeModule.eq_of_beq_true
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
eqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = true
⊢ Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂
Tactic:
let eql := of_decide_eq_true eqv
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
eqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = true
eql : Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂ := of_decide_eq_true eqv
⊢ Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂
Theorem: FreeModule.eq_of_beq_true
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
eqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = true
eql : Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂ := of_decide_eq_true eqv
⊢ Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂
Tactic:
assumption
Proof state after:
no goals
Theorem: FreeModule.neq_of_beq_false
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
⊢ ∀ (x₁ x₂ : R[X]), beq_quot x₁ x₂ = false → ¬x₁ = x₂
Tactic:
apply Quotient.ind₂ (motive := fun (x₁ x₂ : R[X]) => x₁.beq_quot x₂ = false → Not (x₁ = x₂))
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
⊢ ∀ (a b : FormalSum R X),
    beq_quot (Quotient.mk (formalSumSetoid R X) a) (Quotient.mk (formalSumSetoid R X) b) = false →
      ¬Quotient.mk (formalSumSetoid R X) a = Quotient.mk (formalSumSetoid R X) b
Theorem: FreeModule.neq_of_beq_false
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
⊢ ∀ (a b : FormalSum R X),
    beq_quot (Quotient.mk (formalSumSetoid R X) a) (Quotient.mk (formalSumSetoid R X) b) = false →
      ¬Quotient.mk (formalSumSetoid R X) a = Quotient.mk (formalSumSetoid R X) b
Tactic:
intro s₁ s₂ neqv
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
neqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = false
⊢ ¬Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂
Theorem: FreeModule.neq_of_beq_false
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
neqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = false
⊢ ¬Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂
Tactic:
let neql := of_decide_eq_false neqv
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
neqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = false
neql : ¬Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂ := of_decide_eq_false neqv
⊢ ¬Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂
Theorem: FreeModule.neq_of_beq_false
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
neqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = false
neql : ¬Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂ := of_decide_eq_false neqv
⊢ ¬Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂
Tactic:
assumption
Proof state after:
no goals
Theorem: FreeModule.equal_coords_of_approx
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
⊢ s₁ ≈ s₂ → FormalSum.coords s₁ = FormalSum.coords s₂
Tactic:
intro hyp
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : s₁ ≈ s₂
⊢ FormalSum.coords s₁ = FormalSum.coords s₂
Theorem: FreeModule.equal_coords_of_approx
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : s₁ ≈ s₂
⊢ FormalSum.coords s₁ = FormalSum.coords s₂
Tactic:
apply funext
Proof state after:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : s₁ ≈ s₂
⊢ ∀ (x : X), FormalSum.coords s₁ x = FormalSum.coords s₂ x
Theorem: FreeModule.equal_coords_of_approx
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : s₁ ≈ s₂
⊢ ∀ (x : X), FormalSum.coords s₁ x = FormalSum.coords s₂ x
Tactic:
intro x₀
Proof state after:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : s₁ ≈ s₂
x₀ : X
⊢ FormalSum.coords s₁ x₀ = FormalSum.coords s₂ x₀
Theorem: FreeModule.equal_coords_of_approx
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : s₁ ≈ s₂
x₀ : X
⊢ FormalSum.coords s₁ x₀ = FormalSum.coords s₂ x₀
Tactic:
exact congrFun hyp x₀
Proof state after:
no goals
Theorem: FormalSum.scmul_coords
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
r : R
s : FormalSum R X
x₀ : X
⊢ r * coords s x₀ = coords (scmul r s) x₀
Tactic:
induction s with
| nil =>
  simp [coords]
| cons h t ih =>
  simp [scmul, coords, monom_coords_mul, left_distrib, ih]
Proof state after:
no goals
Theorem: FormalSum.scmul_coords
Proof state before:
case nil
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
r : R
x₀ : X
⊢ r * coords [] x₀ = coords (scmul r []) x₀
Tactic:
simp [coords]
Proof state after:
no goals
Theorem: FormalSum.scmul_coords
Proof state before:
case cons
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
r : R
x₀ : X
h : R × X
t : List (R × X)
ih : r * coords t x₀ = coords (scmul r t) x₀
⊢ r * coords (h :: t) x₀ = coords (scmul r (h :: t)) x₀
Tactic:
simp [scmul, coords, monom_coords_mul, left_distrib, ih]
Proof state after:
no goals
Theorem: FormalSum.append_coords
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
x₀ : X
⊢ coords s₁ x₀ + coords s₂ x₀ = coords (s₁ ++ s₂) x₀
Tactic:
induction s₁ with
| nil =>
  simp [coords]
| cons h t ih =>
  simp [coords, ← ih, add_assoc]
Proof state after:
no goals
Theorem: FormalSum.append_coords
Proof state before:
case nil
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s₂ : FormalSum R X
x₀ : X
⊢ coords [] x₀ + coords s₂ x₀ = coords ([] ++ s₂) x₀
Tactic:
simp [coords]
Proof state after:
no goals
Theorem: FormalSum.append_coords
Proof state before:
case cons
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s₂ : FormalSum R X
x₀ : X
h : R × X
t : List (R × X)
ih : coords t x₀ + coords s₂ x₀ = coords (t ++ s₂) x₀
⊢ coords (h :: t) x₀ + coords s₂ x₀ = coords (h :: t ++ s₂) x₀
Tactic:
simp [coords, ← ih, add_assoc]
Proof state after:
no goals
Theorem: FormalSum.append_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
⊢ s₁ ≈ s₂ → t₁ ≈ t₂ → s₁ ++ t₁ ≈ s₂ ++ t₂
Tactic:
intro eqv₁ eqv₂
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
eqv₁ : s₁ ≈ s₂
eqv₂ : t₁ ≈ t₂
⊢ s₁ ++ t₁ ≈ s₂ ++ t₂
Theorem: FormalSum.append_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
eqv₁ : s₁ ≈ s₂
eqv₂ : t₁ ≈ t₂
⊢ s₁ ++ t₁ ≈ s₂ ++ t₂
Tactic:
apply funext
Proof state after:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
eqv₁ : s₁ ≈ s₂
eqv₂ : t₁ ≈ t₂
⊢ ∀ (x : X), coords (s₁ ++ t₁) x = coords (s₂ ++ t₂) x
Theorem: FormalSum.append_equiv
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
eqv₁ : s₁ ≈ s₂
eqv₂ : t₁ ≈ t₂
⊢ ∀ (x : X), coords (s₁ ++ t₁) x = coords (s₂ ++ t₂) x
Tactic:
intro x₀
Proof state after:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
eqv₁ : s₁ ≈ s₂
eqv₂ : t₁ ≈ t₂
x₀ : X
⊢ coords (s₁ ++ t₁) x₀ = coords (s₂ ++ t₂) x₀
Theorem: FormalSum.append_equiv
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
eqv₁ : s₁ ≈ s₂
eqv₂ : t₁ ≈ t₂
x₀ : X
⊢ coords (s₁ ++ t₁) x₀ = coords (s₂ ++ t₂) x₀
Tactic:
rw [← append_coords]
Proof state after:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
eqv₁ : s₁ ≈ s₂
eqv₂ : t₁ ≈ t₂
x₀ : X
⊢ coords s₁ x₀ + coords t₁ x₀ = coords (s₂ ++ t₂) x₀
Theorem: FormalSum.append_equiv
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
eqv₁ : s₁ ≈ s₂
eqv₂ : t₁ ≈ t₂
x₀ : X
⊢ coords s₁ x₀ + coords t₁ x₀ = coords (s₂ ++ t₂) x₀
Tactic:
rw [← append_coords]
Proof state after:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
eqv₁ : s₁ ≈ s₂
eqv₂ : t₁ ≈ t₂
x₀ : X
⊢ coords s₁ x₀ + coords t₁ x₀ = coords s₂ x₀ + coords t₂ x₀
Theorem: FormalSum.append_equiv
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
eqv₁ : s₁ ≈ s₂
eqv₂ : t₁ ≈ t₂
x₀ : X
⊢ coords s₁ x₀ + coords t₁ x₀ = coords s₂ x₀ + coords t₂ x₀
Tactic:
have ls : coords s₁ x₀ = coords s₂ x₀ := by 
  apply congrFun eqv₁
Proof state after:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
eqv₁ : s₁ ≈ s₂
eqv₂ : t₁ ≈ t₂
x₀ : X
ls : coords s₁ x₀ = coords s₂ x₀
⊢ coords s₁ x₀ + coords t₁ x₀ = coords s₂ x₀ + coords t₂ x₀
Theorem: FormalSum.append_equiv
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
eqv₁ : s₁ ≈ s₂
eqv₂ : t₁ ≈ t₂
x₀ : X
ls : coords s₁ x₀ = coords s₂ x₀
⊢ coords s₁ x₀ + coords t₁ x₀ = coords s₂ x₀ + coords t₂ x₀
Tactic:
have lt : coords t₁ x₀ = coords t₂ x₀ := by 
  apply congrFun eqv₂
Proof state after:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
eqv₁ : s₁ ≈ s₂
eqv₂ : t₁ ≈ t₂
x₀ : X
ls : coords s₁ x₀ = coords s₂ x₀
lt : coords t₁ x₀ = coords t₂ x₀
⊢ coords s₁ x₀ + coords t₁ x₀ = coords s₂ x₀ + coords t₂ x₀
Theorem: FormalSum.append_equiv
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
eqv₁ : s₁ ≈ s₂
eqv₂ : t₁ ≈ t₂
x₀ : X
ls : coords s₁ x₀ = coords s₂ x₀
lt : coords t₁ x₀ = coords t₂ x₀
⊢ coords s₁ x₀ + coords t₁ x₀ = coords s₂ x₀ + coords t₂ x₀
Tactic:
rw [← ls, ← lt]
Proof state after:
no goals
Theorem: FormalSum.append_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
eqv₁ : s₁ ≈ s₂
eqv₂ : t₁ ≈ t₂
x₀ : X
⊢ coords s₁ x₀ = coords s₂ x₀
Tactic:
apply congrFun eqv₁
Proof state after:
no goals
Theorem: FormalSum.append_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
eqv₁ : s₁ ≈ s₂
eqv₂ : t₁ ≈ t₂
x₀ : X
ls : coords s₁ x₀ = coords s₂ x₀
⊢ coords t₁ x₀ = coords t₂ x₀
Tactic:
apply congrFun eqv₂
Proof state after:
no goals
Theorem: FormalSum.action
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a b : R
s : FormalSum R X
⊢ scmul a (scmul b s) = scmul (a * b) s
Tactic:
induction s with
| nil =>
  simp [scmul]
| cons h t ih =>
  simp [scmul, ih, mul_assoc]
Proof state after:
no goals
Theorem: FormalSum.action
Proof state before:
case nil
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a b : R
⊢ scmul a (scmul b []) = scmul (a * b) []
Tactic:
simp [scmul]
Proof state after:
no goals
Theorem: FormalSum.action
Proof state before:
case cons
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a (scmul b t) = scmul (a * b) t
⊢ scmul a (scmul b (h :: t)) = scmul (a * b) (h :: t)
Tactic:
simp [scmul, ih, mul_assoc]
Proof state after:
no goals
Theorem: FormalSum.act_sum
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
s : FormalSum R X
⊢ scmul a s ++ scmul b s ≈ scmul (a + b) s
Tactic:
induction s with
| nil =>
  simp [scmul]
  apply eqlCoords.refl
| cons h t ih =>
  apply funext; intro x₀
  let il₁ := congrFun ih x₀    
  rw [← append_coords]
  simp [scmul, coords, right_distrib, monom_coords_hom]
  rw [← append_coords] at il₁ 
  rw [← il₁]
  conv =>
    lhs
    rw [add_assoc]
    arg 2
    rw [← add_assoc]
    arg 1
    rw [add_comm]
  conv =>
    lhs
    rw [add_assoc]
    rw [← add_assoc]
Proof state after:
no goals
Theorem: FormalSum.act_sum
Proof state before:
case nil
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
⊢ scmul a [] ++ scmul b [] ≈ scmul (a + b) []
Tactic:
simp [scmul]
Proof state after:
case nil
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
⊢ [] ≈ []
Theorem: FormalSum.act_sum
Proof state before:
case nil
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
⊢ [] ≈ []
Tactic:
apply eqlCoords.refl
Proof state after:
no goals
Theorem: FormalSum.act_sum
Proof state before:
case cons
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
⊢ scmul a (h :: t) ++ scmul b (h :: t) ≈ scmul (a + b) (h :: t)
Tactic:
apply funext
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), coords (scmul a (h :: t) ++ scmul b (h :: t)) x = coords (scmul (a + b) (h :: 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), coords (scmul a (h :: t) ++ scmul b (h :: t)) x = coords (scmul (a + b) (h :: t)) x
Tactic:
intro x₀
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
⊢ coords (scmul a (h :: t) ++ scmul b (h :: t)) x₀ = coords (scmul (a + b) (h :: 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
⊢ coords (scmul a (h :: t) ++ scmul b (h :: t)) x₀ = coords (scmul (a + b) (h :: t)) x₀
Tactic:
let il₁ := congrFun ih x₀
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 ++ scmul b t) x₀ = coords (scmul (a + b) t) x₀ := congrFun ih x₀
⊢ coords (scmul a (h :: t) ++ scmul b (h :: t)) x₀ = coords (scmul (a + b) (h :: 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 ++ scmul b t) x₀ = coords (scmul (a + b) t) x₀ := congrFun ih x₀
⊢ coords (scmul a (h :: t) ++ scmul b (h :: t)) x₀ = coords (scmul (a + b) (h :: t)) x₀
Tactic:
rw [← append_coords]
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 ++ scmul b t) x₀ = coords (scmul (a + b) t) x₀ := congrFun ih x₀
⊢ coords (scmul a (h :: t)) x₀ + coords (scmul b (h :: t)) x₀ = coords (scmul (a + b) (h :: 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 ++ scmul b t) x₀ = coords (scmul (a + b) t) x₀ := congrFun ih x₀
⊢ coords (scmul a (h :: t)) x₀ + coords (scmul b (h :: t)) x₀ = coords (scmul (a + b) (h :: t)) x₀
Tactic:
simp [scmul, coords, right_distrib, monom_coords_hom]
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 ++ scmul b t) x₀ = coords (scmul (a + b) t) x₀ := congrFun ih 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 + 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 ++ scmul b t) x₀ = coords (scmul (a + b) t) x₀ := congrFun ih 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 + b) t) x₀
Tactic:
rw [← append_coords] at il₁
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) + 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 + 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) + 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 + b) t) x₀
Tactic:
rw [← il₁]
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) + 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₀)