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

Tactic:
intro ⟨x, σ⟩ hp

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

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
⊢ 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:
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]

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, σ⟩.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)

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

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
⊢ ∑ 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 f : (Σ x : n, Perm n) → (Σ x : n, Perm n) := fun ⟨x, σ⟩ ↦ ⟨σ i, σ * swap i j⟩

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⟩
⊢ ∑ 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, σ⟩ ∈ t s
⊢ f (f ⟨x, σ⟩) = ⟨x, σ⟩

Tactic:
rw [mem_sigma, mem_filter, mem_ofSign] at 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, σ⟩.fst ∈ univ ∧ sign ⟨x, σ⟩.snd = s ∧ ⟨x, σ⟩.snd j = ⟨x, σ⟩.fst
⊢ f (f ⟨x, σ⟩) = ⟨x, σ⟩