-- Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean
theorem mul_adjp_apply_ne (h : i ≠ j) : (A * adjp 1 A) i j = (A * adjp (-1) A) i j

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun x =>
    match x with
    | ⟨x, σ⟩ => ⟨σ i, σ * swap i j⟩
t : ℤˣ → Finset ((_ : n) × Perm n) := fun s => univ.sigma fun x => filter (fun σ => σ j = x) (ofSign s)
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x : n
σ : Perm n
hp✝ : ⟨x, σ⟩ ∈ univ.sigma fun a => filter (fun x => x j = a) (ofSign 1)
hp : ⟨x, σ⟩.fst ∈ univ ∧ sign ⟨x, σ⟩.snd = 1 ∧ ⟨x, σ⟩.snd j = ⟨x, σ⟩.fst
⊢ {j}ᶜ = {i}.disjUnion {i, j}ᶜ ⋯

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

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun x =>
    match x with
    | ⟨x, σ⟩ => ⟨σ i, σ * swap i j⟩
t : ℤˣ → Finset ((_ : n) × Perm n) := fun s => univ.sigma fun x => filter (fun σ => σ j = x) (ofSign s)
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x : n
σ : Perm n
hp✝ : ⟨x, σ⟩ ∈ univ.sigma fun a => filter (fun x => x j = a) (ofSign 1)
hp : ⟨x, σ⟩.fst ∈ univ ∧ sign ⟨x, σ⟩.snd = 1 ∧ ⟨x, σ⟩.snd j = ⟨x, σ⟩.fst
⊢ i ∈ {j}ᶜ

Proof state:
case refine_2
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun x =>
    match x with
    | ⟨x, σ⟩ => ⟨σ i, σ * swap i j⟩
t : ℤˣ → Finset ((_ : n) × Perm n) := fun s => univ.sigma fun x => filter (fun σ => σ j = x) (ofSign s)
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x : n
σ : Perm n
hp✝ : ⟨x, σ⟩ ∈ univ.sigma fun a => filter (fun x => x j = a) (ofSign (-1))
hp : ⟨x, σ⟩.fst ∈ univ ∧ sign ⟨x, σ⟩.snd = -1 ∧ ⟨x, σ⟩.snd j = ⟨x, σ⟩.fst
⊢ ((fun p x => f p) ⟨x, σ⟩ hp✝).fst ∈ univ ∧ -1 * -1 = 1 ∧ σ i = ((fun p x => f p) ⟨x, σ⟩ hp✝).fst

Tactic:
exact ⟨mem_univ (σ i), rfl, rfl⟩

Result:
no goals

Proof state:
case refine_3
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun x =>
    match x with
    | ⟨x, σ⟩ => ⟨σ i, σ * swap i j⟩
t : ℤˣ → Finset ((_ : n) × Perm n) := fun s => univ.sigma fun x => filter (fun σ => σ j = x) (ofSign s)
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x✝ : n
σ : Perm n
hp✝ : ⟨x✝, σ⟩ ∈ univ.sigma fun a => filter (fun x => x j = a) (ofSign 1)
hp : ⟨x✝, σ⟩.fst ∈ univ ∧ sign ⟨x✝, σ⟩.snd = 1 ∧ ⟨x✝, σ⟩.snd j = ⟨x✝, σ⟩.fst
key : {j}ᶜ = {i}.disjUnion {i, j}ᶜ ⋯
x : n
hx : ¬x = i ∧ ¬x = j
⊢ A x (σ x) = A x (σ ((swap i j) x))

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

Result:
no goals

Proof state:
case refine_3
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun x =>
    match x with
    | ⟨x, σ⟩ => ⟨σ i, σ * swap i j⟩
t : ℤˣ → Finset ((_ : n) × Perm n) := fun s => univ.sigma fun x => filter (fun σ => σ j = x) (ofSign s)
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x : n
σ : Perm n
hp✝ : ⟨x, σ⟩ ∈ univ.sigma fun a => filter (fun x => x j = a) (ofSign 1)
hp : ⟨x, σ⟩.fst ∈ univ ∧ sign ⟨x, σ⟩.snd = 1 ∧ ⟨x, σ⟩.snd j = ⟨x, σ⟩.fst
key : {j}ᶜ = {i}.disjUnion {i, j}ᶜ ⋯
⊢ A i ⟨x, σ⟩.fst * ∏ k ∈ {j}ᶜ, A k (⟨x, σ⟩.snd k) =
    A i ((fun p x => f p) ⟨x, σ⟩ hp✝).fst * ∏ k ∈ {j}ᶜ, A k (((fun p x => f p) ⟨x, σ⟩ hp✝).snd k)

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

Result:
case refine_3
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun x =>
    match x with
    | ⟨x, σ⟩ => ⟨σ i, σ * swap i j⟩
t : ℤˣ → Finset ((_ : n) × Perm n) := fun s => univ.sigma fun x => filter (fun σ => σ j = x) (ofSign s)
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x : n
σ : Perm n
hp✝ : ⟨x, σ⟩ ∈ univ.sigma fun a => filter (fun x => x j = a) (ofSign 1)
hp : ⟨x, σ⟩.fst ∈ univ ∧ sign ⟨x, σ⟩.snd = 1 ∧ ⟨x, σ⟩.snd j = ⟨x, σ⟩.fst
key : {j}ᶜ = {i}.disjUnion {i, j}ᶜ ⋯
⊢ A i x * A i (σ i) * ∏ x ∈ {i, j}ᶜ, A x (σ x) = A i (σ i) * A i (σ j) * ∏ x ∈ {i, j}ᶜ, A x (σ ((swap i j) x))