awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A : Matrix n n R
i : n
a : (A * adjp 1 A) i i + detp (-1) A * 1 i i = (A * adjp (-1) A) i i + detp 1 A * 1 i i
⊢ (A * adjp 1 A + HSMul.hSMul (β := Matrix n n R) (detp (-1) A) 1) i i =
    (A * adjp (-1) A + HSMul.hSMul (β := Matrix n n R) (detp 1 A) 1) i i

Tactic:
simp_rw [add_apply, smul_apply, smul_eq_mul]

Premises used: Matrix.add_apply, Matrix.smul_apply, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
a : (A * adjp 1 A) i j + detp (-1) A * 1 i j = (A * adjp (-1) A) i j + detp 1 A * 1 i j
⊢ (A * adjp 1 A + HSMul.hSMul (β := Matrix n n R) (detp (-1) A) 1) i j =
    (A * adjp (-1) A + HSMul.hSMul (β := Matrix n n R) (detp 1 A) 1) i j

Tactic:
simp_rw [add_apply, smul_apply, smul_eq_mul]

Premises used: Matrix.add_apply, Matrix.smul_apply, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A : Matrix n n R
i : n
a : detp 1 A + detp (-1) A * 1 i i = detp (-1) A + detp 1 A * 1 i i
a₁ : detp 1 A + detp (-1) A * 1 = detp (-1) A + detp 1 A * 1
a₂ : detp 1 A + detp (-1) A = detp (-1) A + detp 1 A
⊢ (A * adjp 1 A) i i + detp (-1) A * 1 i i = (A * adjp (-1) A) i i + detp 1 A * 1 i i

Tactic:
simp_rw [mul_adjp_apply_eq, one_apply_eq, mul_one, add_comm]

Premises used: add_comm, Matrix.mul_adjp_apply_eq, mul_one, Matrix.one_apply_eq
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
a : (A * adjp (-1) A) i j + detp (-1) A * 1 i j = (A * adjp (-1) A) i j + detp 1 A * 1 i j
a₁ : (A * adjp (-1) A) i j + detp (-1) A * 0 = (A * adjp (-1) A) i j + detp 1 A * 0
⊢ (A * adjp 1 A) i j + detp (-1) A * 1 i j = (A * adjp (-1) A) i j + detp 1 A * 1 i j

Tactic:
simp_rw [mul_adjp_apply_ne A i j h, one_apply_ne h, mul_zero]

Premises used: Matrix.one_apply_ne, MulZeroClass.mul_zero, Matrix.mul_adjp_apply_ne
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
i j k : n
hij : i ≠ j
revert : ∀ (k : n), IsAddUnit (A i k * B k j)
⊢ IsAddUnit (A i k * B k j)

Tactic:
revert k
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
i j : n
hij : i ≠ j
rw : IsAddUnit.{u_3} (M := R) 0
⊢ ∀ (k : n), IsAddUnit (A i k * B k j)

Tactic:
rw [← IsAddUnit.sum_univ_iff, ← mul_apply, hAB, diagonal_apply_ne _ hij]

Premises used: Matrix.mul_apply, IsAddUnit.sum_univ_iff, Matrix.diagonal_apply_ne
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
i j : n
hij : i ≠ j
⊢ IsAddUnit.{u_3} (M := R) 0

Tactic:
isAddUnit_zero

Premises used: isAddUnit_zero
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
i j : n
hij : i ≠ j
⊢ IsAddUnit.{u_3} (M := R) 0

Tactic:
exact isAddUnit_zero

Premises used: isAddUnit_zero
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
h : ∀ {s t : ℤˣ}, s ≠ t → IsAddUnit (detp s A * detp t B)
⊢ Ne (α := ℤˣ) 1 (-1)

Tactic:
decide
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
h : ∀ {s t : ℤˣ}, s ≠ t → IsAddUnit (detp s A * detp t B)
⊢ Ne (α := ℤˣ) (-1) 1

Tactic:
decide
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
suffices : ∀ {s t : ℤˣ}, s ≠ t → IsAddUnit (detp s A * detp t B)
⊢ 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))
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
simp_rw :
  ∀ (a : Perm n),
    Membership.mem (γ := Finset (Perm n)) (ofSign s) a →
      ∀ (a_2 : Perm n),
        Membership.mem (γ := Finset (Perm n)) (ofSign t) a_2 →
          IsAddUnit (HMul.hMul (α := R) (∏ k : n, A k ((a : (a : n) → n) k)) (∏ k : n, B k ((a_2 : (a : n) → n) k)))
⊢ IsAddUnit (detp s A * detp t B)

Tactic:
simp_rw [detp, sum_mul_sum, IsAddUnit.sum_iff]

Premises used: IsAddUnit.sum_iff, Matrix.detp, Finset.sum_mul_sum
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign s) σ
τ : Perm n
hτ : Membership.mem (γ := Finset (Perm n)) (ofSign t) τ
rw :
  ∀ (hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = s) (τ : Perm n)
    (hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t),
    IsAddUnit (HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((τ : (a : n) → n) k)))
⊢ IsAddUnit (HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((τ : (a : n) → n) k)))

Tactic:
rw [mem_ofSign] at hσ hτ

Premises used: Equiv.Perm.mem_ofSign
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
σ : Perm n
hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = s
τ : Perm n
hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t
rw :
  ∀ (hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = s) (τ : Perm n)
    (h :
      Ne (α := ℤˣ) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ⁻¹ : ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ : ℤˣ))
    (hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t),
    IsAddUnit (HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((τ : (a : n) → n) k)))
⊢ IsAddUnit (HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((τ : (a : n) → n) k)))

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

Premises used: Equiv.Perm.sign_inv
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
σ : Perm n
hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = s
τ : Perm n
h :
  Ne (α := ℤˣ) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ⁻¹ : ℤˣ)
    (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ : ℤˣ)
hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t
⊢ σ⁻¹ ≠ τ

Tactic:
replace h := ne_of_apply_ne sign h
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
σ : Perm n
hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = s
τ : Perm n
hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t
h : σ⁻¹ ≠ τ
⊢ ¬1 = τ * σ

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

Premises used: eq_comm, ne_eq, eq_inv_iff_mul_eq_one
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
σ : Perm n
hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = s
τ : Perm n
hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t
h : ¬1 = τ * σ
⊢ ∃ (x : n), ¬x = (τ : (a : n) → n) ((σ : (a : n) → n) x : n)

Tactic:
simp_rw [Equiv.ext_iff, not_forall, Perm.mul_apply, Perm.one_apply] at h

Premises used: Equiv.ext_iff, Equiv.Perm.one_apply, Equiv.Perm.mul_apply, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
σ : Perm n
hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = s
τ : Perm n
hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t
h : ∃ (x : n), ¬x = (τ : (a : n) → n) ((σ : (a : n) → n) x : n)
obtain :
  ∀ (k : n) (hk : ¬k = (τ : (a : n) → n) ((σ : (a : n) → n) k : n)),
    IsAddUnit (HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((τ : (a : n) → n) k)))
⊢ IsAddUnit (HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((τ : (a : n) → n) k)))

Tactic:
obtain ⟨k, hk⟩ := h
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
σ : Perm n
hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = s
τ : Perm n
hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t
k : n
hk : ¬k = (τ : (a : n) → n) ((σ : (a : n) → n) k : n)
rw :
  IsAddUnit
    (HSMul.hSMul (β := R)
      (A k ((σ : (a : n) → n) k) * B ((σ : (a : n) → n) k) ((τ : (a : n) → n) ((σ : (a : n) → n) k : n)))
      (∏ x ∈ erase univ k,
        A x ((σ : (a : n) → n) x) * B ((σ : (a : n) → n) x) ((τ : (a : n) → n) ((σ : (a : n) → n) x : n))))
⊢ IsAddUnit (HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((τ : (a : n) → n) k)))

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

Premises used: Finset.mem_univ, Finset.prod_mul_distrib, Finset.univ, Finset.mul_prod_erase, Equiv.prod_comp, mul_comm, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
σ : Perm n
hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = s
τ : Perm n
hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t
k : n
hk : ¬k = (τ : (a : n) → n) ((σ : (a : n) → n) k : n)
⊢ IsAddUnit
    (HSMul.hSMul (β := R)
      (A k ((σ : (a : n) → n) k) * B ((σ : (a : n) → n) k) ((τ : (a : n) → n) ((σ : (a : n) → n) k : n)))
      (∏ x ∈ erase univ k,
        A x ((σ : (a : n) → n) x) * B ((σ : (a : n) → n) x) ((τ : (a : n) → n) ((σ : (a : n) → n) x : n))))

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

Premises used: Matrix.isAddUnit_mul, DFunLike.coe, IsAddUnit.smul_right
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
σ : Perm n
hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = s
τ : Perm n
hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = t
k : n
hk : ¬k = (τ : (a : n) → n) ((σ : (a : n) → n) k : n)
⊢ IsAddUnit
    (HSMul.hSMul (β := R)
      (A k ((σ : (a : n) → n) k) * B ((σ : (a : n) → n) k) ((τ : (a : n) → n) ((σ : (a : n) → n) k : n)))
      (∏ x ∈ erase univ k,
        A x ((σ : (a : n) → n) x) * B ((σ : (a : n) → n) x) ((τ : (a : n) → n) ((σ : (a : n) → n) x : n))))

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

Premises used: Matrix.isAddUnit_mul, DFunLike.coe, IsAddUnit.smul_right
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
h : ∀ {s t : ℤˣ}, s ≠ t → IsAddUnit (detp s A • (B * adjp t B))
⊢ Ne (α := ℤˣ) 1 (-1)

Tactic:
decide
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
h : ∀ {s t : ℤˣ}, s ≠ t → IsAddUnit (detp s A • (B * adjp t B))
⊢ Ne (α := ℤˣ) (-1) 1

Tactic:
decide
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
suffices : ∀ {s t : ℤˣ}, s ≠ t → IsAddUnit (detp s A • (B * adjp t B))
⊢ IsAddUnit (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B))

Tactic:
suffices h : ∀ {s t}, s ≠ t → IsAddUnit (detp s A • (B * adjp t B)) from
    (h (by decide)).add (h (by decide))
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
rw : ∀ (i j : n), IsAddUnit ((detp s A • (B * adjp t B)) i j)
⊢ IsAddUnit (detp s A • (B * adjp t B))

Tactic:
rw [isAddUnit_iff]

Premises used: Matrix.isAddUnit_iff
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
i j : n
simp_rw :
  ∀ (a : n),
    Membership.mem (γ := Finset n) univ a →
      ∀ (a_2 : Perm n),
        Membership.mem (γ := Finset (Perm n)) ({x ∈ ofSign t | (x : (a : n) → n) j = a}) a_2 →
          ∀ (a_4 : Perm n),
            Membership.mem (γ := Finset (Perm n)) (ofSign s) a_4 →
              IsAddUnit ((∏ k : n, A k ((a_4 : (a : n) → n) k)) * (B i a * ∏ k ∈ {j}ᶜ, B k ((a_2 : (a : n) → n) k)))
⊢ 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]

Premises used: Finset.mul_sum, Matrix.adjp_apply, Matrix.mul_apply, Matrix.smul_apply, IsAddUnit.sum_iff, Matrix.detp, smul_eq_mul, Finset.sum_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
i j k : n
hk : Membership.mem (γ := Finset n) univ k
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) ({x ∈ ofSign t | (x : (a : n) → n) j = k}) σ
τ : Perm n
hτ : Membership.mem (γ := Finset (Perm n)) (ofSign s) τ
rw :
  ∀ (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign t) σ ∧ (σ : (a : n) → n) j = k) (τ : Perm n)
    (hτ : Membership.mem (γ := Finset (Perm n)) (ofSign s) τ),
    IsAddUnit ((∏ k : n, A k ((τ : (a : n) → n) k)) * (B i k * ∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))
⊢ IsAddUnit ((∏ k : n, A k ((τ : (a : n) → n) k)) * (B i k * ∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))

Tactic:
rw [mem_filter] at hσ

Premises used: Finset.mem_filter
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
i j k : n
hk : Membership.mem (γ := Finset n) univ k
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign t) σ ∧ (σ : (a : n) → n) j = k
τ : Perm n
hτ : Membership.mem (γ := Finset (Perm n)) (ofSign s) τ
rw :
  ∀ (hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = t ∧ (σ : (a : n) → n) j = k) (τ : Perm n)
    (hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = s),
    IsAddUnit ((∏ k : n, A k ((τ : (a : n) → n) k)) * (B i k * ∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))
⊢ IsAddUnit ((∏ k : n, A k ((τ : (a : n) → n) k)) * (B i k * ∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))

Tactic:
rw [mem_ofSign] at hσ hτ

Premises used: Equiv.Perm.mem_ofSign
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
i j k : n
hk : Membership.mem (γ := Finset n) univ k
σ : Perm n
hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = t ∧ (σ : (a : n) → n) j = k
τ : Perm n
hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = s
rw :
  ∀ (hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = t ∧ (σ : (a : n) → n) j = k) (τ : Perm n)
    (h :
      Ne (α := ℤˣ) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ⁻¹ : ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ))
    (hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = s),
    IsAddUnit ((∏ k : n, A k ((τ : (a : n) → n) k)) * (B i k * ∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))
⊢ IsAddUnit ((∏ k : n, A k ((τ : (a : n) → n) k)) * (B i k * ∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))

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

Premises used: And.left, Equiv.Perm.sign_inv
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
i j k : n
hk : Membership.mem (γ := Finset n) univ k
σ : Perm n
hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = t ∧ (σ : (a : n) → n) j = k
τ : Perm n
h :
  Ne (α := ℤˣ) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ⁻¹ : ℤˣ)
    (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)
hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = s
⊢ τ⁻¹ ≠ σ

Tactic:
replace h := ne_of_apply_ne sign h
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
i j k : n
hk : Membership.mem (γ := Finset n) univ k
σ : Perm n
hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = t ∧ (σ : (a : n) → n) j = k
τ : Perm n
hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = s
h : τ⁻¹ ≠ σ
⊢ ¬σ * τ = 1

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

Premises used: eq_comm, ne_eq, eq_inv_iff_mul_eq_one
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
i j k : n
hk : Membership.mem (γ := Finset n) univ k
σ : Perm n
hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = t ∧ (σ : (a : n) → n) j = k
τ : Perm n
hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = s
h : ¬σ * τ = 1
obtain :
  ∀ (l : n) (hl1 : l ∈ (σ * τ).support) (hl2 : l ≠ (τ⁻¹ : (a : n) → n) j),
    IsAddUnit ((∏ k : n, A k ((τ : (a : n) → n) k)) * (B i k * ∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))
⊢ IsAddUnit ((∏ k : n, A k ((τ : (a : n) → n) k)) * (B i k * ∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))

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

Premises used: Equiv.Perm.one_lt_card_support_of_ne_one, Inv.inv, Finset.exists_mem_ne, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
i j k : n
hk : Membership.mem (γ := Finset n) univ k
σ : Perm n
hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = t ∧ (σ : (a : n) → n) j = k
τ : Perm n
hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = s
h : ¬σ * τ = 1
l : n
hl1 : l ∈ (σ * τ).support
hl2 : l ≠ (τ⁻¹ : (a : n) → n) j
⊢ l ≠ (σ * τ : (a : n) → n) l

Tactic:
rw [mem_support, ne_comm] at hl1

Premises used: Equiv.Perm.mem_support, ne_comm
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
i j k : n
hk : Membership.mem (γ := Finset n) univ k
σ : Perm n
hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = t ∧ (σ : (a : n) → n) j = k
τ : Perm n
hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = s
h : ¬σ * τ = 1
l : n
hl1 : l ∈ (σ * τ).support
hl2 : l ≠ (τ⁻¹ : (a : n) → n) j
hl1₁ : l ≠ (σ * τ : (a : n) → n) l
⊢ l ≠ (τ⁻¹ : (a : n) → n) j

Tactic:
rw [mem_support, ne_comm] at hl1

Premises used: Equiv.Perm.mem_support, ne_comm
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
i j k : n
hk : Membership.mem (γ := Finset n) univ k
σ : Perm n
hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = t ∧ (σ : (a : n) → n) j = k
τ : Perm n
hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = s
h : ¬σ * τ = 1
l : n
hl1 : l ≠ (σ * τ : (a : n) → n) l
hl2 : l ≠ (τ⁻¹ : (a : n) → n) j
⊢ Membership.mem (γ := Finset n) (singleton (α := n) ((τ⁻¹ : (a : n) → n) j : n))ᶜ l

Tactic:
rw [ne_eq, ← mem_singleton, ← mem_compl] at hl2

Premises used: Finset.mem_singleton, Finset.mem_compl, ne_eq
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
i j k : n
hk : Membership.mem (γ := Finset n) univ k
σ : Perm n
hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = t ∧ (σ : (a : n) → n) j = k
τ : Perm n
hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = s
h : ¬σ * τ = 1
l : n
hl1 : l ≠ (σ * τ : (a : n) → n) l
hl2 : Membership.mem (γ := Finset n) (singleton (α := n) ((τ⁻¹ : (a : n) → n) j : n))ᶜ l
rw :
  IsAddUnit
    (HMul.hMul (α := R) (∏ i ∈ (singleton (α := n) ((τ⁻¹ : (a : n) → n) j : n))ᶜ, A i ((τ : (a : n) → n) i))
        (∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)) •
      ((∏ i ∈ singleton (α := n) ((τ⁻¹ : (a : n) → n) j : n), A i ((τ : (a : n) → n) i)) * B i k))
⊢ IsAddUnit ((∏ k : n, A k ((τ : (a : n) → n) k)) * (B i k * ∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))

Tactic:
rw [← prod_mul_prod_compl {τ⁻¹ j}, mul_mul_mul_comm, mul_comm, ← smul_eq_mul]

Premises used: mul_mul_mul_comm, Finset.prod_mul_prod_compl, Inv.inv, mul_comm, smul_eq_mul, Singleton.singleton, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
R : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
i j k : n
hk : Membership.mem (γ := Finset n) univ k
σ : Perm n
hσ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ = t ∧ (σ : (a : n) → n) j = k
τ : Perm n
hτ : ((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ = s
h : ¬σ * τ = 1
l : n
hl1 : l ≠ (σ * τ : (a : n) → n) l
hl2 : Membership.mem (γ := Finset n) (singleton (α := n) ((τ⁻¹ : (a : n) → n) j : n))ᶜ l
hr :
  IsAddUnit
    (HMul.hMul (α := R) (∏ i ∈ (singleton (α := n) ((τ⁻¹ : (a : n) → n) j : n))ᶜ, A i ((τ : (a : n) → n) i))
      (∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))
⊢ IsAddUnit
    (HMul.hMul (α := R) (∏ i ∈ (singleton (α := n) ((τ⁻¹ : (a : n) → n) j : n))ᶜ, A i ((τ : (a : n) → n) i))
        (∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)) •
      ((∏ i ∈ singleton (α := n) ((τ⁻¹ : (a : n) → n) j : n), A i ((τ : (a : n) → n) i)) * B i k))

Tactic:
apply IsAddUnit.smul_right

Premises used: IsAddUnit.smul_right