Theorem: Function.ExtendByZero.linearMap_injective (Matroid/ForMathlib/LinearAlgebra/StdBasis.lean)

State before:
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
ι η : Type u_7
inst✝ : Semiring R
s : ι → η
hs : Injective s
⊢ Injective ⇑(linearMap R s)
Tactic:
intro x x' h
State after:
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
ι η : Type u_7
inst✝ : Semiring R
s : ι → η
hs : Injective s
x x' : ι → R
h : (linearMap R s) x = (linearMap R s) x'
⊢ x = x'

State before:
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
ι η : Type u_7
inst✝ : Semiring R
s : ι → η
hs : Injective s
x x' : ι → R
h : (linearMap R s) x = (linearMap R s) x'
⊢ x = x'
Tactic:
ext i
State after:
case h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
ι η : Type u_7
inst✝ : Semiring R
s : ι → η
hs : Injective s
x x' : ι → R
h : (linearMap R s) x = (linearMap R s) x'
i : ι
⊢ x i = x' i

State before:
case h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
ι η : Type u_7
inst✝ : Semiring R
s : ι → η
hs : Injective s
x x' : ι → R
h : (linearMap R s) x = (linearMap R s) x'
i : ι
⊢ x i = x' i
Tactic:
replace h := _root_.congr_fun h (s i)
State after:
case h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
ι η : Type u_7
inst✝ : Semiring R
s : ι → η
hs : Injective s
x x' : ι → R
i : ι
h : (linearMap R s) x (s i) = (linearMap R s) x' (s i)
⊢ x i = x' i

State before:
case h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
ι η : Type u_7
inst✝ : Semiring R
s : ι → η
hs : Injective s
x x' : ι → R
i : ι
h : (linearMap R s) x (s i) = (linearMap R s) x' (s i)
⊢ x i = x' i
Tactic:
simp only [linearMap_apply, exists_apply_eq_apply, not_true] at h
State after:
case h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
ι η : Type u_7
inst✝ : Semiring R
s : ι → η
hs : Injective s
x x' : ι → R
i : ι
h : extend s x 0 (s i) = extend s x' 0 (s i)
⊢ x i = x' i

State before:
case h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
ι η : Type u_7
inst✝ : Semiring R
s : ι → η
hs : Injective s
x x' : ι → R
i : ι
h : extend s x 0 (s i) = extend s x' 0 (s i)
⊢ x i = x' i
Tactic:
rwa [hs.extend_apply, hs.extend_apply] at h
State after:
no goals