Theorem: equalOnList_of_equal (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
⊢ f = g → equalOnList l f g
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
hyp : f = g
⊢ equalOnList l f g

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

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

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

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

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

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