internlm/Lean-Github huggingface dataset:
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
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
⊢ x ∈ support ((a₀, x₀) :: t)
Tactic:
have d : support ((a₀, x₀) :: t) = x₀ :: (support t) := 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
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
⊢ x ∈ support ((a₀, x₀) :: 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
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
⊢ x ∈ support ((a₀, x₀) :: t)
Tactic:
rw [d]
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
d : support ((a₀, x₀) :: t) = x₀ :: support t
⊢ x ∈ x₀ :: support 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
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
⊢ x ∈ x₀ :: support t
Tactic:
match p : x₀ == x with
| true =>
  have eqn : x₀ = x := of_decide_eq_true p
  rw [eqn]
  apply List.mem_of_elem_eq_true
  simp [List.elem]
| false =>
  rw [coords, monomCoeff, p, zero_add] at hyp
  let step := nonzero_coord_in_support t x hyp
  apply List.mem_of_elem_eq_true
  simp [List.elem]
  have p' : (x == x₀) = false := by
    have eqn := of_decide_eq_false p
    have eqn' : ¬(x = x₀) := by
      intro contra
      let contra' := Eq.symm contra
      contradiction
    exact decide_eq_false eqn'
  rw [p']
  apply List.elem_eq_true_of_mem
  exact step
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
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
⊢ support ((a₀, x₀) :: t) = x₀ :: support t
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
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = true
⊢ x ∈ x₀ :: support t
Tactic:
have eqn : x₀ = x := of_decide_eq_true p
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
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = true
eqn : x₀ = x
⊢ x ∈ x₀ :: support 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
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = true
eqn : x₀ = x
⊢ x ∈ x₀ :: support t
Tactic:
rw [eqn]
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
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = true
eqn : x₀ = x
⊢ x ∈ x :: support 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
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = true
eqn : x₀ = x
⊢ x ∈ x :: support t
Tactic:
apply List.mem_of_elem_eq_true
Proof state after:
case a
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
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = true
eqn : x₀ = x
⊢ List.elem x (x :: support t) = true
Theorem: nonzero_coord_in_support
Proof state before:
case a
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
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = true
eqn : x₀ = x
⊢ List.elem x (x :: support t) = true
Tactic:
simp [List.elem]
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
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
⊢ x ∈ x₀ :: support t
Tactic:
rw [coords, monomCoeff, p, zero_add] 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
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
⊢ x ∈ x₀ :: support 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
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
⊢ x ∈ x₀ :: support t
Tactic:
let step := nonzero_coord_in_support t 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
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
⊢ x ∈ x₀ :: support 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
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
⊢ x ∈ x₀ :: support t
Tactic:
apply List.mem_of_elem_eq_true
Proof state after:
case a
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 t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
⊢ List.elem x (x₀ :: support t) = true
Theorem: nonzero_coord_in_support
Proof state before:
case a
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 t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
⊢ List.elem x (x₀ :: support t) = true
Tactic:
simp [List.elem]
Proof state after:
case a
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 t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
⊢ (match x == x₀ with
    | true => true
    | false => List.elem x (support t)) =
    true
Theorem: nonzero_coord_in_support
Proof state before:
case a
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 t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
⊢ (match x == x₀ with
    | true => true
    | false => List.elem x (support t)) =
    true
Tactic:
have p' : (x == x₀) = false := by
  have eqn := of_decide_eq_false p
  have eqn' : ¬(x = x₀) := by
    intro contra
    let contra' := Eq.symm contra
    contradiction
  exact decide_eq_false eqn'
Proof state after:
case a
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 t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
p' : (x == x₀) = false
⊢ (match x == x₀ with
    | true => true
    | false => List.elem x (support t)) =
    true
Theorem: nonzero_coord_in_support
Proof state before:
case a
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 t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
p' : (x == x₀) = false
⊢ (match x == x₀ with
    | true => true
    | false => List.elem x (support t)) =
    true
Tactic:
rw [p']
Proof state after:
case a
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 t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
p' : (x == x₀) = false
⊢ (match false with
    | true => true
    | false => List.elem x (support t)) =
    true
Theorem: nonzero_coord_in_support
Proof state before:
case a
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 t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
p' : (x == x₀) = false
⊢ (match false with
    | true => true
    | false => List.elem x (support t)) =
    true
Tactic:
apply List.elem_eq_true_of_mem
Proof state after:
case a.h
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 t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
p' : (x == x₀) = false
⊢ x ∈ support t
Theorem: nonzero_coord_in_support
Proof state before:
case a.h
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 t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
p' : (x == x₀) = false
⊢ x ∈ support t
Tactic:
exact step
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
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
⊢ (x == x₀) = false
Tactic:
have eqn := of_decide_eq_false p
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 t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
eqn : ¬x₀ = x
⊢ (x == x₀) = false
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
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
eqn : ¬x₀ = x
⊢ (x == x₀) = false
Tactic:
have eqn' : ¬(x = x₀) := by
  intro contra
  let contra' := Eq.symm contra
  contradiction
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 t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
eqn : ¬x₀ = x
eqn' : ¬x = x₀
⊢ (x == x₀) = false
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
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
eqn : ¬x₀ = x
eqn' : ¬x = x₀
⊢ (x == x₀) = false
Tactic:
exact decide_eq_false eqn'
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
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
eqn : ¬x₀ = x
⊢ ¬x = x₀
Tactic:
intro contra
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 t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
eqn : ¬x₀ = x
contra : x = x₀
⊢ False
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
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
eqn : ¬x₀ = x
contra : x = x₀
⊢ False
Tactic:
let contra' := Eq.symm contra
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 t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
eqn : ¬x₀ = x
contra : x = x₀
contra' : x₀ = x := contra.symm
⊢ False
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
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
eqn : ¬x₀ = x
contra : x = x₀
contra' : x₀ = x := contra.symm
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: equalOnList_of_equal
Proof state before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
⊢ f = g → equalOnList l f g
Tactic:
intro hyp
Proof state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
hyp : f = g
⊢ equalOnList l f g
Theorem: equalOnList_of_equal
Proof state before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
hyp : f = g
⊢ equalOnList l f g
Tactic:
induction l with
| nil =>
  rw [equalOnList]
| cons h t step =>
  rw [equalOnList]
  apply And.intro
  rw [hyp]
  exact step
Proof state after:
no goals
Theorem: equalOnList_of_equal
Proof state before:
case nil
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
hyp : f = g
⊢ equalOnList [] f g
Tactic:
rw [equalOnList]
Proof state after:
no goals
Theorem: equalOnList_of_equal
Proof state before:
case cons
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
hyp : f = g
h : X
t : List X
step : equalOnList t f g
⊢ equalOnList (h :: t) f g
Tactic:
rw [equalOnList]
Proof state after:
case cons
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
hyp : f = g
h : X
t : List X
step : equalOnList t f g
⊢ f h = g h ∧ equalOnList t f g
Theorem: equalOnList_of_equal
Proof state before:
case cons
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
hyp : f = g
h : X
t : List X
step : equalOnList t f g
⊢ f h = g h ∧ equalOnList t f g
Tactic:
apply And.intro
Proof state after:
case cons.left
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
hyp : f = g
h : X
t : List X
step : equalOnList t f g
⊢ f h = g h

case cons.right
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
hyp : f = g
h : X
t : List X
step : equalOnList t f g
⊢ equalOnList t f g
Theorem: equalOnList_of_equal
Proof state before:
case cons.left
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
hyp : f = g
h : X
t : List X
step : equalOnList t f g
⊢ f h = g h

case cons.right
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
hyp : f = g
h : X
t : List X
step : equalOnList t f g
⊢ equalOnList t f g
Tactic:
rw [hyp]
Proof state after:
case cons.right
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
hyp : f = g
h : X
t : List X
step : equalOnList t f g
⊢ equalOnList t f g
Theorem: equalOnList_of_equal
Proof state before:
case cons.right
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
hyp : f = g
h : X
t : List X
step : equalOnList t f g
⊢ equalOnList t f g
Tactic:
exact step
Proof state after:
no goals
Theorem: eq_mem_of_equalOnList
Proof state before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
x : X
mhyp : x ∈ []
⊢ equalOnList [] f g → f x = g x
Tactic:
contradiction
Proof state after:
no goals
Theorem: eq_mem_of_equalOnList
Proof state before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
x h : X
t : List X
mhyp : x ∈ h :: t
⊢ equalOnList (h :: t) f g → f x = g x
Tactic:
intro hyp
Proof state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
x h : X
t : List X
mhyp : x ∈ h :: t
hyp : equalOnList (h :: t) f g
⊢ f x = g x
Theorem: eq_mem_of_equalOnList
Proof state before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
x h : X
t : List X
mhyp : x ∈ h :: t
hyp : equalOnList (h :: t) f g
⊢ f x = g x
Tactic:
simp [equalOnList] at hyp
Proof state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
x h : X
t : List X
mhyp : x ∈ h :: t
hyp : f h = g h ∧ equalOnList t f g
⊢ f x = g x
Theorem: eq_mem_of_equalOnList
Proof state before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
x h : X
t : List X
mhyp : x ∈ h :: t
hyp : f h = g h ∧ equalOnList t f g
⊢ f x = g x
Tactic:
cases mhyp
Proof state after:
case head
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
x : X
t : List X
hyp : f x = g x ∧ equalOnList t f g
⊢ f x = g x

case tail
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
x h : X
t : List X
hyp : f h = g h ∧ equalOnList t f g
a✝ : List.Mem x t
⊢ f x = g x
Theorem: eq_mem_of_equalOnList
Proof state before:
case head
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
x : X
t : List X
hyp : f x = g x ∧ equalOnList t f g
⊢ f x = g x

case tail
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
x h : X
t : List X
hyp : f h = g h ∧ equalOnList t f g
a✝ : List.Mem x t
⊢ f x = g x
Tactic:
exact hyp.left
Proof state after:
case tail
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
x h : X
t : List X
hyp : f h = g h ∧ equalOnList t f g
a✝ : List.Mem x t
⊢ f x = g x
Theorem: eq_mem_of_equalOnList
Proof state before:
case tail
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
x h : X
t : List X
hyp : f h = g h ∧ equalOnList t f g
a✝ : List.Mem x t
⊢ f x = g x
Tactic:
have inTail : x ∈ t := by
  assumption
Proof state after:
case tail
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
x h : X
t : List X
hyp : f h = g h ∧ equalOnList t f g
a✝ : List.Mem x t
inTail : x ∈ t
⊢ f x = g x
Theorem: eq_mem_of_equalOnList
Proof state before:
case tail
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
x h : X
t : List X
hyp : f h = g h ∧ equalOnList t f g
a✝ : List.Mem x t
inTail : x ∈ t
⊢ f x = g x
Tactic:
have step := eq_mem_of_equalOnList t f g x inTail hyp.right
Proof state after:
case tail
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
x h : X
t : List X
hyp : f h = g h ∧ equalOnList t f g
a✝ : List.Mem x t
inTail : x ∈ t
step : f x = g x
⊢ f x = g x
Theorem: eq_mem_of_equalOnList
Proof state before:
case tail
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
x h : X
t : List X
hyp : f h = g h ∧ equalOnList t f g
a✝ : List.Mem x t
inTail : x ∈ t
step : f x = g x
⊢ f x = g x
Tactic:
exact step
Proof state after:
no goals
Theorem: eq_mem_of_equalOnList
Proof state before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
x h : X
t : List X
hyp : f h = g h ∧ equalOnList t f g
a✝ : List.Mem x t
⊢ x ∈ t
Tactic:
assumption
Proof state after:
no goals
Theorem: eqlCoords.refl
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
⊢ eqlCoords R X s s
Tactic:
rfl
Proof state after:
no goals
Theorem: eqlCoords.symm
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
⊢ eqlCoords R X s₁ s₂ → eqlCoords R X s₂ 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 : eqlCoords R X s₁ s₂
⊢ eqlCoords R X s₂ s₁
Theorem: eqlCoords.symm
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : eqlCoords R X s₁ s₂
⊢ eqlCoords R X s₂ 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 : eqlCoords R X s₁ s₂
⊢ ∀ (x : X), FormalSum.coords s₂ x = FormalSum.coords s₁ x
Theorem: eqlCoords.symm
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : eqlCoords R X 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 : eqlCoords R X s₁ s₂
x : X
⊢ FormalSum.coords s₂ x = FormalSum.coords s₁ x