awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Integer (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
i : m
j : n
k : ℕ
hk : A.den = (A i j).den * k
rw : HDiv.hDiv (α := ℚ) (↑((HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A).map Rat.num i j) : ℚ) (↑A.den : ℚ) = A i j
rw₁ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A i j).num : ℚ) (↑A.den : ℚ) = A i j
rw₂ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) (A i j)).num : ℚ) (↑A.den : ℚ) = A i j
rw₃ : HDiv.hDiv (α := ℚ) (↑((↑A.den : ℚ) * A i j).num : ℚ) (↑A.den : ℚ) = A i j
rw₄ : HDiv.hDiv (α := ℚ) (↑(A i j * (↑A.den : ℚ)).num : ℚ) (↑A.den : ℚ) = A i j
rw₅ : (↑(A i j * (↑A.den : ℚ)).num : ℚ) = A i j * (↑A.den : ℚ)
rw₆ : (↑(A i j * (↑((A i j).den * k) : ℚ)).num : ℚ) = A i j * (↑((A i j).den * k) : ℚ)
rw₇ :
  (↑(A i j * HMul.hMul (α := ℚ) (↑(A i j).den : ℚ) (↑k : ℚ)).num : ℚ) =
    A i j * HMul.hMul (α := ℚ) (↑(A i j).den : ℚ) (↑k : ℚ)
rw₈ : (↑(A i j * (↑(A i j).den : ℚ) * (↑k : ℚ)).num : ℚ) = A i j * (↑(A i j).den : ℚ) * (↑k : ℚ)
rw₉ : (↑(HMul.hMul (α := ℚ) (↑(A i j).num : ℚ) (↑k : ℚ)).num : ℚ) = HMul.hMul (α := ℚ) (↑(A i j).num : ℚ) (↑k : ℚ)
rw₁₀ :
  (↑(HMul.hMul (α := ℚ) (↑(A i j).num : ℚ) (↑(↑k : ℤ) : ℚ)).num : ℚ) =
    HMul.hMul (α := ℚ) (↑(A i j).num : ℚ) (↑(↑k : ℤ) : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑(A.num i j) : ℚ) (↑A.den : ℚ) = A i j
have rw₁₁ : Eq (α := ℚ) (↑(Rat.num (↑((A i j).num * (↑k : ℤ)) : ℚ)) : ℚ) (↑((A i j).num * (↑k : ℤ)) : ℚ)
Tactic: rw [Matrix.num, map_apply, smul_apply, smul_eq_mul, mul_comm,
    div_eq_iff <| Nat.cast_ne_zero.mpr A.den_ne_zero, hk, Nat.cast_mul, ← mul_assoc,
    Rat.mul_den_eq_num, ← Int.cast_natCast k, ← Int.cast_mul, Rat.num_intCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Integer (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
i : m
j : n
k : ℕ
hk : A.den = (A i j).den * k
rw : HDiv.hDiv (α := ℚ) (↑((HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A).map Rat.num i j) : ℚ) (↑A.den : ℚ) = A i j
rw₁ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A i j).num : ℚ) (↑A.den : ℚ) = A i j
rw₂ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) (A i j)).num : ℚ) (↑A.den : ℚ) = A i j
rw₃ : HDiv.hDiv (α := ℚ) (↑((↑A.den : ℚ) * A i j).num : ℚ) (↑A.den : ℚ) = A i j
rw₄ : HDiv.hDiv (α := ℚ) (↑(A i j * (↑A.den : ℚ)).num : ℚ) (↑A.den : ℚ) = A i j
rw₅ : (↑(A i j * (↑A.den : ℚ)).num : ℚ) = A i j * (↑A.den : ℚ)
rw₆ : (↑(A i j * (↑((A i j).den * k) : ℚ)).num : ℚ) = A i j * (↑((A i j).den * k) : ℚ)
rw₇ :
  (↑(A i j * HMul.hMul (α := ℚ) (↑(A i j).den : ℚ) (↑k : ℚ)).num : ℚ) =
    A i j * HMul.hMul (α := ℚ) (↑(A i j).den : ℚ) (↑k : ℚ)
rw₈ : (↑(A i j * (↑(A i j).den : ℚ) * (↑k : ℚ)).num : ℚ) = A i j * (↑(A i j).den : ℚ) * (↑k : ℚ)
rw₉ : (↑(HMul.hMul (α := ℚ) (↑(A i j).num : ℚ) (↑k : ℚ)).num : ℚ) = HMul.hMul (α := ℚ) (↑(A i j).num : ℚ) (↑k : ℚ)
rw₁₀ :
  (↑(HMul.hMul (α := ℚ) (↑(A i j).num : ℚ) (↑(↑k : ℤ) : ℚ)).num : ℚ) =
    HMul.hMul (α := ℚ) (↑(A i j).num : ℚ) (↑(↑k : ℤ) : ℚ)
rw₁₁ : Eq (α := ℚ) (↑(Rat.num (↑((A i j).num * (↑k : ℤ)) : ℚ)) : ℚ) (↑((A i j).num * (↑k : ℤ)) : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑(A.num i j) : ℚ) (↑A.den : ℚ) = A i j
have rw₁₂ : Eq (α := ℚ) (↑((A i j).num * (↑k : ℤ)) : ℚ) (↑((A i j).num * (↑k : ℤ)) : ℚ)
Tactic: rw [Matrix.num, map_apply, smul_apply, smul_eq_mul, mul_comm,
    div_eq_iff <| Nat.cast_ne_zero.mpr A.den_ne_zero, hk, Nat.cast_mul, ← mul_assoc,
    Rat.mul_den_eq_num, ← Int.cast_natCast k, ← Int.cast_mul, Rat.num_intCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Integer (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
⊢ HSMul.hSMul (α := ℚ) (β := Matrix m n ℚ) (↑A.den : ℚ)⁻¹ (A.num.map Int.cast) = A
have a : ∀ (i : m) (j : n), HSMul.hSMul (α := ℚ) (β := Matrix m n ℚ) (↑A.den : ℚ)⁻¹ (A.num.map Int.cast) i j = A i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Integer (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
⊢ (-A).num = -A.num
have a : ∀ (i : m) (j : n), (-A).num i j = (-A.num) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Integer (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
⊢ Aᵀ.num = A.numᵀ
have a : ∀ (i : n) (j : m), Aᵀ.num i j = A.numᵀ i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsStablyFiniteRing R
inst_2 : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Surjective (α := Fin n → R) (β := Fin m → R) (⇑f : (a : Fin n → R) → Fin m → R)
⊢ m ≤ n
have by_contra! : ∀ (lt : n < m), False
Tactic: by_contra! lt
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsStablyFiniteRing R
inst_2 : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Surjective (α := Fin n → R) (β := Fin m → R) (⇑f : (a : Fin n → R) → Fin m → R)
lt : n < m
p : (Fin m → R) →ₗ[R] Fin n → R := funLeft R R (Fin.castLE ⋯)
⊢ False
have hp : Surjective (α := Fin m → R) (β := Fin n → R) (⇑p : (a : Fin m → R) → Fin n → R)
Tactic: have hp : Surjective p := funLeft_surjective_of_injective _ _ _ (Fin.castLE_injective lt.le)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsStablyFiniteRing R
inst_2 : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Surjective (α := Fin n → R) (β := Fin m → R) (⇑f : (a : Fin n → R) → Fin m → R)
lt : n < m
p : (Fin m → R) →ₗ[R] Fin n → R := funLeft R R (Fin.castLE ⋯)
hp : Surjective (α := Fin m → R) (β := Fin n → R) (⇑p : (a : Fin m → R) → Fin n → R)
⊢ False
have this : Injective (α := Fin m → R) (β := Fin n → R) (⇑p : (a : Fin m → R) → Fin n → R)
Tactic: have : Injective p := .of_comp_right
      (Module.End.injective_of_surjective_fin (f := p ∘ₗ f) (hp.comp hf)) hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsStablyFiniteRing R
inst_2 : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Surjective (α := Fin n → R) (β := Fin m → R) (⇑f : (a : Fin n → R) → Fin m → R)
lt : n < m
p : (Fin m → R) →ₗ[R] Fin n → R := funLeft R R (Fin.castLE ⋯)
hp : Surjective (α := Fin m → R) (β := Fin n → R) (⇑p : (a : Fin m → R) → Fin n → R)
this : Injective (α := Fin m → R) (β := Fin n → R) (⇑p : (a : Fin m → R) → Fin n → R)
⊢ False
have have : ∀ (i : ℕ) (lt_1 : i < n) (eq : Fin.castLE sorry (⟨i, lt_1⟩ : Fin n) = ⟨n, lt⟩), False
Tactic: have ⟨⟨i, lt⟩, eq⟩ := injective_comp_right_iff_surjective.mp this ⟨n, lt⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber (goal)
Goal:
R : Type u_1
inst : Semiring R
⊢ RankCondition R ↔ ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber (goal)
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
⊢ RankCondition R ↔ ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber (goal)
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
⊢ RankCondition R ↔ ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber (goal)
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
⊢ RankCondition R ↔ ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber (goal)
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
⊢ RankCondition R ↔ ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber (goal)
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
⊢ RankCondition R ↔ ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber (goal)
Goal:
R : Type u_1
inst : Semiring R
⊢ RankCondition.{u_1} Rᵐᵒᵖ ↔ RankCondition R
have simp_rw : (∀ (n m : ℕ) (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
    Eq (α := Matrix (Fin m) (Fin m) R)
        ((Equiv.symm (Equiv.mapMatrix opEquiv) : (a : Matrix (Fin m) (Fin m) Rᵐᵒᵖ) → Matrix (Fin m) (Fin m) R)
            (HMul.hMul (α := Matrix (Fin m) (Fin n) Rᵐᵒᵖ) (β := Matrix (Fin n) (Fin m) Rᵐᵒᵖ)
              ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin m) (Fin n) Rᵐᵒᵖ) a_1 :
                Matrix (Fin m) (Fin n) Rᵐᵒᵖ)
              ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin n) (Fin m) R) → Matrix (Fin n) (Fin m) Rᵐᵒᵖ) a :
                Matrix (Fin n) (Fin m) Rᵐᵒᵖ)) :
          Matrix (Fin m) (Fin m) R)
        ((Equiv.symm (Equiv.mapMatrix opEquiv) : (a : Matrix (Fin m) (Fin m) Rᵐᵒᵖ) → Matrix (Fin m) (Fin m) R) 1 :
          Matrix (Fin m) (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
Tactic: simp_rw [rankCondition_iff_matrix, ← opEquiv.mapMatrix.forall_congr_right,
    ← opEquiv.mapMatrix.symm.injective.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber (goal)
Goal:
R : Type u_1
inst : Semiring R
⊢ (∀ (n m : ℕ) (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      Eq (α := Matrix (Fin m) (Fin m) R)
          ((Equiv.symm (Equiv.mapMatrix opEquiv) : (a : Matrix (Fin m) (Fin m) Rᵐᵒᵖ) → Matrix (Fin m) (Fin m) R)
              (HMul.hMul (α := Matrix (Fin m) (Fin n) Rᵐᵒᵖ) (β := Matrix (Fin n) (Fin m) Rᵐᵒᵖ)
                ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin m) (Fin n) Rᵐᵒᵖ) a_1 :
                  Matrix (Fin m) (Fin n) Rᵐᵒᵖ)
                ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin n) (Fin m) R) → Matrix (Fin n) (Fin m) Rᵐᵒᵖ) a :
                  Matrix (Fin n) (Fin m) Rᵐᵒᵖ)) :
            Matrix (Fin m) (Fin m) R)
          ((Equiv.symm (Equiv.mapMatrix opEquiv) : (a : Matrix (Fin m) (Fin m) Rᵐᵒᵖ) → Matrix (Fin m) (Fin m) R) 1 :
            Matrix (Fin m) (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
have a : ∀ (n m : ℕ),
  (∀ (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      Eq (α := Matrix (Fin m) (Fin m) R)
          ((Equiv.symm (Equiv.mapMatrix opEquiv) : (a : Matrix (Fin m) (Fin m) Rᵐᵒᵖ) → Matrix (Fin m) (Fin m) R)
              (HMul.hMul (α := Matrix (Fin m) (Fin n) Rᵐᵒᵖ) (β := Matrix (Fin n) (Fin m) Rᵐᵒᵖ)
                ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin m) (Fin n) Rᵐᵒᵖ) a_1 :
                  Matrix (Fin m) (Fin n) Rᵐᵒᵖ)
                ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin n) (Fin m) R) → Matrix (Fin n) (Fin m) Rᵐᵒᵖ) a :
                  Matrix (Fin n) (Fin m) Rᵐᵒᵖ)) :
            Matrix (Fin m) (Fin m) R)
          ((Equiv.symm (Equiv.mapMatrix opEquiv) : (a : Matrix (Fin m) (Fin m) Rᵐᵒᵖ) → Matrix (Fin m) (Fin m) R) 1 :
            Matrix (Fin m) (Fin m) R) →
        m ≤ n) ↔
    ∀ (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
Tactic: congr! 2 with n m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber (goal)
Goal:
R : Type u_1
inst : Semiring R
n m : ℕ
⊢ (∀ (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      Eq (α := Matrix (Fin m) (Fin m) R)
          ((Equiv.symm (Equiv.mapMatrix opEquiv) : (a : Matrix (Fin m) (Fin m) Rᵐᵒᵖ) → Matrix (Fin m) (Fin m) R)
              (HMul.hMul (α := Matrix (Fin m) (Fin n) Rᵐᵒᵖ) (β := Matrix (Fin n) (Fin m) Rᵐᵒᵖ)
                ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin m) (Fin n) Rᵐᵒᵖ) a_1 :
                  Matrix (Fin m) (Fin n) Rᵐᵒᵖ)
                ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin n) (Fin m) R) → Matrix (Fin n) (Fin m) Rᵐᵒᵖ) a :
                  Matrix (Fin n) (Fin m) Rᵐᵒᵖ)) :
            Matrix (Fin m) (Fin m) R)
          ((Equiv.symm (Equiv.mapMatrix opEquiv) : (a : Matrix (Fin m) (Fin m) Rᵐᵒᵖ) → Matrix (Fin m) (Fin m) R) 1 :
            Matrix (Fin m) (Fin m) R) →
        m ≤ n) ↔
    ∀ (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
have a : ∀ (a : Matrix (Fin m) (Fin n) R),
  (∀ (a_1 : Matrix (Fin n) (Fin m) R),
      Eq (α := Matrix (Fin m) (Fin m) R)
          ((Equiv.symm (Equiv.mapMatrix opEquiv) : (a : Matrix (Fin m) (Fin m) Rᵐᵒᵖ) → Matrix (Fin m) (Fin m) R)
              (HMul.hMul (α := Matrix (Fin m) (Fin n) Rᵐᵒᵖ) (β := Matrix (Fin n) (Fin m) Rᵐᵒᵖ)
                ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin m) (Fin n) Rᵐᵒᵖ) a :
                  Matrix (Fin m) (Fin n) Rᵐᵒᵖ)
                ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin n) (Fin m) R) → Matrix (Fin n) (Fin m) Rᵐᵒᵖ) a_1 :
                  Matrix (Fin n) (Fin m) Rᵐᵒᵖ)) :
            Matrix (Fin m) (Fin m) R)
          ((Equiv.symm (Equiv.mapMatrix opEquiv) : (a : Matrix (Fin m) (Fin m) Rᵐᵒᵖ) → Matrix (Fin m) (Fin m) R) 1 :
            Matrix (Fin m) (Fin m) R) →
        m ≤ n) ↔
    ∀ (g : Matrix (Fin m) (Fin n) R),
      HMul.hMul (β := Matrix (Fin n) (Fin m) R) g
            ((AddEquiv.toEquiv (transposeAddEquiv (Fin m) (Fin n) R) :
                  (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin n) (Fin m) R)
                a :
              Matrix (Fin n) (Fin m) R) =
          1 →
        m ≤ n
Tactic: refine forall_comm.trans <| .trans (forall_congr' ?_) (transposeAddEquiv ..).forall_congr_right