-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem Basis.ext_alternating {f g : N₁ [⋀^ι]→ₗ[R'] N₂} (e : Basis ι₁ R' N₁)
    (h : ∀ v : ι → ι₁, Function.Injective v → (f fun i => e (v i)) = g fun i => e (v i)) :
    f = g

Proof state:
case pos
ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i => e (v i)) = g fun i => e (v i)
v : ι → ι₁
hi : Function.Injective v
⊢ (↑f fun i => e (v i)) = ↑g fun i => e (v i)

Tactic:
exact h v hi

Result:
no goals

Proof state:
case neg
ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i => e (v i)) = g fun i => e (v i)
v : ι → ι₁
hi : ¬Function.Injective v
⊢ (↑f fun i => e (v i)) = ↑g fun i => e (v i)

Tactic:
have : ¬Function.Injective fun i => e (v i) := hi.imp Function.Injective.of_comp

Result:
case neg
ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i => e (v i)) = g fun i => e (v i)
v : ι → ι₁
hi : ¬Function.Injective v
this : ¬Function.Injective fun i => e (v i)
⊢ (↑f fun i => e (v i)) = ↑g fun i => e (v i)

Proof state:
ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i => e (v i)) = g fun i => e (v i)
v : ι → ι₁
⊢ (↑f fun i => e (v i)) = ↑g fun i => e (v i)

Tactic:
by_cases hi : Function.Injective v

Result:
case pos
ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i => e (v i)) = g fun i => e (v i)
v : ι → ι₁
hi : Function.Injective v
⊢ (↑f fun i => e (v i)) = ↑g fun i => e (v i)

case neg
ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i => e (v i)) = g fun i => e (v i)
v : ι → ι₁
hi : ¬Function.Injective v
⊢ (↑f fun i => e (v i)) = ↑g fun i => e (v i)

Proof state:
case neg
ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i => e (v i)) = g fun i => e (v i)
v : ι → ι₁
hi : ¬Function.Injective v
this : ¬Function.Injective fun i => e (v i)
⊢ (↑f fun i => e (v i)) = ↑g fun i => e (v i)

Tactic:
rw [coe_multilinearMap, coe_multilinearMap, f.map_eq_zero_of_not_injective _ this,
  g.map_eq_zero_of_not_injective _ this]

Result:
no goals

Proof state:
ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i => e (v i)) = g fun i => e (v i)
⊢ f = g

Tactic:
refine AlternatingMap.coe_multilinearMap_injective (Basis.ext_multilinear e fun v => ?_)

Result:
ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i => e (v i)) = g fun i => e (v i)
v : ι → ι₁
⊢ (↑f fun i => e (v i)) = ↑g fun i => e (v i)