-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem vecMul_surjective_iff_exists_left_inverse
    [DecidableEq n] [Fintype m] [Finite n] {A : Matrix m n R} :
    Function.Surjective A.vecMul ↔ ∃ B : Matrix n m R, B * A = 1

Proof state:
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
⊢ (Function.Surjective fun v => v ᵥ* A) ↔ ∃ B, B * A = 1

Tactic:
cases nonempty_fintype n

Result:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
val✝ : Fintype n
⊢ (Function.Surjective fun v => v ᵥ* A) ↔ ∃ B, B * A = 1

Proof state:
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
val✝ : Fintype n
x✝ : ∃ B, B * A = 1
y : n → R
B : Matrix n m R
hBA : B * A = 1
⊢ (fun v => v ᵥ* A) (y ᵥ* B) = y

Tactic:
simp [hBA]

Result:
no goals

Proof state:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
val✝ : Fintype n
⊢ (Function.Surjective fun v => v ᵥ* A) ↔ ∃ B, B * A = 1

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨y ᵥ* B, by simp [hBA]⟩⟩

Result:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
val✝ : Fintype n
h : Function.Surjective fun v => v ᵥ* A
⊢ ∃ B, B * A = 1

Proof state:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
val✝ : Fintype n
h : Function.Surjective fun v => v ᵥ* A
rows : n → m → R
hrows : ∀ (x : n), (fun v => v ᵥ* A) (rows x) = Pi.single x 1
i j : n
⊢ (of rows * A) i j = 1 i j

Tactic:
rw [mul_apply_eq_vecMul, one_eq_pi_single, ← hrows]

Result:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
val✝ : Fintype n
h : Function.Surjective fun v => v ᵥ* A
rows : n → m → R
hrows : ∀ (x : n), (fun v => v ᵥ* A) (rows x) = Pi.single x 1
i j : n
⊢ (of rows i ᵥ* A) j = (fun v => v ᵥ* A) (rows i) j

Proof state:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
val✝ : Fintype n
h : Function.Surjective fun v => v ᵥ* A
rows : n → m → R
hrows : ∀ (x : n), (fun v => v ᵥ* A) (rows x) = Pi.single x 1
i j : n
⊢ (of rows i ᵥ* A) j = (fun v => v ᵥ* A) (rows i) j

Tactic:
rfl

Result:
no goals

Proof state:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
val✝ : Fintype n
h : Function.Surjective fun v => v ᵥ* A
rows : n → m → R
hrows : ∀ (x : n), (fun v => v ᵥ* A) (rows x) = Pi.single x 1
⊢ ∃ B, B * A = 1

Tactic:
refine ⟨Matrix.of rows, Matrix.ext fun i j => ?_⟩

Result:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
val✝ : Fintype n
h : Function.Surjective fun v => v ᵥ* A
rows : n → m → R
hrows : ∀ (x : n), (fun v => v ᵥ* A) (rows x) = Pi.single x 1
i j : n
⊢ (of rows * A) i j = 1 i j