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)
ι : 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
⊢ σ (if k = i then j else if k = j then i else k) = σ k
have neg : ∀ (h : ¬k = i) (h : ¬k = j), σ k = σ k
Tactic: split_ifs with h h
-- 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σ_1 : ¬Function.Injective σ
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))
have hσ₁ : ∀ (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]
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σ_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) (∑ τ ∈ 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 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))
Tactic: rw [← mul_neg_one, hf (mem_ofSign.mpr (sign_swap hij)), sum_map]
-- 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
hij : i ≠ j
hσ : ∀ (k : n), σ ((swap i j : (a : n) → n) k) = σ k
⊢ 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))
have 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))))
Tactic: simp_rw [prod_mul_distrib, mulRightEmbedding_apply, Perm.mul_apply]
-- 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
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))))
have 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)))
Tactic: refine sum_congr rfl fun τ hτ ↦ congr_arg (_ * ·) ?_
-- 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
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) (∏ x : n, B (σ x) ((τ : (a : n) → n) x))
    (∏ x : n, B (σ x) ((τ : (a : n) → n) ((swap i j : (a : n) → n) x : n)))
have 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)))
Tactic: rw [← Equiv.prod_comp (swap i j)]
-- 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
s : ℤˣ
A : Matrix n n R
i : n
⊢ (A * adjp s A) i i = detp s A
have 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))
Tactic: have key := sum_fiberwise_eq_sum_filter (ofSign s) univ (· i) fun σ ↦ ∏ k, A k (σ k)
-- 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
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))
⊢ (A * adjp s A) i i = detp s A
have 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))
Tactic: simp_rw [mem_univ, filter_true] at key
Cleared hypotheses: key
-- 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
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))
⊢ (A * adjp s A) i i = detp s A
have 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))
Tactic: simp_rw [mul_apply, adjp_apply, mul_sum, detp, ← key]
-- 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
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))
have 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)
Tactic: refine sum_congr rfl fun x hx ↦ 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
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}) σ
⊢ A i x * ∏ k ∈ {i}ᶜ, A k ((σ : (a : n) → n) k) = ∏ k : n, A k ((σ : (a : n) → n) k)
have 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))
Tactic: rw [← prod_mul_prod_compl ({i} : Finset n), prod_singleton, (mem_filter.mp hσ).2]
-- 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
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))
⊢ A i x * ∏ k ∈ {i}ᶜ, A k ((σ : (a : n) → n) k) = ∏ k : n, A k ((σ : (a : n) → n) k)
have 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)
Tactic: rw [← prod_mul_prod_compl ({i} : Finset n), prod_singleton, (mem_filter.mp hσ).2]
-- 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
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)
⊢ A i x * ∏ k ∈ {i}ᶜ, A k ((σ : (a : n) → n) k) = ∏ k : n, A k ((σ : (a : n) → n) k)
have rw₂ : A i x * ∏ k ∈ {i}ᶜ, A k ((σ : (a : n) → n) k) = A i x * ∏ i ∈ {i}ᶜ, A i ((σ : (a : n) → n) i)
Tactic: rw [← prod_mul_prod_compl ({i} : Finset n), prod_singleton, (mem_filter.mp hσ).2]
-- 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 : Matrix n n R
i j : n
h : i ≠ j
⊢ (A * adjp 1 A) i j = (A * adjp (-1) A) i j
have 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))
Tactic: simp_rw [mul_apply, adjp_apply, mul_sum, sum_sigma']
-- 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 : 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
⊢ f (f (Sigma.mk (β := fun (x : n) ↦ Perm n) x σ)) = Sigma.mk (β := fun (x : n) ↦ Perm n) x σ
have 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 σ)
Tactic: rw [mem_sigma, mem_filter, mem_ofSign] at hp
Cleared hypotheses: hp
-- 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 : 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)
⊢ f (f (Sigma.mk (β := fun (x : n) ↦ Perm n) x σ)) = Sigma.mk (β := fun (x : n) ↦ Perm n) x σ
have 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)
Tactic: simp_rw [f, Perm.mul_apply, swap_apply_left, hp.2.2, mul_swap_mul_self]
-- 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 : 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)
⊢ f (f (Sigma.mk (β := fun (x : n) ↦ Perm n) x σ)) = Sigma.mk (β := fun (x : n) ↦ Perm n) x σ
have 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)
Tactic: simp_rw [f, Perm.mul_apply, swap_apply_left, hp.2.2, mul_swap_mul_self]
-- 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 : 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)
⊢ f (f (Sigma.mk (β := fun (x : n) ↦ Perm n) x σ)) = Sigma.mk (β := fun (x : n) ↦ Perm n) x σ
have 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 σ)
Tactic: simp_rw [f, Perm.mul_apply, swap_apply_left, hp.2.2, mul_swap_mul_self]
-- 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 : 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}
⊢ 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))
have hf : ∀ {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]