awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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)
have 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)))
Tactic: simp_rw [detp, sum_mul_sum, prod_mul_distrib]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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)))
have 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)))
Tactic: refine sum_congr rfl fun σ hσ ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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 * 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)))
have 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))))
Tactic: simp_rw [hf hσ, sum_map, mulRightEmbedding_apply, Perm.mul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (hypothesis)
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)
⊢ 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)
have 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)
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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (hypothesis)
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' := ⋯ }
⊢ 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)
have hι : ∀ {σ : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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)
have 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))
Tactic: simp_rw [h, neg_mul_neg, mul_one, detp, mul_apply, prod_univ_sum, Fintype.piFinset_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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 : ℤˣ
⊢ ∑ 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))
have 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))
Tactic: rw [sum_comm, ← sum_compl_add_sum bij, sum_map, sum_disjUnion]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (hypothesis)
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)) ⋯)
⊢ 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)
have 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)
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ι]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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)
⊢ 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)
have 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 [h, h, neg_neg, add_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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)
have 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))
Tactic: rw [add_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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)
have 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))
Tactic: conv_rhs => rw [add_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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))
have 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))
Tactic: refine congr_arg₂ (· + ·) (sum_congr rfl fun σ hσ ↦ ?_) (add_comm _ _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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 σ
have contrapose : ∀ (hσ : Function.Injective σ), σ ∉ bijᶜ
Tactic: contrapose hσ
Cleared hypotheses: hσ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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 σ
⊢ σ ∉ bijᶜ
have rw : ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) univ a ∧ (ι : (a : Perm n) → n → n) a = σ
Tactic: rw [notMem_compl, mem_map, ofSign_disjUnion]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (hypothesis)
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ᶜ
⊢ 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))
have hσ₁ : ¬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⟩
Cleared hypotheses: hσ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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 σ
⊢ 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))
have 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))
Tactic: obtain ⟨i, j, hσ, hij⟩ := Function.not_injective_iff.mp hσ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
have rw : σ (if k = i then j else if k = j then i else k) = σ k
Tactic: rw [swap_apply_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
⊢ σ (if k = i then j else if k = j then i else k) = σ k
have pos : ∀ (h : k = i), σ j = σ k
Tactic: split_ifs with h h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
⊢ σ (if k = i then j else if k = j then i else k) = σ k
have pos₁ : ∀ (h : ¬k = i) (h : k = j), σ i = σ k
Tactic: split_ifs with h h