awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
zero : ∀ (h_card : Fintype.card n = 0), A.adjugate.adjugate = A.det ^ HSub.hSub (α := ℕ) 0 2 • A
succ : ∀ (n' : ℕ) (h_card : Fintype.card n = n' + 1), A.adjugate.adjugate = A.det ^ (n' + 1 - 2) • A
⊢ A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A

Tactic:
rcases h_card : Fintype.card n with _ | n'

Premises used: Fintype.card
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
h_card : Fintype.card n = 0
⊢ A.adjugate.adjugate = A.det ^ HSub.hSub (α := ℕ) 0 2 • A

Tactic:
subsingleton [Fintype.card_eq_zero_iff.mp h_card]

Premises used: Fintype.card_eq_zero_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n' : ℕ
h_card : Fintype.card n = n' + 1
succ :
  ∀ (h_card : Fintype.card n = HAdd.hAdd (α := ℕ) 0 1), A.adjugate.adjugate = A.det ^ (HAdd.hAdd (α := ℕ) 0 1 - 2) • A
succ₁ : ∀ (n_1 : ℕ) (h_card : Fintype.card n = n_1 + 1 + 1), A.adjugate.adjugate = A.det ^ (n_1 + 1 + 1 - 2) • A
⊢ A.adjugate.adjugate = A.det ^ (n' + 1 - 2) • A

Tactic:
cases n'
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
h_card : Fintype.card n = HAdd.hAdd (α := ℕ) 0 1
⊢ A.adjugate.adjugate = A.det ^ (HAdd.hAdd (α := ℕ) 0 1 - 2) • A

Tactic:
(h h_card).elim

Premises used: False.elim
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
h_card : Fintype.card n = HAdd.hAdd (α := ℕ) 0 1
⊢ A.adjugate.adjugate = A.det ^ (HAdd.hAdd (α := ℕ) 0 1 - 2) • A

Tactic:
exact (h h_card).elim

Premises used: False.elim
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
succ : A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A
⊢ A.adjugate.adjugate = A.det ^ (n_1 + 1 + 1 - 2) • A

Tactic:
rw [← h_card]
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
succ : A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
⊢ A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A

Tactic:
suffices adjugate (adjugate A') = det A' ^ (Fintype.card n - 2) • A' by
    rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_adjugate, this,
      ← AlgHom.map_det, ← map_pow (MvPolynomial.aeval fun p : n × n ↦ A p.1 p.2),
      AlgHom.mapMatrix_apply, AlgHom.mapMatrix_apply, Matrix.map_smul' _ _ _ (map_mul _)]
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ Fintype.card n - 2 + 1 = Fintype.card n - 1

Tactic:
simp [h_card]
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ Fintype.card n - 2 + 1 = Fintype.card n - 1

Tactic:
have h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1 := by simp [h_card]
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
⊢ IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det

Tactic:
have is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) (det A') := fun x y =>
    mul_left_cancel₀ (det_mvPolynomialX_ne_zero n ℤ)
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
succ :
  Eq.{v + 1} (α := Matrix n n (MvPolynomial (n × n) ℤ))
    ((fun (x : Matrix n n (MvPolynomial (n × n) ℤ)) ↦ A'.det • x) A'.adjugate.adjugate)
    ((fun (x : Matrix n n (MvPolynomial (n × n) ℤ)) ↦ A'.det • x) (A'.det ^ (Fintype.card n - 2) • A'))
⊢ A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'

Tactic:
apply is_reg.matrix

Premises used: IsSMulRegular.matrix
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n_1 : ℕ
h_card : Fintype.card n = n_1 + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
succ : A'.det • A'.adjugate.adjugate = (A'.det * A'.det ^ (Fintype.card n - 2)) • A'
succ₁ : A'.det • A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2 + 1) • A'
succ₂ : A'.det • A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 1) • A'
succ₃ succ₄ : A'.det ^ (Fintype.card n - 1) • A' = A'.det ^ (Fintype.card n - 1) • A'
⊢ A'.det • A'.adjugate.adjugate = A'.det • A'.det ^ (Fintype.card n - 2) • A'

Tactic:
rw [smul_smul, ← pow_succ', h_card', det_smul_adjugate_adjugate]

Premises used: smul_smul, Matrix.det_smul_adjugate_adjugate, pow_succ'
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : Nontrivial n
⊢ A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A

Tactic:
adjugate_adjugate _ <| Fintype.one_lt_card.ne'

Premises used: Fintype.one_lt_card, Matrix.adjugate_adjugate, LT.lt.ne'
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
intro : ∀ (val : Fintype m), B i j ∈ K
⊢ B i j ∈ K

Tactic:
cases nonempty_fintype m

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
⊢ A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)

Tactic:
have hA' : A'.map K.subtype = A.submatrix id e := rfl
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
⊢ A.submatrix id (⇑e : (a : m) → n) * B.submatrix (⇑e : (a : m) → n) id = 1

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
⊢ IsUnit (M := Matrix m m L) (A.submatrix id (⇑e : (a : m) → n))

Tactic:
have h_unit : IsUnit (A.submatrix id e) :=
      .of_mul_eq_one (B.submatrix e id) (by simpa)
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
h_unit : IsUnit (M := Matrix m m L) (A.submatrix id (⇑e : (a : m) → n))
⊢ det (A.submatrix id (⇑e : (a : m) → n)) = (K.subtype : (a : ↥K) → L) A'.det

Tactic:
simp [A', K.subtype.map_det, map, submatrix]

Premises used: Subfield.subtype, Matrix.submatrix, RingHom.map_det, Matrix.map
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
h_unit : IsUnit (M := Matrix m m L) (A.submatrix id (⇑e : (a : m) → n))
⊢ det (A.submatrix id (⇑e : (a : m) → n)) = (K.subtype : (a : ↥K) → L) A'.det

Tactic:
have h_det : (A.submatrix id e).det = K.subtype A'.det := by
      simp [A', K.subtype.map_det, map, submatrix]
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
h_unit : IsUnit (M := Matrix m m L) (A.submatrix id (⇑e : (a : m) → n))
h_det : det (A.submatrix id (⇑e : (a : m) → n)) = (K.subtype : (a : ↥K) → L) A'.det
⊢ IsUnit A'

Tactic:
simpa [isUnit_iff_isUnit_det, h_det] using h_unit

Premises used: Matrix.isUnit_iff_isUnit_det
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
⊢ IsUnit A'

Tactic:
have hA : IsUnit A' := by
    have h_unit : IsUnit (A.submatrix id e) :=
      .of_mul_eq_one (B.submatrix e id) (by simpa)
    have h_det : (A.submatrix id e).det = K.subtype A'.det := by
      simp [A', K.subtype.map_det, map, submatrix]
    simpa [isUnit_iff_isUnit_det, h_det] using h_unit
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
hA : IsUnit A'
intro : ∀ (B' : Matrix.{u_1, u_1, u_3} m m ↥K) (hB : A' * B' = 1), B i j ∈ K
⊢ B i j ∈ K

Tactic:
obtain ⟨B', hB⟩ := isUnit_iff_exists_inv.mp hA

Premises used: isUnit_iff_exists_inv, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
hA : IsUnit A'
B' : Matrix.{u_1, u_1, u_3} m m ↥K
hB : A' * B' = 1
this : map (B'.submatrix (⇑e.symm : (a : n) → m) id) (⇑K.subtype : (a : ↥K) → L) = B
⊢ B i j ∈ K

Tactic:
simp [← this]
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
hA : IsUnit A'
B' : Matrix.{u_1, u_1, u_3} m m ↥K
hB : A' * B' = 1
intro : map (B'.submatrix (⇑e.symm : (a : n) → m) id) (⇑K.subtype : (a : ↥K) → L) = B
⊢ B i j ∈ K

Tactic:
suffices (B'.submatrix e.symm id).map K.subtype = B by simp [← this]
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
hA : IsUnit A'
B' : Matrix.{u_1, u_1, u_3} m m ↥K
hB : A' * B' = 1
⊢ Eq (α := Matrix m m L)
    ((fun (C : Matrix.{u_1, u_1, u_3} m m ↥K) ↦ (C.map (⇑K.subtype : (a : ↥K) → L) : Matrix m m L)) (A' * B'))
    ((fun (C : Matrix.{u_1, u_1, u_3} m m ↥K) ↦ (C.map (⇑K.subtype : (a : ↥K) → L) : Matrix m m L)) 1)

Tactic:
replace hB := congr_arg (fun C ↦ C.map K.subtype) hB
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
hA : IsUnit A'
B' : Matrix.{u_1, u_1, u_3} m m ↥K
hB :
  Eq (α := Matrix m m L)
    ((fun (C : Matrix.{u_1, u_1, u_3} m m ↥K) ↦ (C.map (⇑K.subtype : (a : ↥K) → L) : Matrix m m L)) (A' * B'))
    ((fun (C : Matrix.{u_1, u_1, u_3} m m ↥K) ↦ (C.map (⇑K.subtype : (a : ↥K) → L) : Matrix m m L)) 1)
⊢ HMul.hMul (α := Matrix m m L) (A'.map (⇑K.subtype : (a : ↥K) → L)) (B'.map (⇑K.subtype : (a : ↥K) → L)) =
    map (α := ↥K) 1 (⇑K.subtype : (a : ↥K) → L)

Tactic:
simp_rw [Matrix.map_mul] at hB

Premises used: Matrix.map_mul
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
hA : IsUnit A'
B' : Matrix.{u_1, u_1, u_3} m m ↥K
hB :
  HMul.hMul (α := Matrix m m L) (A'.map (⇑K.subtype : (a : ↥K) → L)) (B'.map (⇑K.subtype : (a : ↥K) → L)) =
    map (α := ↥K) 1 (⇑K.subtype : (a : ↥K) → L)
⊢ HMul.hMul (β := Matrix n m L) (A.submatrix id id)
      (submatrix (B'.map (⇑K.subtype : (a : ↥K) → L)) (⇑e.symm : (a : n) → m) id) =
    map (α := ↥K) 1 (⇑K.subtype : (a : ↥K) → L)

Tactic:
rw [hA', ← e.symm_symm, ← submatrix_id_mul_left] at hB

Premises used: Equiv.symm_symm, Matrix.submatrix_id_mul_left
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
hA : IsUnit A'
B' : Matrix.{u_1, u_1, u_3} m m ↥K
hB :
  HMul.hMul (β := Matrix n m L) (A.submatrix id id)
      (submatrix (B'.map (⇑K.subtype : (a : ↥K) → L)) (⇑e.symm : (a : n) → m) id) =
    map (α := ↥K) 1 (⇑K.subtype : (a : ↥K) → L)
⊢ HMul.hMul (β := Matrix n m L) A (map (B'.submatrix (⇑e.symm : (a : n) → m) id) (⇑K.subtype : (a : ↥K) → L)) = 1

Tactic:
simpa using hB
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
hA : IsUnit A'
B' : Matrix.{u_1, u_1, u_3} m m ↥K
hB : A' * B' = 1
⊢ HMul.hMul (β := Matrix n m L) A (map (B'.submatrix (⇑e.symm : (a : n) → m) id) (⇑K.subtype : (a : ↥K) → L)) = 1

Tactic:
replace hB : A * (B'.submatrix e.symm id).map K.subtype = 1 := by
    replace hB := congr_arg (fun C ↦ C.map K.subtype) hB
    simp_rw [Matrix.map_mul] at hB
    rw [hA', ← e.symm_symm, ← submatrix_id_mul_left] at hB
    simpa using hB
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
hA : IsUnit A'
B' : Matrix.{u_1, u_1, u_3} m m ↥K
hB : HMul.hMul (β := Matrix n m L) A (map (B'.submatrix (⇑e.symm : (a : n) → m) id) (⇑K.subtype : (a : ↥K) → L)) = 1
⊢ map (B'.submatrix (⇑e.symm : (a : n) → m) id) (⇑K.subtype : (a : ↥K) → L) = B

Tactic:
simpa [← Matrix.mul_assoc, (mul_eq_one_comm_of_equiv e).mp hAB] using congr_arg (B * ·) hB

Premises used: HMul.hMul, Matrix.mul_assoc, congr_arg, Matrix.mul_eq_one_comm_of_equiv, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val : Fintype m
A' : Matrix.{u_1, u_1, u_3} m m ↥K :=
  (of : (a : m → m → ↥K) → Matrix m m ↥K) fun (i j : m) ↦
    Subtype.mk (p := fun (x : L) ↦ x ∈ K) (A.submatrix id (⇑e : (a : m) → n) i j) ⋯
hA' : A'.map (⇑K.subtype : (a : ↥K) → L) = A.submatrix id (⇑e : (a : m) → n)
hA : IsUnit A'
B' : Matrix.{u_1, u_1, u_3} m m ↥K
hB : HMul.hMul (β := Matrix n m L) A (map (B'.submatrix (⇑e.symm : (a : n) → m) id) (⇑K.subtype : (a : ↥K) → L)) = 1
⊢ map (B'.submatrix (⇑e.symm : (a : n) → m) id) (⇑K.subtype : (a : ↥K) → L) = B

Tactic:
classical
  simpa [← Matrix.mul_assoc, (mul_eq_one_comm_of_equiv e).mp hAB] using congr_arg (B * ·) hB

Premises used: HMul.hMul, Matrix.mul_assoc, congr_arg
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : n) (j : m), B i j ∈ K
i : m
j : n
⊢ Bᵀ * Aᵀ = 1

Tactic:
simpa using congr_arg transpose hAB

Premises used: congr_arg, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : n) (j : m), B i j ∈ K
i : m
j : n
⊢ Bᵀ * Aᵀ = 1

Tactic:
replace hAB : Bᵀ * Aᵀ = 1 := by simpa using congr_arg transpose hAB
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
h_mem : ∀ (i : n) (j : m), B i j ∈ K
i : m
j : n
hAB : Bᵀ * Aᵀ = 1
rw : Aᵀ j i ∈ K
⊢ A i j ∈ K

Tactic:
rw [← A.transpose_apply]

Premises used: Matrix.transpose_apply
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
h_mem : ∀ (i : n) (j : m), Bᵀ j i ∈ K
i : m
j : n
hAB : Bᵀ * Aᵀ = 1
⊢ Aᵀ j i ∈ K

Tactic:
mem_subfield_of_mul_eq_one_of_mem_subfield_right e K hAB (fun i j ↦ h_mem j i) j i

Premises used: Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_right
-- Module: Mathlib.LinearAlgebra.Matrix.BaseChange
Goal:
m : Type u_1
n : Type u_2
L : Type u_3
inst : Finite m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
h_mem : ∀ (i : n) (j : m), Bᵀ j i ∈ K
i : m
j : n
hAB : Bᵀ * Aᵀ = 1
⊢ Aᵀ j i ∈ K

Tactic:
exact mem_subfield_of_mul_eq_one_of_mem_subfield_right e K hAB (fun i j ↦ h_mem j i) j i

Premises used: Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_right
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
⊢ e.toMatrix v i j = (((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R) : (a : ι) → R) i

Tactic:
rfl

Premises used: Module.Basis.toMatrix, rfl