awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : Invertible A
⊢ A⁻¹ * A = 1

Tactic:
nonsing_inv_mul A (isUnit_det_of_invertible A)

Premises used: Matrix.isUnit_det_of_invertible, Matrix.nonsing_inv_mul
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
B : Matrix m n α
inst_3 : Invertible A
⊢ B * A * A⁻¹ = B

Tactic:
mul_nonsing_inv_cancel_right A B (isUnit_det_of_invertible A)

Premises used: Matrix.isUnit_det_of_invertible, Matrix.mul_nonsing_inv_cancel_right
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
B : Matrix n m α
inst_3 : Invertible A
⊢ A * (A⁻¹ * B) = B

Tactic:
mul_nonsing_inv_cancel_left A B (isUnit_det_of_invertible A)

Premises used: Matrix.isUnit_det_of_invertible, Matrix.mul_nonsing_inv_cancel_left
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
B : Matrix m n α
inst_3 : Invertible A
⊢ B * A⁻¹ * A = B

Tactic:
nonsing_inv_mul_cancel_right A B (isUnit_det_of_invertible A)

Premises used: Matrix.isUnit_det_of_invertible, Matrix.nonsing_inv_mul_cancel_right
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
B : Matrix n m α
inst_3 : Invertible A
⊢ A⁻¹ * (A * B) = B

Tactic:
nonsing_inv_mul_cancel_left A B (isUnit_det_of_invertible A)

Premises used: Matrix.isUnit_det_of_invertible, Matrix.nonsing_inv_mul_cancel_left
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : Invertible A
B C : Matrix n m α
h : A⁻¹ * B = C
rw : B = A * (A⁻¹ * B)
rw₁ rw₂ : B = B
⊢ B = A * C

Tactic:
rw [← h, mul_inv_cancel_left_of_invertible]

Premises used: Matrix.mul_inv_cancel_left_of_invertible
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : Invertible A
B C : Matrix n m α
h : B = A * C
rw : A⁻¹ * (A * C) = C
rw₁ rw₂ : C = C
⊢ A⁻¹ * B = C

Tactic:
rw [h, inv_mul_cancel_left_of_invertible]

Premises used: Matrix.inv_mul_cancel_left_of_invertible
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : Invertible A
B C : Matrix m n α
h : B * A⁻¹ = C
rw : B = B * A⁻¹ * A
rw₁ rw₂ : B = B
⊢ B = C * A

Tactic:
rw [← h, inv_mul_cancel_right_of_invertible]

Premises used: Matrix.inv_mul_cancel_right_of_invertible
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : Invertible A
B C : Matrix m n α
h : B = C * A
rw : C * A * A⁻¹ = C
rw₁ rw₂ : C = C
⊢ B * A⁻¹ = C

Tactic:
rw [h, mul_inv_cancel_right_of_invertible]

Premises used: Matrix.mul_inv_cancel_right_of_invertible
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : Invertible A
u v : n → α
hM : u = A *ᵥ v
rw : A⁻¹ *ᵥ A *ᵥ v = v
rw₁ : (A⁻¹ * A) *ᵥ v = v
rw₂ : 1 *ᵥ v = v
rw₃ rw₄ : v = v
⊢ A⁻¹ *ᵥ u = v

Tactic:
rw [hM, Matrix.mulVec_mulVec, Matrix.inv_mul_of_invertible, Matrix.one_mulVec]

Premises used: Matrix.inv_mul_of_invertible, Matrix.one_mulVec, Matrix.mulVec_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : Invertible A
x x_1 : Matrix n m α
h : Eq (α := Matrix n m α) ((fun (x : Matrix n m α) ↦ A * x) x) ((fun (x : Matrix n m α) ↦ A * x) x_1)
⊢ x = x_1

Tactic:
simpa only [inv_mul_cancel_left_of_invertible] using congr_arg (A⁻¹ * ·) h

Premises used: HMul.hMul, congr_arg, Inv.inv, Matrix.inv_mul_cancel_left_of_invertible
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : Invertible A
a x : Matrix m n α
hax : Eq (α := Matrix m n α) ((fun (x : Matrix m n α) ↦ x * A) a) ((fun (x : Matrix m n α) ↦ x * A) x)
⊢ a = x

Tactic:
simpa only [mul_inv_cancel_right_of_invertible] using congr_arg (· * A⁻¹) hax

Premises used: HMul.hMul, Matrix.mul_inv_cancel_right_of_invertible, congr_arg, Inv.inv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : Invertible A
x y : Matrix n m α
⊢ A * x = A * y ↔ x = y

Tactic:
(mul_right_injective_of_invertible A).eq_iff

Premises used: Matrix.mul_right_injective_of_invertible, Function.Injective.eq_iff
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
inst_3 : Invertible A
x y : Matrix m n α
⊢ x * A = y * A ↔ x = y

Tactic:
(mul_left_injective_of_invertible A).eq_iff

Premises used: Function.Injective.eq_iff, Matrix.mul_left_injective_of_invertible
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
hA : A.IsSymm
⊢ A⁻¹.IsSymm

Tactic:
hA.adjugate.smul _

Premises used: Matrix.IsSymm.smul, Matrix.IsSymm.adjugate
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : CommRing α
A : Matrix m n α
B : Matrix n m α
h : A * B = 1
x x_1 : Matrix l m α
g : Eq (α := Matrix l n α) ((fun (x : Matrix l m α) ↦ x * A) x) ((fun (x : Matrix l m α) ↦ x * A) x_1)
⊢ x = x_1

Tactic:
simpa only [Matrix.mul_assoc, Matrix.mul_one, h] using congr_arg (· * B) g

Premises used: HMul.hMul, Matrix.mul_assoc, congr_arg, Matrix.mul_one
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : CommRing α
A : Matrix m n α
B : Matrix n m α
h : A * B = 1
x x_1 : Matrix m l α
g : Eq (α := Matrix n l α) ((fun (x : Matrix m l α) ↦ B * x) x) ((fun (x : Matrix m l α) ↦ B * x) x_1)
⊢ x = x_1

Tactic:
simpa only [← Matrix.mul_assoc, Matrix.one_mul, h] using congr_arg (A * ·) g

Premises used: HMul.hMul, Matrix.mul_assoc, congr_arg, Matrix.one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Finite n
A : Matrix m n R
intro :
  ∀ (val : Fintype n), (Function.Surjective (β := n → R) fun (v : m → R) ↦ v ᵥ* A) ↔ ∃ (B : Matrix n m R), B * A = 1
⊢ (Function.Surjective (β := n → R) fun (v : m → R) ↦ v ᵥ* A) ↔ ∃ (B : Matrix n m R), B * A = 1

Tactic:
cases nonempty_fintype n

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Finite n
A : Matrix m n R
val : Fintype n
h : ∃ (B : Matrix n m R), B * A = 1
y : n → R
B : Matrix n m R
hBA : B * A = 1
⊢ (fun (v : m → R) ↦ v ᵥ* A) (y ᵥ* B) = y

Tactic:
simp [hBA]
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Finite n
A : Matrix m n R
val : Fintype n
intro : ∀ (h : Function.Surjective (β := n → R) fun (v : m → R) ↦ v ᵥ* A), ∃ (B : Matrix n m R), B * A = 1
⊢ (Function.Surjective (β := n → R) fun (v : m → R) ↦ v ᵥ* A) ↔ ∃ (B : Matrix n m R), B * A = 1

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨y ᵥ* B, by simp [hBA]⟩⟩
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Finite n
A : Matrix m n R
val : Fintype n
h : Function.Surjective (β := n → R) fun (v : m → R) ↦ v ᵥ* A
intro :
  ∀ (rows : n → m → R)
    (hrows : ∀ (x : n), Eq (α := n → R) ((fun (v : m → R) ↦ v ᵥ* A) (rows x)) (Pi.single (M := fun (a : n) ↦ R) x 1)),
    ∃ (B : Matrix n m R), B * A = 1
⊢ ∃ (B : Matrix n m R), B * A = 1

Tactic:
choose rows hrows using (h <| Pi.single · 1)

Premises used: Pi.single, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Finite n
A : Matrix m n R
val : Fintype n
h : Function.Surjective (β := n → R) fun (v : m → R) ↦ v ᵥ* A
rows : n → m → R
hrows : ∀ (x : n), Eq (α := n → R) ((fun (v : m → R) ↦ v ᵥ* A) (rows x)) (Pi.single (M := fun (a : n) ↦ R) x 1)
⊢ ∃ (B : Matrix n m R), B * A = 1

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

Premises used: Matrix.of, Exists.intro, DFunLike.coe, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Finite n
A : Matrix m n R
val : Fintype n
h : Function.Surjective (β := n → R) fun (v : m → R) ↦ v ᵥ* A
rows : n → m → R
hrows : ∀ (x : n), Eq (α := n → R) ((fun (v : m → R) ↦ v ᵥ* A) (rows x)) (Pi.single (M := fun (a : n) ↦ R) x 1)
intro :
  ∀ (i j : n), HMul.hMul (α := Matrix n m R) ((of : (a : n → m → R) → Matrix n m R) rows : Matrix n m R) A i j = 1 i j
⊢ ∃ (B : Matrix n m R), B * A = 1

Tactic:
refine ⟨Matrix.of rows, Matrix.ext fun i j => ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Finite n
A : Matrix m n R
val : Fintype n
h : Function.Surjective (β := n → R) fun (v : m → R) ↦ v ᵥ* A
rows : n → m → R
hrows : ∀ (x : n), Eq (α := n → R) ((fun (v : m → R) ↦ v ᵥ* A) (rows x)) (Pi.single (M := fun (a : n) ↦ R) x 1)
i j : n
intro : ((of : (a : n → m → R) → Matrix n m R) rows i ᵥ* A) j = (fun (v : m → R) ↦ v ᵥ* A) (rows i) j
⊢ HMul.hMul (α := Matrix n m R) ((of : (a : n → m → R) → Matrix n m R) rows : Matrix n m R) A i j = 1 i j

Tactic:
rw [mul_apply_eq_vecMul, one_eq_pi_single, ← hrows]

Premises used: Matrix.one_eq_pi_single, Matrix.mul_apply_eq_vecMul
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Finite n
A : Matrix m n R
val : Fintype n
h : Function.Surjective (β := n → R) fun (v : m → R) ↦ v ᵥ* A
rows : n → m → R
hrows : ∀ (x : n), Eq (α := n → R) ((fun (v : m → R) ↦ v ᵥ* A) (rows x)) (Pi.single (M := fun (a : n) ↦ R) x 1)
i j : n
⊢ ((of : (a : n → m → R) → Matrix n m R) rows i ᵥ* A) j = (fun (v : m → R) ↦ v ᵥ* A) (rows i) j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq m
inst_2 : Finite m
inst_3 : Fintype n
A : Matrix m n R
intro : ∀ (val : Fintype m), Function.Surjective A.mulVec ↔ ∃ (B : Matrix n m R), A * B = 1
⊢ Function.Surjective A.mulVec ↔ ∃ (B : Matrix n m R), A * B = 1

Tactic:
cases nonempty_fintype m

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq m
inst_2 : Finite m
inst_3 : Fintype n
A : Matrix m n R
val : Fintype m
h : ∃ (B : Matrix n m R), A * B = 1
y : m → R
B : Matrix n m R
hBA : A * B = 1
⊢ A *ᵥ B *ᵥ y = y

Tactic:
simp [hBA]
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq m
inst_2 : Finite m
inst_3 : Fintype n
A : Matrix m n R
val : Fintype m
intro : ∀ (h : Function.Surjective A.mulVec), ∃ (B : Matrix n m R), A * B = 1
⊢ Function.Surjective A.mulVec ↔ ∃ (B : Matrix n m R), A * B = 1

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨B *ᵥ y, by simp [hBA]⟩⟩
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq m
inst_2 : Finite m
inst_3 : Fintype n
A : Matrix m n R
val : Fintype m
h : Function.Surjective A.mulVec
intro :
  ∀ (cols : m → n → R) (hcols : ∀ (x : m), A *ᵥ cols x = Pi.single (M := fun (a : m) ↦ R) x 1),
    ∃ (B : Matrix n m R), A * B = 1
⊢ ∃ (B : Matrix n m R), A * B = 1

Tactic:
choose cols hcols using (h <| Pi.single · 1)

Premises used: Pi.single, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq m
inst_2 : Finite m
inst_3 : Fintype n
A : Matrix m n R
val : Fintype m
h : Function.Surjective A.mulVec
cols : m → n → R
hcols : ∀ (x : m), A *ᵥ cols x = Pi.single (M := fun (a : m) ↦ R) x 1
⊢ ∃ (B : Matrix n m R), A * B = 1

Tactic:
⟨(Matrix.of cols)ᵀ, Matrix.ext fun i j ↦ ?_⟩

Premises used: Matrix.of, Matrix.transpose, Exists.intro, DFunLike.coe, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq m
inst_2 : Finite m
inst_3 : Fintype n
A : Matrix m n R
val : Fintype m
h : Function.Surjective A.mulVec
cols : m → n → R
hcols : ∀ (x : m), A *ᵥ cols x = Pi.single (M := fun (a : m) ↦ R) x 1
intro : ∀ (i j : m), HMul.hMul (β := Matrix n m R) A ((of : (a : m → n → R) → Matrix m n R) cols)ᵀ i j = 1 i j
⊢ ∃ (B : Matrix n m R), A * B = 1

Tactic:
refine ⟨(Matrix.of cols)ᵀ, Matrix.ext fun i j ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq m
inst_2 : Finite m
inst_3 : Fintype n
A : Matrix m n R
val : Fintype m
h : Function.Surjective A.mulVec
cols : m → n → R
hcols : ∀ (x : m), A *ᵥ cols x = Pi.single (M := fun (a : m) ↦ R) x 1
i j : m
intro : HMul.hMul (β := Matrix n m R) A ((of : (a : m → n → R) → Matrix m n R) cols)ᵀ i j = (A *ᵥ cols j) i
⊢ HMul.hMul (β := Matrix n m R) A ((of : (a : m → n → R) → Matrix m n R) cols)ᵀ i j = 1 i j

Tactic:
rw [one_eq_pi_single, Pi.single_comm, ← hcols j]

Premises used: Matrix.one_eq_pi_single, Pi.single_comm
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq m
inst_2 : Finite m
inst_3 : Fintype n
A : Matrix m n R
val : Fintype m
h : Function.Surjective A.mulVec
cols : m → n → R
hcols : ∀ (x : m), A *ᵥ cols x = Pi.single (M := fun (a : m) ↦ R) x 1
i j : m
⊢ HMul.hMul (β := Matrix n m R) A ((of : (a : m → n → R) → Matrix m n R) cols)ᵀ i j = (A *ᵥ cols j) i

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
R : Type u_2
inst_1 : CommRing R
inst_2 : Fintype m
A : Matrix m m R
rw : (∃ (B : Matrix m m R), B * A = 1) ↔ IsUnit A
rw₁ rw₂ : (∃ (B : Matrix m m R), B * A = 1) ↔ ∃ (b : Matrix m m R), b * A = 1
⊢ (Function.Surjective (β := m → R) fun (v : m → R) ↦ v ᵥ* A) ↔ IsUnit A

Tactic:
rw [vecMul_surjective_iff_exists_left_inverse, isUnit_iff_exists_inv']

Premises used: Matrix.vecMul_surjective_iff_exists_left_inverse, isUnit_iff_exists_inv'
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
R : Type u_2
inst_1 : CommRing R
inst_2 : Fintype m
A : Matrix m m R
rw : (∃ (B : Matrix m m R), A * B = 1) ↔ IsUnit A
rw₁ rw₂ : (∃ (B : Matrix m m R), A * B = 1) ↔ ∃ (b : Matrix m m R), A * b = 1
⊢ Function.Surjective A.mulVec ↔ IsUnit A

Tactic:
rw [mulVec_surjective_iff_exists_right_inverse, isUnit_iff_exists_inv]

Premises used: isUnit_iff_exists_inv, Matrix.mulVec_surjective_iff_exists_right_inverse
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
⊢ (Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A) ↔ IsUnit A

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
refine_1 : ∀ (h : Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A), IsUnit A
refine_2 : ∀ (h : IsUnit A), Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A
⊢ (Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A) ↔ IsUnit A

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
h : Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A
refine_1 : Function.Surjective (β := m → K) fun (v : m → K) ↦ v ᵥ* A
⊢ IsUnit A

Tactic:
rw [← vecMul_surjective_iff_isUnit]

Premises used: Matrix.vecMul_surjective_iff_isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
h : Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A
⊢ Function.Surjective (β := m → K) fun (v : m → K) ↦ v ᵥ* A

Tactic:
LinearMap.surjective_of_injective (f := A.vecMulLinear) h

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.vecMul, LinearMap.surjective_of_injective, Finset.sum
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
h : Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A
⊢ Function.Surjective (β := m → K) fun (v : m → K) ↦ v ᵥ* A

Tactic:
exact LinearMap.surjective_of_injective (f := A.vecMulLinear) h

Premises used: LinearMap.surjective_of_injective
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
h : IsUnit A
⊢ Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A

Tactic:
vecMul_injective_of_isUnit h

Premises used: Matrix.vecMul_injective_of_isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
h : IsUnit A
⊢ Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A

Tactic:
exact vecMul_injective_of_isUnit h

Premises used: Matrix.vecMul_injective_of_isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
rw : Function.Injective A.mulVec ↔ Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* Aᵀ
⊢ Function.Injective A.mulVec ↔ IsUnit A

Tactic:
rw [← isUnit_transpose, ← vecMul_injective_iff_isUnit]

Premises used: Matrix.vecMul_injective_iff_isUnit, Matrix.isUnit_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
⊢ Function.Injective A.mulVec ↔ Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* Aᵀ

Tactic:
simp_rw [vecMul_transpose]

Premises used: Matrix.vecMul_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
rw : LinearIndependent K Aᵀ.col ↔ IsUnit A
rw₁ : Function.Injective Aᵀ.mulVec ↔ IsUnit A
rw₂ : Function.Injective (α := m → K) (β := m → K) (⇑Aᵀ.mulVecLin : (a : m → K) → m → K) ↔ IsUnit A
rw₃ : Function.Injective (α := m → K) (β := m → K) (⇑A.vecMulLinear : (a : m → K) → m → K) ↔ IsUnit A
rw₄ :
  Function.Injective (α := m → K) (β := m → K) (⇑A.vecMulLinear : (a : m → K) → m → K) ↔
    Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A
rw₅ rw₆ :
  (Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A) ↔ Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A
⊢ LinearIndependent K A.row ↔ IsUnit A

Tactic:
rw [← col_transpose, ← mulVec_injective_iff, ← coe_mulVecLin, mulVecLin_transpose,
    ← vecMul_injective_iff_isUnit, coe_vecMulLinear]

Premises used: Matrix.coe_mulVecLin, Matrix.col_transpose, Matrix.coe_vecMulLinear, Matrix.mulVecLin_transpose, Matrix.vecMul_injective_iff_isUnit, Matrix.mulVec_injective_iff
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
rw : LinearIndependent K Aᵀ.row ↔ IsUnit A
rw₁ : IsUnit Aᵀ ↔ IsUnit A
rw₂ rw₃ : IsUnit A ↔ IsUnit A
⊢ LinearIndependent K A.col ↔ IsUnit A

Tactic:
rw [← row_transpose, linearIndependent_rows_iff_isUnit, isUnit_transpose]

Premises used: Matrix.row_transpose, Matrix.isUnit_transpose, Matrix.linearIndependent_rows_iff_isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
R : Type u_2
inst_1 : CommRing R
inst_2 : Fintype m
A : Matrix m m R
inst_3 : Invertible A
⊢ Function.Surjective (β := m → R) fun (v : m → R) ↦ v ᵥ* A

Tactic:
vecMul_surjective_iff_isUnit.2 <| isUnit_of_invertible A

Premises used: Iff.mpr, isUnit_of_invertible, Matrix.vecMul_surjective_iff_isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
R : Type u_2
inst_1 : CommRing R
inst_2 : Fintype m
A : Matrix m m R
inst_3 : Invertible A
⊢ Function.Surjective A.mulVec

Tactic:
mulVec_surjective_iff_isUnit.2 <| isUnit_of_invertible A

Premises used: Iff.mpr, isUnit_of_invertible, Matrix.mulVec_surjective_iff_isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
inst_3 : Invertible A
⊢ Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A

Tactic:
vecMul_injective_iff_isUnit.2 <| isUnit_of_invertible A

Premises used: Iff.mpr, isUnit_of_invertible, Matrix.vecMul_injective_iff_isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
inst_3 : Invertible A
⊢ Function.Injective A.mulVec

Tactic:
mulVec_injective_iff_isUnit.2 <| isUnit_of_invertible A

Premises used: Iff.mpr, isUnit_of_invertible, Matrix.mulVec_injective_iff_isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
inst_3 : Invertible A
⊢ LinearIndependent K A.row

Tactic:
linearIndependent_rows_iff_isUnit.2 <| isUnit_of_invertible A

Premises used: Iff.mpr, isUnit_of_invertible, Matrix.linearIndependent_rows_iff_isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
inst_3 : Invertible A
⊢ LinearIndependent K A.col

Tactic:
linearIndependent_cols_iff_isUnit.2 <| isUnit_of_invertible A

Premises used: Iff.mpr, isUnit_of_invertible, Matrix.linearIndependent_cols_iff_isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
pos : ∀ (h : IsUnit A.det), A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0
neg : ∀ (h : ¬IsUnit A.det), A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0

Tactic:
by_cases h : IsUnit A.det

Premises used: IsUnit, Matrix.det
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0

Tactic:
Or.inl ⟨nonsing_inv_mul _ h, mul_nonsing_inv _ h⟩

Premises used: Matrix.nonsing_inv_mul, And.intro, Or.inl, Matrix.mul_nonsing_inv