awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
f : (_ : n) × Perm n → (_ : n) × Perm n :=
  fun (x : (_ : n) × Perm n) ↦
    match (motive := (_ : n) × Perm n → (_ : n) × Perm n) x with
    | ⟨x, σ⟩ => Sigma.mk (β := fun (x : n) ↦ Perm n) ((σ : (a : n) → n) i) (σ * swap i j)
t : (s : ℤˣ) → Finset ((_ : n) × Perm n) :=
  fun (s : ℤˣ) ↦ Finset.sigma (α := fun (x : n) ↦ Perm n) univ fun (x : n) ↦ {σ ∈ ofSign s | (σ : (a : n) → n) j = x}
hf : ∀ {s : ℤˣ}, ∀ p ∈ t s, f (f p) = p
x_1 : n
σ : Perm n
hp_1 :
  Membership.mem (γ := Finset ((_ : n) × Perm n))
    (Finset.sigma (α := fun (a : n) ↦ Perm n) univ fun (a : n) ↦ {x ∈ ofSign 1 | (x : (a : n) → n) j = a})
    (Sigma.mk (β := fun (i : n) ↦ Perm n) x_1 σ)
hp :
  Membership.mem (γ := Finset n) univ
      (Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x_1 σ)) ∧
    Eq (α := ℤˣ)
        (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
            (Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x_1 σ)) :
          ℤˣ)
        (1 : ℤˣ) ∧
      ((Sigma.snd (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x_1 σ) : Perm n) : (a : n) → n) j =
        Sigma.fst (β := fun (i : n) ↦ Perm n) (Sigma.mk (β := fun (i : n) ↦ Perm n) x_1 σ)
key : Eq (α := Finset n) {j}ᶜ (disjUnion {i} {i, j}ᶜ ⋯)
x : n
hx : ¬x = i ∧ ¬x = j
⊢ A x ((σ : (a : n) → n) x) = A x ((σ : (a : n) → n) ((swap i j : (a : n) → n) x : n))
have refine_3 : A x ((σ : (a : n) → n) x) = A x ((σ : (a : n) → n) x)
Tactic: rw [swap_apply_of_ne_of_ne hx.1 hx.2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
⊢ A * adjp 1 A + HSMul.hSMul (β := Matrix n n R) (detp (-1) A) 1 =
    A * adjp (-1) A + HSMul.hSMul (β := Matrix n n R) (detp 1 A) 1
have a : ∀ (i j : n),
  (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: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
⊢ (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
have a : (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: rcases eq_or_ne i j with rfl | h
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
a :
  (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
⊢ (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
have a₁ : ∀ (h : 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: rcases eq_or_ne i j with rfl | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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 * 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
have 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 [add_apply, smul_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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 * 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
have 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
Tactic: simp_rw [add_apply, smul_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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 * adjp 1 A) i i + detp (-1) A * 1 i i = (A * adjp (-1) A) i i + detp 1 A * 1 i i
have a : detp 1 A + detp (-1) A * 1 i i = detp (-1) A + detp 1 A * 1 i i
Tactic: simp_rw [mul_adjp_apply_eq, one_apply_eq, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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 * adjp 1 A) i i + detp (-1) A * 1 i i = (A * adjp (-1) A) i i + detp 1 A * 1 i i
have a₁ : detp 1 A + detp (-1) A * 1 = detp (-1) A + detp 1 A * 1
Tactic: simp_rw [mul_adjp_apply_eq, one_apply_eq, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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 * adjp 1 A) i i + detp (-1) A * 1 i i = (A * adjp (-1) A) i i + detp 1 A * 1 i i
have a₂ : detp 1 A + detp (-1) A = detp (-1) A + detp 1 A
Tactic: simp_rw [mul_adjp_apply_eq, one_apply_eq, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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 * adjp 1 A) i j + detp (-1) A * 1 i j = (A * adjp (-1) A) i j + detp 1 A * 1 i j
have 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
Tactic: simp_rw [mul_adjp_apply_ne A i j h, one_apply_ne h, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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) i j + detp (-1) A * 1 i j = (A * adjp (-1) A) i j + detp 1 A * 1 i j
have a₁ : (A * adjp (-1) A) i j + detp (-1) A * 0 = (A * adjp (-1) A) i j + detp 1 A * 0
Tactic: simp_rw [mul_adjp_apply_ne A i j h, one_apply_ne h, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
⊢ IsAddUnit (A i k * B k j)
have revert : ∀ (k : n), IsAddUnit (A i k * B k j)
Tactic: revert k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
⊢ ∀ (k : n), IsAddUnit (A i k * B k j)
have rw : IsAddUnit.{u_3} (M := R) 0
Tactic: rw [← IsAddUnit.sum_univ_iff, ← mul_apply, hAB, diagonal_apply_ne _ hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
⊢ IsAddUnit (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B)
have suffices : ∀ {s t : ℤˣ}, s ≠ t → IsAddUnit (detp s A * detp t B)
Tactic: suffices h : ∀ {s t}, s ≠ t → IsAddUnit (detp s A * detp t B) from
    (h (by decide)).add (h (by decide))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
⊢ IsAddUnit (detp s A * detp t B)
have 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)))
Tactic: simp_rw [detp, sum_mul_sum, IsAddUnit.sum_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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) τ
⊢ IsAddUnit (HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((τ : (a : n) → n) k)))
have 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)))
Tactic: rw [mem_ofSign] at hσ hτ
Cleared hypotheses: hσ, τ, hτ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
⊢ IsAddUnit (HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((τ : (a : n) → n) k)))
have 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)))
Tactic: rw [← hσ, ← hτ, ← sign_inv] at h
Cleared hypotheses: h, hσ, τ, hτ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (hypothesis)
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
⊢ IsAddUnit (HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((τ : (a : n) → n) k)))
have h₁ : σ⁻¹ ≠ τ
Tactic: replace h := ne_of_apply_ne sign h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (hypothesis)
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 : σ⁻¹ ≠ τ
⊢ IsAddUnit (HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((τ : (a : n) → n) k)))
have h₁ : ¬1 = τ * σ
Tactic: rw [ne_eq, eq_comm, eq_inv_iff_mul_eq_one, eq_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (hypothesis)
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 = τ * σ
⊢ IsAddUnit (HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((τ : (a : n) → n) k)))
have h₁ : ∃ (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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)
⊢ IsAddUnit (HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((τ : (a : n) → n) k)))
have 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)))
Tactic: obtain ⟨k, hk⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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 (HMul.hMul (α := R) (∏ k : n, A k ((σ : (a : n) → n) k)) (∏ k : n, B k ((τ : (a : n) → n) k)))
have 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))))
Tactic: rw [mul_comm, ← Equiv.prod_comp σ, mul_comm, ← prod_mul_distrib,
    ← mul_prod_erase univ _ (mem_univ k), ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
⊢ IsAddUnit (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B))
have suffices : ∀ {s t : ℤˣ}, s ≠ t → IsAddUnit (detp s A • (B * adjp t B))
Tactic: suffices h : ∀ {s t}, s ≠ t → IsAddUnit (detp s A • (B * adjp t B)) from
    (h (by decide)).add (h (by decide))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
⊢ IsAddUnit (detp s A • (B * adjp t B))
have rw : ∀ (i j : n), IsAddUnit ((detp s A • (B * adjp t B)) i j)
Tactic: rw [isAddUnit_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
⊢ IsAddUnit ((detp s A • (B * adjp t B)) i j)
have 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)))
Tactic: simp_rw [smul_apply, smul_eq_mul, mul_apply, detp, adjp_apply, mul_sum, sum_mul,
    IsAddUnit.sum_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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) τ
⊢ IsAddUnit ((∏ k : n, A k ((τ : (a : n) → n) k)) * (B i k * ∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))
have 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)))
Tactic: rw [mem_filter] at hσ
Cleared hypotheses: hσ, τ, hτ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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) τ
⊢ IsAddUnit ((∏ k : n, A k ((τ : (a : n) → n) k)) * (B i k * ∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))
have 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)))
Tactic: rw [mem_ofSign] at hσ hτ
Cleared hypotheses: hσ, τ, hτ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
⊢ IsAddUnit ((∏ k : n, A k ((τ : (a : n) → n) k)) * (B i k * ∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))
have 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)))
Tactic: rw [← hσ.1, ← hτ, ← sign_inv] at h
Cleared hypotheses: h, hσ, τ, hτ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (hypothesis)
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
⊢ IsAddUnit ((∏ k : n, A k ((τ : (a : n) → n) k)) * (B i k * ∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))
have h₁ : τ⁻¹ ≠ σ
Tactic: replace h := ne_of_apply_ne sign h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (hypothesis)
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 : τ⁻¹ ≠ σ
⊢ IsAddUnit ((∏ k : n, A k ((τ : (a : n) → n) k)) * (B i k * ∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))
have h₁ : ¬σ * τ = 1
Tactic: rw [ne_eq, eq_comm, eq_inv_iff_mul_eq_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
⊢ IsAddUnit ((∏ k : n, A k ((τ : (a : n) → n) k)) * (B i k * ∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))
have 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)))
Tactic: obtain ⟨l, hl1, hl2⟩ := exists_mem_ne (one_lt_card_support_of_ne_one h) (τ⁻¹ j)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (hypothesis)
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
⊢ IsAddUnit ((∏ k : n, A k ((τ : (a : n) → n) k)) * (B i k * ∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))
have hl1₁ : l ≠ (σ * τ : (a : n) → n) l
Tactic: rw [mem_support, ne_comm] at hl1
Cleared hypotheses: hl1, hl2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (hypothesis)
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
⊢ IsAddUnit ((∏ k : n, A k ((τ : (a : n) → n) k)) * (B i k * ∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))
have hl2₁ : Membership.mem (γ := Finset n) (singleton (α := n) ((τ⁻¹ : (a : n) → n) j : n))ᶜ l
Tactic: rw [ne_eq, ← mem_singleton, ← mem_compl] at hl2
Cleared hypotheses: hl2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
⊢ IsAddUnit ((∏ k : n, A k ((τ : (a : n) → n) k)) * (B i k * ∏ k ∈ {j}ᶜ, B k ((σ : (a : n) → n) k)))
have 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))
Tactic: rw [← prod_mul_prod_compl {τ⁻¹ j}, mul_mul_mul_comm, mul_comm, ← smul_eq_mul]