Theorem: FreeModule.eql_on_support_of_true (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
⊢ beqOnSupport l f g = true → 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 : beqOnSupport l f g = true
⊢ 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 : beqOnSupport l f g = true
⊢ equalOnList l f g
Tactic:
induction l with
| nil =>
  simp [equalOnList]
| cons h t step =>
  simp [equalOnList]
  simp [beqOnSupport, List.all] at hyp
  let p₂ := step hyp.right
  exact And.intro hyp.left p₂
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 : beqOnSupport [] f g = true
⊢ equalOnList [] f g
Tactic:
simp [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
h : X
t : List X
step : beqOnSupport t f g = true → equalOnList t f g
hyp : beqOnSupport (h :: t) f g = true
⊢ equalOnList (h :: t) f g
Tactic:
simp [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
h : X
t : List X
step : beqOnSupport t f g = true → equalOnList t f g
hyp : beqOnSupport (h :: t) f g = true
⊢ 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
h : X
t : List X
step : beqOnSupport t f g = true → equalOnList t f g
hyp : beqOnSupport (h :: t) f g = true
⊢ f h = g h ∧ equalOnList t f g
Tactic:
simp [beqOnSupport, List.all] at hyp
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
h : X
t : List X
step : beqOnSupport t f g = true → equalOnList t f g
hyp : f h = g h ∧ List.foldr (fun a r => decide (f a = g a) && r) true t = true
⊢ 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
h : X
t : List X
step : beqOnSupport t f g = true → equalOnList t f g
hyp : f h = g h ∧ List.foldr (fun a r => decide (f a = g a) && r) true t = true
⊢ f h = g h ∧ equalOnList t f g
Tactic:
let p₂ := step hyp.right
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
h : X
t : List X
step : beqOnSupport t f g = true → equalOnList t f g
hyp : f h = g h ∧ List.foldr (fun a r => decide (f a = g a) && r) true t = true
p₂ : equalOnList t f g := step hyp.right
⊢ 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
h : X
t : List X
step : beqOnSupport t f g = true → equalOnList t f g
hyp : f h = g h ∧ List.foldr (fun a r => decide (f a = g a) && r) true t = true
p₂ : equalOnList t f g := step hyp.right
⊢ f h = g h ∧ equalOnList t f g
Tactic:
exact And.intro hyp.left p₂
State after:
no goals