-- Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean
theorem isAddUnit_detp_mul_detp (hAB : A * B = 1) :
    IsAddUnit (detp 1 A * detp (-1) B + detp (-1) A * detp 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
σ : Perm n
hσ : σ ∈ ofSign s
τ : Perm n
hτ : τ ∈ ofSign t
⊢ IsAddUnit ((∏ k : n, A k (σ k)) * ∏ k : n, 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
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
⊢ IsAddUnit ((∏ k : n, A k (σ k)) * ∏ k : n, 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 : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
h : ¬1 = τ * σ
⊢ IsAddUnit ((∏ k : n, A k (σ k)) * ∏ k : n, B k (τ k))

Tactic:
simp_rw [Equiv.ext_iff, not_forall, Perm.mul_apply, Perm.one_apply] 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 : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
h : ∃ x, ¬x = τ (σ x)
⊢ IsAddUnit ((∏ k : n, A k (σ k)) * ∏ k : n, B k (τ k))

Proof state:
case 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 : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
k : n
hk : ¬k = τ (σ k)
⊢ IsAddUnit ((A k (σ k) * B (σ k) (τ (σ k))) • ∏ x ∈ univ.erase k, A x (σ x) * B (σ x) (τ (σ x)))

Tactic:
exact (isAddUnit_mul hAB k (τ (σ k)) (σ k) hk).smul_right _

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
⊢ IsAddUnit (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B)

Tactic:
suffices h : ∀ {s t}, s ≠ t → IsAddUnit (detp s A * detp t B) from
  (h (by decide)).add (h (by decide))

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 : ℤˣ}, s ≠ t → IsAddUnit (detp s A * detp t 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 : ℤˣ}, s ≠ t → IsAddUnit (detp s A * detp t B)

Tactic:
intro s t 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
⊢ IsAddUnit (detp s A * detp t 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
⊢ ∀ a ∈ ofSign s, ∀ a_2 ∈ ofSign t, IsAddUnit ((∏ k : n, A k (a k)) * ∏ k : n, B k (a_2 k))

Tactic:
intro σ 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
σ : Perm n
hσ : σ ∈ ofSign s
τ : Perm n
hτ : τ ∈ ofSign t
⊢ IsAddUnit ((∏ k : n, A k (σ k)) * ∏ k : n, 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 * detp t B)

Tactic:
simp_rw [detp, sum_mul_sum, 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
⊢ ∀ a ∈ ofSign s, ∀ a_2 ∈ ofSign t, IsAddUnit ((∏ k : n, A k (a k)) * ∏ k : n, B k (a_2 k))

Proof state:
case 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 : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
k : n
hk : ¬k = τ (σ k)
⊢ IsAddUnit ((∏ k : n, A k (σ k)) * ∏ k : n, B k (τ k))

Tactic:
rw [mul_comm, ← Equiv.prod_comp σ, mul_comm, ← prod_mul_distrib,
  ← mul_prod_erase univ _ (mem_univ k), ← smul_eq_mul]

Result:
case 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 : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
k : n
hk : ¬k = τ (σ k)
⊢ IsAddUnit ((A k (σ k) * B (σ k) (τ (σ k))) • ∏ x ∈ univ.erase k, A x (σ x) * B (σ x) (τ (σ x)))

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
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
⊢ IsAddUnit ((∏ k : n, A k (σ k)) * ∏ k : n, B k (τ k))

Tactic:
rw [← hσ, ← 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 : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
h : sign σ⁻¹ ≠ sign τ
hτ : sign τ = t
⊢ IsAddUnit ((∏ k : n, A k (σ k)) * ∏ k : n, 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 * detp 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 : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
h : ∃ x, ¬x = τ (σ x)
⊢ IsAddUnit ((∏ k : n, A k (σ k)) * ∏ k : n, B k (τ k))

Tactic:
obtain ⟨k, hk⟩ := h

Result:
case 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 : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
k : n
hk : ¬k = τ (σ k)
⊢ IsAddUnit ((∏ k : n, A k (σ k)) * ∏ k : n, 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 : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
h : sign σ⁻¹ ≠ sign τ
hτ : sign τ = t
⊢ IsAddUnit ((∏ k : n, A k (σ k)) * ∏ k : n, B k (τ k))

Tactic:
replace h := ne_of_apply_ne sign 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 : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
h : σ⁻¹ ≠ τ
⊢ IsAddUnit ((∏ k : n, A k (σ k)) * ∏ k : n, 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 * detp 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 : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
h : σ⁻¹ ≠ τ
⊢ IsAddUnit ((∏ k : n, A k (σ k)) * ∏ k : n, B k (τ k))

Tactic:
rw [ne_eq, eq_comm, eq_inv_iff_mul_eq_one, eq_comm] 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 : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
h : ¬1 = τ * σ
⊢ IsAddUnit ((∏ k : n, A k (σ k)) * ∏ k : n, B k (τ k))