awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
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 : ℤ)) : ℚ)
rw₁₂ rw₁₃ : Eq (α := ℚ) (↑((A i j).num * (↑k : ℤ)) : ℚ) (↑((A i j).num * (↑k : ℤ)) : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑(A.num i j) : ℚ) (↑A.den : ℚ) = A i j

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]

Premises used: Iff.mpr, Int.cast_natCast, mul_assoc, Matrix.map_apply, Matrix.smul_apply, Matrix.den_ne_zero, Matrix.num, Int.cast_mul, div_eq_iff, Nat.cast_mul, Rat.mul_den_eq_num, mul_comm, smul_eq_mul, Rat.num_intCast, Nat.cast_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
a : ∀ (i : m) (j : n), HSMul.hSMul (α := ℚ) (β := Matrix m n ℚ) (↑A.den : ℚ)⁻¹ (A.num.map Int.cast) i j = A i j
⊢ HSMul.hSMul (α := ℚ) (β := Matrix m n ℚ) (↑A.den : ℚ)⁻¹ (A.num.map Int.cast) = A

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
i : m
j : n
⊢ HSMul.hSMul (α := ℚ) (β := Matrix m n ℚ) (↑A.den : ℚ)⁻¹ (A.num.map Int.cast) i j = A i j

Tactic:
simp [← Matrix.num_div_den A, div_eq_inv_mul]

Premises used: Matrix.num_div_den, div_eq_inv_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
⊢ ∀ (c : ℕ), (-A).den ∣ c ↔ A.den ∣ c

Tactic:
simp [den_dvd_iff]

Premises used: Matrix.den_dvd_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
a : ∀ (i : m) (j : n), (-A).num i j = (-A.num) i j
⊢ (-A).num = -A.num

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
i : m
j : n
⊢ (-A).num i j = (-A.num) i j

Tactic:
simp [Matrix.num]

Premises used: Matrix.num
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
x : ℕ
⊢ Aᵀ.den ∣ x ↔ A.den ∣ x

Tactic:
simpa [den_dvd_iff] using forall_comm

Premises used: forall_comm, Matrix.den_dvd_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
a : ∀ (i : n) (j : m), Aᵀ.num i j = A.numᵀ i j
⊢ Aᵀ.num = A.numᵀ

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
i : n
j : m
⊢ Aᵀ.num i j = A.numᵀ i j

Tactic:
simp [Matrix.num]

Premises used: Matrix.num
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℤ
⊢ Matrix.den (A.map Int.cast) = 1

Tactic:
simp [← Nat.dvd_one, Matrix.den_dvd_iff]

Premises used: Nat.dvd_one, Matrix.den_dvd_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℤ
⊢ Matrix.num (A.map Int.cast) = A

Tactic:
simp [Matrix.num, Function.comp_def]

Premises used: Function.comp_def, Matrix.num
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℕ
⊢ Matrix.den (A.map Nat.cast) = 1

Tactic:
simp [← Nat.dvd_one, Matrix.den_dvd_iff]

Premises used: Nat.dvd_one, Matrix.den_dvd_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℕ
⊢ Matrix.num (A.map Nat.cast) = A.map Nat.cast

Tactic:
simp [Matrix.num, Function.comp_def]

Premises used: Function.comp_def, Matrix.num
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
inst : Fintype m
inst_1 : DecidableEq m
a : ℕ
⊢ Matrix.den.{u_1, u_1} (m := m) (n := m) (↑a : Matrix m m ℚ) = 1

Tactic:
simpa [← diagonal_natCast] using den_map_natCast (a : Matrix m m ℕ)

Premises used: Matrix.diagonal_natCast, Nat.cast, Matrix.den_map_natCast
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
inst : Fintype m
inst_1 : DecidableEq m
a : ℕ
⊢ Eq.{u_1 + 1} (α := Matrix m m ℤ) (Matrix.num (↑a : Matrix m m ℚ)) (↑a : Matrix m m ℤ)

Tactic:
simpa [← diagonal_natCast] using num_map_natCast (a : Matrix m m ℕ)

Premises used: Matrix.diagonal_natCast, Nat.cast, Matrix.num_map_natCast
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
inst : Fintype m
inst_1 : DecidableEq m
a : ℕ
inst_2 : a.AtLeastTwo
⊢ Matrix.den.{u_1, u_1} (m := m) (n := m) (OfNat.ofNat a) = 1

Tactic:
den_natCast a

Premises used: Matrix.den_natCast
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
inst : Fintype m
inst_1 : DecidableEq m
a : ℕ
inst_2 : a.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := Matrix m m ℤ) (Matrix.num (OfNat.ofNat a)) (↑a : Matrix m m ℤ)

Tactic:
num_natCast a

Premises used: Matrix.num_natCast
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
inst : Fintype m
inst_1 : DecidableEq m
a : ℤ
⊢ Matrix.den.{u_1, u_1} (m := m) (n := m) (↑a : Matrix m m ℚ) = 1

Tactic:
simpa [← diagonal_intCast] using den_map_intCast (a : Matrix m m ℤ)

Premises used: Int.cast, Matrix.den_map_intCast, Matrix.diagonal_intCast
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
inst : Fintype m
inst_1 : DecidableEq m
a : ℤ
⊢ Eq.{u_1 + 1} (α := Matrix m m ℤ) (Matrix.num (↑a : Matrix m m ℚ)) (↑a : Matrix m m ℤ)

Tactic:
simpa [← diagonal_intCast] using num_map_intCast (a : Matrix m m ℤ)

Premises used: Int.cast, Matrix.num_map_intCast, Matrix.diagonal_intCast
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
⊢ Matrix.den.{u_1, u_2} (m := m) (n := n) 0 = 1

Tactic:
den_map_natCast 0

Premises used: Matrix.den_map_natCast, Matrix.map, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
⊢ Eq (α := Matrix m n ℤ) (Matrix.num 0) 0

Tactic:
num_map_natCast 0

Premises used: Matrix.num_map_natCast, Matrix.map, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
inst : Fintype m
inst_1 : DecidableEq m
⊢ Matrix.den.{u_1, u_1} (m := m) (n := m) 1 = 1

Tactic:
den_natCast 1

Premises used: OfNat.ofNat, Matrix.den_natCast
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
inst : Fintype m
inst_1 : DecidableEq m
⊢ Eq.{u_1 + 1} (α := Matrix m m ℤ) (Matrix.num 1) 1

Tactic:
num_natCast 1

Premises used: Matrix.num_natCast, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
R : Type u_1
inst : Semiring R
inst_1 : OrzechProperty R
⊢ IsStablyFiniteRing R

Tactic:
isStablyFiniteRing_iff_injective_of_surjective.mpr fun _ ↦
    OrzechProperty.injective_of_surjective_endomorphism

Premises used: Iff.mpr, isStablyFiniteRing_iff_injective_of_surjective, OrzechProperty.injective_of_surjective_endomorphism
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
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)
by_contra! : ∀ (lt : n < m), False
⊢ m ≤ n

Tactic:
by_contra! lt
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
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 ⋯)
⊢ 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)
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
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)
⊢ 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
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
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)
have : ∀ (i : ℕ) (lt_1 : i < n) (eq : Fin.castLE ⋯ (⟨i, lt_1⟩ : Fin n) = ⟨n, lt⟩), False
⊢ False

Tactic:
have ⟨⟨i, lt⟩, eq⟩ := injective_comp_right_iff_surjective.mp this ⟨n, lt⟩
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
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_1 : 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)
i : ℕ
lt : i < n
eq : Fin.castLE ⋯ (⟨i, lt⟩ : Fin n) = ⟨n, lt_1⟩
⊢ False

Tactic:
lt.ne congr($eq)

Premises used: congrArg, id, Fin.val, LT.lt.ne
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
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_1 : 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)
i : ℕ
lt : i < n
eq : Fin.castLE ⋯ (⟨i, lt⟩ : Fin n) = ⟨n, lt_1⟩
⊢ False

Tactic:
exact lt.ne congr($eq)

Premises used: congrArg, id, Fin.val, LT.lt.ne
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
R : Type u_1
inst : Semiring R
⊢ RankCondition R ↔ ∀ (n m : ℕ) (f : (Fin n → R) →ₗ[R] Fin m → R) (g : (Fin m → R) →ₗ[R] Fin n → R), f ∘ₗ g = 1 → m ≤ n

Tactic:
(rankCondition_iff R).trans ⟨fun h _ _ f _ eq ↦ h f (surjective_of_comp_eq_id _ _ eq),
    fun h _ _ _ hf ↦ have ⟨_, eq⟩ := Module.projective_lifting_property _ .id hf; h _ _ _ _ eq⟩

Premises used: LinearMap.id, rankCondition_iff, LE.le, LinearMap.surjective_of_comp_eq_id, _private.0.rankCondition_iff_le_of_comp_eq_one.match_1, Iff.intro, Iff.trans, Module.projective_lifting_property
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
R : Type u_1
inst : Semiring R
h : ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), f * g = 1 → g * f = 1 → n = m
n m : ℕ
e : (Fin n → R) ≃ₗ[R] Fin m → R
⊢ HMul.hMul (α := Matrix (Fin n) (Fin m) R) (β := Matrix (Fin m) (Fin n) R)
      ((toMatrixRight' : (a : (Fin n → R) →ₗ[R] Fin m → R) → Matrix (Fin n) (Fin m) R)
          (↑e : (Fin n → R) →ₗ[R] Fin m → R) :
        Matrix (Fin n) (Fin m) R)
      ((toMatrixRight' : (a : (Fin m → R) →ₗ[R] Fin n → R) → Matrix (Fin m) (Fin n) R)
          (↑e.symm : (Fin m → R) →ₗ[R] Fin n → R) :
        Matrix (Fin m) (Fin n) R) =
    1

Tactic:
simp [← toMatrixRight'_comp]

Premises used: LinearMap.toMatrixRight'_comp
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
R : Type u_1
inst : Semiring R
h : ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), f * g = 1 → g * f = 1 → n = m
n m : ℕ
e : (Fin n → R) ≃ₗ[R] Fin m → R
⊢ HMul.hMul (α := Matrix (Fin m) (Fin n) R) (β := Matrix (Fin n) (Fin m) R)
      ((toMatrixRight' : (a : (Fin m → R) →ₗ[R] Fin n → R) → Matrix (Fin m) (Fin n) R)
          (↑e.symm : (Fin m → R) →ₗ[R] Fin n → R) :
        Matrix (Fin m) (Fin n) R)
      ((toMatrixRight' : (a : (Fin n → R) →ₗ[R] Fin m → R) → Matrix (Fin n) (Fin m) R)
          (↑e : (Fin n → R) →ₗ[R] Fin m → R) :
        Matrix (Fin n) (Fin m) R) =
    1

Tactic:
simp [← toMatrixRight'_comp]

Premises used: LinearMap.toMatrixRight'_comp
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
R : Type u_1
inst : Semiring R
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
⊢ RankCondition.{u_1} Rᵐᵒᵖ ↔ RankCondition R

Tactic:
simp_rw [rankCondition_iff_matrix, ← opEquiv.mapMatrix.forall_congr_right,
    ← opEquiv.mapMatrix.symm.injective.eq_iff]

Premises used: MulOpposite.opEquiv, Equiv.mapMatrix, Function.Injective.eq_iff, rankCondition_iff_matrix, Equiv.injective, Equiv.symm, Equiv.forall_congr_right
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
R : Type u_1
inst : Semiring R
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
⊢ (∀ (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:
congr! 2 with n m
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
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

Tactic:
forall_comm.trans <| .trans (forall_congr' ?_) (transposeAddEquiv ..).forall_congr_right

Premises used: forall_comm, forall_congr', Iff.trans, AddEquiv.toEquiv, Equiv.forall_congr_right, Matrix.transposeAddEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
R : Type u_1
inst : Semiring R
n m : ℕ
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
⊢ (∀ (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:
refine forall_comm.trans <| .trans (forall_congr' ?_) (transposeAddEquiv ..).forall_congr_right

Premises used: forall_comm, Iff.trans
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
R : Type u_1
inst : Semiring R
n m : ℕ
⊢ ∀ (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:
fun f ↦ .trans (forall_congr' fun g ↦ ?_) (transposeAddEquiv ..).forall_congr_right

Premises used: forall_congr', Iff.trans, AddEquiv.toEquiv, Equiv.forall_congr_right, Fin, Matrix.transposeAddEquiv