-- 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:
case refine_1
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 ∧
    sign ((fun p x => f p) ⟨x, σ⟩ hp✝).snd = -1 ∧
      ((fun p x => f p) ⟨x, σ⟩ hp✝).snd j = ((fun p x => f p) ⟨x, σ⟩ hp✝).fst

Tactic:
rw [Perm.mul_apply, sign_mul, hp.2.1, sign_swap h, swap_apply_right]

Result:
case refine_1
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

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)
s : ℤˣ
⊢ ∀ p ∈ t s, f (f p) = p

Tactic:
intro ⟨x, σ⟩ hp

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)
s : ℤˣ
x : n
σ : Perm n
hp : ⟨x, σ⟩ ∈ t s
⊢ f (f ⟨x, σ⟩) = ⟨x, σ⟩

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
⊢ i ∈ {j}ᶜ

Tactic:
rwa [mem_compl, mem_singleton]

Result:
no goals

Proof state:
case refine_1
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)
⊢ (fun p x => f p) ⟨x, σ⟩ hp ∈ univ.sigma fun a => filter (fun x => x j = a) (ofSign (-1))

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

Result:
case refine_1
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 ∧
    sign ((fun p x => f p) ⟨x, σ⟩ hp✝).snd = -1 ∧
      ((fun p x => f p) ⟨x, σ⟩ hp✝).snd j = ((fun p x => f p) ⟨x, σ⟩ hp✝).fst

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)
⊢ 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:
rw [mem_sigma, mem_filter, mem_ofSign] at hp

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
⊢ 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)