-- 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 ∈ univ.sigma fun a => filter (fun x => x j = a) (ofSign 1), A i x.fst * ∏ k ∈ {j}ᶜ, A k (x.snd k) =
    ∑ x ∈ univ.sigma fun a => filter (fun x => x j = a) (ofSign (-1)), A i x.fst * ∏ k ∈ {j}ᶜ, A k (x.snd k)

Tactic:
refine sum_bij' (fun p _ ↦ f p) (fun p _ ↦ f p) ?_ ?_ hf hf ?_

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
⊢ ∀ (a : (_ : n) × Perm n) (ha : a ∈ univ.sigma fun a => filter (fun x => x j = a) (ofSign 1)),
    (fun p x => f p) a ha ∈ univ.sigma fun a => filter (fun x => x j = a) (ofSign (-1))

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
⊢ ∀ (a : (_ : n) × Perm n) (ha : a ∈ univ.sigma fun a => filter (fun x => x j = a) (ofSign (-1))),
    (fun p x => f p) a ha ∈ univ.sigma fun a => filter (fun x => x j = a) (ofSign 1)

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
⊢ ∀ (a : (_ : n) × Perm n) (ha : a ∈ univ.sigma fun a => filter (fun x => x j = a) (ofSign 1)),
    A i a.fst * ∏ k ∈ {j}ᶜ, A k (a.snd k) =
      A i ((fun p x => f p) a ha).fst * ∏ k ∈ {j}ᶜ, A k (((fun p x => f p) a ha).snd k)

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
⊢ (A * adjp 1 A) i j = (A * adjp (-1) A) i j

Tactic:
simp_rw [mul_apply, adjp_apply, mul_sum, sum_sigma']

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
⊢ ∑ x ∈ univ.sigma fun a => filter (fun x => x j = a) (ofSign 1), A i x.fst * ∏ k ∈ {j}ᶜ, A k (x.snd k) =
    ∑ x ∈ univ.sigma fun a => filter (fun x => x j = a) (ofSign (-1)), A i x.fst * ∏ k ∈ {j}ᶜ, A k (x.snd k)

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
⊢ ∀ (a : (_ : n) × Perm n) (ha : a ∈ univ.sigma fun a => filter (fun x => x j = a) (ofSign 1)),
    (fun p x => f p) a ha ∈ univ.sigma fun a => filter (fun x => x j = a) (ofSign (-1))

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

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
⊢ _root_.Disjoint {i} {i, j}ᶜ

Tactic:
simp

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 * A i (σ i) * ∏ x ∈ {i, j}ᶜ, A x (σ x) = A i (σ i) * A i (σ j) * ∏ x ∈ {i, j}ᶜ, A x (σ ((swap i j) x))

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

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 (σ i) * A i x * ∏ x ∈ {i, j}ᶜ, A x (σ x) = A i (σ i) * A i ⟨x, σ⟩.fst * ∏ x ∈ {i, j}ᶜ, A x (σ ((swap i j) x))

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, j}ᶜ
⊢ A x (σ x) = A x (σ ((swap i j) x))

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

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}ᶜ ⋯
x : n
hx : ¬x = i ∧ ¬x = j
⊢ A x (σ x) = A x (σ ((swap i j) x))