awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
ι : Type u_7
ι₁ : Type u_10
inst : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst_1 : CommSemiring R'
inst_2 : AddCommMonoid N₁
inst_3 : AddCommMonoid N₂
inst_4 : Module R' N₁
inst_5 : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h :
  ∀ (v : ι → ι₁),
    Function.Injective v →
      Eq.{u_13 + 1} (α := N₂) ((f : (a : ι → N₁) → N₂) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i) : N₂)
        ((g : (a : ι → N₁) → N₂) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i) : N₂)
v : (i : ι) → ι₁
hi : ¬Function.Injective v
this : ¬Function.Injective.{u_7 + 1, u_12 + 1} (β := N₁) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i)
neg :
  Eq.{u_13 + 1} (α := N₂) ((f : (a : ι → N₁) → N₂) fun (i : ι) ↦ ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) : N₂)
    (((↑g : MultilinearMap R' (fun (x : ι) ↦ N₁) N₂) : (a : (i : ι) → N₁) → N₂) fun (i : ι) ↦
        ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) :
      N₂)
neg₁ :
  Eq.{u_13 + 1} (α := N₂) ((f : (a : ι → N₁) → N₂) fun (i : ι) ↦ ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) : N₂)
    ((g : (a : ι → N₁) → N₂) fun (i : ι) ↦ ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) : N₂)
neg₂ :
  Eq.{u_13 + 1} (α := N₂) (0 : N₂)
    ((g : (a : ι → N₁) → N₂) fun (i : ι) ↦ ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) : N₂)
⊢ Eq.{u_13 + 1} (α := N₂)
    (((↑f : MultilinearMap R' (fun (x : ι) ↦ N₁) N₂) : (a : (i : ι) → N₁) → N₂) fun (i : ι) ↦
        ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) :
      N₂)
    (((↑g : MultilinearMap R' (fun (x : ι) ↦ N₁) N₂) : (a : (i : ι) → N₁) → N₂) fun (i : ι) ↦
        ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) :
      N₂)
have neg₃ : Eq.{u_13 + 1} (α := N₂) 0 0
Tactic: rw [coe_multilinearMap, coe_multilinearMap, f.map_eq_zero_of_not_injective _ this,
      g.map_eq_zero_of_not_injective _ this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst_11 : CommSemiring R'
inst_12 : AddCommMonoid M''
inst_13 : AddCommMonoid M₂''
inst_14 : AddCommMonoid N''
inst_15 : AddCommMonoid N₂''
inst_16 : Module R' M''
inst_17 : Module R' M₂''
inst_18 : Module R' N''
inst_19 : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x x_1 : M'' [⋀^ι]→ₗ[R'] N''
⊢ (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap (x + x_1) =
    (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap x + (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap x_1
have H : ∀ (x_2 : ι → M''),
  Eq.{u_14 + 1} (α := N₂'') (((↑e : N'' →ₗ[R'] N₂'').compAlternatingMap (x + x_1) : (a : ι → M'') → N₂'') x_2 : N₂'')
    (((↑e : N'' →ₗ[R'] N₂'').compAlternatingMap x + (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap x_1 :
          (a : ι → M'') → N₂'')
        x_2 :
      N₂'')
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst_11 : CommSemiring R'
inst_12 : AddCommMonoid M''
inst_13 : AddCommMonoid M₂''
inst_14 : AddCommMonoid N''
inst_15 : AddCommMonoid N₂''
inst_16 : Module R' M''
inst_17 : Module R' M₂''
inst_18 : Module R' N''
inst_19 : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x : R'
x_1 : M'' [⋀^ι]→ₗ[R'] N''
⊢ (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap (x • x_1) =
    HSMul.hSMul (α := R') ((RingHom.id R' : (a : R') → R') x : R') ((↑e : N'' →ₗ[R'] N₂'').compAlternatingMap x_1)
have H : ∀ (x_2 : ι → M''),
  Eq.{u_14 + 1} (α := N₂'') (((↑e : N'' →ₗ[R'] N₂'').compAlternatingMap (x • x_1) : (a : ι → M'') → N₂'') x_2 : N₂'')
    ((HSMul.hSMul (α := R') ((RingHom.id R' : (a : R') → R') x : R') ((↑e : N'' →ₗ[R'] N₂'').compAlternatingMap x_1) :
          (a : ι → M'') → N₂'')
        x_2 :
      N₂'')
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst_11 : CommSemiring R'
inst_12 : AddCommMonoid M''
inst_13 : AddCommMonoid M₂''
inst_14 : AddCommMonoid N''
inst_15 : AddCommMonoid N₂''
inst_16 : Module R' M''
inst_17 : Module R' M₂''
inst_18 : Module R' N''
inst_19 : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x : M'' [⋀^ι]→ₗ[R'] N''
⊢ (fun (f : M'' [⋀^ι]→ₗ[R'] N₂'') ↦ (↑e.symm : N₂'' →ₗ[R'] N'').compAlternatingMap f)
      ((fun (f : M'' [⋀^ι]→ₗ[R'] N'') ↦ (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap f) x) =
    x
have H : ∀ (x_1 : ι → M''),
  Eq.{u_13 + 1} (α := N'')
    (((fun (f : M'' [⋀^ι]→ₗ[R'] N₂'') ↦ (↑e.symm : N₂'' →ₗ[R'] N'').compAlternatingMap f)
            ((fun (f : M'' [⋀^ι]→ₗ[R'] N'') ↦ (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap f) x) :
          (a : ι → M'') → N'')
        x_1 :
      N'')
    ((x : (a : ι → M'') → N'') x_1 : N'')
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst_11 : CommSemiring R'
inst_12 : AddCommMonoid M''
inst_13 : AddCommMonoid M₂''
inst_14 : AddCommMonoid N''
inst_15 : AddCommMonoid N₂''
inst_16 : Module R' M''
inst_17 : Module R' M₂''
inst_18 : Module R' N''
inst_19 : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x : M'' [⋀^ι]→ₗ[R'] N₂''
⊢ (fun (f : M'' [⋀^ι]→ₗ[R'] N'') ↦ (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap f)
      ((fun (f : M'' [⋀^ι]→ₗ[R'] N₂'') ↦ (↑e.symm : N₂'' →ₗ[R'] N'').compAlternatingMap f) x) =
    x
have H : ∀ (x_1 : ι → M''),
  Eq.{u_14 + 1} (α := N₂'')
    (((fun (f : M'' [⋀^ι]→ₗ[R'] N'') ↦ (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap f)
            ((fun (f : M'' [⋀^ι]→ₗ[R'] N₂'') ↦ (↑e.symm : N₂'' →ₗ[R'] N'').compAlternatingMap f) x) :
          (a : ι → M'') → N₂'')
        x_1 :
      N₂'')
    ((x : (a : ι → M'') → N₂'') x_1 : N₂'')
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Curry (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R N
n : ℕ
g : M₂ →ₗ[R] M
f : M [⋀^Fin n.succ]→ₗ[R] N
m : M₂
v : Fin n → M₂
i : Fin n.succ
⊢ Eq.{u_2 + 1} (α := M)
    (((fun (x : Fin n.succ) ↦ g) i : (a : (fun (x : Fin n.succ) ↦ M₂) i) → (fun (x : Fin n.succ) ↦ M) i)
        (Fin.cons (α := fun (x : Fin n.succ) ↦ M₂) m v i : M₂) :
      (fun (x : Fin n.succ) ↦ M) i)
    (Fin.cons (α := fun (x : Fin n.succ) ↦ M) ((g : (a : M₂) → M) m)
        (fun (i : Fin n) ↦ ((fun (x : Fin n) ↦ g) i : (a : (fun (x : Fin n) ↦ M₂) i) → (fun (x : Fin n) ↦ M) i) (v i))
        i :
      M)
have zero : Eq.{u_2 + 1} (α := M)
  (((fun (x : Fin n.succ) ↦ g) 0 : (a : (fun (x : Fin n.succ) ↦ M₂) 0) → (fun (x : Fin n.succ) ↦ M) 0)
      (Fin.cons (α := fun (x : Fin n.succ) ↦ M₂) m v 0 : M₂) :
    (fun (x : Fin n.succ) ↦ M) 0)
  (Fin.cons (α := fun (x : Fin n.succ) ↦ M) ((g : (a : M₂) → M) m)
      (fun (i : Fin n) ↦ ((fun (x : Fin n) ↦ g) i : (a : (fun (x : Fin n) ↦ M₂) i) → (fun (x : Fin n) ↦ M) i) (v i)) 0 :
    M)
Tactic: cases i using Fin.cases
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Curry (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R N
n : ℕ
g : M₂ →ₗ[R] M
f : M [⋀^Fin n.succ]→ₗ[R] N
m : M₂
v : Fin n → M₂
i : Fin n.succ
zero :
  Eq.{u_2 + 1} (α := M)
    (((fun (x : Fin n.succ) ↦ g) 0 : (a : (fun (x : Fin n.succ) ↦ M₂) 0) → (fun (x : Fin n.succ) ↦ M) 0)
        (Fin.cons (α := fun (x : Fin n.succ) ↦ M₂) m v 0 : M₂) :
      (fun (x : Fin n.succ) ↦ M) 0)
    (Fin.cons (α := fun (x : Fin n.succ) ↦ M) ((g : (a : M₂) → M) m)
        (fun (i : Fin n) ↦ ((fun (x : Fin n) ↦ g) i : (a : (fun (x : Fin n) ↦ M₂) i) → (fun (x : Fin n) ↦ M) i) (v i))
        0 :
      M)
⊢ Eq.{u_2 + 1} (α := M)
    (((fun (x : Fin n.succ) ↦ g) i : (a : (fun (x : Fin n.succ) ↦ M₂) i) → (fun (x : Fin n.succ) ↦ M) i)
        (Fin.cons (α := fun (x : Fin n.succ) ↦ M₂) m v i : M₂) :
      (fun (x : Fin n.succ) ↦ M) i)
    (Fin.cons (α := fun (x : Fin n.succ) ↦ M) ((g : (a : M₂) → M) m)
        (fun (i : Fin n) ↦ ((fun (x : Fin n) ↦ g) i : (a : (fun (x : Fin n) ↦ M₂) i) → (fun (x : Fin n) ↦ M) i) (v i))
        i :
      M)
have succ : ∀ (i : Fin n),
  Eq.{u_2 + 1} (α := M)
    (((fun (x : Fin n.succ) ↦ g) i.succ : (a : (fun (x : Fin n.succ) ↦ M₂) i.succ) → (fun (x : Fin n.succ) ↦ M) i.succ)
        (Fin.cons (α := fun (x : Fin n.succ) ↦ M₂) m v i.succ : M₂) :
      (fun (x : Fin n.succ) ↦ M) i.succ)
    (Fin.cons (α := fun (x : Fin n.succ) ↦ M) ((g : (a : M₂) → M) m)
        (fun (i : Fin n) ↦ ((fun (x : Fin n) ↦ g) i : (a : (fun (x : Fin n) ↦ M₂) i) → (fun (x : Fin n) ↦ M) i) (v i))
        i.succ :
      M)
Tactic: cases i using Fin.cases
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (hypothesis)
Goal:
ιa : Type u_1
ιb : Type u_2
inst : Fintype ιa
inst_1 : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst_2 : CommSemiring R'
inst_3 : AddCommGroup N₁
inst_4 : Module R' N₁
inst_5 : AddCommGroup N₂
inst_6 : Module R' N₂
inst_7 : AddCommMonoid Mᵢ
inst_8 : Module R' Mᵢ
inst_9 : DecidableEq ιa
inst_10 : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
H : (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range : Perm (ιa ⊕ ιb) → Perm (ιa ⊕ ιb) → Prop) σ₁ σ₂
⊢ Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    ((fun (σ : Perm (ιa ⊕ ιb)) ↦
        HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
          (MultilinearMap.domDomCongr σ
            ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
              (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
      σ₁)
    ((fun (σ : Perm (ιa ⊕ ιb)) ↦
        HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
          (MultilinearMap.domDomCongr σ
            ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
              (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
      σ₂)
have H₁ : σ₁⁻¹ * σ₂ ∈ (Perm.sumCongrHom ιa ιb).range
Tactic: rw [QuotientGroup.leftRel_apply] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
Goal:
ιa : Type u_1
ιb : Type u_2
inst : Fintype ιa
inst_1 : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst_2 : CommSemiring R'
inst_3 : AddCommGroup N₁
inst_4 : Module R' N₁
inst_5 : AddCommGroup N₂
inst_6 : Module R' N₂
inst_7 : AddCommMonoid Mᵢ
inst_8 : Module R' Mᵢ
inst_9 : DecidableEq ιa
inst_10 : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
H : σ₁⁻¹ * σ₂ ∈ (Perm.sumCongrHom ιa ιb).range
⊢ Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    ((fun (σ : Perm (ιa ⊕ ιb)) ↦
        HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
          (MultilinearMap.domDomCongr σ
            ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
              (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
      σ₁)
    ((fun (σ : Perm (ιa ⊕ ιb)) ↦
        HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
          (MultilinearMap.domDomCongr σ
            ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
              (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
      σ₂)
have obtain : ∀ (sl : Perm ιa) (sr : Perm ιb)
  (h : (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) = σ₁⁻¹ * σ₂),
  Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    ((fun (σ : Perm (ιa ⊕ ιb)) ↦
        HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
          (MultilinearMap.domDomCongr σ
            ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
              (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
      σ₁)
    ((fun (σ : Perm (ιa ⊕ ιb)) ↦
        HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
          (MultilinearMap.domDomCongr σ
            ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
              (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
      σ₂)
Tactic: obtain ⟨⟨sl, sr⟩, h⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
Goal:
ιa : Type u_1
ιb : Type u_2
inst : Fintype ιa
inst_1 : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst_2 : CommSemiring R'
inst_3 : AddCommGroup N₁
inst_4 : Module R' N₁
inst_5 : AddCommGroup N₂
inst_6 : Module R' N₂
inst_7 : AddCommMonoid Mᵢ
inst_8 : Module R' Mᵢ
inst_9 : DecidableEq ιa
inst_10 : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
h : (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) = σ₁⁻¹ * σ₂
⊢ Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    ((fun (σ : Perm (ιa ⊕ ιb)) ↦
        HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
          (MultilinearMap.domDomCongr σ
            ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
              (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
      σ₁)
    ((fun (σ : Perm (ιa ⊕ ιb)) ↦
        HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
          (MultilinearMap.domDomCongr σ
            ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
              (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
      σ₂)
have H : ∀ (v : (i : ιa ⊕ ιb) → Mᵢ),
  Eq (α := N₁ ⊗[R'] N₂)
    (((fun (σ : Perm (ιa ⊕ ιb)) ↦
              HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
                (MultilinearMap.domDomCongr σ
                  ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                    (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
            σ₁ :
          (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
        v :
      N₁ ⊗[R'] N₂)
    (((fun (σ : Perm (ιa ⊕ ιb)) ↦
              HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
                (MultilinearMap.domDomCongr σ
                  ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                    (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
            σ₂ :
          (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
        v :
      N₁ ⊗[R'] N₂)
Tactic: ext v
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
Goal:
ιa : Type u_1
ιb : Type u_2
inst : Fintype ιa
inst_1 : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst_2 : CommSemiring R'
inst_3 : AddCommGroup N₁
inst_4 : Module R' N₁
inst_5 : AddCommGroup N₂
inst_6 : Module R' N₂
inst_7 : AddCommMonoid Mᵢ
inst_8 : Module R' Mᵢ
inst_9 : DecidableEq ιa
inst_10 : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
h : (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) = σ₁⁻¹ * σ₂
v : (i : ιa ⊕ ιb) → Mᵢ
⊢ Eq (α := N₁ ⊗[R'] N₂)
    (((fun (σ : Perm (ιa ⊕ ιb)) ↦
              HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
                (MultilinearMap.domDomCongr σ
                  ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                    (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
            σ₁ :
          (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
        v :
      N₁ ⊗[R'] N₂)
    (((fun (σ : Perm (ιa ⊕ ιb)) ↦
              HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
                (MultilinearMap.domDomCongr σ
                  ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                    (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
            σ₂ :
          (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
        v :
      N₁ ⊗[R'] N₂)
have H : HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ₁ : ℤˣ)
    (((a : (a : ιa → Mᵢ) → N₁) fun (i₁ : ιa) ↦ v ((σ₁ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ⊗ₜ[R']
        (b : (a : ιb → Mᵢ) → N₂) fun (i₂ : ιb) ↦ v ((σ₁ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
      N₁ ⊗[R'] N₂) =
  HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ₂ : ℤˣ)
    (((a : (a : ιa → Mᵢ) → N₁) fun (i₁ : ιa) ↦ v ((σ₂ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ⊗ₜ[R']
        (b : (a : ιb → Mᵢ) → N₂) fun (i₂ : ιb) ↦ v ((σ₂ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
      N₁ ⊗[R'] N₂)
Tactic: simp only [MultilinearMap.domDomCongr_apply, MultilinearMap.domCoprod_apply,
      coe_multilinearMap, MultilinearMap.smul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (hypothesis)
Goal:
ιa : Type u_1
ιb : Type u_2
inst : Fintype ιa
inst_1 : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst_2 : CommSemiring R'
inst_3 : AddCommGroup N₁
inst_4 : Module R' N₁
inst_5 : AddCommGroup N₂
inst_6 : Module R' N₂
inst_7 : AddCommMonoid Mᵢ
inst_8 : Module R' Mᵢ
inst_9 : DecidableEq ιa
inst_10 : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
h : (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) = σ₁⁻¹ * σ₂
v : (i : ιa ⊕ ιb) → Mᵢ
⊢ HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ₁ : ℤˣ)
      (((a : (a : ιa → Mᵢ) → N₁) fun (i₁ : ιa) ↦ v ((σ₁ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ⊗ₜ[R']
          (b : (a : ιb → Mᵢ) → N₂) fun (i₂ : ιb) ↦ v ((σ₁ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
        N₁ ⊗[R'] N₂) =
    HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ₂ : ℤˣ)
      (((a : (a : ιa → Mᵢ) → N₁) fun (i₁ : ιa) ↦ v ((σ₂ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ⊗ₜ[R']
          (b : (a : ιb → Mᵢ) → N₂) fun (i₂ : ιb) ↦ v ((σ₂ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
        N₁ ⊗[R'] N₂)
have h₁ : σ₂ =
  HMul.hMul (β := Perm (ιa ⊕ ιb)) σ₁
    ((Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) : Perm (ιa ⊕ ιb))
Tactic: replace h := inv_mul_eq_iff_eq_mul.mp h.symm
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (hypothesis)
Goal:
ιa : Type u_1
ιb : Type u_2
inst : Fintype ιa
inst_1 : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst_2 : CommSemiring R'
inst_3 : AddCommGroup N₁
inst_4 : Module R' N₁
inst_5 : AddCommGroup N₂
inst_6 : Module R' N₂
inst_7 : AddCommMonoid Mᵢ
inst_8 : Module R' Mᵢ
inst_9 : DecidableEq ιa
inst_10 : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
v : (i : ιa ⊕ ιb) → Mᵢ
h :
  σ₂ =
    HMul.hMul (β := Perm (ιa ⊕ ιb)) σ₁
      ((Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) : Perm (ιa ⊕ ιb))
⊢ HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ₁ : ℤˣ)
      (((a : (a : ιa → Mᵢ) → N₁) fun (i₁ : ιa) ↦ v ((σ₁ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ⊗ₜ[R']
          (b : (a : ιb → Mᵢ) → N₂) fun (i₂ : ιb) ↦ v ((σ₁ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
        N₁ ⊗[R'] N₂) =
    HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ₂ : ℤˣ)
      (((a : (a : ιa → Mᵢ) → N₁) fun (i₁ : ιa) ↦ v ((σ₂ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ⊗ₜ[R']
          (b : (a : ιb → Mᵢ) → N₂) fun (i₂ : ιb) ↦ v ((σ₂ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
        N₁ ⊗[R'] N₂)
have this : ((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ)
    (HMul.hMul (β := Perm (ιa ⊕ ιb)) σ₁
      ((Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) : Perm (ιa ⊕ ιb))) =
  HMul.hMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ₁ : ℤˣ)
    (HMul.hMul (α := ℤˣ) (β := ℤˣ) (((Perm.sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) sl : ℤˣ)
      (((Perm.sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) sr : ℤˣ))
Tactic: have : Equiv.Perm.sign (σ₁ * Perm.sumCongrHom _ _ (sl, sr))
      = Equiv.Perm.sign σ₁ * (Equiv.Perm.sign sl * Equiv.Perm.sign sr) := by simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
Goal:
ιa : Type u_1
ιb : Type u_2
inst : Fintype ιa
inst_1 : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst_2 : CommSemiring R'
inst_3 : AddCommGroup N₁
inst_4 : Module R' N₁
inst_5 : AddCommGroup N₂
inst_6 : Module R' N₂
inst_7 : AddCommMonoid Mᵢ
inst_8 : Module R' Mᵢ
inst_9 : DecidableEq ιa
inst_10 : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
⊢ HAdd.hAdd (α := N₁ ⊗[R'] N₂) (β := N₁ ⊗[R'] N₂)
      ((summand a b σ : (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂) v : N₁ ⊗[R'] N₂)
      ((summand a b (swap i j • σ) : (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂) v : N₁ ⊗[R'] N₂) =
    0
have h : ∀ (a_1 : Perm (ιa ⊕ ιb)),
  HAdd.hAdd (α := N₁ ⊗[R'] N₂) (β := N₁ ⊗[R'] N₂)
      ((summand a b (Quotient.mk'' a_1) : (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂) v : N₁ ⊗[R'] N₂)
      ((summand a b (HSMul.hSMul (β := Perm.ModSumCongr ιa ιb) (swap i j) (Quotient.mk'' a_1)) :
            (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
          v :
        N₁ ⊗[R'] N₂) =
    0
Tactic: induction σ using Quotient.inductionOn'
Cleared hypotheses: σ