-- Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean
theorem isAddUnit_detp_smul_mul_adjp (hAB : A * B = 1) :
    IsAddUnit (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B))

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
h : s ≠ t
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : σ ∈ filter (fun x => x j = k) (ofSign t)
τ : Perm n
hτ : τ ∈ ofSign s
⊢ IsAddUnit ((∏ k : n, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Tactic:
rw [mem_filter] at hσ

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
h : s ≠ t
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : σ ∈ ofSign t ∧ σ j = k
τ : Perm n
hτ : τ ∈ ofSign s
⊢ IsAddUnit ((∏ k : n, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
h : s ≠ t
⊢ IsAddUnit (detp s A • (B * adjp t B))

Tactic:
rw [isAddUnit_iff]

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
h : s ≠ t
⊢ ∀ (i j : n), IsAddUnit ((detp s A • (B * adjp t B)) i j)

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
h : s ≠ t
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
⊢ IsAddUnit ((∏ k : n, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Tactic:
rw [← hσ.1, ← hτ, ← sign_inv] at h

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
h : sign τ⁻¹ ≠ sign σ
hτ : sign τ = s
⊢ IsAddUnit ((∏ k : n, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
h : ∀ {s t : ℤˣ}, s ≠ t → IsAddUnit (detp s A • (B * adjp t B))
⊢ 1 ≠ -1

Tactic:
decide

Result:
no goals

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
h : s ≠ t
i j : n
⊢ IsAddUnit ((detp s A • (B * adjp t B)) i j)

Tactic:
simp_rw [smul_apply, smul_eq_mul, mul_apply, detp, adjp_apply, mul_sum, sum_mul,
  IsAddUnit.sum_iff]

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
h : s ≠ t
i j : n
⊢ ∀ a ∈ univ,
    ∀ a_2 ∈ filter (fun x => x j = a) (ofSign t),
      ∀ a_4 ∈ ofSign s, IsAddUnit ((∏ k : n, A k (a_4 k)) * (B i a * ∏ k ∈ {j}ᶜ, B k (a_2 k)))

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
h : ¬σ * τ = 1
l : n
hl1 : l ≠ (σ * τ) l
hl2 : l ∈ {τ⁻¹ j}ᶜ
⊢ ∀ (k : n), k ∈ {τ⁻¹ j}ᶜ ↔ τ k ∈ {j}ᶜ

Tactic:
simp [inv_def, eq_symm_apply]

Result:
no goals

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
h : ¬σ * τ = 1
⊢ IsAddUnit ((∏ k : n, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Tactic:
obtain ⟨l, hl1, hl2⟩ := exists_ne_of_one_lt_card (one_lt_card_support_of_ne_one h) (τ⁻¹ j)

Result:
case intro.intro
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
h : ¬σ * τ = 1
l : n
hl1 : l ∈ (σ * τ).support
hl2 : l ≠ τ⁻¹ j
⊢ IsAddUnit ((∏ k : n, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Proof state:
case intro.intro
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
h : ¬σ * τ = 1
l : n
hl1 : l ≠ (σ * τ) l
hl2 : l ∈ {τ⁻¹ j}ᶜ
⊢ IsAddUnit (((∏ i ∈ {τ⁻¹ j}ᶜ, A i (τ i)) * ∏ k ∈ {j}ᶜ, B k (σ k)) • ((∏ i ∈ {τ⁻¹ j}, A i (τ i)) * B i k))

Tactic:
apply IsAddUnit.smul_right

Result:
case intro.intro.hr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
h : ¬σ * τ = 1
l : n
hl1 : l ≠ (σ * τ) l
hl2 : l ∈ {τ⁻¹ j}ᶜ
⊢ IsAddUnit ((∏ i ∈ {τ⁻¹ j}ᶜ, A i (τ i)) * ∏ k ∈ {j}ᶜ, B k (σ k))

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
h : τ⁻¹ ≠ σ
⊢ IsAddUnit ((∏ k : n, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Tactic:
rw [ne_eq, eq_comm, eq_inv_iff_mul_eq_one] at h

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
h : ¬σ * τ = 1
⊢ IsAddUnit ((∏ k : n, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
h : s ≠ t
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : σ ∈ ofSign t ∧ σ j = k
τ : Perm n
hτ : τ ∈ ofSign s
⊢ IsAddUnit ((∏ k : n, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Tactic:
rw [mem_ofSign] at hσ hτ

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
h : s ≠ t
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
⊢ IsAddUnit ((∏ k : n, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
h : s ≠ t
⊢ ∀ (i j : n), IsAddUnit ((detp s A • (B * adjp t B)) i j)

Tactic:
intro i j

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
h : s ≠ t
i j : n
⊢ IsAddUnit ((detp s A • (B * adjp t B)) i j)

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
h : ∀ {s t : ℤˣ}, s ≠ t → IsAddUnit (detp s A • (B * adjp t B))
⊢ -1 ≠ 1

Tactic:
decide

Result:
no goals

Proof state:
case intro.intro.hr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
s t : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
h : ¬σ * τ = 1
l : n
hl1 : l ≠ (σ * τ) l
hl2 : l ∈ {τ⁻¹ j}ᶜ
h0 : ∀ (k : n), k ∈ {τ⁻¹ j}ᶜ ↔ τ k ∈ {j}ᶜ
⊢ IsAddUnit ((A l (τ l) * B (τ l) (σ (τ l))) • ∏ x ∈ {τ⁻¹ j}ᶜ.erase l, A x (τ x) * B (τ x) (σ (τ x)))

Tactic:
exact (isAddUnit_mul hAB l (σ (τ l)) (τ l) hl1).smul_right _

Result:
no goals