Theorem: eq_mem_of_equalOnList (UnitConjecture/FreeModule.lean)

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
State after:
no goals

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals