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)
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 : ℤˣ),
    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:
replace h (s) : detp s (A * B) =
      ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i : n, A i (σ i) * B (σ i) (τ i) +
        (detp 1 A * detp s B + detp (-1) A * detp (-s) B) := by
    simp_rw [h, neg_mul_neg, mul_one, detp, mul_apply, prod_univ_sum, Fintype.piFinset_univ]
    rw [sum_comm, ← sum_compl_add_sum bij, sum_map, sum_disjUnion]
    simp_rw [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)
ι : 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)
rw :
  ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign 1, ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i) +
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B)) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign (-1), ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i) +
        (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) +
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)
⊢ detp 1 (A * B) + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) =
    detp (-1) (A * B) + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)

Tactic:
rw [h, h, neg_neg, add_assoc]

Premises used: add_assoc, neg_neg
-- 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)
rw :
  ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign (-1), ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i) +
    (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B))
| ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign (-1), ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i) +
      (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) +
    (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)

Tactic:
rw [add_assoc]

Premises used: add_assoc
-- 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)
conv_rhs :
  ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign 1, ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i) +
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B)) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign (-1), ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i) +
      (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B))
⊢ ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign 1, ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i) +
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B)) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign (-1), ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i) +
        (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) +
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)

Tactic:
conv_rhs => rw [add_assoc]

Premises used: add_assoc
-- 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)
⊢ ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign 1, ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i) +
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B)) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign (-1), ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i) +
      (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B))

Tactic:
congr_arg₂ (· + ·) (sum_congr rfl fun σ hσ ↦ ?_) (add_comm _ _)

Premises used: add_comm, HAdd.hAdd, Finset.sum_congr, rfl, congr_arg₂
-- 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)
refine :
  ∀ (σ : n → n) (hσ : σ ∈ bijᶜ),
    Eq.{u_3 + 1} (α := R) (∑ τ ∈ ofSign 1, ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i))
      (∑ τ ∈ ofSign (-1), ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i))
⊢ ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign 1, ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i) +
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B)) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign (-1), ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i) +
      (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B))

Tactic:
refine congr_arg₂ (· + ·) (sum_congr rfl fun σ hσ ↦ ?_) (add_comm _ _)

Premises used: add_comm, HAdd.hAdd, Finset.sum_congr, rfl, congr_arg₂
-- 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σ : σ ∈ bijᶜ
contrapose : ∀ (hσ : Function.Injective σ), σ ∉ bijᶜ
⊢ ¬Function.Injective σ

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
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σ : Function.Injective σ
rw : ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) univ a ∧ (ι : (a : Perm n) → n → n) a = σ
⊢ σ ∉ bijᶜ

Tactic:
rw [notMem_compl, mem_map, ofSign_disjUnion]

Premises used: Finset.mem_map, Equiv.Perm.ofSign_disjUnion, Finset.notMem_compl
-- 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σ : Function.Injective σ
⊢ ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) univ a ∧ (ι : (a : Perm n) → n → n) a = σ

Tactic:
⟨Equiv.ofBijective σ hσ.bijective_of_finite, mem_univ _, rfl⟩

Premises used: Finset.mem_univ, Function.Injective.bijective_of_finite, And.intro, Equiv.ofBijective, Exists.intro, 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σ : Function.Injective σ
⊢ ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) univ a ∧ (ι : (a : Perm n) → n → n) a = σ

Tactic:
exact ⟨Equiv.ofBijective σ hσ.bijective_of_finite, mem_univ _, 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σ : σ ∈ bijᶜ
⊢ ¬Function.Injective σ

Tactic:
replace hσ : ¬ Function.Injective σ := by
    contrapose hσ
    rw [notMem_compl, mem_map, ofSign_disjUnion]
    exact ⟨Equiv.ofBijective σ hσ.bijective_of_finite, mem_univ _, 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σ : ¬Function.Injective σ
obtain :
  ∀ (i j : n) (hσ : σ i = σ j) (hij : i ≠ j),
    Eq.{u_3 + 1} (α := R) (∑ τ ∈ ofSign 1, ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i))
      (∑ τ ∈ ofSign (-1), ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i))
⊢ Eq.{u_3 + 1} (α := R) (∑ τ ∈ ofSign 1, ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i))
    (∑ τ ∈ ofSign (-1), ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i))

Tactic:
obtain ⟨i, j, hσ, hij⟩ := Function.not_injective_iff.mp hσ

Premises used: Iff.mp, Function.not_injective_iff
-- 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
hσ : σ i = σ j
hij : i ≠ j
k : n
rw : σ (if k = i then j else if k = j then i else k) = σ k
⊢ σ ((swap i j : (a : n) → n) k) = σ k

Tactic:
rw [swap_apply_def]

Premises used: Equiv.swap_apply_def
-- 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
hσ : σ i = σ j
hij : i ≠ j
k : n
pos : ∀ (h : k = i), σ j = σ k
pos₁ : ∀ (h : ¬k = i) (h : k = j), σ i = σ k
neg : ∀ (h : ¬k = i) (h : ¬k = j), σ k = σ k
⊢ σ (if k = i then j else if k = j then i else k) = σ k

Tactic:
split_ifs with h 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)
ι : 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_1 :
  ∀ (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
hσ : σ i = σ j
hij : i ≠ j
k : n
h : k = i
⊢ σ j = σ k

Tactic:
simp only [hσ, 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)
ι : 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_1 :
  ∀ (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
hσ : σ i = σ j
hij : i ≠ j
k : n
h_2 : ¬k = i
h : k = j
⊢ σ i = σ k

Tactic:
simp only [hσ, 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)
ι : 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_1 :
  ∀ (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
hσ : σ i = σ j
hij : i ≠ j
k : n
h_2 : ¬k = i
h : ¬k = j
⊢ σ k = σ k

Tactic:
simp only [hσ, 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)
ι : 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
hσ : σ i = σ j
hij : i ≠ j
⊢ ∀ (k : n), σ ((swap i j : (a : n) → n) k) = σ k

Tactic:
replace hσ k : σ (swap i j k) = σ k := by
    rw [swap_apply_def]
    split_ifs with h h <;> simp only [hσ, 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)
ι : 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
rw :
  Eq.{u_3 + 1} (α := R) (∑ τ ∈ ofSign 1, ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i))
    (∑ x ∈ ofSign 1,
      ∏ i_1 : n,
        A i_1 (σ i_1) *
          B (σ i_1) ((((mulRightEmbedding (swap i j) : (a : Perm n) → Perm n) x : Perm n) : (a : n) → n) i_1))
⊢ Eq.{u_3 + 1} (α := R) (∑ τ ∈ ofSign 1, ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i))
    (∑ τ ∈ ofSign (-1), ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i))

Tactic:
rw [← mul_neg_one, hf (mem_ofSign.mpr (sign_swap hij)), sum_map]

Premises used: Iff.mpr, Finset.sum_map, Equiv.Perm.mem_ofSign, mul_neg_one, Equiv.Perm.sign_swap
-- 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
simp_rw :
  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))))
⊢ Eq.{u_3 + 1} (α := R) (∑ τ ∈ ofSign 1, ∏ i : n, A i (σ i) * B (σ i) ((τ : (a : n) → n) i))
    (∑ x ∈ ofSign 1,
      ∏ i_1 : n,
        A i_1 (σ i_1) *
          B (σ i_1) ((((mulRightEmbedding (swap i j) : (a : Perm n) → Perm n) x : Perm n) : (a : n) → n) i_1))

Tactic:
simp_rw [prod_mul_distrib, mulRightEmbedding_apply, Perm.mul_apply]

Premises used: Finset.prod_mul_distrib, mulRightEmbedding_apply, Equiv.Perm.mul_apply