case ofRepr
ι : Type u_1
ι' : Type ?u.4334
R : Type u_2
R₂ : Type ?u.4340
K : Type ?u.4343
M : Type u_3
M' : Type ?u.4349
M'' : Type ?u.4352
V : Type u
V' : Type ?u.4357
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
g : Basis ι R M
repr✝ : M ≃ₗ[R] ι →₀ R
h : { repr := repr✝ }.repr = g.repr
⊢ { repr := repr✝ } = g
ι : Type u_1
ι' : Type ?u.4334
R : Type u_2
R₂ : Type ?u.4340
K : Type ?u.4343
M : Type u_3
M' : Type ?u.4349
M'' : Type ?u.4352
V : Type u
V' : Type ?u.4357
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
f g : Basis ι R M
h : f.repr = g.repr
⊢ f = g
cases f
case ofRepr.ofRepr
ι : Type u_1
ι' : Type ?u.4334
R : Type u_2
R₂ : Type ?u.4340
K : Type ?u.4343
M : Type u_3
M' : Type ?u.4349
M'' : Type ?u.4352
V : Type u
V' : Type ?u.4357
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
repr✝¹ repr✝ : M ≃ₗ[R] ι →₀ R
h : { repr := repr✝¹ }.repr = { repr := repr✝ }.repr
⊢ { repr := repr✝¹ } = { repr := repr✝ }
case ofRepr
ι : Type u_1
ι' : Type ?u.4334
R : Type u_2
R₂ : Type ?u.4340
K : Type ?u.4343
M : Type u_3
M' : Type ?u.4349
M'' : Type ?u.4352
V : Type u
V' : Type ?u.4357
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
g : Basis ι R M
repr✝ : M ≃ₗ[R] ι →₀ R
h : { repr := repr✝ }.repr = g.repr
⊢ { repr := repr✝ } = g
cases g
no goals
case ofRepr.ofRepr
ι : Type u_1
ι' : Type ?u.4334
R : Type u_2
R₂ : Type ?u.4340
K : Type ?u.4343
M : Type u_3
M' : Type ?u.4349
M'' : Type ?u.4352
V : Type u
V' : Type ?u.4357
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
repr✝¹ repr✝ : M ≃ₗ[R] ι →₀ R
h : { repr := repr✝¹ }.repr = { repr := repr✝ }.repr
⊢ { repr := repr✝¹ } = { repr := repr✝ }
congr