awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
α : Type u_4
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommRing α
ι : Type u_5
inst_3 : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
rwa :
  (A * 1 + A * (A⁻¹ * (replicateCol ι u * replicateRow ι v))).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
rwa₁ : IsUnit A.det
rwa₂ :
  (A * (1 + A⁻¹ * (replicateCol ι u * replicateRow ι v))).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
rwa₃ : IsUnit A.det
rwa₄ :
  A.det * (1 + A⁻¹ * (replicateCol ι u * replicateRow ι v)).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
rwa₅ : IsUnit A.det
rwa₆ :
  A.det * (1 + A⁻¹ * replicateCol ι u * replicateRow ι v).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
rwa₇ : IsUnit A.det
rwa₈ :
  A.det * (1 + replicateRow ι v * (A⁻¹ * replicateCol ι u)).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
rwa₉ : IsUnit A.det
⊢ (A * 1 + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
have rwa₁₀ : A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det =
  A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
Tactic: rwa [← Matrix.mul_nonsing_inv_cancel_left A (replicateCol ι u * replicateRow ι v),
    ← Matrix.mul_add, det_mul, ← Matrix.mul_assoc, det_one_add_mul_comm, ← Matrix.mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
⊢ (A + U * V).det = A.det * (1 + V * A⁻¹ * U).det
have nth_rewrite : (A * 1 + U * V).det = A.det * (1 + V * A⁻¹ * U).det
Tactic: nth_rewrite 1 [← Matrix.mul_one A]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
⊢ (A * 1 + U * V).det = A.det * (1 + V * A⁻¹ * U).det
have rwa : (A * 1 + A * (A⁻¹ * (U * V))).det = A.det * (1 + V * A⁻¹ * U).det
Tactic: rwa [← Matrix.mul_nonsing_inv_cancel_left A (U * V), ← Matrix.mul_add,
    det_mul, ← Matrix.mul_assoc, det_one_add_mul_comm, ← Matrix.mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
rwa : (A * 1 + A * (A⁻¹ * (U * V))).det = A.det * (1 + V * A⁻¹ * U).det
rwa₁ : IsUnit A.det
⊢ (A * 1 + U * V).det = A.det * (1 + V * A⁻¹ * U).det
have rwa₂ : (A * (1 + A⁻¹ * (U * V))).det = A.det * (1 + V * A⁻¹ * U).det
Tactic: rwa [← Matrix.mul_nonsing_inv_cancel_left A (U * V), ← Matrix.mul_add,
    det_mul, ← Matrix.mul_assoc, det_one_add_mul_comm, ← Matrix.mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
rwa : (A * 1 + A * (A⁻¹ * (U * V))).det = A.det * (1 + V * A⁻¹ * U).det
rwa₁ : IsUnit A.det
rwa₂ : (A * (1 + A⁻¹ * (U * V))).det = A.det * (1 + V * A⁻¹ * U).det
rwa₃ : IsUnit A.det
⊢ (A * 1 + U * V).det = A.det * (1 + V * A⁻¹ * U).det
have rwa₄ : A.det * (1 + A⁻¹ * (U * V)).det = A.det * (1 + V * A⁻¹ * U).det
Tactic: rwa [← Matrix.mul_nonsing_inv_cancel_left A (U * V), ← Matrix.mul_add,
    det_mul, ← Matrix.mul_assoc, det_one_add_mul_comm, ← Matrix.mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
rwa : (A * 1 + A * (A⁻¹ * (U * V))).det = A.det * (1 + V * A⁻¹ * U).det
rwa₁ : IsUnit A.det
rwa₂ : (A * (1 + A⁻¹ * (U * V))).det = A.det * (1 + V * A⁻¹ * U).det
rwa₃ : IsUnit A.det
rwa₄ : A.det * (1 + A⁻¹ * (U * V)).det = A.det * (1 + V * A⁻¹ * U).det
rwa₅ : IsUnit A.det
⊢ (A * 1 + U * V).det = A.det * (1 + V * A⁻¹ * U).det
have rwa₆ : A.det * (1 + A⁻¹ * U * V).det = A.det * (1 + V * A⁻¹ * U).det
Tactic: rwa [← Matrix.mul_nonsing_inv_cancel_left A (U * V), ← Matrix.mul_add,
    det_mul, ← Matrix.mul_assoc, det_one_add_mul_comm, ← Matrix.mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
rwa : (A * 1 + A * (A⁻¹ * (U * V))).det = A.det * (1 + V * A⁻¹ * U).det
rwa₁ : IsUnit A.det
rwa₂ : (A * (1 + A⁻¹ * (U * V))).det = A.det * (1 + V * A⁻¹ * U).det
rwa₃ : IsUnit A.det
rwa₄ : A.det * (1 + A⁻¹ * (U * V)).det = A.det * (1 + V * A⁻¹ * U).det
rwa₅ : IsUnit A.det
rwa₆ : A.det * (1 + A⁻¹ * U * V).det = A.det * (1 + V * A⁻¹ * U).det
rwa₇ : IsUnit A.det
⊢ (A * 1 + U * V).det = A.det * (1 + V * A⁻¹ * U).det
have rwa₈ : A.det * (1 + V * (A⁻¹ * U)).det = A.det * (1 + V * A⁻¹ * U).det
Tactic: rwa [← Matrix.mul_nonsing_inv_cancel_left A (U * V), ← Matrix.mul_add,
    det_mul, ← Matrix.mul_assoc, det_one_add_mul_comm, ← Matrix.mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
rwa : (A * 1 + A * (A⁻¹ * (U * V))).det = A.det * (1 + V * A⁻¹ * U).det
rwa₁ : IsUnit A.det
rwa₂ : (A * (1 + A⁻¹ * (U * V))).det = A.det * (1 + V * A⁻¹ * U).det
rwa₃ : IsUnit A.det
rwa₄ : A.det * (1 + A⁻¹ * (U * V)).det = A.det * (1 + V * A⁻¹ * U).det
rwa₅ : IsUnit A.det
rwa₆ : A.det * (1 + A⁻¹ * U * V).det = A.det * (1 + V * A⁻¹ * U).det
rwa₇ : IsUnit A.det
rwa₈ : A.det * (1 + V * (A⁻¹ * U)).det = A.det * (1 + V * A⁻¹ * U).det
rwa₉ : IsUnit A.det
⊢ (A * 1 + U * V).det = A.det * (1 + V * A⁻¹ * U).det
have rwa₁₀ : A.det * (1 + V * A⁻¹ * U).det = A.det * (1 + V * A⁻¹ * U).det
Tactic: rwa [← Matrix.mul_nonsing_inv_cancel_left A (U * V), ← Matrix.mul_add,
    det_mul, ← Matrix.mul_assoc, det_one_add_mul_comm, ← Matrix.mul_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
d : n → R
⊢ detp 1 (diagonal d) = ∏ i : n, d i
have rw : Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((1 : (a : n) → n) k)) (∏ i : n, d i)
Tactic: rw [detp, sum_eq_single_of_mem 1]
-- 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
d : n → R
rw : Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((1 : (a : n) → n) k)) (∏ i : n, d i)
⊢ detp 1 (diagonal d) = ∏ i : n, d i
have h : Membership.mem (γ := Finset (Perm n)) (ofSign 1) 1
Tactic: rw [detp, sum_eq_single_of_mem 1]
-- 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
d : n → R
rw : Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((1 : (a : n) → n) k)) (∏ i : n, d i)
h : Membership.mem (γ := Finset (Perm n)) (ofSign 1) 1
⊢ detp 1 (diagonal d) = ∏ i : n, d i
have h₀ : ∀ (b : Perm n),
  Membership.mem (γ := Finset (Perm n)) (ofSign 1) b →
    b ≠ 1 → Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((b : (a : n) → n) k)) 0
Tactic: rw [detp, sum_eq_single_of_mem 1]
-- 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
d : n → R
σ : Perm n
hσ1 : σ ≠ 1
⊢ Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((σ : (a : n) → n) k)) 0
have h₀ : ∀ (i : n) (hi : ¬Eq (α := n) ((σ : (a : n) → n) i : n) ((1 : (a : n) → n) i : n)),
  Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((σ : (a : n) → n) k)) 0
Tactic: obtain ⟨i, hi⟩ := not_forall.mp (mt Perm.ext_iff.mpr hσ1)
-- 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
⊢ Eq.{u_3 + 1} (α := R) (detp.{u_1, u_3} (n := n) 1 1) 1
have rw : Eq.{u_3 + 1} (α := R) (detp.{u_1, u_3} (n := n) 1 (diagonal fun (x : n) ↦ 1)) 1
Tactic: rw [← diagonal_one, detp_one_diagonal, prod_const_one]
-- 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
rw : Eq.{u_3 + 1} (α := R) (detp.{u_1, u_3} (n := n) 1 (diagonal fun (x : n) ↦ 1)) 1
⊢ Eq.{u_3 + 1} (α := R) (detp.{u_1, u_3} (n := n) 1 1) 1
have rw₁ : Eq.{u_3 + 1} (α := R) (∏ i : n, 1) 1
Tactic: rw [← diagonal_one, detp_one_diagonal, prod_const_one]
-- 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
rw : Eq.{u_3 + 1} (α := R) (detp.{u_1, u_3} (n := n) 1 (diagonal fun (x : n) ↦ 1)) 1
rw₁ : Eq.{u_3 + 1} (α := R) (∏ i : n, 1) 1
⊢ Eq.{u_3 + 1} (α := R) (detp.{u_1, u_3} (n := n) 1 1) 1
have rw₂ : Eq.{u_3 + 1} (α := R) 1 1
Tactic: rw [← diagonal_one, detp_one_diagonal, prod_const_one]
-- 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
d : n → R
⊢ detp (-1) (diagonal d) = 0
have rw : ∀ (x : Perm n),
  Membership.mem (γ := Finset (Perm n)) (ofSign (-1)) x →
    Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((x : (a : n) → n) k)) 0
Tactic: rw [detp, sum_eq_zero]
-- 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
d : n → R
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign (-1)) σ
⊢ σ ≠ 1
have contrapose : ∀ (hσ : σ = 1), σ ∉ ofSign (-1)
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
d : n → R
σ : Perm n
hσ : σ = 1
⊢ σ ∉ ofSign (-1)
have rw : ¬Eq (α := ℤˣ) 1 (-1)
Tactic: rw [hσ, mem_ofSign, sign_one]
-- 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
d : n → R
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign (-1)) σ
⊢ Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((σ : (a : n) → n) k)) 0
have hσ1 : σ ≠ 1
Tactic: have hσ1 : σ ≠ 1 := by
    contrapose hσ
    rw [hσ, mem_ofSign, sign_one]
    decide
-- 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
d : n → R
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign (-1)) σ
hσ1 : σ ≠ 1
⊢ Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((σ : (a : n) → n) k)) 0
have obtain : ∀ (i : n) (hi : ¬Eq (α := n) ((σ : (a : n) → n) i : n) ((1 : (a : n) → n) i : n)),
  Eq.{u_3 + 1} (α := R) (∏ k : n, diagonal d k ((σ : (a : n) → n) k)) 0
Tactic: obtain ⟨i, hi⟩ := not_forall.mp (mt Perm.ext_iff.mpr hσ1)
-- 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
⊢ Eq.{u_3 + 1} (α := R) (detp.{u_1, u_3} (n := n) (-1) 1) 0
have rw : Eq.{u_3 + 1} (α := R) (detp.{u_1, u_3} (n := n) (-1) (diagonal fun (x : n) ↦ 1)) 0
Tactic: rw [← diagonal_one, detp_neg_one_diagonal]
-- 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
rw : Eq.{u_3 + 1} (α := R) (detp.{u_1, u_3} (n := n) (-1) (diagonal fun (x : n) ↦ 1)) 0
⊢ Eq.{u_3 + 1} (α := R) (detp.{u_1, u_3} (n := n) (-1) 1) 0
have rw₁ : Eq.{u_3 + 1} (α := R) 0 0
Tactic: rw [← diagonal_one, detp_neg_one_diagonal]
-- 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
s t : ℤˣ
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ
⊢ ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
have h : ∀ (τ : Perm n),
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔ τ ∈ Finset.map (mulRightEmbedding σ) (ofSign t)
Tactic: ext τ
-- 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
s t : ℤˣ
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ
τ : Perm n
⊢ Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔ τ ∈ Finset.map (mulRightEmbedding σ) (ofSign t)
have h : Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
  ∃ (a : Perm n),
    Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ (mulRightEmbedding σ : (a : Perm n) → Perm n) a = τ
Tactic: simp_rw [mem_map, mulRightEmbedding_apply, ← eq_mul_inv_iff_mul_eq, exists_eq_right,
      mem_ofSign, map_mul, map_inv, mul_inv_eq_iff_eq_mul, mem_ofSign.mp hσ]
-- 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
s t : ℤˣ
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ
τ : Perm n
h :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n),
      Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ (mulRightEmbedding σ : (a : Perm n) → Perm n) a = τ
⊢ Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔ τ ∈ Finset.map (mulRightEmbedding σ) (ofSign t)
have h₁ : Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
  ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ a * σ = τ
Tactic: simp_rw [mem_map, mulRightEmbedding_apply, ← eq_mul_inv_iff_mul_eq, exists_eq_right,
      mem_ofSign, map_mul, map_inv, mul_inv_eq_iff_eq_mul, mem_ofSign.mp hσ]
-- 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
s t : ℤˣ
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ
τ : Perm n
h :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n),
      Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ (mulRightEmbedding σ : (a : Perm n) → Perm n) a = τ
h₁ :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ a * σ = τ
⊢ Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔ τ ∈ Finset.map (mulRightEmbedding σ) (ofSign t)
have h₂ : Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
  ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ a = τ * σ⁻¹
Tactic: simp_rw [mem_map, mulRightEmbedding_apply, ← eq_mul_inv_iff_mul_eq, exists_eq_right,
      mem_ofSign, map_mul, map_inv, mul_inv_eq_iff_eq_mul, mem_ofSign.mp hσ]
-- 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
s t : ℤˣ
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ
τ : Perm n
h :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n),
      Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ (mulRightEmbedding σ : (a : Perm n) → Perm n) a = τ
h₁ :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ a * σ = τ
h₂ :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ a = τ * σ⁻¹
⊢ Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔ τ ∈ Finset.map (mulRightEmbedding σ) (ofSign t)
have h₃ : Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔ Membership.mem (γ := Finset (Perm n)) (ofSign t) (τ * σ⁻¹)
Tactic: simp_rw [mem_map, mulRightEmbedding_apply, ← eq_mul_inv_iff_mul_eq, exists_eq_right,
      mem_ofSign, map_mul, map_inv, mul_inv_eq_iff_eq_mul, mem_ofSign.mp hσ]
-- 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
s t : ℤˣ
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ
τ : Perm n
h :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n),
      Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ (mulRightEmbedding σ : (a : Perm n) → Perm n) a = τ
h₁ :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ a * σ = τ
h₂ :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ a = τ * σ⁻¹
h₃ :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔ Membership.mem (γ := Finset (Perm n)) (ofSign t) (τ * σ⁻¹)
⊢ Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔ τ ∈ Finset.map (mulRightEmbedding σ) (ofSign t)
have h₄ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t * s ↔ ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹) = t
Tactic: simp_rw [mem_map, mulRightEmbedding_apply, ← eq_mul_inv_iff_mul_eq, exists_eq_right,
      mem_ofSign, map_mul, map_inv, mul_inv_eq_iff_eq_mul, mem_ofSign.mp hσ]
-- 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
s t : ℤˣ
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ
τ : Perm n
h :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n),
      Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ (mulRightEmbedding σ : (a : Perm n) → Perm n) a = τ
h₁ :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ a * σ = τ
h₂ :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ a = τ * σ⁻¹
h₃ :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔ Membership.mem (γ := Finset (Perm n)) (ofSign t) (τ * σ⁻¹)
h₄ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t * s ↔ ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹) = t
⊢ Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔ τ ∈ Finset.map (mulRightEmbedding σ) (ofSign t)
have h₅ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t * s ↔
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ : ℤˣ)
      (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ⁻¹ : ℤˣ) =
    t
Tactic: simp_rw [mem_map, mulRightEmbedding_apply, ← eq_mul_inv_iff_mul_eq, exists_eq_right,
      mem_ofSign, map_mul, map_inv, mul_inv_eq_iff_eq_mul, mem_ofSign.mp hσ]
-- 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
s t : ℤˣ
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ
τ : Perm n
h :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n),
      Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ (mulRightEmbedding σ : (a : Perm n) → Perm n) a = τ
h₁ :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ a * σ = τ
h₂ :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ a = τ * σ⁻¹
h₃ :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔ Membership.mem (γ := Finset (Perm n)) (ofSign t) (τ * σ⁻¹)
h₄ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t * s ↔ ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹) = t
h₅ :
  ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t * s ↔
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ : ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ⁻¹ : ℤˣ) =
      t
⊢ Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔ τ ∈ Finset.map (mulRightEmbedding σ) (ofSign t)
have h₆ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t * s ↔
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ : ℤˣ)
      ((((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ)⁻¹ : ℤˣ) =
    t
Tactic: simp_rw [mem_map, mulRightEmbedding_apply, ← eq_mul_inv_iff_mul_eq, exists_eq_right,
      mem_ofSign, map_mul, map_inv, mul_inv_eq_iff_eq_mul, mem_ofSign.mp hσ]
-- 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
s t : ℤˣ
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ
τ : Perm n
h :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n),
      Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ (mulRightEmbedding σ : (a : Perm n) → Perm n) a = τ
h₁ :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ a * σ = τ
h₂ :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔
    ∃ (a : Perm n), Membership.mem (γ := Finset (Perm n)) (ofSign t) a ∧ a = τ * σ⁻¹
h₃ :
  Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔ Membership.mem (γ := Finset (Perm n)) (ofSign t) (τ * σ⁻¹)
h₄ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t * s ↔ ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹) = t
h₅ :
  ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t * s ↔
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ : ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ⁻¹ : ℤˣ) =
      t
h₆ :
  ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t * s ↔
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ : ℤˣ)
        ((((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ)⁻¹ : ℤˣ) =
      t
⊢ Membership.mem (γ := Finset (Perm n)) (ofSign (t * s)) τ ↔ τ ∈ Finset.map (mulRightEmbedding σ) (ofSign t)
have h₇ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t * s ↔
  ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ =
    HMul.hMul (β := ℤˣ) t (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)
Tactic: simp_rw [mem_map, mulRightEmbedding_apply, ← eq_mul_inv_iff_mul_eq, exists_eq_right,
      mem_ofSign, map_mul, map_inv, mul_inv_eq_iff_eq_mul, mem_ofSign.mp hσ]
-- 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
⊢ 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 hf : ∀ {s t : ℤˣ} {σ : Perm n} (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ),
  ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
Tactic: have hf {s t} {σ : Perm n} (hσ : σ ∈ ofSign s) :
      ofSign (t * s) = (ofSign t).map (mulRightEmbedding σ) := by
    ext τ
    simp_rw [mem_map, mulRightEmbedding_apply, ← eq_mul_inv_iff_mul_eq, exists_eq_right,
      mem_ofSign, map_mul, map_inv, mul_inv_eq_iff_eq_mul, mem_ofSign.mp hσ]