awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
d : n → R
rw : Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((1 : (a : n) → n) k)) (∏ i : n, d i)
h : Membership.mem (γ := Finset (Perm n)) (ofSign 1) 1
h₀ :
  ∀ (b : Perm n),
    Membership.mem (γ := Finset (Perm n)) (ofSign 1) b →
      b ≠ 1 → Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((b : (a : n) → n) k)) 0
⊢ detp 1 (diagonal d) = ∏ i : n, d i

Tactic:
rw [detp, sum_eq_single_of_mem 1]

Premises used: Finset.sum_eq_single_of_mem, Matrix.detp, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
d : n → R
⊢ Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((1 : (a : n) → n) k)) (∏ i : n, d i)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
d : n → R
⊢ Membership.mem (γ := Finset (Perm n)) (ofSign 1) 1

Tactic:
simp [ofSign]

Premises used: Equiv.Perm.ofSign
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
d : n → R
σ : Perm n
hσ1 : σ ≠ 1
h₀ :
  ∀ (i : n) (hi : ¬Eq (α := n) ((σ : (a : n) → n) i : n) ((1 : (a : n) → n) i : n)),
    Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((σ : (a : n) → n) k)) 0
⊢ Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((σ : (a : n) → n) k)) 0

Tactic:
obtain ⟨i, hi⟩ := not_forall.mp (mt Perm.ext_iff.mpr hσ1)

Premises used: Iff.mpr, mt, Equiv.Perm.ext_iff, Iff.mp, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
d : n → R
σ : Perm n
hσ1 : σ ≠ 1
i : n
hi : ¬Eq (α := n) ((σ : (a : n) → n) i : n) ((1 : (a : n) → n) i : n)
⊢ Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((σ : (a : n) → n) k)) 0

Tactic:
prod_eq_zero (mem_univ i) (diagonal_apply_ne' _ hi)

Premises used: Finset.mem_univ, Matrix.diagonal_apply_ne', Finset.prod_eq_zero
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
d : n → R
σ : Perm n
hσ1 : σ ≠ 1
i : n
hi : ¬Eq (α := n) ((σ : (a : n) → n) i : n) ((1 : (a : n) → n) i : n)
⊢ Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((σ : (a : n) → n) k)) 0

Tactic:
exact prod_eq_zero (mem_univ i) (diagonal_apply_ne' _ hi)
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
rw : Eq.{u_3 + 1} (α := R) (detp.{u_1, u_3} (n := n) 1 (diagonal fun (x : n) ↦ 1)) 1
rw₁ : Eq.{u_3 + 1} (α := R) (∏ i : n, 1) 1
rw₂ rw₃ : Eq.{u_3 + 1} (α := R) 1 1
⊢ Eq.{u_3 + 1} (α := R) (detp.{u_1, u_3} (n := n) 1 1) 1

Tactic:
rw [← diagonal_one, detp_one_diagonal, prod_const_one]

Premises used: Finset.prod_const_one, Matrix.detp_one_diagonal, Matrix.diagonal_one
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
d : n → R
rw :
  ∀ (x : Perm n),
    Membership.mem (γ := Finset (Perm n)) (ofSign (-1)) x →
      Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((x : (a : n) → n) k)) 0
⊢ detp (-1) (diagonal d) = 0

Tactic:
rw [detp, sum_eq_zero]

Premises used: Finset.sum_eq_zero, Matrix.detp
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
d : n → R
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign (-1)) σ
contrapose : ∀ (hσ : σ = 1), σ ∉ ofSign (-1)
⊢ σ ≠ 1

Tactic:
contrapose hσ
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
d : n → R
σ : Perm n
hσ : σ = 1
rw : ¬Eq (α := ℤˣ) 1 (-1)
⊢ σ ∉ ofSign (-1)

Tactic:
rw [hσ, mem_ofSign, sign_one]

Premises used: Equiv.Perm.mem_ofSign, Equiv.Perm.sign_one
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
d : n → R
σ : Perm n
hσ : σ = 1
⊢ ¬Eq (α := ℤˣ) 1 (-1)

Tactic:
decide
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
d : n → R
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign (-1)) σ
⊢ σ ≠ 1

Tactic:
have hσ1 : σ ≠ 1 := by
    contrapose hσ
    rw [hσ, mem_ofSign, sign_one]
    decide
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
d : n → R
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign (-1)) σ
hσ1 : σ ≠ 1
obtain :
  ∀ (i : n) (hi : ¬Eq (α := n) ((σ : (a : n) → n) i : n) ((1 : (a : n) → n) i : n)),
    Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((σ : (a : n) → n) k)) 0
⊢ Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((σ : (a : n) → n) k)) 0

Tactic:
obtain ⟨i, hi⟩ := not_forall.mp (mt Perm.ext_iff.mpr hσ1)

Premises used: Iff.mpr, mt, Equiv.Perm.ext_iff, Iff.mp, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
d : n → R
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign (-1)) σ
hσ1 : σ ≠ 1
i : n
hi : ¬Eq (α := n) ((σ : (a : n) → n) i : n) ((1 : (a : n) → n) i : n)
⊢ Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((σ : (a : n) → n) k)) 0

Tactic:
prod_eq_zero (mem_univ i) (diagonal_apply_ne' _ hi)

Premises used: Finset.mem_univ, Matrix.diagonal_apply_ne', Finset.prod_eq_zero
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
d : n → R
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign (-1)) σ
hσ1 : σ ≠ 1
i : n
hi : ¬Eq (α := n) ((σ : (a : n) → n) i : n) ((1 : (a : n) → n) i : n)
⊢ Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((σ : (a : n) → n) k)) 0

Tactic:
exact prod_eq_zero (mem_univ i) (diagonal_apply_ne' _ hi)
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
rw : Eq.{u_3 + 1} (α := R) (detp.{u_1, u_3} (n := n) (-1) (diagonal fun (x : n) ↦ 1)) 0
rw₁ rw₂ : Eq.{u_3 + 1} (α := R) 0 0
⊢ Eq.{u_3 + 1} (α := R) (detp.{u_1, u_3} (n := n) (-1) 1) 0

Tactic:
rw [← diagonal_one, detp_neg_one_diagonal]

Premises used: Matrix.diagonal_one, Matrix.detp_neg_one_diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
s : ℤˣ
A : Matrix n n R
i j : n
⊢ adjp s A i j = ∑ σ ∈ ofSign s with (σ : (a : n) → n) j = i, ∏ k ∈ {j}ᶜ, A k ((σ : (a : n) → n) k)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Matrix.adjp, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
s t : ℤˣ
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ
h :
  ∀ (τ : Perm n),
    Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔ τ ∈ Finset.map (mulRightEmbedding σ) (ofSign t)
⊢ ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)

Tactic:
ext τ
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
s t : ℤˣ
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ
τ : Perm n
h :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n),
      Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ (mulRightEmbedding σ : (a : Perm n) → Perm n) a = τ
h₁ :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ a * σ = τ
h₂ :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ a = τ * σ⁻¹
h₃ :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔ Membership.mem (γ := Finset (Perm n)) (ofSign t) (τ * σ⁻¹)
h₄ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t * s ↔ ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹) = t
h₅ :
  ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t * s ↔
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ : ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ⁻¹ : ℤˣ) =
      t
h₆ :
  ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t * s ↔
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ : ℤˣ)
        ((((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ)⁻¹ : ℤˣ) =
      t
h₇ :
  ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t * s ↔
    ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ =
      HMul.hMul (β := ℤˣ) t (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)
⊢ Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔ τ ∈ Finset.map (mulRightEmbedding σ) (ofSign t)

Tactic:
simp_rw [mem_map, mulRightEmbedding_apply, ← eq_mul_inv_iff_mul_eq, exists_eq_right,
      mem_ofSign, map_mul, map_inv, mul_inv_eq_iff_eq_mul, mem_ofSign.mp hσ]

Premises used: map_inv, mulRightEmbedding_apply, exists_eq_right, eq_mul_inv_iff_mul_eq, Equiv.Perm.mem_ofSign, map_mul, Iff.mp, Finset.mem_map, mul_inv_eq_iff_eq_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
⊢ ∀ {s t : ℤˣ} {σ : Perm n} (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ),
    ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)

Tactic:
have hf {s t} {σ : Perm n} (hσ : σ ∈ ofSign s) :
      ofSign (t * s) = (ofSign t).map (mulRightEmbedding σ) := by
    ext τ
    simp_rw [mem_map, mulRightEmbedding_apply, ← eq_mul_inv_iff_mul_eq, exists_eq_right,
      mem_ofSign, map_mul, map_inv, mul_inv_eq_iff_eq_mul, mem_ofSign.mp hσ]
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
hf :
  ∀ {s t : ℤˣ} {σ : Perm n} (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ),
    ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
s t : ℤˣ
simp_rw :
  Eq.{u_3 + 1} (α := R)
    (∑ i ∈ ofSign s,
      ∑ j ∈ ofSign t, HMul.hMul (α := R) (∏ k : n, A k ((i : (a : n) → n) k)) (∏ k : n, B k ((j : (a : n) → n) k)))
    (∑ x ∈ ofSign s,
      ∑ x_1 ∈ ofSign (t * s),
        HMul.hMul (α := R) (∏ x_2 : n, A x_2 ((x : (a : n) → n) x_2))
          (∏ x_2 : n, B ((x : (a : n) → n) x_2) ((x_1 : (a : n) → n) x_2)))
⊢ detp s A * detp t B =
    ∑ σ ∈ ofSign s,
      ∑ τ ∈ ofSign (t * s), ∏ k : n, A k ((σ : (a : n) → n) k) * B ((σ : (a : n) → n) k) ((τ : (a : n) → n) k)

Tactic:
simp_rw [detp, sum_mul_sum, prod_mul_distrib]

Premises used: Finset.prod_mul_distrib, Matrix.detp, Finset.sum_mul_sum
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
hf :
  ∀ {s t : ℤˣ} {σ : Perm n} (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ),
    ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
s t : ℤˣ
⊢ Eq.{u_3 + 1} (α := R)
    (∑ i ∈ ofSign s,
      ∑ j ∈ ofSign t, HMul.hMul (α := R) (∏ k : n, A k ((i : (a : n) → n) k)) (∏ k : n, B k ((j : (a : n) → n) k)))
    (∑ x ∈ ofSign s,
      ∑ x_1 ∈ ofSign (t * s),
        HMul.hMul (α := R) (∏ x_2 : n, A x_2 ((x : (a : n) → n) x_2))
          (∏ x_2 : n, B ((x : (a : n) → n) x_2) ((x_1 : (a : n) → n) x_2)))

Tactic:
sum_congr rfl fun σ hσ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
hf :
  ∀ {s t : ℤˣ} {σ : Perm n} (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ),
    ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
s t : ℤˣ
refine :
  ∀ (σ : Perm n) (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ),
    Eq.{u_3 + 1} (α := R)
      (∑ j ∈ ofSign t, HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((j : (a : n) → n) k)))
      (∑ x ∈ ofSign (t * s),
        HMul.hMul (α := R) (∏ x : n, A x ((σ : (a : n) → n) x))
          (∏ x_1 : n, B ((σ : (a : n) → n) x_1) ((x : (a : n) → n) x_1)))
⊢ Eq.{u_3 + 1} (α := R)
    (∑ i ∈ ofSign s,
      ∑ j ∈ ofSign t, HMul.hMul (α := R) (∏ k : n, A k ((i : (a : n) → n) k)) (∏ k : n, B k ((j : (a : n) → n) k)))
    (∑ x ∈ ofSign s,
      ∑ x_1 ∈ ofSign (t * s),
        HMul.hMul (α := R) (∏ x_2 : n, A x_2 ((x : (a : n) → n) x_2))
          (∏ x_2 : n, B ((x : (a : n) → n) x_2) ((x_1 : (a : n) → n) x_2)))

Tactic:
refine sum_congr rfl fun σ hσ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
hf :
  ∀ {s t : ℤˣ} {σ : Perm n} (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ),
    ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
s t : ℤˣ
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ
simp_rw :
  Eq.{u_3 + 1} (α := R)
    (∑ j ∈ ofSign t, HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((j : (a : n) → n) k)))
    (∑ x ∈ ofSign t,
      HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k))
        (∏ x_1 : n, B ((σ : (a : n) → n) x_1) ((x : (a : n) → n) ((σ : (a : n) → n) x_1 : n))))
⊢ Eq.{u_3 + 1} (α := R)
    (∑ j ∈ ofSign t, HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((j : (a : n) → n) k)))
    (∑ x ∈ ofSign (t * s),
      HMul.hMul (α := R) (∏ x : n, A x ((σ : (a : n) → n) x))
        (∏ x_1 : n, B ((σ : (a : n) → n) x_1) ((x : (a : n) → n) x_1)))

Tactic:
simp_rw [hf hσ, sum_map, mulRightEmbedding_apply, Perm.mul_apply]

Premises used: Finset.sum_map, mulRightEmbedding_apply, Equiv.Perm.mul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
hf :
  ∀ {s t : ℤˣ} {σ : Perm n} (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ),
    ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
s t : ℤˣ
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ
⊢ Eq.{u_3 + 1} (α := R)
    (∑ j ∈ ofSign t, HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((j : (a : n) → n) k)))
    (∑ x ∈ ofSign t,
      HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k))
        (∏ x_1 : n, B ((σ : (a : n) → n) x_1) ((x : (a : n) → n) ((σ : (a : n) → n) x_1 : n))))

Tactic:
sum_congr rfl fun τ hτ ↦ (congr_arg (_ * ·) (Equiv.prod_comp σ _).symm)

Premises used: HMul.hMul, Finset.univ, Finset.prod, congr_arg, Equiv.prod_comp, Eq.symm, DFunLike.coe, Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
hf :
  ∀ {s t : ℤˣ} {σ : Perm n} (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ),
    ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
s t : ℤˣ
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ
⊢ Eq.{u_3 + 1} (α := R)
    (∑ j ∈ ofSign t, HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((j : (a : n) → n) k)))
    (∑ x ∈ ofSign t,
      HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k))
        (∏ x_1 : n, B ((σ : (a : n) → n) x_1) ((x : (a : n) → n) ((σ : (a : n) → n) x_1 : n))))

Tactic:
exact sum_congr rfl fun τ hτ ↦ (congr_arg (_ * ·) (Equiv.prod_comp σ _).symm)

Premises used: HMul.hMul, congr_arg, Equiv.prod_comp, Eq.symm, Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
hf :
  ∀ {s t : ℤˣ} {σ : Perm n} (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ),
    ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
⊢ ∀ {s t : ℤˣ},
    detp s A * detp t B =
      ∑ σ ∈ ofSign s,
        ∑ τ ∈ ofSign (t * s), ∏ k : n, A k ((σ : (a : n) → n) k) * B ((σ : (a : n) → n) k) ((τ : (a : n) → n) k)

Tactic:
have h {s t} : detp s A * detp t B =
      ∑ σ ∈ ofSign s, ∑ τ ∈ ofSign (t * s), ∏ k, A k (σ k) * B (σ k) (τ k) := by
    simp_rw [detp, sum_mul_sum, prod_mul_distrib]
    refine sum_congr rfl fun σ hσ ↦ ?_
    simp_rw [hf hσ, sum_map, mulRightEmbedding_apply, Perm.mul_apply]
    exact sum_congr rfl fun τ hτ ↦ (congr_arg (_ * ·) (Equiv.prod_comp σ _).symm)
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
hf :
  ∀ {s t : ℤˣ} {σ : Perm n} (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ),
    ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
h :
  ∀ {s t : ℤˣ},
    detp s A * detp t B =
      ∑ σ ∈ ofSign s,
        ∑ τ ∈ ofSign (t * s), ∏ k : n, A k ((σ : (a : n) → n) k) * B ((σ : (a : n) → n) k) ((τ : (a : n) → n) k)
ι : Perm n ↪ n → n := { toFun := fun (e : n ≃ n) ↦ (⇑e : (a : n) → n), inj' := ⋯ }
⊢ ∀ {σ : Perm n} {x : n}, Eq (α := n) ((ι : (a : Perm n) → n → n) σ x : n) ((σ : (a : n) → n) x : n)

Tactic:
have hι {σ x} : ι σ x = σ x := rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
hf :
  ∀ {s t : ℤˣ} {σ : Perm n} (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ),
    ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
h :
  ∀ {s t : ℤˣ},
    detp s A * detp t B =
      ∑ σ ∈ ofSign s,
        ∑ τ ∈ ofSign (t * s), ∏ k : n, A k ((σ : (a : n) → n) k) * B ((σ : (a : n) → n) k) ((τ : (a : n) → n) k)
ι : Perm n ↪ n → n := { toFun := fun (e : n ≃ n) ↦ (⇑e : (a : n) → n), inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, Eq (α := n) ((ι : (a : Perm n) → n → n) σ x : n) ((σ : (a : n) → n) x : n)
bij : Finset (n → n) := Finset.map ι (disjUnion (ofSign 1) (ofSign (-1)) ⋯)
s : ℤˣ
simp_rw :
  ∑ x ∈ ofSign s, ∑ x_1 : (a : n) → n, ∏ i : n, A i (x_1 i) * B (x_1 i) ((x : (a : n) → n) i) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i) +
      HAdd.hAdd (α := R)
        (∑ x ∈ ofSign 1,
          ∑ x_1 ∈ ofSign s, ∏ k : n, A k ((x : (a : n) → n) k) * B ((x : (a : n) → n) k) ((x_1 : (a : n) → n) k))
        (∑ x ∈ ofSign (-1),
          ∑ x_1 ∈ ofSign s, ∏ k : n, A k ((x : (a : n) → n) k) * B ((x : (a : n) → n) k) ((x_1 : (a : n) → n) k))
⊢ detp s (A * B) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i) +
      (detp 1 A * detp s B + detp (-1) A * detp (-s) B)

Tactic:
simp_rw [h, neg_mul_neg, mul_one, detp, mul_apply, prod_univ_sum, Fintype.piFinset_univ]

Premises used: Fintype.piFinset_univ, Matrix.mul_apply, Matrix.detp, neg_mul_neg, mul_one, Finset.prod_univ_sum
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
hf :
  ∀ {s t : ℤˣ} {σ : Perm n} (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ),
    ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
h :
  ∀ {s t : ℤˣ},
    detp s A * detp t B =
      ∑ σ ∈ ofSign s,
        ∑ τ ∈ ofSign (t * s), ∏ k : n, A k ((σ : (a : n) → n) k) * B ((σ : (a : n) → n) k) ((τ : (a : n) → n) k)
ι : Perm n ↪ n → n := { toFun := fun (e : n ≃ n) ↦ (⇑e : (a : n) → n), inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, Eq (α := n) ((ι : (a : Perm n) → n → n) σ x : n) ((σ : (a : n) → n) x : n)
bij : Finset (n → n) := Finset.map ι (disjUnion (ofSign 1) (ofSign (-1)) ⋯)
s : ℤˣ
rw :
  ∑ i ∈ bijᶜ, ∑ x ∈ ofSign s, ∏ i_1 : n, A i_1 (i i_1) * B (i i_1) ((x : (a : n) → n) i_1) +
      HAdd.hAdd (α := R)
        (∑ x ∈ ofSign 1,
          ∑ x_1 ∈ ofSign s,
            ∏ i : n, A i ((ι : (a : Perm n) → n → n) x i) * B ((ι : (a : Perm n) → n → n) x i) ((x_1 : (a : n) → n) i))
        (∑ x ∈ ofSign (-1),
          ∑ x_1 ∈ ofSign s,
            ∏ i : n,
              A i ((ι : (a : Perm n) → n → n) x i) * B ((ι : (a : Perm n) → n → n) x i) ((x_1 : (a : n) → n) i)) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i) +
      HAdd.hAdd (α := R)
        (∑ x ∈ ofSign 1,
          ∑ x_1 ∈ ofSign s, ∏ k : n, A k ((x : (a : n) → n) k) * B ((x : (a : n) → n) k) ((x_1 : (a : n) → n) k))
        (∑ x ∈ ofSign (-1),
          ∑ x_1 ∈ ofSign s, ∏ k : n, A k ((x : (a : n) → n) k) * B ((x : (a : n) → n) k) ((x_1 : (a : n) → n) k))
⊢ ∑ x ∈ ofSign s, ∑ x_1 : (a : n) → n, ∏ i : n, A i (x_1 i) * B (x_1 i) ((x : (a : n) → n) i) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i) +
      HAdd.hAdd (α := R)
        (∑ x ∈ ofSign 1,
          ∑ x_1 ∈ ofSign s, ∏ k : n, A k ((x : (a : n) → n) k) * B ((x : (a : n) → n) k) ((x_1 : (a : n) → n) k))
        (∑ x ∈ ofSign (-1),
          ∑ x_1 ∈ ofSign s, ∏ k : n, A k ((x : (a : n) → n) k) * B ((x : (a : n) → n) k) ((x_1 : (a : n) → n) k))

Tactic:
rw [sum_comm, ← sum_compl_add_sum bij, sum_map, sum_disjUnion]

Premises used: Finset.sum_map, Finset.sum_disjUnion, Finset.sum_compl_add_sum, Finset.sum_comm
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
hf :
  ∀ {s t : ℤˣ} {σ : Perm n} (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ),
    ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
h :
  ∀ {s t : ℤˣ},
    detp s A * detp t B =
      ∑ σ ∈ ofSign s,
        ∑ τ ∈ ofSign (t * s), ∏ k : n, A k ((σ : (a : n) → n) k) * B ((σ : (a : n) → n) k) ((τ : (a : n) → n) k)
ι : Perm n ↪ n → n := { toFun := fun (e : n ≃ n) ↦ (⇑e : (a : n) → n), inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, Eq (α := n) ((ι : (a : Perm n) → n → n) σ x : n) ((σ : (a : n) → n) x : n)
bij : Finset (n → n) := Finset.map ι (disjUnion (ofSign 1) (ofSign (-1)) ⋯)
s : ℤˣ
⊢ ∑ i ∈ bijᶜ, ∑ x ∈ ofSign s, ∏ i_1 : n, A i_1 (i i_1) * B (i i_1) ((x : (a : n) → n) i_1) +
      HAdd.hAdd (α := R)
        (∑ x ∈ ofSign 1,
          ∑ x_1 ∈ ofSign s,
            ∏ i : n, A i ((ι : (a : Perm n) → n → n) x i) * B ((ι : (a : Perm n) → n → n) x i) ((x_1 : (a : n) → n) i))
        (∑ x ∈ ofSign (-1),
          ∑ x_1 ∈ ofSign s,
            ∏ i : n,
              A i ((ι : (a : Perm n) → n → n) x i) * B ((ι : (a : Perm n) → n → n) x i) ((x_1 : (a : n) → n) i)) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i) +
      HAdd.hAdd (α := R)
        (∑ x ∈ ofSign 1,
          ∑ x_1 ∈ ofSign s, ∏ k : n, A k ((x : (a : n) → n) k) * B ((x : (a : n) → n) k) ((x_1 : (a : n) → n) k))
        (∑ x ∈ ofSign (-1),
          ∑ x_1 ∈ ofSign s, ∏ k : n, A k ((x : (a : n) → n) k) * B ((x : (a : n) → n) k) ((x_1 : (a : n) → n) k))

Tactic:
simp_rw [hι]