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

Tactic:
exact ⟨mem_univ (σ i), rfl, rfl⟩
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x : n
σ : Perm n
hp :
  Membership.mem (γ := Finset ((_ : n) × Perm n))
    (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
    (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
⊢ Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) ∧
    Eq (α := ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
            (Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) :
          ℤˣ)
        (1 : ℤˣ) ∧
      ((Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) : Perm n) : (a : n) → n) j =
        Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)

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

Premises used: Finset.mem_sigma, Equiv.Perm.mem_ofSign, Finset.mem_filter
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x : n
σ : Perm n
hp_1 :
  Membership.mem (γ := Finset ((_ : n) × Perm n))
    (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
    (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
hp :
  Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) ∧
    Eq (α := ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
            (Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) :
          ℤˣ)
        (1 : ℤˣ) ∧
      ((Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) : Perm n) : (a : n) → n) j =
        Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
⊢ _root_.Disjoint (α := Finset n) {i} {i, j}ᶜ

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x : n
σ : Perm n
hp_1 :
  Membership.mem (γ := Finset ((_ : n) × Perm n))
    (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
    (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
hp :
  Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) ∧
    Eq (α := ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
            (Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) :
          ℤˣ)
        (1 : ℤˣ) ∧
      ((Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) : Perm n) : (a : n) → n) j =
        Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
rw : Membership.mem (γ := Finset n) {j}ᶜ i
⊢ Eq (α := Finset n) {j}ᶜ (disjUnion {i} {i, j}ᶜ ⋯)

Tactic:
rw [singleton_disjUnion, cons_eq_insert, compl_insert, insert_erase]

Premises used: Finset.singleton_disjUnion, Finset.compl_insert, Finset.cons_eq_insert, Finset.insert_erase
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x : n
σ : Perm n
hp_1 :
  Membership.mem (γ := Finset ((_ : n) × Perm n))
    (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
    (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
hp :
  Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) ∧
    Eq (α := ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
            (Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) :
          ℤˣ)
        (1 : ℤˣ) ∧
      ((Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) : Perm n) : (a : n) → n) j =
        Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
rwa : i ∉ {j}
rwa₁ rwa₂ rwa₃ rwa₄ : ¬i = j
⊢ Membership.mem (γ := Finset n) {j}ᶜ i

Tactic:
rwa [mem_compl, mem_singleton]

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

Tactic:
have key : ({j}ᶜ : Finset n) = disjUnion ({i} : Finset n) ({i, j} : Finset n)ᶜ (by simp) := by
      rw [singleton_disjUnion, cons_eq_insert, compl_insert, insert_erase]
      rwa [mem_compl, mem_singleton]
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x : n
σ : Perm n
hp_1 :
  Membership.mem (γ := Finset ((_ : n) × Perm n))
    (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
    (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
hp :
  Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) ∧
    Eq (α := ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
            (Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) :
          ℤˣ)
        (1 : ℤˣ) ∧
      ((Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) : Perm n) : (a : n) → n) j =
        Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
key : Eq (α := Finset n) {j}ᶜ (disjUnion {i} {i, j}ᶜ ⋯)
refine_3 :
  A i x * A i ((σ : (a : n) → n) i) * ∏ x ∈ {i, j}ᶜ, A x ((σ : (a : n) → n) x) =
    A i ((σ : (a : n) → n) i) * A i ((σ : (a : n) → n) j) *
      ∏ x ∈ {i, j}ᶜ, A x ((σ : (a : n) → n) ((swap i j : (a : n) → n) x : n))
⊢ A i (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) *
      ∏ k ∈ {j}ᶜ,
        A k
          (((Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) : Perm n) : (a : n) → n)
            k) =
    A i
        (Sigma.fst (β := fun (i : n) ↦ Perm n)
          ((fun (p : (_ : n) × Perm n)
                (x :
                  Membership.mem (γ := Finset ((_ : n) × Perm n))
                    (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦
                      {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
                    p) ↦
              f p)
            (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) hp_1)) *
      ∏ k ∈ {j}ᶜ,
        A k
          (((Sigma.snd (β := fun (i : n) ↦ Perm n)
                  ((fun (p : (_ : n) × Perm n)
                        (x :
                          Membership.mem (γ := Finset ((_ : n) × Perm n))
                            (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦
                              {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
                            p) ↦
                      f p)
                    (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) hp_1) :
                Perm n) :
              (a : n) → n)
            k)

Tactic:
simp_rw [key, prod_disjUnion, prod_singleton, f, Perm.mul_apply, swap_apply_left, ← mul_assoc]

Premises used: Finset.prod_singleton, mul_assoc, Finset.prod_disjUnion, Equiv.Perm.mul_apply, Equiv.swap_apply_left
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x : n
σ : Perm n
hp_1 :
  Membership.mem (γ := Finset ((_ : n) × Perm n))
    (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
    (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
hp :
  Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) ∧
    Eq (α := ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
            (Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) :
          ℤˣ)
        (1 : ℤˣ) ∧
      ((Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) : Perm n) : (a : n) → n) j =
        Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
key : Eq (α := Finset n) {j}ᶜ (disjUnion {i} {i, j}ᶜ ⋯)
refine_3 :
  A i ((σ : (a : n) → n) i) * A i x * ∏ x ∈ {i, j}ᶜ, A x ((σ : (a : n) → n) x) =
    A i ((σ : (a : n) → n) i) * A i (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) *
      ∏ x ∈ {i, j}ᶜ, A x ((σ : (a : n) → n) ((swap i j : (a : n) → n) x : n))
⊢ A i x * A i ((σ : (a : n) → n) i) * ∏ x ∈ {i, j}ᶜ, A x ((σ : (a : n) → n) x) =
    A i ((σ : (a : n) → n) i) * A i ((σ : (a : n) → n) j) *
      ∏ x ∈ {i, j}ᶜ, A x ((σ : (a : n) → n) ((swap i j : (a : n) → n) x : n))

Tactic:
rw [mul_comm (A i x) (A i (σ i)), hp.2.2]

Premises used: And.right, mul_comm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x : n
σ : Perm n
hp_1 :
  Membership.mem (γ := Finset ((_ : n) × Perm n))
    (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
    (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
hp :
  Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) ∧
    Eq (α := ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
            (Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) :
          ℤˣ)
        (1 : ℤˣ) ∧
      ((Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) : Perm n) : (a : n) → n) j =
        Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
key : Eq (α := Finset n) {j}ᶜ (disjUnion {i} {i, j}ᶜ ⋯)
⊢ A i ((σ : (a : n) → n) i) * A i x * ∏ x ∈ {i, j}ᶜ, A x ((σ : (a : n) → n) x) =
    A i ((σ : (a : n) → n) i) * A i (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) *
      ∏ x ∈ {i, j}ᶜ, A x ((σ : (a : n) → n) ((swap i j : (a : n) → n) x : n))

Tactic:
congr_arg _ (prod_congr rfl fun x hx ↦ ?_)

Premises used: Finset.prod_congr, congr_arg, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x : n
σ : Perm n
hp_1 :
  Membership.mem (γ := Finset ((_ : n) × Perm n))
    (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
    (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
hp :
  Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) ∧
    Eq (α := ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
            (Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) :
          ℤˣ)
        (1 : ℤˣ) ∧
      ((Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ) : Perm n) : (a : n) → n) j =
        Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)
key : Eq (α := Finset n) {j}ᶜ (disjUnion {i} {i, j}ᶜ ⋯)
refine_3 :
  ∀ (x : n) (hx : Membership.mem (γ := Finset n) {i, j}ᶜ x),
    A x ((σ : (a : n) → n) x) = A x ((σ : (a : n) → n) ((swap i j : (a : n) → n) x : n))
⊢ A i ((σ : (a : n) → n) i) * A i x * ∏ x ∈ {i, j}ᶜ, A x ((σ : (a : n) → n) x) =
    A i ((σ : (a : n) → n) i) * A i (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x σ)) *
      ∏ x ∈ {i, j}ᶜ, A x ((σ : (a : n) → n) ((swap i j : (a : n) → n) x : n))

Tactic:
refine congr_arg _ (prod_congr rfl fun x hx ↦ ?_)

Premises used: Finset.prod_congr, congr_arg, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x_1 : n
σ : Perm n
hp_1 :
  Membership.mem (γ := Finset ((_ : n) × Perm n))
    (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
    (Sigma.mk (β := fun (i : n) ↦ Perm n) x_1 σ)
hp :
  Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x_1 σ)) ∧
    Eq (α := ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
            (Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x_1 σ)) :
          ℤˣ)
        (1 : ℤˣ) ∧
      ((Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x_1 σ) : Perm n) : (a : n) → n) j =
        Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x_1 σ)
key : Eq (α := Finset n) {j}ᶜ (disjUnion {i} {i, j}ᶜ ⋯)
x : n
hx : Membership.mem (γ := Finset n) {i, j}ᶜ x
⊢ ¬x = i ∧ ¬x = j

Tactic:
rw [mem_compl, mem_insert, mem_singleton, not_or] at hx

Premises used: Finset.mem_singleton, Finset.mem_insert, Finset.mem_compl, not_or
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x_1 : n
σ : Perm n
hp_1 :
  Membership.mem (γ := Finset ((_ : n) × Perm n))
    (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
    (Sigma.mk (β := fun (i : n) ↦ Perm n) x_1 σ)
hp :
  Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x_1 σ)) ∧
    Eq (α := ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
            (Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x_1 σ)) :
          ℤˣ)
        (1 : ℤˣ) ∧
      ((Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x_1 σ) : Perm n) : (a : n) → n) j =
        Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x_1 σ)
key : Eq (α := Finset n) {j}ᶜ (disjUnion {i} {i, j}ᶜ ⋯)
x : n
hx : ¬x = i ∧ ¬x = j
refine_3 refine_3₁ : A x ((σ : (a : n) → n) x) = A x ((σ : (a : n) → n) x)
⊢ A x ((σ : (a : n) → n) x) = A x ((σ : (a : n) → n) ((swap i j : (a : n) → n) x : n))

Tactic:
rw [swap_apply_of_ne_of_ne hx.1 hx.2]

Premises used: Equiv.swap_apply_of_ne_of_ne, And.right, And.left
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A : Matrix n n R
a :
  ∀ (i j : n),
    (A * adjp 1 A + HSMul.hSMul (β := Matrix n n R) (detp (-1) A) 1) i j =
      (A * adjp (-1) A + HSMul.hSMul (β := Matrix n n R) (detp 1 A) 1) i j
⊢ A * adjp 1 A + HSMul.hSMul (β := Matrix n n R) (detp (-1) A) 1 =
    A * adjp (-1) A + HSMul.hSMul (β := Matrix n n R) (detp 1 A) 1

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A : Matrix n n R
i j : n
a :
  (A * adjp 1 A + HSMul.hSMul (β := Matrix n n R) (detp (-1) A) 1) i i =
    (A * adjp (-1) A + HSMul.hSMul (β := Matrix n n R) (detp 1 A) 1) i i
a₁ :
  ∀ (h : i ≠ j),
    (A * adjp 1 A + HSMul.hSMul (β := Matrix n n R) (detp (-1) A) 1) i j =
      (A * adjp (-1) A + HSMul.hSMul (β := Matrix n n R) (detp 1 A) 1) i j
⊢ (A * adjp 1 A + HSMul.hSMul (β := Matrix n n R) (detp (-1) A) 1) i j =
    (A * adjp (-1) A + HSMul.hSMul (β := Matrix n n R) (detp 1 A) 1) i j

Tactic:
rcases eq_or_ne i j with rfl | h

Premises used: eq_or_ne, rfl