no goals
R : Type u_1
inst✝¹⁴ : Semiring R
M : Type u_3
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
N : Type u_4
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
P : Type ?u.370920
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M' : Type ?u.370950
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
N' : Type ?u.371338
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_5
ι' : Type ?u.371729
ι'' : Type ?u.371732
M₂ : Type u_2
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type ?u.371765
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f : M₂ →ₗ[R] M
hf : Function.Surjective ↑f
g₁ g₂ : AlternatingMap R M N ι
h : (fun g => compLinearMap g f) g₁ = (fun g => compLinearMap g f) g₂
x : ι → M
⊢ ↑g₁ x = ↑g₂ x
simpa [Function.surjInv_eq hf] using ext_iff.mp h (Function.surjInv hf ∘ x)