internlm/Lean-Github huggingface dataset:
Theorem: GroupRing.first_arg_invariant
Proof state before:
case swap.h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) := swap a₁ a₂ x₁ x₂ tail
prev : mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail' :=
  first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel'
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) +
      coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀) +
      coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
Tactic:
let pl := congrFun prev x₀
Proof state after:
case swap.h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) := swap a₁ a₂ x₁ x₂ tail
prev : mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail' :=
  first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel'
pl : coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ :=
  congrFun prev x₀
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) +
      coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀) +
      coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
Theorem: GroupRing.first_arg_invariant
Proof state before:
case swap.h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) := swap a₁ a₂ x₁ x₂ tail
prev : mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail' :=
  first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel'
pl : coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ :=
  congrFun prev x₀
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) +
      coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀) +
      coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
Tactic:
rw [pl]
Proof state after:
case swap.h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) := swap a₁ a₂ x₁ x₂ tail
prev : mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail' :=
  first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel'
pl : coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ :=
  congrFun prev x₀
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) +
      coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀) +
      coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
Theorem: GroupRing.first_arg_invariant
Proof state before:
case swap.h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) := swap a₁ a₂ x₁ x₂ tail
prev : mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail' :=
  first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel'
pl : coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ :=
  congrFun prev x₀
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) +
      coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀) +
      coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
Tactic:
simp
Proof state after:
case swap.h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) := swap a₁ a₂ x₁ x₂ tail
prev : mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail' :=
  first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel'
pl : coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ :=
  congrFun prev x₀
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀)
Theorem: GroupRing.first_arg_invariant
Proof state before:
case swap.h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) := swap a₁ a₂ x₁ x₂ tail
prev : mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail' :=
  first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel'
pl : coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ :=
  congrFun prev x₀
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀)
Tactic:
rw [← add_assoc]
Proof state after:
case swap.h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) := swap a₁ a₂ x₁ x₂ tail
prev : mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail' :=
  first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel'
pl : coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ :=
  congrFun prev x₀
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀ =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀)
Theorem: GroupRing.first_arg_invariant
Proof state before:
case swap.h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) := swap a₁ a₂ x₁ x₂ tail
prev : mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail' :=
  first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel'
pl : coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ :=
  congrFun prev x₀
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀ =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀)
Tactic:
rw [← add_assoc]
Proof state after:
case swap.h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) := swap a₁ a₂ x₁ x₂ tail
prev : mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail' :=
  first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel'
pl : coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ :=
  congrFun prev x₀
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀ =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀
Theorem: GroupRing.first_arg_invariant
Proof state before:
case swap.h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) := swap a₁ a₂ x₁ x₂ tail
prev : mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail' :=
  first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel'
pl : coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ :=
  congrFun prev x₀
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀ =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀
Tactic:
simp
Proof state after:
case swap.h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) := swap a₁ a₂ x₁ x₂ tail
prev : mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail' :=
  first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel'
pl : coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ :=
  congrFun prev x₀
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + monomCoeff R G x₀ (a₂ * b, x₂ * h) =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h)
Theorem: GroupRing.first_arg_invariant
Proof state before:
case swap.h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
x₀ : G
rel' : ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) := swap a₁ a₂ x₁ x₂ tail
prev : mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail' :=
  first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel'
pl : coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ :=
  congrFun prev x₀
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + monomCoeff R G x₀ (a₂ * b, x₂ * h) =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h)
Tactic:
conv =>
  lhs 
  rw [add_comm]
Proof state after:
no goals
Theorem: GroupRing.first_arg_invariant
Proof state before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
x₀ : G
⊢ ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
Tactic:
apply ElementaryMove.swap
Proof state after:
no goals
Theorem: groupInclusionHom_injective'
Proof state before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
hR : 1 ≠ 0
⊢ Function.Injective ↑(groupInclusionHom G)
Tactic:
intro _ _
Proof state after:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
hR : 1 ≠ 0
a₁✝ a₂✝ : G
⊢ ↑(groupInclusionHom G) a₁✝ = ↑(groupInclusionHom G) a₂✝ → a₁✝ = a₂✝
Theorem: groupInclusionHom_injective'
Proof state before:
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
hR : 1 ≠ 0
a₁✝ a₂✝ : G
⊢ ↑(groupInclusionHom G) a₁✝ = ↑(groupInclusionHom G) a₂✝ → a₁✝ = a₂✝
Tactic:
apply baseInclusion_injective (1 : R) hR (X := G)
Proof state after:
no goals
Theorem: groupInclusionHom_injective
Proof state before:
R : Type
inst✝⁷ : Ring R
inst✝⁶ : DecidableEq R
G✝ : Type
inst✝⁵ : Group G✝
inst✝⁴ : DecidableEq G✝
F : Type
inst✝³ : Field F
inst✝² : DecidableEq F
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
⊢ Function.Injective ↑(groupInclusionHom G)
Tactic:
intro _ _
Proof state after:
R : Type
inst✝⁷ : Ring R
inst✝⁶ : DecidableEq R
G✝ : Type
inst✝⁵ : Group G✝
inst✝⁴ : DecidableEq G✝
F : Type
inst✝³ : Field F
inst✝² : DecidableEq F
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
a₁✝ a₂✝ : G
⊢ ↑(groupInclusionHom G) a₁✝ = ↑(groupInclusionHom G) a₂✝ → a₁✝ = a₂✝
Theorem: groupInclusionHom_injective
Proof state before:
R : Type
inst✝⁷ : Ring R
inst✝⁶ : DecidableEq R
G✝ : Type
inst✝⁵ : Group G✝
inst✝⁴ : DecidableEq G✝
F : Type
inst✝³ : Field F
inst✝² : DecidableEq F
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
a₁✝ a₂✝ : G
⊢ ↑(groupInclusionHom G) a₁✝ = ↑(groupInclusionHom G) a₂✝ → a₁✝ = a₂✝
Tactic:
apply groupInclusionHom_injective'
Proof state after:
case hR
R : Type
inst✝⁷ : Ring R
inst✝⁶ : DecidableEq R
G✝ : Type
inst✝⁵ : Group G✝
inst✝⁴ : DecidableEq G✝
F : Type
inst✝³ : Field F
inst✝² : DecidableEq F
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
a₁✝ a₂✝ : G
⊢ 1 ≠ 0
Theorem: groupInclusionHom_injective
Proof state before:
case hR
R : Type
inst✝⁷ : Ring R
inst✝⁶ : DecidableEq R
G✝ : Type
inst✝⁵ : Group G✝
inst✝⁴ : DecidableEq G✝
F : Type
inst✝³ : Field F
inst✝² : DecidableEq F
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
a₁✝ a₂✝ : G
⊢ 1 ≠ 0
Tactic:
have : (0 : F) ≠ (1 : F) := zero_ne_one
Proof state after:
case hR
R : Type
inst✝⁷ : Ring R
inst✝⁶ : DecidableEq R
G✝ : Type
inst✝⁵ : Group G✝
inst✝⁴ : DecidableEq G✝
F : Type
inst✝³ : Field F
inst✝² : DecidableEq F
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
a₁✝ a₂✝ : G
this : 0 ≠ 1
⊢ 1 ≠ 0
Theorem: groupInclusionHom_injective
Proof state before:
case hR
R : Type
inst✝⁷ : Ring R
inst✝⁶ : DecidableEq R
G✝ : Type
inst✝⁵ : Group G✝
inst✝⁴ : DecidableEq G✝
F : Type
inst✝³ : Field F
inst✝² : DecidableEq F
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
a₁✝ a₂✝ : G
this : 0 ≠ 1
⊢ 1 ≠ 0
Tactic:
simp_all only [ne_eq, zero_ne_one, not_false_iff, one_ne_zero]
Proof state after:
no goals
Theorem: ringInclusionHom_injective'
Proof state before:
R : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
G✝ : Type
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
⊢ Function.Injective ↑(ringInclusionHom G)
Tactic:
intro _ _
Proof state after:
R : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
G✝ : Type
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
a₁✝ a₂✝ : R
⊢ ↑(ringInclusionHom G) a₁✝ = ↑(ringInclusionHom G) a₂✝ → a₁✝ = a₂✝
Theorem: ringInclusionHom_injective'
Proof state before:
R : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
G✝ : Type
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
a₁✝ a₂✝ : R
⊢ ↑(ringInclusionHom G) a₁✝ = ↑(ringInclusionHom G) a₂✝ → a₁✝ = a₂✝
Tactic:
apply coeffInclusion_injective
Proof state after:
no goals
Theorem: monom_coords_hom
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x₀ x : X
a b : R
⊢ monomCoeff R X x₀ (a + b, x) = monomCoeff R X x₀ (a, x) + monomCoeff R X x₀ (b, x)
Tactic:
repeat
  (
    rw [monomCoeff])
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x₀ x : X
a b : R
⊢ (match (a + b, x).2 == x₀ with
    | true => (a + b, x).1
    | false => 0) =
    (match (a, x).2 == x₀ with
      | true => (a, x).1
      | false => 0) +
      match (b, x).2 == x₀ with
      | true => (b, x).1
      | false => 0
Theorem: monom_coords_hom
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x₀ x : X
a b : R
⊢ (match (a + b, x).2 == x₀ with
    | true => (a + b, x).1
    | false => 0) =
    (match (a, x).2 == x₀ with
      | true => (a, x).1
      | false => 0) +
      match (b, x).2 == x₀ with
      | true => (b, x).1
      | false => 0
Tactic:
cases x == x₀ <;> simp
Proof state after:
no goals
Theorem: monom_coords_hom
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x₀ x : X
a b : R
⊢ (match (a + b, x).2 == x₀ with
    | true => (a + b, x).1
    | false => 0) =
    (match (a, x).2 == x₀ with
      | true => (a, x).1
      | false => 0) +
      monomCoeff R X x₀ (b, x)
Tactic:
(
  rw [monomCoeff])
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x₀ x : X
a b : R
⊢ (match (a + b, x).2 == x₀ with
    | true => (a + b, x).1
    | false => 0) =
    (match (a, x).2 == x₀ with
      | true => (a, x).1
      | false => 0) +
      match (b, x).2 == x₀ with
      | true => (b, x).1
      | false => 0
Theorem: monom_coords_hom
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x₀ x : X
a b : R
⊢ (match (a + b, x).2 == x₀ with
    | true => (a + b, x).1
    | false => 0) =
    (match (a, x).2 == x₀ with
      | true => (a, x).1
      | false => 0) +
      monomCoeff R X x₀ (b, x)
Tactic:
rw [monomCoeff]
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x₀ x : X
a b : R
⊢ (match (a + b, x).2 == x₀ with
    | true => (a + b, x).1
    | false => 0) =
    (match (a, x).2 == x₀ with
      | true => (a, x).1
      | false => 0) +
      match (b, x).2 == x₀ with
      | true => (b, x).1
      | false => 0
Theorem: monom_coords_mul
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x x₀ : X
a b : R
⊢ monomCoeff R X x₀ (a * b, x) = a * monomCoeff R X x₀ (b, x)
Tactic:
repeat
  (
    rw [monomCoeff])
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x x₀ : X
a b : R
⊢ (match (a * b, x).2 == x₀ with
    | true => (a * b, x).1
    | false => 0) =
    a *
      match (b, x).2 == x₀ with
      | true => (b, x).1
      | false => 0
Theorem: monom_coords_mul
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x x₀ : X
a b : R
⊢ (match (a * b, x).2 == x₀ with
    | true => (a * b, x).1
    | false => 0) =
    a *
      match (b, x).2 == x₀ with
      | true => (b, x).1
      | false => 0
Tactic:
cases x == x₀ <;> simp
Proof state after:
no goals
Theorem: monom_coords_mul
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x x₀ : X
a b : R
⊢ (match (a * b, x).2 == x₀ with
    | true => (a * b, x).1
    | false => 0) =
    a * monomCoeff R X x₀ (b, x)
Tactic:
(
  rw [monomCoeff])
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x x₀ : X
a b : R
⊢ (match (a * b, x).2 == x₀ with
    | true => (a * b, x).1
    | false => 0) =
    a *
      match (b, x).2 == x₀ with
      | true => (b, x).1
      | false => 0
Theorem: monom_coords_mul
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x x₀ : X
a b : R
⊢ (match (a * b, x).2 == x₀ with
    | true => (a * b, x).1
    | false => 0) =
    a * monomCoeff R X x₀ (b, x)
Tactic:
rw [monomCoeff]
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x x₀ : X
a b : R
⊢ (match (a * b, x).2 == x₀ with
    | true => (a * b, x).1
    | false => 0) =
    a *
      match (b, x).2 == x₀ with
      | true => (b, x).1
      | false => 0
Theorem: monom_coords_at_zero
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x₀ x : X
⊢ monomCoeff R X x₀ (0, x) = 0
Tactic:
rw [monomCoeff]
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x₀ x : X
⊢ (match (0, x).2 == x₀ with
    | true => (0, x).1
    | false => 0) =
    0
Theorem: monom_coords_at_zero
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x₀ x : X
⊢ (match (0, x).2 == x₀ with
    | true => (0, x).1
    | false => 0) =
    0
Tactic:
cases x == x₀ <;> rfl
Proof state after:
no goals
Theorem: nonzero_coord_in_support
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
x : X
hyp : 0 ≠ coords [] x
⊢ x ∈ support []
Tactic:
have d : coords [] x = (0 : R) := by
  rfl
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
x : X
hyp : 0 ≠ coords [] x
d : coords [] x = 0
⊢ x ∈ support []
Theorem: nonzero_coord_in_support
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
x : X
hyp : 0 ≠ coords [] x
d : coords [] x = 0
⊢ x ∈ support []
Tactic:
rw [d] at hyp
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
x : X
hyp : 0 ≠ 0
d : coords [] x = 0
⊢ x ∈ support []
Theorem: nonzero_coord_in_support
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
x : X
hyp : 0 ≠ 0
d : coords [] x = 0
⊢ x ∈ support []
Tactic:
contradiction
Proof state after:
no goals
Theorem: nonzero_coord_in_support
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
x : X
hyp : 0 ≠ coords [] x
⊢ coords [] x = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: nonzero_coord_in_support
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
⊢ ∀ (x : X), 0 ≠ coords (h :: t) x → x ∈ support (h :: t)
Tactic:
intro x hyp
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
hyp : 0 ≠ coords (h :: t) x
⊢ x ∈ support (h :: t)
Theorem: nonzero_coord_in_support
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
hyp : 0 ≠ coords (h :: t) x
⊢ x ∈ support (h :: t)
Tactic:
let (a₀, x₀) := h
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
⊢ x ∈ support ((a₀, x₀) :: t)