-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
R : Type u_1
inst : Semiring R
simp_rw :
  (∀ (n m : ℕ) (f : (Fin n → R) →ₗ[R] Fin m → R) (g : (Fin m → R) →ₗ[R] Fin n → R), f ∘ₗ g = 1 → m ≤ n) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
simp_rw₁ :
  (∀ (n m : ℕ) (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      Eq (α := (Fin m → R) →ₗ[R] Fin m → R)
          ((LinearEquiv.toEquiv toLinearMapRight' : (a : Matrix (Fin n) (Fin m) R) → (Fin n → R) →ₗ[R] Fin m → R) a ∘ₗ
            (LinearEquiv.toEquiv toLinearMapRight' : (a : Matrix (Fin m) (Fin n) R) → (Fin m → R) →ₗ[R] Fin n → R) a_1)
          1 →
        m ≤ n) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
simp_rw₂ :
  (∀ (n m : ℕ) (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      Eq (α := (Fin m → R) →ₗ[R] Fin m → R)
          ((toLinearMapRight' : (a : Matrix (Fin n) (Fin m) R) → (Fin n → R) →ₗ[R] Fin m → R) a ∘ₗ
            (toLinearMapRight' : (a : Matrix (Fin m) (Fin n) R) → (Fin m → R) →ₗ[R] Fin n → R) a_1)
          1 →
        m ≤ n) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
simp_rw₃ :
  (∀ (n m : ℕ) (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      Eq (α := (Fin m → R) →ₗ[R] Fin m → R)
          ((toLinearMapRight' : (a : Matrix (Fin m) (Fin m) R) → (Fin m → R) →ₗ[R] Fin m → R) (a_1 * a) :
            (Fin m → R) →ₗ[R] Fin m → R)
          (1 : (Fin m → R) →ₗ[R] Fin m → R) →
        m ≤ n) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
simp_rw₄ :
  (∀ (n m : ℕ) (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      Eq (α := (Fin m → R) →ₗ[R] Fin m → R)
          ((toLinearMapRight' : (a : Matrix (Fin m) (Fin m) R) → (Fin m → R) →ₗ[R] Fin m → R) (a_1 * a) :
            (Fin m → R) →ₗ[R] Fin m → R)
          (LinearMap.id : (Fin m → R) →ₗ[R] Fin m → R) →
        m ≤ n) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
simp_rw₅ :
  (∀ (n m : ℕ) (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      Eq (α := (Fin m → R) →ₗ[R] Fin m → R)
          ((toLinearMapRight' : (a : Matrix (Fin m) (Fin m) R) → (Fin m → R) →ₗ[R] Fin m → R) (a_1 * a) :
            (Fin m → R) →ₗ[R] Fin m → R)
          ((toLinearMapRight' : (a : Matrix (Fin m) (Fin m) R) → (Fin m → R) →ₗ[R] Fin m → R) 1 :
            (Fin m → R) →ₗ[R] Fin m → R) →
        m ≤ n) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
⊢ RankCondition R ↔ ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n

Tactic:
simp_rw [rankCondition_iff_le_of_comp_eq_one, ← toLinearMapRight'.toEquiv
    |>.forall_congr_right, LinearEquiv.coe_toEquiv, ← toLinearMapRight'_mul,
    Module.End.one_eq_id, ← toLinearMapRight'_one, toLinearMapRight'.injective.eq_iff]

Premises used: LinearEquiv.coe_toEquiv, Matrix.toLinearMapRight'_mul, Matrix.toLinearMapRight', Module.End.one_eq_id, rankCondition_iff_le_of_comp_eq_one, Function.Injective.eq_iff, LinearEquiv.toEquiv, LinearEquiv.injective, Equiv.forall_congr_right, Matrix.toLinearMapRight'_one