case h.h
ι : Type u_1
ι' : Type ?u.247588
R : Type u_2
R₂ : Type ?u.247594
K : Type ?u.247597
M : Type u_3
M' : Type ?u.247603
M'' : Type ?u.247606
V : Type u
V' : Type ?u.247611
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module R M'
b b₁✝ : Basis ι R M
i : ι
c : R
x : M
R₁ : Type ?u.247723
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type ?u.247927
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
b₁ b₂ : Basis ι R M
h : ∀ (x : M) (i : ι), ↑(↑b₁.repr x) i = ↑(↑b₂.repr x) i
x✝ : M
a✝ : ι
⊢ ↑(↑b₁.repr x✝) a✝ = ↑(↑b₂.repr x✝) a✝
ι : Type u_1
ι' : Type ?u.247588
R : Type u_2
R₂ : Type ?u.247594
K : Type ?u.247597
M : Type u_3
M' : Type ?u.247603
M'' : Type ?u.247606
V : Type u
V' : Type ?u.247611
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module R M'
b b₁✝ : Basis ι R M
i : ι
c : R
x : M
R₁ : Type ?u.247723
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type ?u.247927
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
b₁ b₂ : Basis ι R M
h : ∀ (x : M) (i : ι), ↑(↑b₁.repr x) i = ↑(↑b₂.repr x) i
⊢ b₁.repr = b₂.repr
ext
no goals
case h.h
ι : Type u_1
ι' : Type ?u.247588
R : Type u_2
R₂ : Type ?u.247594
K : Type ?u.247597
M : Type u_3
M' : Type ?u.247603
M'' : Type ?u.247606
V : Type u
V' : Type ?u.247611
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module R M'
b b₁✝ : Basis ι R M
i : ι
c : R
x : M
R₁ : Type ?u.247723
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type ?u.247927
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
b₁ b₂ : Basis ι R M
h : ∀ (x : M) (i : ι), ↑(↑b₁.repr x) i = ↑(↑b₂.repr x) i
x✝ : M
a✝ : ι
⊢ ↑(↑b₁.repr x✝) a✝ = ↑(↑b₂.repr x✝) a✝
apply h