-- 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
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
rwa₆ :
  ∀
    (h :
      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
⊢ 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 + 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