-- Mathlib/LinearAlgebra/Matrix/BaseChange.lean
lemma mem_subfield_of_mul_eq_one_of_mem_subfield_right
    (h_mem : ∀ i j, A i j ∈ K) (i : n) (j : m) :
    B i j ∈ K

Proof state:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : 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 m m ↥K := of fun i j => ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
h_unit : IsUnit (A.submatrix id ⇑e)
⊢ IsUnit A'

Tactic:
have h_det : (A.submatrix id e).det = K.subtype A'.det := by
  simp [A', K.subtype.map_det, map, submatrix]

Result:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : 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 m m ↥K := of fun i j => ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
h_unit : IsUnit (A.submatrix id ⇑e)
h_det : (A.submatrix id ⇑e).det = K.subtype A'.det
⊢ IsUnit A'

Proof state:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : 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 m m ↥K := of fun i j => ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
hA : IsUnit A'
B' : Matrix m m ↥K
hB : A' * B' = 1
⊢ A * (B'.submatrix (⇑e.symm) id).map ⇑K.subtype = 1

Tactic:
replace hB := congr_arg (fun C ↦ C.map K.subtype) hB

Result:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : 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 m m ↥K := of fun i j => ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
hA : IsUnit A'
B' : Matrix m m ↥K
hB : (fun C => C.map ⇑K.subtype) (A' * B') = (fun C => C.map ⇑K.subtype) 1
⊢ A * (B'.submatrix (⇑e.symm) id).map ⇑K.subtype = 1

Proof state:
case intro
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : 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 m m ↥K := of fun i j => ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
hA : IsUnit A'
⊢ B i j ∈ K

Tactic:
obtain ⟨B', hB⟩ := exists_right_inverse_iff_isUnit.mpr hA

Result:
case intro.intro
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : 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 m m ↥K := of fun i j => ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
hA : IsUnit A'
B' : Matrix m m ↥K
hB : A' * B' = 1
⊢ B i j ∈ K

Proof state:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : 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 m m ↥K := of fun i j => ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
hA : IsUnit A'
B' : Matrix m m ↥K
hB : A.submatrix id id * (B'.map ⇑K.subtype).submatrix (⇑e.symm) id = map 1 ⇑K.subtype
⊢ A * (B'.submatrix (⇑e.symm) id).map ⇑K.subtype = 1

Tactic:
simpa using hB

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : 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
⊢ B i j ∈ K

Tactic:
cases nonempty_fintype m

Result:
case intro
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : 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
⊢ B i j ∈ K

Proof state:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : 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 m m ↥K := of fun i j => ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
⊢ A.submatrix id ⇑e * B.submatrix (⇑e) id = 1

Tactic:
simpa

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : 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 m m ↥K := of fun i j => ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
hA : IsUnit A'
B' : Matrix m m ↥K
hB : A' * B' = 1
this : (B'.submatrix (⇑e.symm) id).map ⇑K.subtype = B
⊢ B i j ∈ K

Tactic:
simp [← this]

Result:
no goals

Proof state:
case intro
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : 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 m m ↥K := of fun i j => ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
⊢ B i j ∈ K

Tactic:
have hA : IsUnit A' := by
  have h_unit : IsUnit (A.submatrix id e) :=
    isUnit_of_right_inverse (B := 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

Result:
case intro
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : 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 m m ↥K := of fun i j => ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
hA : IsUnit A'
⊢ B i j ∈ K

Proof state:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : 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 m m ↥K := of fun i j => ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
hA : IsUnit A'
B' : Matrix m m ↥K
hB : A'.map ⇑K.subtype * B'.map ⇑K.subtype = map 1 ⇑K.subtype
⊢ A * (B'.submatrix (⇑e.symm) id).map ⇑K.subtype = 1

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

Result:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : 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 m m ↥K := of fun i j => ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
hA : IsUnit A'
B' : Matrix m m ↥K
hB : A.submatrix id id * (B'.map ⇑K.subtype).submatrix (⇑e.symm) id = map 1 ⇑K.subtype
⊢ A * (B'.submatrix (⇑e.symm) id).map ⇑K.subtype = 1