awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M_1 : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
ι : Type u_4
inst_7 : DecidableEq ι
M : Type u_5
inst_8 : AddCommGroup M
inst_9 : Module R M
s : Module.Relations.Solution (relations R ι M) N
inst_10 : DecidableEq ι
m : (i : ι) → M
i : ι
x y : M
⊢ Eq.{u_2 + 1} (α := N)
    ((Finsupp.linearCombination R s.var : (a : (relations R ι M).G →₀ R) → N)
        (Module.Relations.relation (relations R ι M) (Rels.add m i x y)) :
      N)
    (0 : N)

Tactic:
have := s.linearCombination_var_relation (.add m i x y)
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M_1 : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
ι : Type u_4
inst_7 : DecidableEq ι
M : Type u_5
inst_8 : AddCommGroup M
inst_9 : Module R M
s : Module.Relations.Solution (relations R ι M) N
inst_10 : DecidableEq ι
m : (i : ι) → M
i : ι
x y : M
this :
  Eq.{u_2 + 1} (α := N)
    ((Finsupp.linearCombination R s.var : (a : (ι → M) →₀ R) → N)
        (HAdd.hAdd (α := ((a : ι) → M) →₀ R) (Finsupp.single (update (β := fun (a : ι) ↦ M) m i x) 1)
            (Finsupp.single (update (β := fun (a : ι) ↦ M) m i y) 1) -
          Finsupp.single (update (β := fun (a : ι) ↦ M) m i (x + y)) 1) :
      N)
    (0 : N)
⊢ s.var (update (β := fun (a : ι) ↦ M) m i x) + s.var (update (β := fun (a : ι) ↦ M) m i y) =
    s.var (update (β := fun (a : ι) ↦ M) m i (x + y))

Tactic:
rw [map_sub, map_add, Finsupp.linearCombination_single, one_smul,
          Finsupp.linearCombination_single, one_smul,
          Finsupp.linearCombination_single, one_smul, sub_eq_zero] at this

Premises used: map_sub, sub_eq_zero, map_add, Finsupp.linearCombination_single, one_smul
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M_1 : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
ι : Type u_4
inst_7 : DecidableEq ι
M : Type u_5
inst_8 : AddCommGroup M
inst_9 : Module R M
s : Module.Relations.Solution (relations R ι M) N
inst_10 : DecidableEq ι
m : (i : ι) → M
i : ι
x y : M
this :
  s.var (update (β := fun (a : ι) ↦ M) m i x) + s.var (update (β := fun (a : ι) ↦ M) m i y) =
    s.var (update (β := fun (a : ι) ↦ M) m i (x + y))
⊢ s.var (update (β := fun (a : ι) ↦ M) m i (x + y)) =
    s.var (update (β := fun (a : ι) ↦ M) m i x) + s.var (update (β := fun (a : ι) ↦ M) m i y)

Tactic:
this.symm

Premises used: Eq.symm
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M_1 : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
ι : Type u_4
inst_7 : DecidableEq ι
M : Type u_5
inst_8 : AddCommGroup M
inst_9 : Module R M
s : Module.Relations.Solution (relations R ι M) N
inst_10 : DecidableEq ι
m : (i : ι) → M
i : ι
x y : M
this :
  s.var (update (β := fun (a : ι) ↦ M) m i x) + s.var (update (β := fun (a : ι) ↦ M) m i y) =
    s.var (update (β := fun (a : ι) ↦ M) m i (x + y))
⊢ s.var (update (β := fun (x : ι) ↦ M) m i (x + y)) =
    s.var (update (β := fun (x : ι) ↦ M) m i x) + s.var (update (β := fun (x : ι) ↦ M) m i y)

Tactic:
convert! this.symm

Premises used: Eq.symm
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M_1 : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
ι : Type u_4
inst_7 : DecidableEq ι
M : Type u_5
inst_8 : AddCommGroup M
inst_9 : Module R M
s : Module.Relations.Solution (relations R ι M) N
inst_10 : DecidableEq ι
m : (i : ι) → M
i : ι
r : R
x : M
⊢ Eq.{u_2 + 1} (α := N)
    ((Finsupp.linearCombination R s.var : (a : (relations R ι M).G →₀ R) → N)
        (Module.Relations.relation (relations R ι M) (Rels.smul m i r x)) :
      N)
    (0 : N)

Tactic:
have := s.linearCombination_var_relation (.smul m i r x)
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M_1 : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
ι : Type u_4
inst_7 : DecidableEq ι
M : Type u_5
inst_8 : AddCommGroup M
inst_9 : Module R M
s : Module.Relations.Solution (relations R ι M) N
inst_10 : DecidableEq ι
m : (i : ι) → M
i : ι
r : R
x : M
this :
  Eq.{u_2 + 1} (α := N)
    ((Finsupp.linearCombination R s.var : (a : (ι → M) →₀ R) → N)
        (Finsupp.single (update (β := fun (a : ι) ↦ M) m i (r • x)) 1 -
          HSMul.hSMul (β := ((a : ι) → M) →₀ R) r (Finsupp.single (update (β := fun (a : ι) ↦ M) m i x) 1)) :
      N)
    (0 : N)
⊢ s.var (update (β := fun (a : ι) ↦ M) m i (r • x)) = r • s.var (update (β := fun (a : ι) ↦ M) m i x)

Tactic:
rw [Finsupp.smul_single, smul_eq_mul, mul_one, map_sub,
          Finsupp.linearCombination_single, one_smul,
          Finsupp.linearCombination_single, sub_eq_zero] at this

Premises used: map_sub, sub_eq_zero, Finsupp.linearCombination_single, one_smul, smul_eq_mul, mul_one, Finsupp.smul_single
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M_1 : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
ι : Type u_4
inst_7 : DecidableEq ι
M : Type u_5
inst_8 : AddCommGroup M
inst_9 : Module R M
s : Module.Relations.Solution (relations R ι M) N
inst_10 : DecidableEq ι
m : (i : ι) → M
i : ι
r : R
x : M
this : s.var (update (β := fun (a : ι) ↦ M) m i (r • x)) = r • s.var (update (β := fun (a : ι) ↦ M) m i x)
⊢ s.var (update (β := fun (a : ι) ↦ M) m i (r • x)) = r • s.var (update (β := fun (a : ι) ↦ M) m i x)

Tactic:
this
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M_1 : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
ι : Type u_4
inst_7 : DecidableEq ι
M : Type u_5
inst_8 : AddCommGroup M
inst_9 : Module R M
s : Module.Relations.Solution (relations R ι M) N
inst_10 : DecidableEq ι
m : (i : ι) → M
i : ι
r : R
x : M
this : s.var (update (β := fun (a : ι) ↦ M) m i (r • x)) = r • s.var (update (β := fun (a : ι) ↦ M) m i x)
⊢ s.var (update (β := fun (x : ι) ↦ M) m i (r • x)) = r • s.var (update (β := fun (x : ι) ↦ M) m i x)

Tactic:
convert! this
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M_1 : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
ι : Type u_4
inst_7 : DecidableEq ι
M : Type u_5
inst_8 : AddCommGroup M
inst_9 : Module R M
s : Module.Relations.Solution (relations R ι M) N
v : ι → M
i j : ι
hm : v i = v j
hij : i ≠ j
⊢ s.var v = 0

Tactic:
simpa using s.linearCombination_var_relation (.alt v i j hm hij)

Premises used: exteriorPower.presentation.Rels.alt, Module.Relations.Solution.linearCombination_var_relation
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M_1 : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
ι : Type u_4
inst_7 : DecidableEq ι
M : Type u_5
inst_8 : AddCommGroup M
inst_9 : Module R M
f : M [⋀^ι]→ₗ[R] N
m : ι → M
i : ι
x y : M
⊢ Eq.{u_2 + 1} (α := N)
    ((Finsupp.linearCombination R fun (m : Module.Relations.G (relations R ι M)) ↦ (f : (a : ι → M) → N) m :
          (a : (relations R ι M).G →₀ R) → N)
        (Module.Relations.relation (relations R ι M) (Rels.add m i x y)) :
      N)
    (0 : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M_1 : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
ι : Type u_4
inst_7 : DecidableEq ι
M : Type u_5
inst_8 : AddCommGroup M
inst_9 : Module R M
f : M [⋀^ι]→ₗ[R] N
m : ι → M
i : ι
r : R
x : M
⊢ Eq.{u_2 + 1} (α := N)
    ((Finsupp.linearCombination R fun (m : Module.Relations.G (relations R ι M)) ↦ (f : (a : ι → M) → N) m :
          (a : (relations R ι M).G →₀ R) → N)
        (Module.Relations.relation (relations R ι M) (Rels.smul m i r x)) :
      N)
    (0 : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M_1 : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
ι : Type u_4
inst_7 : DecidableEq ι
M : Type u_5
inst_8 : AddCommGroup M
inst_9 : Module R M
f : M [⋀^ι]→ₗ[R] N
v : ι → M
i j : ι
hm : v i = v j
hij : i ≠ j
⊢ Eq.{u_2 + 1} (α := N)
    ((Finsupp.linearCombination R fun (m : Module.Relations.G (relations R ι M)) ↦ (f : (a : ι → M) → N) m :
          (a : (relations R ι M).G →₀ R) → N)
        (Module.Relations.relation (relations R ι M) (Rels.alt v i j hm hij)) :
      N)
    (0 : N)

Tactic:
simpa using f.map_eq_zero_of_eq v hm hij

Premises used: AlternatingMap.map_eq_zero_of_eq
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
N_1 : Type u_4
inst_7 : AddCommGroup N_1
inst_8 : Module R N_1
s : Module.Relations.Solution (relations R (Fin n) M) N_1
⊢ Module.Relations.Solution.postcomp (M := ↥(⋀[R]^n M))
      ((Equiv.symm relationsSolutionEquiv :
          (a : M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n M)) → (relations R (Fin n) M).Solution ↥(⋀[R]^n M))
        (ιMulti R n))
      ((ExteriorAlgebra.liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N_1) → ExteriorAlgebra R M →ₗ[R] N_1)
          (update (β := fun (i : ℕ) ↦ M [⋀^Fin i]→ₗ[R] N_1) 0 n
            ((relationsSolutionEquiv : (a : (relations R (Fin n) M).Solution N_1) → M [⋀^Fin n]→ₗ[R] N_1) s)) ∘ₗ
        Submodule.subtype (⋀[R]^n M)) =
    s

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N_1 : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N_1
inst_4 : Module R N_1
inst_5 : AddCommGroup N'
inst_6 : Module R N'
N : Type u_4
x : AddCommGroup N
x_1 : Module R N
f f' : ↥(⋀[R]^n M) →ₗ[R] N
h :
  Eq (α := Module.Relations.Solution (relations R (Fin n) M) N)
    (Module.Relations.Solution.postcomp
      ((Equiv.symm relationsSolutionEquiv :
          (a : M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n M)) → (relations R (Fin n) M).Solution ↥(⋀[R]^n M))
        (ιMulti R n))
      f)
    (Module.Relations.Solution.postcomp
      ((Equiv.symm relationsSolutionEquiv :
          (a : M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n M)) → (relations R (Fin n) M).Solution ↥(⋀[R]^n M))
        (ιMulti R n))
      f')
rw :
  ∀ (s : (↑(range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M))) : Type (max u u_1))),
    Eq.{u_4 + 1} (α := N) ((f : (a : ↥(⋀[R]^n M)) → N) (↑s : ↥(⋀[R]^n M)) : N)
      ((f' : (a : ↥(⋀[R]^n M)) → N) (↑s : ↥(⋀[R]^n M)) : N)
⊢ f = f'

Tactic:
rw [Submodule.linearMap_eq_iff_of_span_eq_top _ _ (ιMulti_span R n M)]

Premises used: Submodule.linearMap_eq_iff_of_span_eq_top, exteriorPower.ιMulti_span
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N_1 : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N_1
inst_4 : Module R N_1
inst_5 : AddCommGroup N'
inst_6 : Module R N'
N : Type u_4
x : AddCommGroup N
x_1 : Module R N
f_1 f' : ↥(⋀[R]^n M) →ₗ[R] N
h :
  Eq (α := Module.Relations.Solution (relations R (Fin n) M) N)
    (Module.Relations.Solution.postcomp
      ((Equiv.symm relationsSolutionEquiv :
          (a : M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n M)) → (relations R (Fin n) M).Solution ↥(⋀[R]^n M))
        (ιMulti R n))
      f_1)
    (Module.Relations.Solution.postcomp
      ((Equiv.symm relationsSolutionEquiv :
          (a : M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n M)) → (relations R (Fin n) M).Solution ↥(⋀[R]^n M))
        (ιMulti R n))
      f')
f : Fin n → M
⊢ Eq.{u_4 + 1} (α := N)
    ((f_1 : (a : ↥(⋀[R]^n M)) → N)
        ((↑(Subtype.mk (p := fun (x : ↥(⋀[R]^n M)) ↦
                Membership.mem (γ := Set ↥(⋀[R]^n M))
                  (range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M))) x)
                ((ιMulti R n : (a : Fin n → M) → ↥(⋀[R]^n M)) f) ⋯) :
            ↥(⋀[R]^n M)) :
          ↥(⋀[R]^n M)) :
      N)
    ((f' : (a : ↥(⋀[R]^n M)) → N)
        ((↑(Subtype.mk (p := fun (x : ↥(⋀[R]^n M)) ↦
                Membership.mem (γ := Set ↥(⋀[R]^n M))
                  (range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M))) x)
                ((ιMulti R n : (a : Fin n → M) → ↥(⋀[R]^n M)) f) ⋯) :
            ↥(⋀[R]^n M)) :
          ↥(⋀[R]^n M)) :
      N)

Tactic:
Module.Relations.Solution.congr_var h f

Premises used: Module.Relations.Solution.congr_var
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N_1 : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N_1
inst_4 : Module R N_1
inst_5 : AddCommGroup N'
inst_6 : Module R N'
N : Type u_4
x : AddCommGroup N
x_1 : Module R N
f_1 f' : ↥(⋀[R]^n M) →ₗ[R] N
h :
  Eq (α := Module.Relations.Solution (relations R (Fin n) M) N)
    (Module.Relations.Solution.postcomp
      ((Equiv.symm relationsSolutionEquiv :
          (a : M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n M)) → (relations R (Fin n) M).Solution ↥(⋀[R]^n M))
        (ιMulti R n))
      f_1)
    (Module.Relations.Solution.postcomp
      ((Equiv.symm relationsSolutionEquiv :
          (a : M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n M)) → (relations R (Fin n) M).Solution ↥(⋀[R]^n M))
        (ιMulti R n))
      f')
f : Fin n → M
⊢ Eq.{u_4 + 1} (α := N)
    ((f_1 : (a : ↥(⋀[R]^n M)) → N)
        ((↑(Subtype.mk (p := fun (x : ↥(⋀[R]^n M)) ↦
                Membership.mem (γ := Set ↥(⋀[R]^n M))
                  (range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M))) x)
                ((ιMulti R n : (a : Fin n → M) → ↥(⋀[R]^n M)) f) ⋯) :
            ↥(⋀[R]^n M)) :
          ↥(⋀[R]^n M)) :
      N)
    ((f' : (a : ↥(⋀[R]^n M)) → N)
        ((↑(Subtype.mk (p := fun (x : ↥(⋀[R]^n M)) ↦
                Membership.mem (γ := Set ↥(⋀[R]^n M))
                  (range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M))) x)
                ((ιMulti R n : (a : Fin n → M) → ↥(⋀[R]^n M)) f) ⋯) :
            ↥(⋀[R]^n M)) :
          ↥(⋀[R]^n M)) :
      N)

Tactic:
exact Module.Relations.Solution.congr_var h f

Premises used: Module.Relations.Solution.congr_var
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f g : ↥(⋀[R]^n M) →ₗ[R] N
heq : f.compAlternatingMap (ιMulti R n) = g.compAlternatingMap (ιMulti R n)
var :
  ∀ (f_1 : Module.Relations.G (Module.Presentation.toRelations (M := ↥(⋀[R]^n M)) (presentation R n M))),
    Module.Relations.Solution.var
        (Module.Relations.Solution.postcomp (Module.Presentation.toSolution (presentation R n M)) f) f_1 =
      Module.Relations.Solution.var
        (Module.Relations.Solution.postcomp (Module.Presentation.toSolution (presentation R n M)) g) f_1
⊢ Eq (α := Module.Relations.Solution (Module.Presentation.toRelations (M := ↥(⋀[R]^n M)) (presentation R n M)) N)
    (Module.Relations.Solution.postcomp (Module.Presentation.toSolution (presentation R n M)) f)
    (Module.Relations.Solution.postcomp (Module.Presentation.toSolution (presentation R n M)) g)

Tactic:
ext f
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f_1 g : ↥(⋀[R]^n M) →ₗ[R] N
heq : f_1.compAlternatingMap (ιMulti R n) = g.compAlternatingMap (ιMulti R n)
f : Module.Relations.G (Module.Presentation.toRelations (M := ↥(⋀[R]^n M)) (presentation R n M))
⊢ Module.Relations.Solution.var
      (Module.Relations.Solution.postcomp (Module.Presentation.toSolution (presentation R n M)) f_1) f =
    Module.Relations.Solution.var
      (Module.Relations.Solution.postcomp (Module.Presentation.toSolution (presentation R n M)) g) f

Tactic:
apply DFunLike.congr_fun heq

Premises used: DFunLike.congr_fun
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M [⋀^Fin n]→ₗ[R] N
obtain :
  ∀ (φ : ↥(⋀[R]^n M) →ₗ[R] N),
    Eq (α := M [⋀^Fin n]→ₗ[R] N)
      (LinearMap.compAlternatingMap
        ((alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] N)
          ((LinearEquiv.symm alternatingMapLinearEquiv : (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N) φ))
        (ιMulti R n))
      ((LinearEquiv.symm alternatingMapLinearEquiv : (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N) φ)
⊢ LinearMap.compAlternatingMap ((alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] N) f)
      (ιMulti R n) =
    f

Tactic:
obtain ⟨φ, rfl⟩ := alternatingMapLinearEquiv.symm.surjective f

Premises used: exteriorPower.alternatingMapLinearEquiv, LinearEquiv.symm, LinearEquiv.surjective, rfl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
φ : ↥(⋀[R]^n M) →ₗ[R] N
dsimp :
  Eq (α := M [⋀^Fin n]→ₗ[R] N)
    (LinearMap.compAlternatingMap
      ((LinearEquiv.symm
            (Equiv.toLinearEquiv
              (Equiv.trans (Module.Relations.Solution.IsPresentation.linearMapEquiv ⋯)
                presentation.relationsSolutionEquiv)
              ⋯) :
          (a : M [⋀^Fin n]→ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] N)
        ((Equiv.toLinearEquiv
              (Equiv.trans (Module.Relations.Solution.IsPresentation.linearMapEquiv ⋯)
                presentation.relationsSolutionEquiv)
              ⋯ :
            (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N)
          φ))
      (ιMulti R n))
    ((Equiv.toLinearEquiv
          (Equiv.trans (Module.Relations.Solution.IsPresentation.linearMapEquiv ⋯) presentation.relationsSolutionEquiv)
          ⋯ :
        (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N)
      φ)
⊢ Eq (α := M [⋀^Fin n]→ₗ[R] N)
    (LinearMap.compAlternatingMap
      ((alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] N)
        ((LinearEquiv.symm alternatingMapLinearEquiv : (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N) φ))
      (ιMulti R n))
    ((LinearEquiv.symm alternatingMapLinearEquiv : (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N) φ)

Tactic:
dsimp [alternatingMapLinearEquiv]

Premises used: exteriorPower.alternatingMapLinearEquiv
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
φ : ↥(⋀[R]^n M) →ₗ[R] N
simp :
  φ.compAlternatingMap (ιMulti R n) =
    (Equiv.toLinearEquiv
          (Equiv.trans (Module.Relations.Solution.IsPresentation.linearMapEquiv ⋯) presentation.relationsSolutionEquiv)
          ⋯ :
        (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N)
      φ
⊢ Eq (α := M [⋀^Fin n]→ₗ[R] N)
    (LinearMap.compAlternatingMap
      ((LinearEquiv.symm
            (Equiv.toLinearEquiv
              (Equiv.trans (Module.Relations.Solution.IsPresentation.linearMapEquiv ⋯)
                presentation.relationsSolutionEquiv)
              ⋯) :
          (a : M [⋀^Fin n]→ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] N)
        ((Equiv.toLinearEquiv
              (Equiv.trans (Module.Relations.Solution.IsPresentation.linearMapEquiv ⋯)
                presentation.relationsSolutionEquiv)
              ⋯ :
            (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N)
          φ))
      (ιMulti R n))
    ((Equiv.toLinearEquiv
          (Equiv.trans (Module.Relations.Solution.IsPresentation.linearMapEquiv ⋯) presentation.relationsSolutionEquiv)
          ⋯ :
        (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N)
      φ)

Tactic:
simp only [LinearEquiv.symm_apply_apply]

Premises used: LinearEquiv.symm_apply_apply
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
φ : ↥(⋀[R]^n M) →ₗ[R] N
⊢ φ.compAlternatingMap (ιMulti R n) =
    (Equiv.toLinearEquiv
          (Equiv.trans (Module.Relations.Solution.IsPresentation.linearMapEquiv ⋯) presentation.relationsSolutionEquiv)
          ⋯ :
        (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N)
      φ

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M [⋀^Fin n]→ₗ[R] N
a : Fin n → M
⊢ Eq.{u_2 + 1} (α := N)
    ((((alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] N) f : ↥(⋀[R]^n M) →ₗ[R] N) :
          (a : ↥(⋀[R]^n M)) → N)
        ((ιMulti R n : (a : Fin n → M) → ↥(⋀[R]^n M)) a : ↥(⋀[R]^n M)) :
      N)
    ((f : (a : Fin n → M) → N) a : N)

Tactic:
DFunLike.congr_fun (alternatingMapLinearEquiv_comp_ιMulti f) a

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn, exteriorPower.alternatingMapLinearEquiv_comp_ιMulti
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
F : ↥(⋀[R]^n M) →ₗ[R] N
m : Fin n → M
obtain :
  ∀ (f : M [⋀^Fin n]→ₗ[R] N),
    Eq.{u_2 + 1} (α := N)
      ((((LinearEquiv.symm alternatingMapLinearEquiv : (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N)
                ((alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] N) f) :
              M [⋀^Fin n]→ₗ[R] N) :
            (a : Fin n → M) → N)
          m :
        N)
      ((LinearMap.compAlternatingMap ((alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] N) f)
              (ιMulti R n) :
            (a : Fin n → M) → N)
          m :
        N)
⊢ Eq.{u_2 + 1} (α := N)
    ((((LinearEquiv.symm alternatingMapLinearEquiv : (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N) F :
            M [⋀^Fin n]→ₗ[R] N) :
          (a : Fin n → M) → N)
        m :
      N)
    ((F.compAlternatingMap (ιMulti R n) : (a : Fin n → M) → N) m : N)

Tactic:
obtain ⟨f, rfl⟩ := alternatingMapLinearEquiv.surjective F

Premises used: exteriorPower.alternatingMapLinearEquiv, LinearEquiv.surjective, rfl