internlm/Lean-Github huggingface dataset:
Theorem: FormalSum.equiv_of_equal_coeffs
Proof state before:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
x : X
d : monomCoeff R X x (coords t x₀, x₀) + coords ys x = coords t x
⊢ monomCoeff R X x (a₀ + coords t x₀, x₀) + coords ys x =
    monomCoeff R X x (a₀, x₀) + (monomCoeff R X x (coords t x₀, x₀) + coords ys x)
Tactic:
simp [monom_coords_hom, coords, add_assoc]
Proof state after:
no goals
Theorem: FormalSum.equiv_of_equal_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
⊢ List.length ys + 1 < List.length t + 1
Tactic:
apply Nat.succ_lt_succ
Proof state after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
⊢ List.length ys < List.length t
Theorem: FormalSum.equiv_of_equal_coeffs
Proof state before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
⊢ List.length ys < List.length t
Tactic:
exact ineqn
Proof state after:
no goals
Theorem: FormalSum.equiv_of_equal_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
_x✝ : (s₁ : FormalSum R X) ×' (s₂ : FormalSum R X) ×' ∀ (x : X), coords s₁ x = coords s₂ x
a✝² :
  ∀ (y : (s₁ : FormalSum R X) ×' (s₂ : FormalSum R X) ×' ∀ (x : X), coords s₁ x = coords s₂ x),
    (invImage (fun a => PSigma.casesOn a fun s snd => PSigma.casesOn snd fun s₂ snd => List.length s)
            instWellFoundedRelation).1
        y _x✝ →
      y.1 ≃ y.2.1
s₁ : FormalSum R X
s₂✝ : (s₂ : FormalSum R X) ×' ∀ (x : X), coords s₁ x = coords s₂ x
a✝¹ :
  ∀ (y : (s₁ : FormalSum R X) ×' (s₂ : FormalSum R X) ×' ∀ (x : X), coords s₁ x = coords s₂ x),
    (invImage (fun a => PSigma.casesOn a fun s snd => PSigma.casesOn snd fun s₂ snd => List.length s)
            instWellFoundedRelation).1
        y { fst := s₁, snd := s₂✝ } →
      y.1 ≃ y.2.1
s₂ : FormalSum R X
hyp✝¹ : ∀ (x : X), coords s₁ x = coords s₂ x
a✝ :
  ∀ (y : (s₁ : FormalSum R X) ×' (s₂ : FormalSum R X) ×' ∀ (x : X), coords s₁ x = coords s₂ x),
    (invImage (fun a => PSigma.casesOn a fun s snd => PSigma.casesOn snd fun s₂ snd => List.length s)
            instWellFoundedRelation).1
        y { fst := s₁, snd := { fst := s₂, snd := hyp✝¹ } } →
      y.1 ≃ y.2.1
h : R × X
t : List (R × X)
hyp✝ : ∀ (x : X), coords (h :: t) x = coords s₂ x
x✝¹ :
  ∀ (y : (s₁ : FormalSum R X) ×' (s₂ : FormalSum R X) ×' ∀ (x : X), coords s₁ x = coords s₂ x),
    (invImage (fun a => PSigma.casesOn a fun s snd => PSigma.casesOn snd fun s₂ snd => List.length s)
            instWellFoundedRelation).1
        y { fst := h :: t, snd := { fst := s₂, snd := hyp✝ } } →
      y.1 ≃ y.2.1
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
⊢ (invImage (fun a => PSigma.casesOn a fun s snd => PSigma.casesOn snd fun s₂ snd => List.length s)
        instWellFoundedRelation).1
    { fst := s₃, snd := { fst := s₂, snd := (_ : ∀ (x : X), coords s₃ x = coords s₂ x) } }
    { fst := h :: t, snd := { fst := s₂, snd := hyp✝ } }
Tactic:
assumption
Proof state after:
no goals
Theorem: FormalSum.func_eql_of_move_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
⊢ (∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂) → ∀ (s₁ s₂ : FormalSum R X), s₁ ≈ s₂ → f s₁ = f s₂
Tactic:
intro hyp
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
⊢ ∀ (s₁ s₂ : FormalSum R X), s₁ ≈ s₂ → f s₁ = f s₂
Theorem: FormalSum.func_eql_of_move_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
⊢ ∀ (s₁ s₂ : FormalSum R X), s₁ ≈ s₂ → f s₁ = f s₂
Tactic:
let fbar : FreeModuleAux R X → β := Quot.lift f hyp
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
⊢ ∀ (s₁ s₂ : FormalSum R X), s₁ ≈ s₂ → f s₁ = f s₂
Theorem: FormalSum.func_eql_of_move_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
⊢ ∀ (s₁ s₂ : FormalSum R X), s₁ ≈ s₂ → f s₁ = f s₂
Tactic:
let fct : ∀ s : FormalSum R X, f s = fbar (sum s) := by
  apply Quot.liftBeta
  apply hyp
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
⊢ ∀ (s₁ s₂ : FormalSum R X), s₁ ≈ s₂ → f s₁ = f s₂
Theorem: FormalSum.func_eql_of_move_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
⊢ ∀ (s₁ s₂ : FormalSum R X), s₁ ≈ s₂ → f s₁ = f s₂
Tactic:
intro s₁ s₂ sim
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
⊢ f s₁ = f s₂
Theorem: FormalSum.func_eql_of_move_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
⊢ f s₁ = f s₂
Tactic:
have ec : eqlCoords R X s₁ s₂ := sim
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : eqlCoords R X s₁ s₂
⊢ f s₁ = f s₂
Theorem: FormalSum.func_eql_of_move_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : eqlCoords R X s₁ s₂
⊢ f s₁ = f s₂
Tactic:
rw [eqlCoords] at ec
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
⊢ f s₁ = f s₂
Theorem: FormalSum.func_eql_of_move_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
⊢ f s₁ = f s₂
Tactic:
have pullback : sum s₁ = sum s₂ := by
  apply equiv_of_equal_coeffs
  intro x
  exact congrFun ec x
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
pullback : sum s₁ = sum s₂
⊢ f s₁ = f s₂
Theorem: FormalSum.func_eql_of_move_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
pullback : sum s₁ = sum s₂
⊢ f s₁ = f s₂
Tactic:
simp [fct, pullback]
Proof state after:
no goals
Theorem: FormalSum.func_eql_of_move_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
⊢ ∀ (s : FormalSum R X), f s = fbar (sum s)
Tactic:
apply Quot.liftBeta
Proof state after:
case c
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
⊢ ∀ (a b : FormalSum R X), ?r a b → f a = f b

case r
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
⊢ FormalSum R X → FormalSum R X → Prop
Theorem: FormalSum.func_eql_of_move_equiv
Proof state before:
case c
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
⊢ ∀ (a b : FormalSum R X), ?r a b → f a = f b

case r
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
⊢ FormalSum R X → FormalSum R X → Prop
Tactic:
apply hyp
Proof state after:
no goals
Theorem: FormalSum.func_eql_of_move_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
⊢ sum s₁ = sum s₂
Tactic:
apply equiv_of_equal_coeffs
Proof state after:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
⊢ ∀ (x : X), coords s₁ x = coords s₂ x
Theorem: FormalSum.func_eql_of_move_equiv
Proof state before:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
⊢ ∀ (x : X), coords s₁ x = coords s₂ x
Tactic:
intro x
Proof state after:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
x : X
⊢ coords s₁ x = coords s₂ x
Theorem: FormalSum.func_eql_of_move_equiv
Proof state before:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
x : X
⊢ coords s₁ x = coords s₂ x
Tactic:
exact congrFun ec x
Proof state after:
no goals
Theorem: monom_elem_eq_of_coord_eq_nonzero
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
non_zero : a ≠ 0
x₀ x₁ : X
⊢ coords [(a, x₀)] = coords [(a, x₁)] → x₀ = x₁
Tactic:
intro hyp
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
non_zero : a ≠ 0
x₀ x₁ : X
hyp : coords [(a, x₀)] = coords [(a, x₁)]
⊢ x₀ = x₁
Theorem: monom_elem_eq_of_coord_eq_nonzero
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
non_zero : a ≠ 0
x₀ x₁ : X
hyp : coords [(a, x₀)] = coords [(a, x₁)]
⊢ x₀ = x₁
Tactic:
have sup₀ : support [(a, x₀)] = [x₀] := by
  rfl
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
non_zero : a ≠ 0
x₀ x₁ : X
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
⊢ x₀ = x₁
Theorem: monom_elem_eq_of_coord_eq_nonzero
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
non_zero : a ≠ 0
x₀ x₁ : X
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
⊢ x₀ = x₁
Tactic:
have c₁ : coords [(a, x₁)] x₁ = a := by
  simp [coords, monomCoeff]
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
non_zero : a ≠ 0
x₀ x₁ : X
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
⊢ x₀ = x₁
Theorem: monom_elem_eq_of_coord_eq_nonzero
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
non_zero : a ≠ 0
x₀ x₁ : X
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
⊢ x₀ = x₁
Tactic:
rw [← c₁] at non_zero
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : coords [(a, x₁)] x₁ ≠ 0
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
⊢ x₀ = x₁
Theorem: monom_elem_eq_of_coord_eq_nonzero
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : coords [(a, x₁)] x₁ ≠ 0
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
⊢ x₀ = x₁
Tactic:
symm at non_zero
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₁)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
⊢ x₀ = x₁
Theorem: monom_elem_eq_of_coord_eq_nonzero
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₁)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
⊢ x₀ = x₁
Tactic:
rw [← hyp] at non_zero
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₀)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
⊢ x₀ = x₁
Theorem: monom_elem_eq_of_coord_eq_nonzero
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₀)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
⊢ x₀ = x₁
Tactic:
let lem := nonzero_coord_in_support [(a, x₀)] x₁ non_zero
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₀)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
lem : x₁ ∈ support [(a, x₀)] := nonzero_coord_in_support [(a, x₀)] x₁ non_zero
⊢ x₀ = x₁
Theorem: monom_elem_eq_of_coord_eq_nonzero
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₀)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
lem : x₁ ∈ support [(a, x₀)] := nonzero_coord_in_support [(a, x₀)] x₁ non_zero
⊢ x₀ = x₁
Tactic:
simp [support] at lem
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₀)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
lem : x₁ = x₀
⊢ x₀ = x₁
Theorem: monom_elem_eq_of_coord_eq_nonzero
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₀)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
lem : x₁ = x₀
⊢ x₀ = x₁
Tactic:
apply Eq.symm
Proof state after:
case h
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₀)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
lem : x₁ = x₀
⊢ x₁ = x₀
Theorem: monom_elem_eq_of_coord_eq_nonzero
Proof state before:
case h
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₀)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
lem : x₁ = x₀
⊢ x₁ = x₀
Tactic:
assumption
Proof state after:
no goals
Theorem: monom_elem_eq_of_coord_eq_nonzero
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
non_zero : a ≠ 0
x₀ x₁ : X
hyp : coords [(a, x₀)] = coords [(a, x₁)]
⊢ support [(a, x₀)] = [x₀]
Tactic:
rfl
Proof state after:
no goals
Theorem: monom_elem_eq_of_coord_eq_nonzero
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
non_zero : a ≠ 0
x₀ x₁ : X
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
⊢ coords [(a, x₁)] x₁ = a
Tactic:
simp [coords, monomCoeff]
Proof state after:
no goals
Theorem: monom_coeff_eq_of_coord_eq
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x : X
a₀ a₁ : R
⊢ coords [(a₀, x)] = coords [(a₁, x)] → a₀ = a₁
Tactic:
intro hyp
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x : X
a₀ a₁ : R
hyp : coords [(a₀, x)] = coords [(a₁, x)]
⊢ a₀ = a₁
Theorem: monom_coeff_eq_of_coord_eq
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x : X
a₀ a₁ : R
hyp : coords [(a₀, x)] = coords [(a₁, x)]
⊢ a₀ = a₁
Tactic:
let h₁ := congrFun hyp x
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x : X
a₀ a₁ : R
hyp : coords [(a₀, x)] = coords [(a₁, x)]
h₁ : coords [(a₀, x)] x = coords [(a₁, x)] x := congrFun hyp x
⊢ a₀ = a₁
Theorem: monom_coeff_eq_of_coord_eq
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x : X
a₀ a₁ : R
hyp : coords [(a₀, x)] = coords [(a₁, x)]
h₁ : coords [(a₀, x)] x = coords [(a₁, x)] x := congrFun hyp x
⊢ a₀ = a₁
Tactic:
simp [coords, monomCoeff] at h₁
Proof state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x : X
a₀ a₁ : R
hyp : coords [(a₀, x)] = coords [(a₁, x)]
h₁ : a₀ = a₁
⊢ a₀ = a₁
Theorem: monom_coeff_eq_of_coord_eq
Proof state before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
x : X
a₀ a₁ : R
hyp : coords [(a₀, x)] = coords [(a₁, x)]
h₁ : a₀ = a₁
⊢ a₀ = a₁
Tactic:
assumption
Proof state after:
no goals
Theorem: coeffInclusion_injective
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
a₀ a₁ : R
⊢ coeffInclusion x₀ a₀ = coeffInclusion x₀ a₁ → a₀ = a₁
Tactic:
intro hyp
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
a₀ a₁ : R
hyp : coeffInclusion x₀ a₀ = coeffInclusion x₀ a₁
⊢ a₀ = a₁
Theorem: coeffInclusion_injective
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
a₀ a₁ : R
hyp : coeffInclusion x₀ a₀ = coeffInclusion x₀ a₁
⊢ a₀ = a₁
Tactic:
simp [coeffInclusion] at hyp
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
a₀ a₁ : R
hyp : [(a₀, x₀)] ≈ [(a₁, x₀)]
⊢ a₀ = a₁
Theorem: coeffInclusion_injective
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
a₀ a₁ : R
hyp : [(a₀, x₀)] ≈ [(a₁, x₀)]
⊢ a₀ = a₁
Tactic:
exact monom_coeff_eq_of_coord_eq x₀ a₀ a₁ hyp
Proof state after:
no goals