internlm/Lean-Github huggingface dataset:
Theorem: Groupoid.Functor.map_id'
Proof state before:
R : Sort ?u.16460
S : Sort u_3
T : Sort u_2
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X : S
this : 𝟙 (Quiver.PreFunctor.obj Φ.toFunctor.toPreFunctor X) = Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X)
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X) = 𝟙 (Quiver.PreFunctor.obj Φ.toFunctor.toPreFunctor X)
Tactic:
exact this.symm
Proof state after:
no goals
Theorem: Groupoid.Functor.map_inv
Proof state before:
R : Sort ?u.16958
S : Sort u_1
T : Sort u_4
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X Y : S
g : X ⟶ Y
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g ⁻¹ = (Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g) ⁻¹
Tactic:
apply (Groupoid.left_cancel (Φ.map g) _ _).mp
Proof state after:
R : Sort ?u.16958
S : Sort u_1
T : Sort u_4
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X Y : S
g : X ⟶ Y
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g ≫ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g ⁻¹ =
    Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g ≫ (Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g) ⁻¹
Theorem: Groupoid.Functor.map_inv
Proof state before:
R : Sort ?u.16958
S : Sort u_1
T : Sort u_4
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X Y : S
g : X ⟶ Y
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g ≫ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g ⁻¹ =
    Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g ≫ (Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g) ⁻¹
Tactic:
rw [← Φ.map_comp]
Proof state after:
R : Sort ?u.16958
S : Sort u_1
T : Sort u_4
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X Y : S
g : X ⟶ Y
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (g ≫ g ⁻¹ ) =
    Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g ≫ (Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g) ⁻¹
Theorem: Groupoid.Functor.map_inv
Proof state before:
R : Sort ?u.16958
S : Sort u_1
T : Sort u_4
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X Y : S
g : X ⟶ Y
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (g ≫ g ⁻¹ ) =
    Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g ≫ (Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor g) ⁻¹
Tactic:
simp
Proof state after:
no goals
Theorem: AutAction.vadd_zero
Proof state before:
A : Type u_2
B : Type u_1
inst✝² : AddGroup A
inst✝¹ : AddGroup B
α : A → B →+ B
inst✝ : AutAction α
⊢ ∀ {a : A}, a +ᵥ 0 = 0
Tactic:
aesop (rule_sets [AutAction])
Proof state after:
no goals
Theorem: AutAction.vadd_dist
Proof state before:
A : Type u_2
B : Type u_1
inst✝² : AddGroup A
inst✝¹ : AddGroup B
α : A → B →+ B
inst✝ : AutAction α
⊢ ∀ {a : A} {b b' : B}, a +ᵥ (b + b') = a +ᵥ b + (a +ᵥ b')
Tactic:
aesop (rule_sets [AutAction])
Proof state after:
no goals
Theorem: AutAction.compatibility'
Proof state before:
A : Type u_2
B : Type u_1
inst✝² : AddGroup A
inst✝¹ : AddGroup B
α : A → B →+ B
inst✝ : AutAction α
⊢ ∀ {a a' : A} {b : B}, ↑(α a) (↑(α a') b) = ↑(α (a + a')) b
Tactic:
aesop (rule_sets [AutAction])
Proof state after:
no goals
Theorem: AutAction.act_neg_act
Proof state before:
A : Type u_2
B : Type u_1
inst✝² : AddGroup A
inst✝¹ : AddGroup B
α : A → B →+ B
inst✝ : AutAction α
a : A
b : B
⊢ ↑(α a) (↑(α (-a)) b) = b
Tactic:
rw [compatibility']
Proof state after:
A : Type u_2
B : Type u_1
inst✝² : AddGroup A
inst✝¹ : AddGroup B
α : A → B →+ B
inst✝ : AutAction α
a : A
b : B
⊢ ↑(α (a + -a)) b = b
Theorem: AutAction.act_neg_act
Proof state before:
A : Type u_2
B : Type u_1
inst✝² : AddGroup A
inst✝¹ : AddGroup B
α : A → B →+ B
inst✝ : AutAction α
a : A
b : B
⊢ ↑(α (a + -a)) b = b
Tactic:
aesop (erase compatibility) (rule_sets [AutAction])
Proof state after:
no goals
Theorem: AutAction.vadd_of_neg
Proof state before:
A : Type u_2
B : Type u_1
inst✝² : AddGroup A
inst✝¹ : AddGroup B
α : A → B →+ B
inst✝ : AutAction α
⊢ ∀ {a : A} {b : B}, a +ᵥ -b = -(a +ᵥ b)
Tactic:
aesop (rule_sets [AutAction])
Proof state after:
no goals
Theorem: Cocycle.left_id
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
⊢ c 0 q = 0
Tactic:
have := ccl.cocycle_condition 0 0 q
Proof state after:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c 0 0 + c (0 + 0) q = 0 +ᵥ c 0 q + c 0 (0 + q)
⊢ c 0 q = 0
Theorem: Cocycle.left_id
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c 0 0 + c (0 + 0) q = 0 +ᵥ c 0 q + c 0 (0 + q)
⊢ c 0 q = 0
Tactic:
rw [add_zero, zero_add, ccl.cocycle_zero, zero_add, zero_vadd] at this
Proof state after:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c 0 q = c 0 q + c 0 q
⊢ c 0 q = 0
Theorem: Cocycle.left_id
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c 0 q = c 0 q + c 0 q
⊢ c 0 q = 0
Tactic:
simp at this
Proof state after:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c 0 q = 0
⊢ c 0 q = 0
Theorem: Cocycle.left_id
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c 0 q = 0
⊢ c 0 q = 0
Tactic:
assumption
Proof state after:
no goals
Theorem: Cocycle.right_id
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
⊢ c q 0 = 0
Tactic:
have := ccl.cocycle_condition q 0 0
Proof state after:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c q 0 + c (q + 0) 0 = q +ᵥ c 0 0 + c q (0 + 0)
⊢ c q 0 = 0
Theorem: Cocycle.right_id
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c q 0 + c (q + 0) 0 = q +ᵥ c 0 0 + c q (0 + 0)
⊢ c q 0 = 0
Tactic:
rw [add_zero, zero_add, ccl.cocycle_zero] at this
Proof state after:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c q 0 + c q 0 = q +ᵥ 0 + c q 0
⊢ c q 0 = 0
Theorem: Cocycle.right_id
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c q 0 + c q 0 = q +ᵥ 0 + c q 0
⊢ c q 0 = 0
Tactic:
simp at this
Proof state after:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c q 0 = q +ᵥ 0
⊢ c q 0 = 0
Theorem: Cocycle.right_id
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c q 0 = q +ᵥ 0
⊢ c q 0 = 0
Tactic:
rw [this, AutAction.vadd_zero]
Proof state after:
no goals
Theorem: Cocycle.inv_rel
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
⊢ c q (-q) = q +ᵥ c (-q) q
Tactic:
have := ccl.cocycle_condition q (-q) q
Proof state after:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c q (-q) + c (q + -q) q = q +ᵥ c (-q) q + c q (-q + q)
⊢ c q (-q) = q +ᵥ c (-q) q
Theorem: Cocycle.inv_rel
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c q (-q) + c (q + -q) q = q +ᵥ c (-q) q + c q (-q + q)
⊢ c q (-q) = q +ᵥ c (-q) q
Tactic:
simp_all only [add_right_neg, left_id, add_zero, AutAction.vadd_eq, add_left_neg, right_id]
Proof state after:
no goals
Theorem: Cocycle.inv_rel'
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
⊢ c (-q) q = -q +ᵥ c q (-q)
Tactic:
have := inv_rel c (-q)
Proof state after:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c (-q) (- -q) = -q +ᵥ c (- -q) (-q)
⊢ c (-q) q = -q +ᵥ c q (-q)
Theorem: Cocycle.inv_rel'
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c (-q) (- -q) = -q +ᵥ c (- -q) (-q)
⊢ c (-q) q = -q +ᵥ c q (-q)
Tactic:
simp_all only [neg_neg]
Proof state after:
no goals
Theorem: GroupRing.mul_monom_zero
Proof state before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
g x₀ : G
s : FormalSum R G
⊢ coords (mulMonom 0 g s) x₀ = 0
Tactic:
induction s with
| nil =>  
  simp [mulMonom, coords]
| cons h t ih => 
  simp [mulMonom, coords, monom_coords_at_zero]
  assumption
Proof state after:
no goals
Theorem: GroupRing.mul_monom_zero
Proof state before:
case nil
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
g x₀ : G
⊢ coords (mulMonom 0 g []) x₀ = 0
Tactic:
simp [mulMonom, coords]
Proof state after:
no goals
Theorem: GroupRing.mul_monom_zero
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
g x₀ : G
h : R × G
t : List (R × G)
ih : coords (mulMonom 0 g t) x₀ = 0
⊢ coords (mulMonom 0 g (h :: t)) x₀ = 0
Tactic:
simp [mulMonom, coords, monom_coords_at_zero]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
g x₀ : G
h : R × G
t : List (R × G)
ih : coords (mulMonom 0 g t) x₀ = 0
⊢ coords (mulMonom 0 g t) x₀ = 0
Theorem: GroupRing.mul_monom_zero
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
g x₀ : G
h : R × G
t : List (R × G)
ih : coords (mulMonom 0 g t) x₀ = 0
⊢ coords (mulMonom 0 g t) x₀ = 0
Tactic:
assumption
Proof state after:
no goals
Theorem: GroupRing.mul_monom_dist
Proof state before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ s₂ : FormalSum R G
⊢ coords (mulMonom b h (s₁ ++ s₂)) x₀ = coords (mulMonom b h s₁) x₀ + coords (mulMonom b h s₂) x₀
Tactic:
induction s₁ with
| nil => 
  simp [mulMonom, coords]
| cons head tail ih =>
  simp [mulMonom, coords]
  rw [ih]
  simp [add_assoc]
Proof state after:
no goals
Theorem: GroupRing.mul_monom_dist
Proof state before:
case nil
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₂ : FormalSum R G
⊢ coords (mulMonom b h ([] ++ s₂)) x₀ = coords (mulMonom b h []) x₀ + coords (mulMonom b h s₂) x₀
Tactic:
simp [mulMonom, coords]
Proof state after:
no goals
Theorem: GroupRing.mul_monom_dist
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₂ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (tail ++ s₂)) x₀ = coords (mulMonom b h tail) x₀ + coords (mulMonom b h s₂) x₀
⊢ coords (mulMonom b h (head :: tail ++ s₂)) x₀ = coords (mulMonom b h (head :: tail)) x₀ + coords (mulMonom b h s₂) x₀
Tactic:
simp [mulMonom, coords]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₂ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (tail ++ s₂)) x₀ = coords (mulMonom b h tail) x₀ + coords (mulMonom b h s₂) x₀
⊢ monomCoeff R G x₀ (head.1 * b, head.2 * h) + coords (mulMonom b h (tail ++ s₂)) x₀ =
    monomCoeff R G x₀ (head.1 * b, head.2 * h) + coords (mulMonom b h tail) x₀ + coords (mulMonom b h s₂) x₀
Theorem: GroupRing.mul_monom_dist
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₂ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (tail ++ s₂)) x₀ = coords (mulMonom b h tail) x₀ + coords (mulMonom b h s₂) x₀
⊢ monomCoeff R G x₀ (head.1 * b, head.2 * h) + coords (mulMonom b h (tail ++ s₂)) x₀ =
    monomCoeff R G x₀ (head.1 * b, head.2 * h) + coords (mulMonom b h tail) x₀ + coords (mulMonom b h s₂) x₀
Tactic:
rw [ih]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₂ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (tail ++ s₂)) x₀ = coords (mulMonom b h tail) x₀ + coords (mulMonom b h s₂) x₀
⊢ monomCoeff R G x₀ (head.1 * b, head.2 * h) + (coords (mulMonom b h tail) x₀ + coords (mulMonom b h s₂) x₀) =
    monomCoeff R G x₀ (head.1 * b, head.2 * h) + coords (mulMonom b h tail) x₀ + coords (mulMonom b h s₂) x₀
Theorem: GroupRing.mul_monom_dist
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₂ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (tail ++ s₂)) x₀ = coords (mulMonom b h tail) x₀ + coords (mulMonom b h s₂) x₀
⊢ monomCoeff R G x₀ (head.1 * b, head.2 * h) + (coords (mulMonom b h tail) x₀ + coords (mulMonom b h s₂) x₀) =
    monomCoeff R G x₀ (head.1 * b, head.2 * h) + coords (mulMonom b h tail) x₀ + coords (mulMonom b h s₂) x₀
Tactic:
simp [add_assoc]
Proof state after:
no goals
Theorem: GroupRing.mul_dist
Proof state before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x₀ : G
s₁ s₂ s₃ : FormalSum R G
⊢ coords (mul s₁ (s₂ ++ s₃)) x₀ = coords (mul s₁ s₂) x₀ + coords (mul s₁ s₃) x₀
Tactic:
induction s₂ with
| nil => 
  simp [mulMonom, coords]
| cons head tail ih =>
  simp [mulMonom, coords, mul]
  rw [← append_coords]
  rw [← append_coords]
  rw [ih]
  simp [add_assoc]
Proof state after:
no goals
Theorem: GroupRing.mul_dist
Proof state before:
case nil
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x₀ : G
s₁ s₃ : FormalSum R G
⊢ coords (mul s₁ ([] ++ s₃)) x₀ = coords (mul s₁ []) x₀ + coords (mul s₁ s₃) x₀
Tactic:
simp [mulMonom, coords]
Proof state after:
no goals
Theorem: GroupRing.mul_dist
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x₀ : G
s₁ s₃ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mul s₁ (tail ++ s₃)) x₀ = coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
⊢ coords (mul s₁ (head :: tail ++ s₃)) x₀ = coords (mul s₁ (head :: tail)) x₀ + coords (mul s₁ s₃) x₀
Tactic:
simp [mulMonom, coords, mul]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x₀ : G
s₁ s₃ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mul s₁ (tail ++ s₃)) x₀ = coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
⊢ coords (mulMonom head.1 head.2 s₁ ++ mul s₁ (tail ++ s₃)) x₀ =
    coords (mulMonom head.1 head.2 s₁ ++ mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
Theorem: GroupRing.mul_dist
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x₀ : G
s₁ s₃ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mul s₁ (tail ++ s₃)) x₀ = coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
⊢ coords (mulMonom head.1 head.2 s₁ ++ mul s₁ (tail ++ s₃)) x₀ =
    coords (mulMonom head.1 head.2 s₁ ++ mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
Tactic:
rw [← append_coords]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x₀ : G
s₁ s₃ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mul s₁ (tail ++ s₃)) x₀ = coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
⊢ coords (mulMonom head.1 head.2 s₁) x₀ + coords (mul s₁ (tail ++ s₃)) x₀ =
    coords (mulMonom head.1 head.2 s₁ ++ mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
Theorem: GroupRing.mul_dist
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x₀ : G
s₁ s₃ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mul s₁ (tail ++ s₃)) x₀ = coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
⊢ coords (mulMonom head.1 head.2 s₁) x₀ + coords (mul s₁ (tail ++ s₃)) x₀ =
    coords (mulMonom head.1 head.2 s₁ ++ mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
Tactic:
rw [← append_coords]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x₀ : G
s₁ s₃ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mul s₁ (tail ++ s₃)) x₀ = coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
⊢ coords (mulMonom head.1 head.2 s₁) x₀ + coords (mul s₁ (tail ++ s₃)) x₀ =
    coords (mulMonom head.1 head.2 s₁) x₀ + coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
Theorem: GroupRing.mul_dist
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x₀ : G
s₁ s₃ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mul s₁ (tail ++ s₃)) x₀ = coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
⊢ coords (mulMonom head.1 head.2 s₁) x₀ + coords (mul s₁ (tail ++ s₃)) x₀ =
    coords (mulMonom head.1 head.2 s₁) x₀ + coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
Tactic:
rw [ih]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x₀ : G
s₁ s₃ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mul s₁ (tail ++ s₃)) x₀ = coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
⊢ coords (mulMonom head.1 head.2 s₁) x₀ + (coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀) =
    coords (mulMonom head.1 head.2 s₁) x₀ + coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
Theorem: GroupRing.mul_dist
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x₀ : G
s₁ s₃ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mul s₁ (tail ++ s₃)) x₀ = coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
⊢ coords (mulMonom head.1 head.2 s₁) x₀ + (coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀) =
    coords (mulMonom head.1 head.2 s₁) x₀ + coords (mul s₁ tail) x₀ + coords (mul s₁ s₃) x₀
Tactic:
simp [add_assoc]
Proof state after:
no goals
Theorem: GroupRing.mul_monom_monom_assoc
Proof state before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x : G
a b : R
h x₀ : G
s : FormalSum R G
⊢ coords (mulMonom b h (mulMonom a x s)) x₀ = coords (mulMonom (a * b) (x * h) s) x₀
Tactic:
induction s with
| nil => 
  simp [mulMonom, coords]
| cons head tail ih =>
  let (a₁, x₁) := head
  simp [mulMonom, coords, mul_assoc]
  rw [ih]
Proof state after:
no goals
Theorem: GroupRing.mul_monom_monom_assoc
Proof state before:
case nil
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x : G
a b : R
h x₀ : G
⊢ coords (mulMonom b h (mulMonom a x [])) x₀ = coords (mulMonom (a * b) (x * h) []) x₀
Tactic:
simp [mulMonom, coords]
Proof state after:
no goals
Theorem: GroupRing.mul_monom_monom_assoc
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x : G
a b : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mulMonom a x tail)) x₀ = coords (mulMonom (a * b) (x * h) tail) x₀
⊢ coords (mulMonom b h (mulMonom a x (head :: tail))) x₀ = coords (mulMonom (a * b) (x * h) (head :: tail)) x₀
Tactic:
let (a₁, x₁) := head
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x : G
a b : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mulMonom a x tail)) x₀ = coords (mulMonom (a * b) (x * h) tail) x₀
a₁ : R
x₁ : G
⊢ coords (mulMonom b h (mulMonom a x ((a₁, x₁) :: tail))) x₀ = coords (mulMonom (a * b) (x * h) ((a₁, x₁) :: tail)) x₀
Theorem: GroupRing.mul_monom_monom_assoc
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x : G
a b : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mulMonom a x tail)) x₀ = coords (mulMonom (a * b) (x * h) tail) x₀
a₁ : R
x₁ : G
⊢ coords (mulMonom b h (mulMonom a x ((a₁, x₁) :: tail))) x₀ = coords (mulMonom (a * b) (x * h) ((a₁, x₁) :: tail)) x₀
Tactic:
simp [mulMonom, coords, mul_assoc]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x : G
a b : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mulMonom a x tail)) x₀ = coords (mulMonom (a * b) (x * h) tail) x₀
a₁ : R
x₁ : G
⊢ coords (mulMonom b h (mulMonom a x tail)) x₀ = coords (mulMonom (a * b) (x * h) tail) x₀
Theorem: GroupRing.mul_monom_monom_assoc
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
x : G
a b : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mulMonom a x tail)) x₀ = coords (mulMonom (a * b) (x * h) tail) x₀
a₁ : R
x₁ : G
⊢ coords (mulMonom b h (mulMonom a x tail)) x₀ = coords (mulMonom (a * b) (x * h) tail) x₀
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: GroupRing.mul_monom_assoc
Proof state before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ s₂ : FormalSum R G
⊢ coords (mulMonom b h (mul s₁ s₂)) x₀ = coords (mul s₁ (mulMonom b h s₂)) x₀
Tactic:
induction s₂ with
| nil => 
  simp [mulMonom, coords]
| cons head tail ih =>
  let (a, x) := head
  simp [mulMonom, coords, mul]
  rw [← append_coords]
  rw [mul_monom_dist]
  rw [ih]
  simp [add_assoc, mulMonom]
  rw [mul_monom_monom_assoc]
Proof state after:
no goals
Theorem: GroupRing.mul_monom_assoc
Proof state before:
case nil
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ : FormalSum R G
⊢ coords (mulMonom b h (mul s₁ [])) x₀ = coords (mul s₁ (mulMonom b h [])) x₀
Tactic:
simp [mulMonom, coords]
Proof state after:
no goals
Theorem: GroupRing.mul_monom_assoc
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mul s₁ tail)) x₀ = coords (mul s₁ (mulMonom b h tail)) x₀
⊢ coords (mulMonom b h (mul s₁ (head :: tail))) x₀ = coords (mul s₁ (mulMonom b h (head :: tail))) x₀
Tactic:
let (a, x) := head
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mul s₁ tail)) x₀ = coords (mul s₁ (mulMonom b h tail)) x₀
a : R
x : G
⊢ coords (mulMonom b h (mul s₁ ((a, x) :: tail))) x₀ = coords (mul s₁ (mulMonom b h ((a, x) :: tail))) x₀
Theorem: GroupRing.mul_monom_assoc
Proof state before:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mul s₁ tail)) x₀ = coords (mul s₁ (mulMonom b h tail)) x₀
a : R
x : G
⊢ coords (mulMonom b h (mul s₁ ((a, x) :: tail))) x₀ = coords (mul s₁ (mulMonom b h ((a, x) :: tail))) x₀
Tactic:
simp [mulMonom, coords, mul]
Proof state after:
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mul s₁ tail)) x₀ = coords (mul s₁ (mulMonom b h tail)) x₀
a : R
x : G
⊢ coords (mulMonom b h (mulMonom a x s₁ ++ mul s₁ tail)) x₀ =
    coords (mulMonom (a * b) (x * h) s₁ ++ mul s₁ (mulMonom b h tail)) x₀