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 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
    (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))
have 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)))
Tactic: apply IsAddUnit.smul_right
-- 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 : Membership.mem (γ := Finset n) (singleton (α := n) ((τ⁻¹ : (a : n) → n) j : n))ᶜ l
⊢ 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)))
have 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)
Tactic: have h0 : ∀ k, k ∈ ({τ⁻¹ j} : Finset n)ᶜ ↔ τ k ∈ ({j} : Finset n)ᶜ := by
    simp [inv_def, eq_symm_apply]
-- 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
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
    (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)))
have 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))))
Tactic: rw [← prod_equiv τ h0 fun _ _ ↦ rfl, ← prod_mul_distrib, ← mul_prod_erase _ _ hl2, ← smul_eq_mul]
-- 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
hAB : A * B = 1
⊢ detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B
have 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)
Tactic: have key := congr(A * $(mul_adjp_add_detp B))
-- 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
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)
⊢ detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B
have key₁ : 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
Cleared hypotheses: key
-- 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
hAB : A * B = 1
key : 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
have rwa : adjp (-1) B + detp 1 B • A = detp (-1) B • A + adjp 1 B
Tactic: rwa [add_comm, eq_comm, 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 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
⊢ detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B
have rwa₁ : detp (-1) B • A + adjp 1 B = adjp (-1) B + detp 1 B • A
Tactic: rwa [add_comm, eq_comm, add_comm]
-- 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
hAB : A * B = 1
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
have 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)
Tactic: have h0 := detp_mul A B
-- 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
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)
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
have 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
Tactic: rw [hAB, detp_one_one, detp_neg_one_one, zero_add] at h0
Cleared hypotheses: h0
-- 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
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
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
have h : detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B
Tactic: have h := detp_smul_add_adjp hAB
-- 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
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
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
have 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)
Tactic: replace h := congr(detp 1 A • $h + detp (-1) A • $h.symm)
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
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)
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
have h₁ : (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
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
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 + 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)
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
have rwa : ∀
  (h :
    (detp 1 A * detp 1 B) • A + (detp (-1) A * detp (-1) B) • A + (detp 1 A • adjp (-1) B + 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)),
  A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
Tactic: rwa [add_add_add_comm, ← add_smul, add_add_add_comm, ← add_smul, ← h0, add_smul, one_smul,
    add_comm A, add_assoc, ((isAddUnit_detp_mul_detp hAB).smul_right _).add_right_inj] 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
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 + 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)
rwa :
  ∀
    (h :
      (detp 1 A * detp 1 B) • A + (detp (-1) A * detp (-1) B) • A + (detp 1 A • adjp (-1) B + 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)),
    A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
have rwa₁ : ∀
  (h :
    (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B) • A + (detp 1 A • adjp (-1) B + 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)),
  A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
Tactic: rwa [add_add_add_comm, ← add_smul, add_add_add_comm, ← add_smul, ← h0, add_smul, one_smul,
    add_comm A, add_assoc, ((isAddUnit_detp_mul_detp hAB).smul_right _).add_right_inj] 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
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 + 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)
rwa :
  ∀
    (h :
      (detp 1 A * detp 1 B) • A + (detp (-1) A * detp (-1) B) • A + (detp 1 A • adjp (-1) B + 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)),
    A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
rwa₁ :
  ∀
    (h :
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B) • A + (detp 1 A • adjp (-1) B + 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)),
    A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
have rwa₂ : ∀
  (h :
    (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B) • A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) =
      (detp 1 A * detp (-1) B) • A + (detp (-1) A * detp 1 B) • A + (detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B)),
  A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
Tactic: rwa [add_add_add_comm, ← add_smul, add_add_add_comm, ← add_smul, ← h0, add_smul, one_smul,
    add_comm A, add_assoc, ((isAddUnit_detp_mul_detp hAB).smul_right _).add_right_inj] 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
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 + 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)
rwa :
  ∀
    (h :
      (detp 1 A * detp 1 B) • A + (detp (-1) A * detp (-1) B) • A + (detp 1 A • adjp (-1) B + 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)),
    A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
rwa₁ :
  ∀
    (h :
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B) • A + (detp 1 A • adjp (-1) B + 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)),
    A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
rwa₂ :
  ∀
    (h :
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B) • A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) =
        (detp 1 A * detp (-1) B) • A + (detp (-1) A * detp 1 B) • A +
          (detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B)),
    A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
have rwa₃ : ∀
  (h :
    (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B) • A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) =
      (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • A + (detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B)),
  A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
Tactic: rwa [add_add_add_comm, ← add_smul, add_add_add_comm, ← add_smul, ← h0, add_smul, one_smul,
    add_comm A, add_assoc, ((isAddUnit_detp_mul_detp hAB).smul_right _).add_right_inj] 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
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 + 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)
rwa :
  ∀
    (h :
      (detp 1 A * detp 1 B) • A + (detp (-1) A * detp (-1) B) • A + (detp 1 A • adjp (-1) B + 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)),
    A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
rwa₁ :
  ∀
    (h :
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B) • A + (detp 1 A • adjp (-1) B + 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)),
    A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
rwa₂ :
  ∀
    (h :
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B) • A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) =
        (detp 1 A * detp (-1) B) • A + (detp (-1) A * detp 1 B) • A +
          (detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B)),
    A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
rwa₃ :
  ∀
    (h :
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B) • A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) =
        (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • A + (detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B)),
    A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
have rwa₄ : ∀
  (h :
    (1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B)) • A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) =
      (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • A + (detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B)),
  A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
Tactic: rwa [add_add_add_comm, ← add_smul, add_add_add_comm, ← add_smul, ← h0, add_smul, one_smul,
    add_comm A, add_assoc, ((isAddUnit_detp_mul_detp hAB).smul_right _).add_right_inj] 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
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 + 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)
rwa :
  ∀
    (h :
      (detp 1 A * detp 1 B) • A + (detp (-1) A * detp (-1) B) • A + (detp 1 A • adjp (-1) B + 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)),
    A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
rwa₁ :
  ∀
    (h :
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B) • A + (detp 1 A • adjp (-1) B + 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)),
    A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
rwa₂ :
  ∀
    (h :
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B) • A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) =
        (detp 1 A * detp (-1) B) • A + (detp (-1) A * detp 1 B) • A +
          (detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B)),
    A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
rwa₃ :
  ∀
    (h :
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B) • A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) =
        (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • A + (detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B)),
    A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
rwa₄ :
  ∀
    (h :
      (1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B)) • A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) =
        (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • A + (detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B)),
    A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
have rwa₅ : ∀
  (h :
    HSMul.hSMul (α := R) 1 A + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • A +
        (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) =
      (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • A + (detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B)),
  A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
Tactic: rwa [add_add_add_comm, ← add_smul, add_add_add_comm, ← add_smul, ← h0, add_smul, one_smul,
    add_comm A, add_assoc, ((isAddUnit_detp_mul_detp hAB).smul_right _).add_right_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (goal)
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
have refine : ∀ (n : ℕ) {A B : Matrix (Fin n) (Fin n) R} (hAB : A * B = 1), B * A = 1
Tactic: refine ⟨fun n ↦ ⟨fun {A B} hAB ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (hypothesis)
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
⊢ B * A = 1
have 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)
Tactic: have h0 := detp_mul A B
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (hypothesis)
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)
⊢ B * A = 1
have 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
Tactic: rw [hAB, detp_one_one, detp_neg_one_one, zero_add] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SemiringInverse (hypothesis)
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 = 1
have 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)
Tactic: replace h := congr(B * $(detp_smul_adjp hAB))