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 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
⊢ ∀ (k : n),
    Membership.mem (γ := Finset n) (singleton (α := n) ((τ⁻¹ : (a : n) → n) j : n))ᶜ k ↔
      Membership.mem (α := n) (γ := Finset n) {j}ᶜ ((τ : (a : n) → n) k : n)

Tactic:
simp [inv_def, eq_symm_apply]

Premises used: Equiv.Perm.inv_def, Equiv.eq_symm_apply
-- 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
⊢ ∀ (k : n),
    Membership.mem (γ := Finset n) (singleton (α := n) ((τ⁻¹ : (a : n) → n) j : n))ᶜ k ↔
      Membership.mem (α := n) (γ := Finset n) {j}ᶜ ((τ : (a : n) → n) k : n)

Tactic:
have h0 : ∀ k, k ∈ ({τ⁻¹ j} : Finset n)ᶜ ↔ τ k ∈ ({j} : Finset n)ᶜ := by
    simp [inv_def, eq_symm_apply]
-- 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
h0 :
  ∀ (k : n),
    Membership.mem (γ := Finset n) (singleton (α := n) ((τ⁻¹ : (a : n) → n) j : n))ᶜ k ↔
      Membership.mem (α := n) (γ := Finset n) {j}ᶜ ((τ : (a : n) → n) k : n)
hr :
  IsAddUnit
    (HSMul.hSMul (β := R)
      (A l ((τ : (a : n) → n) l) * B ((τ : (a : n) → n) l) ((σ : (a : n) → n) ((τ : (a : n) → n) l : n)))
      (∏ x ∈ erase (singleton (α := n) ((τ⁻¹ : (a : n) → n) j : n))ᶜ l,
        A x ((τ : (a : n) → n) x) * B ((τ : (a : n) → n) x) ((σ : (a : n) → n) ((τ : (a : n) → n) x : n))))
⊢ 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)))

Tactic:
rw [← prod_equiv τ h0 fun _ _ ↦ rfl, ← prod_mul_distrib, ← mul_prod_erase _ _ hl2, ← smul_eq_mul]

Premises used: Finset.prod_mul_distrib, Finset.prod_equiv, Finset.mul_prod_erase, smul_eq_mul, rfl
-- 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
h0 :
  ∀ (k : n),
    Membership.mem (γ := Finset n) (singleton (α := n) ((τ⁻¹ : (a : n) → n) j : n))ᶜ k ↔
      Membership.mem (α := n) (γ := Finset n) {j}ᶜ ((τ : (a : n) → n) k : n)
⊢ IsAddUnit
    (HSMul.hSMul (β := R)
      (A l ((τ : (a : n) → n) l) * B ((τ : (a : n) → n) l) ((σ : (a : n) → n) ((τ : (a : n) → n) l : n)))
      (∏ x ∈ erase (singleton (α := n) ((τ⁻¹ : (a : n) → n) j : n))ᶜ l,
        A x ((τ : (a : n) → n) x) * B ((τ : (a : n) → n) x) ((σ : (a : n) → n) ((τ : (a : n) → n) x : n))))

Tactic:
(isAddUnit_mul hAB l (σ (τ l)) (τ l) hl1).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 : ℤˣ
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
h0 :
  ∀ (k : n),
    Membership.mem (γ := Finset n) (singleton (α := n) ((τ⁻¹ : (a : n) → n) j : n))ᶜ k ↔
      Membership.mem (α := n) (γ := Finset n) {j}ᶜ ((τ : (a : n) → n) k : n)
⊢ IsAddUnit
    (HSMul.hSMul (β := R)
      (A l ((τ : (a : n) → n) l) * B ((τ : (a : n) → n) l) ((σ : (a : n) → n) ((τ : (a : n) → n) l : n)))
      (∏ x ∈ erase (singleton (α := n) ((τ⁻¹ : (a : n) → n) j : n))ᶜ l,
        A x ((τ : (a : n) → n) x) * B ((τ : (a : n) → n) x) ((σ : (a : n) → n) ((τ : (a : n) → n) x : n))))

Tactic:
exact (isAddUnit_mul hAB l (σ (τ l)) (τ l) hl1).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
hAB : A * B = 1
⊢ A * (B * adjp 1 B + HSMul.hSMul (β := Matrix n n R) (detp (-1) B) 1) =
    A * (B * adjp (-1) B + HSMul.hSMul (β := Matrix n n R) (detp 1 B) 1)

Tactic:
have key := congr(A * $(mul_adjp_add_detp B))
-- 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
hAB : A * B = 1
key :
  A * (B * adjp 1 B + HSMul.hSMul (β := Matrix n n R) (detp (-1) B) 1) =
    A * (B * adjp (-1) B + HSMul.hSMul (β := Matrix n n R) (detp 1 B) 1)
⊢ adjp 1 B + detp (-1) B • A = adjp (-1) B + detp 1 B • A

Tactic:
simp_rw [mul_add, ← mul_assoc, hAB, one_mul, Matrix.mul_smul, mul_one] at key

Premises used: Matrix.mul_smul, mul_assoc, mul_add, mul_one, one_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
hAB : A * B = 1
key : adjp 1 B + detp (-1) B • A = adjp (-1) B + detp 1 B • A
rwa : adjp (-1) B + detp 1 B • A = detp (-1) B • A + adjp 1 B
rwa₁ : detp (-1) B • A + adjp 1 B = adjp (-1) B + detp 1 B • A
rwa₂ rwa₃ rwa₄ rwa₅ : adjp 1 B + detp (-1) B • A = adjp (-1) B + detp 1 B • A
⊢ detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B

Tactic:
rwa [add_comm, eq_comm, add_comm]

Premises used: eq_comm, add_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
hAB : A * B = 1
⊢ detp 1 (A * B) + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) =
    detp (-1) (A * B) + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)

Tactic:
have h0 := detp_mul A B
-- 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
hAB : A * B = 1
h0 :
  detp 1 (A * B) + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) =
    detp (-1) (A * B) + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)
⊢ 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B

Tactic:
rw [hAB, detp_one_one, detp_neg_one_one, zero_add] at h0

Premises used: Matrix.detp_neg_one_one, Matrix.detp_one_one, zero_add
-- 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
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
⊢ detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B

Tactic:
have h := detp_smul_add_adjp hAB
-- 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
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h : detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B
⊢ detp 1 A • (detp 1 B • A + adjp (-1) B) + detp (-1) A • (detp (-1) B • A + adjp 1 B) =
    detp 1 A • (detp (-1) B • A + adjp 1 B) + detp (-1) A • (detp 1 B • A + adjp (-1) B)

Tactic:
replace h := congr(detp 1 A • $h + detp (-1) A • $h.symm)
-- 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
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  detp 1 A • (detp 1 B • A + adjp (-1) B) + detp (-1) A • (detp (-1) B • A + adjp 1 B) =
    detp 1 A • (detp (-1) B • A + adjp 1 B) + detp (-1) A • (detp 1 B • A + adjp (-1) B)
⊢ (detp 1 A * detp 1 B) • A + detp 1 A • adjp (-1) B + ((detp (-1) A * detp (-1) B) • A + detp (-1) A • adjp 1 B) =
    (detp 1 A * detp (-1) B) • A + detp 1 A • adjp 1 B + ((detp (-1) A * detp 1 B) • A + detp (-1) A • adjp (-1) B)

Tactic:
simp only [smul_add, smul_smul] at h

Premises used: smul_smul, smul_add
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
m : Type u_2
R : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommSemiring R
s : ℤˣ
A B : Matrix n n R
i j : n
⊢ IsStablyFiniteRing R

Tactic:
⟨fun n ↦ ⟨fun {A B} hAB ↦ ?_⟩⟩

Premises used: IsDedekindFiniteMonoid.mk, IsStablyFiniteRing.mk
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n : Type u_1
m : Type u_2
R : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommSemiring R
s : ℤˣ
A B : Matrix n n R
i j : n
refine : ∀ (n : ℕ) {A B : Matrix (Fin n) (Fin n) R} (hAB : A * B = 1), B * A = 1
⊢ IsStablyFiniteRing R

Tactic:
refine ⟨fun n ↦ ⟨fun {A B} hAB ↦ ?_⟩⟩
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n_1 : Type u_1
m : Type u_2
R : Type u_3
inst : Fintype m
inst_1 : Fintype n_1
inst_2 : DecidableEq m
inst_3 : DecidableEq n_1
inst_4 : CommSemiring R
s : ℤˣ
A_1 B_1 : Matrix n_1 n_1 R
i j : n_1
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
⊢ detp 1 (A * B) + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) =
    detp (-1) (A * B) + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)

Tactic:
have h0 := detp_mul A B
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n_1 : Type u_1
m : Type u_2
R : Type u_3
inst : Fintype m
inst_1 : Fintype n_1
inst_2 : DecidableEq m
inst_3 : DecidableEq n_1
inst_4 : CommSemiring R
s : ℤˣ
A_1 B_1 : Matrix n_1 n_1 R
i j : n_1
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 :
  detp 1 (A * B) + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) =
    detp (-1) (A * B) + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)
⊢ 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B

Tactic:
rw [hAB, detp_one_one, detp_neg_one_one, zero_add] at h0

Premises used: Matrix.detp_neg_one_one, Matrix.detp_one_one, zero_add
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n_1 : Type u_1
m : Type u_2
R : Type u_3
inst : Fintype m
inst_1 : Fintype n_1
inst_2 : DecidableEq m
inst_3 : DecidableEq n_1
inst_4 : CommSemiring R
s : ℤˣ
A_1 B_1 : Matrix n_1 n_1 R
i j : n_1
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
⊢ B * (A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B)) = B * (detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B)

Tactic:
replace h := congr(B * $(detp_smul_adjp hAB))
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n_1 : Type u_1
m : Type u_2
R : Type u_3
inst : Fintype m
inst_1 : Fintype n_1
inst_2 : DecidableEq m
inst_3 : DecidableEq n_1
inst_4 : CommSemiring R
s : ℤˣ
A_1 B_1 : Matrix n_1 n_1 R
i j : n_1
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h : B * (A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B)) = B * (detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B)
⊢ B * A + (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B)) =
    detp 1 A • (B * adjp 1 B) + detp (-1) A • (B * adjp (-1) B)

Tactic:
simp only [mul_add, Matrix.mul_smul] at h

Premises used: Matrix.mul_smul, mul_add
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n_1 : Type u_1
m : Type u_2
R : Type u_3
inst : Fintype m
inst_1 : Fintype n_1
inst_2 : DecidableEq m
inst_3 : DecidableEq n_1
inst_4 : CommSemiring R
s : ℤˣ
A_1 B_1 : Matrix n_1 n_1 R
i j : n_1
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A + (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B)) =
    detp 1 A • (B * adjp 1 B) + detp (-1) A • (B * adjp (-1) B)
⊢ B * A + (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B)) +
      HSMul.hSMul (β := Matrix (Fin n) (Fin n) R) (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) 1 =
    detp 1 A • (B * adjp 1 B) + detp (-1) A • (B * adjp (-1) B) +
      HSMul.hSMul (β := Matrix (Fin n) (Fin n) R) (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) 1

Tactic:
replace h := congr($h + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • 1)
-- Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse
Goal:
n_1 : Type u_1
m : Type u_2
R : Type u_3
inst : Fintype m
inst_1 : Fintype n_1
inst_2 : DecidableEq m
inst_3 : DecidableEq n_1
inst_4 : CommSemiring R
s : ℤˣ
A_1 B_1 : Matrix n_1 n_1 R
i j : n_1
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A + (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B)) +
      HSMul.hSMul (β := Matrix (Fin n) (Fin n) R) (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) 1 =
    detp 1 A • (B * adjp 1 B) + detp (-1) A • (B * adjp (-1) B) +
      HSMul.hSMul (β := Matrix (Fin n) (Fin n) R) (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) 1
⊢ B * A + (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B)) +
      (detp 1 A • HSMul.hSMul (β := Matrix (Fin n) (Fin n) R) (detp (-1) B) 1 +
        detp (-1) A • HSMul.hSMul (β := Matrix (Fin n) (Fin n) R) (detp 1 B) 1) =
    detp 1 A • (B * adjp 1 B) + detp (-1) A • (B * adjp (-1) B) +
      (detp 1 A • HSMul.hSMul (β := Matrix (Fin n) (Fin n) R) (detp (-1) B) 1 +
        detp (-1) A • HSMul.hSMul (β := Matrix (Fin n) (Fin n) R) (detp 1 B) 1)

Tactic:
simp_rw [add_smul, ← smul_smul] at h

Premises used: smul_smul, add_smul
-- 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
h : B * A = 1
⊢ IsUnit A

Tactic:
.of_mul_eq_one_right _ h

Premises used: IsUnit.of_mul_eq_one_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 : Matrix n n R
⊢ (∃ (B : Matrix n n R), B * A = 1) ↔ IsUnit A

Tactic:
isUnit_iff_exists_inv'.symm

Premises used: Iff.symm, isUnit_iff_exists_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
h : A * B = 1
⊢ IsUnit A

Tactic:
.of_mul_eq_one _ h

Premises used: IsUnit.of_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 : Matrix n n R
⊢ (∃ (B : Matrix n n R), A * B = 1) ↔ IsUnit A

Tactic:
isUnit_iff_exists_inv.symm

Premises used: isUnit_iff_exists_inv, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
N₂ : Type u_10
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
ι : Type u_15
inst : Semiring R₁
inst_1 : Semiring S₁
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid N₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₂ S₁ N₂
inst_8 : Fintype n
inst_9 : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
f : Matrix n m N₂
x x_1 : n → R₁
x_2 : m → R₂
⊢ (fun (v : n → R₁) (w : m → R₂) ↦
        (∑ i : n, ∑ j : m, ((σ₂ : (a : R₂) → S₂) (w j) : S₂) •> ((σ₁ : (a : R₁) → S₁) (v i) : S₁) •> f i j : N₂))
      (x + x_1) x_2 =
    HAdd.hAdd (α := N₂)
      ((fun (v : n → R₁) (w : m → R₂) ↦
          (∑ i : n, ∑ j : m, ((σ₂ : (a : R₂) → S₂) (w j) : S₂) •> ((σ₁ : (a : R₁) → S₁) (v i) : S₁) •> f i j : N₂))
        x x_2)
      ((fun (v : n → R₁) (w : m → R₂) ↦
          (∑ i : n, ∑ j : m, ((σ₂ : (a : R₂) → S₂) (w j) : S₂) •> ((σ₁ : (a : R₁) → S₁) (v i) : S₁) •> f i j : N₂))
        x_1 x_2)

Tactic:
simp only [Pi.add_apply, map_add, smul_add, sum_add_distrib, add_smul]

Premises used: Finset.sum_add_distrib, map_add, Pi.add_apply, add_smul, smul_add
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
N₂ : Type u_10
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
ι : Type u_15
inst : Semiring R₁
inst_1 : Semiring S₁
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid N₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₂ S₁ N₂
inst_8 : Fintype n
inst_9 : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
f : Matrix n m N₂
c : R₁
v : n → R₁
w : m → R₂
⊢ (fun (v : n → R₁) (w : m → R₂) ↦
        (∑ i : n, ∑ j : m, ((σ₂ : (a : R₂) → S₂) (w j) : S₂) •> ((σ₁ : (a : R₁) → S₁) (v i) : S₁) •> f i j : N₂))
      (c •> v) w =
    ((σ₁ : (a : R₁) → S₁) c : S₁) •>
      (fun (v : n → R₁) (w : m → R₂) ↦
          (∑ i : n, ∑ j : m, ((σ₂ : (a : R₂) → S₂) (w j) : S₂) •> ((σ₁ : (a : R₁) → S₁) (v i) : S₁) •> f i j : N₂))
        v w

Tactic:
simp only [Pi.smul_apply, smul_sum, smul_eq_mul, σ₁.map_mul, ← smul_comm _ (σ₁ c), mul_smul]

Premises used: Finset.smul_sum, RingHom.map_mul, smul_eq_mul, SMulCommClass.smul_comm, DFunLike.coe, SemigroupAction.mul_smul, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
N₂ : Type u_10
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
ι : Type u_15
inst : Semiring R₁
inst_1 : Semiring S₁
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid N₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₂ S₁ N₂
inst_8 : Fintype n
inst_9 : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
f : Matrix n m N₂
x : n → R₁
x_1 x_2 : m → R₂
⊢ (fun (v : n → R₁) (w : m → R₂) ↦
        (∑ i : n, ∑ j : m, ((σ₂ : (a : R₂) → S₂) (w j) : S₂) •> ((σ₁ : (a : R₁) → S₁) (v i) : S₁) •> f i j : N₂))
      x (x_1 + x_2) =
    HAdd.hAdd (α := N₂)
      ((fun (v : n → R₁) (w : m → R₂) ↦
          (∑ i : n, ∑ j : m, ((σ₂ : (a : R₂) → S₂) (w j) : S₂) •> ((σ₁ : (a : R₁) → S₁) (v i) : S₁) •> f i j : N₂))
        x x_1)
      ((fun (v : n → R₁) (w : m → R₂) ↦
          (∑ i : n, ∑ j : m, ((σ₂ : (a : R₂) → S₂) (w j) : S₂) •> ((σ₁ : (a : R₁) → S₁) (v i) : S₁) •> f i j : N₂))
        x x_2)

Tactic:
simp only [Pi.add_apply, map_add, add_smul, sum_add_distrib]

Premises used: Finset.sum_add_distrib, map_add, Pi.add_apply, add_smul
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
N₂ : Type u_10
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
ι : Type u_15
inst : Semiring R₁
inst_1 : Semiring S₁
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid N₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₂ S₁ N₂
inst_8 : Fintype n
inst_9 : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
f : Matrix n m N₂
x : R₂
v : n → R₁
w : m → R₂
⊢ (fun (v : n → R₁) (w : m → R₂) ↦
        (∑ i : n, ∑ j : m, ((σ₂ : (a : R₂) → S₂) (w j) : S₂) •> ((σ₁ : (a : R₁) → S₁) (v i) : S₁) •> f i j : N₂))
      v (x •> w) =
    ((σ₂ : (a : R₂) → S₂) x : S₂) •>
      (fun (v : n → R₁) (w : m → R₂) ↦
          (∑ i : n, ∑ j : m, ((σ₂ : (a : R₂) → S₂) (w j) : S₂) •> ((σ₁ : (a : R₁) → S₁) (v i) : S₁) •> f i j : N₂))
        v w

Tactic:
simp only [Pi.smul_apply, smul_eq_mul, map_mul, mul_smul, smul_sum]

Premises used: map_mul, Finset.smul_sum, smul_eq_mul, SemigroupAction.mul_smul, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : Semiring R₁
inst_1 : Semiring S₁
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid N₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₂ S₁ N₂
inst_8 : Fintype n
inst_9 : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_10 : DecidableEq n
inst_11 : DecidableEq m
f : Matrix n m N₂
i : n
j : m
rw :
  ∑ i_1 : n,
      ∑ j_1 : m,
        ((σ₂ : (a : R₂) → S₂) (Pi.single (M := fun (a : m) ↦ R₂) j 1 j_1 : R₂) : S₂) •>
          ((σ₁ : (a : R₁) → S₁) (Pi.single (M := fun (a : n) ↦ R₁) i 1 i_1 : R₁) : S₁) •> f i_1 j_1 =
    f i j
⊢ (((toLinearMap₂'Aux σ₁ σ₂ f : (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂) (Pi.single (M := fun (a : n) ↦ R₁) i 1) :
          (m → R₂) →ₛₗ[σ₂] N₂) :
        (a : m → R₂) → N₂)
      (Pi.single (M := fun (a : m) ↦ R₂) j 1) =
    f i j

Tactic:
rw [Matrix.toLinearMap₂'Aux, mk₂'ₛₗ_apply]

Premises used: LinearMap.mk₂'ₛₗ_apply, Matrix.toLinearMap₂'Aux
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : Semiring R₁
inst_1 : Semiring S₁
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid N₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₂ S₁ N₂
inst_8 : Fintype n
inst_9 : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_10 : DecidableEq n
inst_11 : DecidableEq m
f : Matrix n m N₂
i : n
j : m
simp_rw : ∑ x : n, (if i = x then 1 else 0) •> ∑ x_1 : m, (if j = x_1 then 1 else 0) •> f x x_1 = f i j
⊢ ∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j' = f i j

Tactic:
simp_rw [← Finset.smul_sum]

Premises used: Finset.smul_sum
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : Semiring R₁
inst_1 : Semiring S₁
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid N₂
inst_5 : Module S₁ N₂
inst_6 : Module S₂ N₂
inst_7 : SMulCommClass S₂ S₁ N₂
inst_8 : Fintype n
inst_9 : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_10 : DecidableEq n
inst_11 : DecidableEq m
f : Matrix n m N₂
i : n
j : m
⊢ ∑ x : n, (if i = x then 1 else 0) •> ∑ x_1 : m, (if j = x_1 then 1 else 0) •> f x x_1 = f i j

Tactic:
simp only [ite_smul, one_smul, zero_smul, sum_ite_eq, mem_univ, ↓reduceIte]

Premises used: Finset.mem_univ, one_smul, zero_smul, reduceIte, ite_smul, Finset.sum_ite_eq