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
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)
ι : 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)) ⋯)
h :
  ∀ (s : ℤˣ),
    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)
σ : n → n
hσ_1 : ¬Function.Injective σ
i j : n
hij : i ≠ j
hσ : ∀ (k : n), σ ((swap i j : (a : n) → n) k) = σ k
⊢ Eq.{u_3 + 1} (α := R)
    (∑ x ∈ ofSign 1, HMul.hMul (α := R) (∏ x : n, A x (σ x)) (∏ x_1 : n, B (σ x_1) ((x : (a : n) → n) x_1)))
    (∑ x ∈ ofSign 1,
      HMul.hMul (α := R) (∏ x : n, A x (σ x))
        (∏ x_1 : n, B (σ x_1) ((x : (a : n) → n) ((swap i j : (a : n) → n) x_1 : n))))

Tactic:
sum_congr rfl fun τ hτ ↦ congr_arg (_ * ·) ?_

Premises used: HMul.hMul, Finset.univ, Finset.prod, congr_arg, 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)
ι : 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)) ⋯)
h :
  ∀ (s : ℤˣ),
    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)
σ : n → n
hσ_1 : ¬Function.Injective σ
i j : n
hij : i ≠ j
hσ : ∀ (k : n), σ ((swap i j : (a : n) → n) k) = σ k
refine :
  ∀ (τ : Perm n) (hτ : Membership.mem (γ := Finset (Perm n)) (ofSign 1) τ),
    Eq.{u_3 + 1} (α := R) (∏ x : n, B (σ x) ((τ : (a : n) → n) x))
      (∏ x : n, B (σ x) ((τ : (a : n) → n) ((swap i j : (a : n) → n) x : n)))
⊢ Eq.{u_3 + 1} (α := R)
    (∑ x ∈ ofSign 1, HMul.hMul (α := R) (∏ x : n, A x (σ x)) (∏ x_1 : n, B (σ x_1) ((x : (a : n) → n) x_1)))
    (∑ x ∈ ofSign 1,
      HMul.hMul (α := R) (∏ x : n, A x (σ x))
        (∏ x_1 : n, B (σ x_1) ((x : (a : n) → n) ((swap i j : (a : n) → n) x_1 : n))))

Tactic:
refine sum_congr rfl fun τ hτ ↦ congr_arg (_ * ·) ?_

Premises used: HMul.hMul, congr_arg, 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)
ι : 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)) ⋯)
h :
  ∀ (s : ℤˣ),
    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)
σ : n → n
hσ_1 : ¬Function.Injective σ
i j : n
hij : i ≠ j
hσ : ∀ (k : n), σ ((swap i j : (a : n) → n) k) = σ k
τ : Perm n
hτ : Membership.mem (γ := Finset (Perm n)) (ofSign 1) τ
rw :
  Eq.{u_3 + 1} (α := R)
    (∏ i_1 : n, B (σ ((swap i j : (a : n) → n) i_1)) ((τ : (a : n) → n) ((swap i j : (a : n) → n) i_1 : n)))
    (∏ x : n, B (σ x) ((τ : (a : n) → n) ((swap i j : (a : n) → n) x : n)))
⊢ Eq.{u_3 + 1} (α := R) (∏ x : n, B (σ x) ((τ : (a : n) → n) x))
    (∏ x : n, B (σ x) ((τ : (a : n) → n) ((swap i j : (a : n) → n) x : n)))

Tactic:
rw [← Equiv.prod_comp (swap i j)]

Premises used: Equiv.swap, Equiv.prod_comp
-- 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)
ι : 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)) ⋯)
h :
  ∀ (s : ℤˣ),
    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)
σ : n → n
hσ_1 : ¬Function.Injective σ
i j : n
hij : i ≠ j
hσ : ∀ (k : n), σ ((swap i j : (a : n) → n) k) = σ k
τ : Perm n
hτ : Membership.mem (γ := Finset (Perm n)) (ofSign 1) τ
⊢ Eq.{u_3 + 1} (α := R)
    (∏ i_1 : n, B (σ ((swap i j : (a : n) → n) i_1)) ((τ : (a : n) → n) ((swap i j : (a : n) → n) i_1 : n)))
    (∏ x : n, B (σ x) ((τ : (a : n) → n) ((swap i j : (a : n) → n) x : n)))

Tactic:
simp only [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
s : ℤˣ
A : Matrix n n R
i : n
⊢ Eq.{u_3 + 1} (α := R) (∑ j : n, ∑ i ∈ ofSign s with (i : (a : n) → n) i = j, ∏ k : n, A k ((i : (a : n) → n) k))
    (∑ i ∈ ofSign s with Membership.mem (α := n) (γ := Finset n) univ ((i : (a : n) → n) i : n),
      ∏ k : n, A k ((i : (a : n) → n) k))

Tactic:
have key := sum_fiberwise_eq_sum_filter (ofSign s) univ (· i) fun σ ↦ ∏ k, A k (σ k)
-- 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 : n
key :
  Eq.{u_3 + 1} (α := R) (∑ j : n, ∑ i ∈ ofSign s with (i : (a : n) → n) i = j, ∏ k : n, A k ((i : (a : n) → n) k))
    (∑ i ∈ ofSign s with Membership.mem (α := n) (γ := Finset n) univ ((i : (a : n) → n) i : n),
      ∏ k : n, A k ((i : (a : n) → n) k))
⊢ Eq.{u_3 + 1} (α := R) (∑ j : n, ∑ i ∈ ofSign s with (i : (a : n) → n) i = j, ∏ k : n, A k ((i : (a : n) → n) k))
    (∑ i ∈ ofSign s, ∏ k : n, A k ((i : (a : n) → n) k))

Tactic:
simp_rw [mem_univ, filter_true] at key

Premises used: Finset.mem_univ, Finset.filter_true
-- 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 : n
key :
  Eq.{u_3 + 1} (α := R) (∑ j : n, ∑ i ∈ ofSign s with (i : (a : n) → n) i = j, ∏ k : n, A k ((i : (a : n) → n) k))
    (∑ i ∈ ofSign s, ∏ k : n, A k ((i : (a : n) → n) k))
simp_rw :
  Eq.{u_3 + 1} (α := R)
    (∑ x : n, ∑ i_1 ∈ ofSign s with (i_1 : (a : n) → n) i = x, A i x * ∏ k ∈ {i}ᶜ, A k ((i_1 : (a : n) → n) k))
    (∑ j : n, ∑ σ ∈ ofSign s with (σ : (a : n) → n) i = j, ∏ k : n, A k ((σ : (a : n) → n) k))
⊢ (A * adjp s A) i i = detp s A

Tactic:
simp_rw [mul_apply, adjp_apply, mul_sum, detp, ← key]

Premises used: Finset.mul_sum, Matrix.adjp_apply, Matrix.mul_apply, 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
s : ℤˣ
A : Matrix n n R
i : n
key :
  Eq.{u_3 + 1} (α := R) (∑ j : n, ∑ i ∈ ofSign s with (i : (a : n) → n) i = j, ∏ k : n, A k ((i : (a : n) → n) k))
    (∑ i ∈ ofSign s, ∏ k : n, A k ((i : (a : n) → n) k))
⊢ Eq.{u_3 + 1} (α := R)
    (∑ x : n, ∑ i_1 ∈ ofSign s with (i_1 : (a : n) → n) i = x, A i x * ∏ k ∈ {i}ᶜ, A k ((i_1 : (a : n) → n) k))
    (∑ j : n, ∑ σ ∈ ofSign s with (σ : (a : n) → n) i = j, ∏ k : n, A k ((σ : (a : n) → n) k))

Tactic:
sum_congr rfl fun x hx ↦ 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
s : ℤˣ
A : Matrix n n R
i : n
key :
  Eq.{u_3 + 1} (α := R) (∑ j : n, ∑ i ∈ ofSign s with (i : (a : n) → n) i = j, ∏ k : n, A k ((i : (a : n) → n) k))
    (∑ i ∈ ofSign s, ∏ k : n, A k ((i : (a : n) → n) k))
refine :
  ∀ (x : n) (hx : Membership.mem (γ := Finset n) univ x) (σ : Perm n)
    (hσ : Membership.mem (γ := Finset (Perm n)) ({i_1 ∈ ofSign s | (i_1 : (a : n) → n) i = x}) σ),
    A i x * ∏ k ∈ {i}ᶜ, A k ((σ : (a : n) → n) k) = ∏ k : n, A k ((σ : (a : n) → n) k)
⊢ Eq.{u_3 + 1} (α := R)
    (∑ x : n, ∑ i_1 ∈ ofSign s with (i_1 : (a : n) → n) i = x, A i x * ∏ k ∈ {i}ᶜ, A k ((i_1 : (a : n) → n) k))
    (∑ j : n, ∑ σ ∈ ofSign s with (σ : (a : n) → n) i = j, ∏ k : n, A k ((σ : (a : n) → n) k))

Tactic:
refine sum_congr rfl fun x hx ↦ 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
s : ℤˣ
A : Matrix n n R
i : n
key :
  Eq.{u_3 + 1} (α := R) (∑ j : n, ∑ i ∈ ofSign s with (i : (a : n) → n) i = j, ∏ k : n, A k ((i : (a : n) → n) k))
    (∑ i ∈ ofSign s, ∏ k : n, A k ((i : (a : n) → n) k))
x : n
hx : Membership.mem (γ := Finset n) univ x
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) ({i_1 ∈ ofSign s | (i_1 : (a : n) → n) i = x}) σ
rw :
  A i x * ∏ k ∈ {i}ᶜ, A k ((σ : (a : n) → n) k) =
    HMul.hMul (α := R) (∏ i ∈ {i}, A i ((σ : (a : n) → n) i)) (∏ i ∈ {i}ᶜ, A i ((σ : (a : n) → n) i))
rw₁ : A i x * ∏ k ∈ {i}ᶜ, A k ((σ : (a : n) → n) k) = A i ((σ : (a : n) → n) i) * ∏ i ∈ {i}ᶜ, A i ((σ : (a : n) → n) i)
rw₂ rw₃ : A i x * ∏ k ∈ {i}ᶜ, A k ((σ : (a : n) → n) k) = A i x * ∏ i ∈ {i}ᶜ, A i ((σ : (a : n) → n) i)
⊢ A i x * ∏ k ∈ {i}ᶜ, A k ((σ : (a : n) → n) k) = ∏ k : n, A k ((σ : (a : n) → n) k)

Tactic:
rw [← prod_mul_prod_compl ({i} : Finset n), prod_singleton, (mem_filter.mp hσ).2]

Premises used: Finset.prod_singleton, Finset.prod_mul_prod_compl, And.right, Iff.mp, Finset.mem_filter, Singleton.singleton
-- 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 : Matrix n n R
i j : n
h : i ≠ j
simp_rw :
  Eq.{u_3 + 1} (α := R)
    (∑ x ∈ Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a},
      A i (x.fst (β := fun (i : n) ↦ Perm n)) * ∏ k ∈ {j}ᶜ, A k ((x.snd (β := fun (i : n) ↦ Perm n) : (a : n) → n) k))
    (∑ x ∈ Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign (-1) | (x : (a : n) → n) j = a},
      A i (x.fst (β := fun (i : n) ↦ Perm n)) * ∏ k ∈ {j}ᶜ, A k ((x.snd (β := fun (i : n) ↦ Perm n) : (a : n) → n) k))
⊢ (A * adjp 1 A) i j = (A * adjp (-1) A) i j

Tactic:
simp_rw [mul_apply, adjp_apply, mul_sum, sum_sigma']

Premises used: Finset.mul_sum, Matrix.adjp_apply, Matrix.mul_apply, Finset.sum_sigma'
-- 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 : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
s : ℤˣ
x : n
σ : Perm n
hp : Sigma.mk (β := fun (x : n) ↦ Perm n) x σ ∈ t s
⊢ Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (x : n) ↦ Perm n) x σ)) ∧
    ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
          (Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (x : n) ↦ Perm n) x σ)) =
        s ∧
      ((Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (x : n) ↦ Perm n) x σ) : Perm n) : (a : n) → n) j =
        Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (x : n) ↦ Perm n) x σ)

Tactic:
rw [mem_sigma, mem_filter, mem_ofSign] at hp

Premises used: Finset.mem_sigma, Equiv.Perm.mem_ofSign, Finset.mem_filter
-- 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 : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
s : ℤˣ
x : n
σ : Perm n
hp :
  Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (x : n) ↦ Perm n) x σ)) ∧
    ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
          (Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (x : n) ↦ Perm n) x σ)) =
        s ∧
      ((Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (x : n) ↦ Perm n) x σ) : Perm n) : (a : n) → n) j =
        Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (x : n) ↦ Perm n) x σ)
simp_rw :
  Eq (α := (_ : n) × Perm n)
    (Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ * swap i j : (a : n) → n) i) (σ * swap i j * swap i j) : (_ : n) × Perm n)
    (Sigma.mk (β := fun (x : n) ↦ Perm n) x σ : (_ : n) × Perm n)
simp_rw₁ :
  Eq (α := (_ : n) × Perm n)
    (Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) ((swap i j : (a : n) → n) i : n))
        (σ * swap i j * swap i j) :
      (_ : n) × Perm n)
    (Sigma.mk (β := fun (x : n) ↦ Perm n) x σ : (_ : n) × Perm n)
simp_rw₂ :
  Eq (α := (_ : n) × Perm n)
    (Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) j) (σ * swap i j * swap i j) : (_ : n) × Perm n)
    (Sigma.mk (β := fun (x : n) ↦ Perm n) x σ : (_ : n) × Perm n)
simp_rw₃ :
  Eq (α := (_ : n) × Perm n) (Sigma.mk (β := fun (x : n) ↦ Perm n) x (σ * swap i j * swap i j))
    (Sigma.mk (β := fun (x : n) ↦ Perm n) x σ)
⊢ f (f (Sigma.mk (β := fun (x : n) ↦ Perm n) x σ)) = Sigma.mk (β := fun (x : n) ↦ Perm n) x σ

Tactic:
simp_rw [f, Perm.mul_apply, swap_apply_left, hp.2.2, mul_swap_mul_self]

Premises used: Equiv.mul_swap_mul_self, And.right, Equiv.Perm.mul_apply, Equiv.swap_apply_left
-- 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 : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
⊢ ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p

Tactic:
have hf {s} : ∀ p ∈ t s, f (f p) = p := by
    intro ⟨x, σ⟩ hp
    rw [mem_sigma, mem_filter, mem_ofSign] at hp
    simp_rw [f, Perm.mul_apply, swap_apply_left, hp.2.2, mul_swap_mul_self]
-- 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 : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
⊢ Eq.{u_3 + 1} (α := R)
    (∑ x ∈ Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a},
      A i (x.fst (β := fun (i : n) ↦ Perm n)) * ∏ k ∈ {j}ᶜ, A k ((x.snd (β := fun (i : n) ↦ Perm n) : (a : n) → n) k))
    (∑ x ∈ Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign (-1) | (x : (a : n) → n) j = a},
      A i (x.fst (β := fun (i : n) ↦ Perm n)) * ∏ k ∈ {j}ᶜ, A k ((x.snd (β := fun (i : n) ↦ Perm n) : (a : n) → n) k))

Tactic:
sum_bij' (fun p _ ↦ f p) (fun p _ ↦ f p) ?_ ?_ hf hf ?_

Premises used: Finset.sum_bij'
-- 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 : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x : n
σ : Perm n
hp_1 :
  Membership.mem (γ := Finset ((_ : n) × Perm n))
    (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
    (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
hp :
  Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) ∧
    Eq (α := ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
            (Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) :
          ℤˣ)
        (1 : ℤˣ) ∧
      ((Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) : Perm n) : (a : n) → n) j =
        Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
⊢ Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n)
        ((fun (p : (_ : n) × Perm n)
              (x :
                Membership.mem (γ := Finset ((_ : n) × Perm n))
                  (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
                  p) ↦
            f p)
          (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) hp_1)) ∧
    HMul.hMul (α := ℤˣ) 1 (-1) = -1 ∧
      Eq (α := n) ((σ : (a : n) → n) i : n)
        (Sigma.fst (β := fun (i : n) ↦ Perm n)
            ((fun (p : (_ : n) × Perm n)
                  (x :
                    Membership.mem (γ := Finset ((_ : n) × Perm n))
                      (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦
                        {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
                      p) ↦
                f p)
              (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) hp_1) :
          n)

Tactic:
⟨mem_univ (σ i), rfl, rfl⟩

Premises used: Finset.mem_univ, And.intro, DFunLike.coe, 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 : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x : n
σ : Perm n
hp_1 :
  Membership.mem (γ := Finset ((_ : n) × Perm n))
    (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
    (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
hp :
  Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) ∧
    Eq (α := ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
            (Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) :
          ℤˣ)
        (1 : ℤˣ) ∧
      ((Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) : Perm n) : (a : n) → n) j =
        Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
⊢ Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n)
        ((fun (p : (_ : n) × Perm n)
              (x :
                Membership.mem (γ := Finset ((_ : n) × Perm n))
                  (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
                  p) ↦
            f p)
          (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) hp_1)) ∧
    HMul.hMul (α := ℤˣ) 1 (-1) = -1 ∧
      Eq (α := n) ((σ : (a : n) → n) i : n)
        (Sigma.fst (β := fun (i : n) ↦ Perm n)
            ((fun (p : (_ : n) × Perm n)
                  (x :
                    Membership.mem (γ := Finset ((_ : n) × Perm n))
                      (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦
                        {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
                      p) ↦
                f p)
              (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) hp_1) :
          n)

Tactic:
exact ⟨mem_univ (σ i), rfl, 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 : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x : n
σ : Perm n
hp_1 :
  Membership.mem (γ := Finset ((_ : n) × Perm n))
    (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign (-1) | (x : (a : n) → n) j = a})
    (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
hp :
  Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) ∧
    Eq (α := ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
            (Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) :
          ℤˣ)
        (-1 : ℤˣ) ∧
      ((Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) : Perm n) : (a : n) → n) j =
        Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
⊢ Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n)
        ((fun (p : (_ : n) × Perm n)
              (x :
                Membership.mem (γ := Finset ((_ : n) × Perm n))
                  (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦
                    {x ∈ ofSign (-1) | (x : (a : n) → n) j = a})
                  p) ↦
            f p)
          (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) hp_1)) ∧
    HMul.hMul (α := ℤˣ) (-1) (-1) = 1 ∧
      Eq (α := n) ((σ : (a : n) → n) i : n)
        (Sigma.fst (β := fun (i : n) ↦ Perm n)
            ((fun (p : (_ : n) × Perm n)
                  (x :
                    Membership.mem (γ := Finset ((_ : n) × Perm n))
                      (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦
                        {x ∈ ofSign (-1) | (x : (a : n) → n) j = a})
                      p) ↦
                f p)
              (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) hp_1) :
          n)

Tactic:
⟨mem_univ (σ i), rfl, rfl⟩

Premises used: Finset.mem_univ, And.intro, DFunLike.coe, rfl