-- 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)
⊢ ∑ 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:
have hf {s} : ∀ p ∈ t s, f (f p) = p := by
  intro ⟨x, σ⟩ hp
  rw [mem_sigma, mem_filter, mem_ofSign] at hp
  simp_rw [f, Perm.mul_apply, swap_apply_left, hp.2.2, mul_swap_mul_self]

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 ∈ 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:
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, σ⟩.fst ∈ univ ∧ sign ⟨x, σ⟩.snd = s ∧ ⟨x, σ⟩.snd j = ⟨x, σ⟩.fst
⊢ f (f ⟨x, σ⟩) = ⟨x, σ⟩

Tactic:
simp_rw [f, Perm.mul_apply, swap_apply_left, hp.2.2, mul_swap_mul_self]

Result:
no goals

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 ∧
    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_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

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⟩
⊢ ∑ 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:
let t s : Finset (Σ x : n, Perm n) := univ.sigma fun x ↦ (ofSign s).filter fun σ ↦ σ j = x

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

Tactic:
refine congr_arg _ (prod_congr rfl fun x 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, j}ᶜ
⊢ A x (σ x) = 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
⊢ ∀ (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)

Tactic:
intro ⟨x, σ⟩ 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)
⊢ 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)