awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : PartialOrder R
inst_3 : NonUnitalRing R
inst_4 : StarRing R
inst_5 : StarOrderedRing R
inst_6 : NoZeroDivisors R
A : Matrix m n R
v : n → R
⊢ v ᵥ* (Aᴴ * A) = 0 ↔ v ᵥ* Aᴴ = 0

Tactic:
simpa only [← Matrix.replicateRow_vecMul, replicateRow_eq_zero] using
    mul_conjTranspose_mul_self_eq_zero A (replicateRow (Fin 1) v)

Premises used: Matrix.replicateRow_eq_zero, Matrix.replicateRow_vecMul, Matrix.replicateRow, OfNat.ofNat, Fin, Matrix.mul_conjTranspose_mul_self_eq_zero
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : PartialOrder R
inst_3 : NonUnitalRing R
inst_4 : StarRing R
inst_5 : StarOrderedRing R
inst_6 : NoZeroDivisors R
A : Matrix m n R
v : m → R
⊢ v ᵥ* (A * Aᴴ) = 0 ↔ v ᵥ* A = 0

Tactic:
simpa only [conjTranspose_conjTranspose] using vecMul_conjTranspose_mul_self_eq_zero Aᴴ _

Premises used: Matrix.vecMul_conjTranspose_mul_self_eq_zero, Matrix.conjTranspose, Matrix.conjTranspose_conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : PartialOrder R
inst_2 : NonUnitalRing R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : NoZeroDivisors R
v : n → R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : PartialOrder R
inst_2 : NonUnitalRing R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : NoZeroDivisors R
v : n → R
h : Nontrivial R
⊢ 0 < star v ⬝ᵥ v ↔ v ≠ 0

Tactic:
(Fintype.sum_pos_iff_of_nonneg fun i => star_mul_self_nonneg _).trans ?_

Premises used: dotProduct, star_mul_self_nonneg, Fintype.sum_pos_iff_of_nonneg, Iff.trans
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : PartialOrder R
inst_2 : NonUnitalRing R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : NoZeroDivisors R
v : n → R
h : Nontrivial R
refine : (LT.lt (α := n → R) 0 fun (i : n) ↦ star (v i) * v i) ↔ v ≠ 0
⊢ 0 < star v ⬝ᵥ v ↔ v ≠ 0

Tactic:
refine (Fintype.sum_pos_iff_of_nonneg fun i => star_mul_self_nonneg _).trans ?_

Premises used: star_mul_self_nonneg, Fintype.sum_pos_iff_of_nonneg, Iff.trans
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : PartialOrder R
inst_2 : NonUnitalRing R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : NoZeroDivisors R
v : n → R
h : Nontrivial R
simp_rw :
  ((LE.le (α := (i : n) → R) 0 fun (i : n) ↦ star (v i) * v i) ∧ ∃ (i : n), 0 < star (v i) * v i) ↔ ∃ (a : n), v a ≠ 0
⊢ (LT.lt (α := n → R) 0 fun (i : n) ↦ star (v i) * v i) ↔ v ≠ 0

Tactic:
simp_rw [Pi.lt_def, Function.ne_iff, Pi.zero_apply]

Premises used: Pi.lt_def, Pi.zero_apply, Function.ne_iff
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : PartialOrder R
inst_2 : NonUnitalRing R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : NoZeroDivisors R
v : n → R
h : Nontrivial R
⊢ ((LE.le (α := (i : n) → R) 0 fun (i : n) ↦ star (v i) * v i) ∧ ∃ (i : n), 0 < star (v i) * v i) ↔ ∃ (a : n), v a ≠ 0

Tactic:
(and_iff_right fun i => star_mul_self_nonneg (v i)).trans <| exists_congr fun i => ?_

Premises used: and_iff_right, star_mul_self_nonneg, exists_congr, Iff.trans
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : PartialOrder R
inst_2 : NonUnitalRing R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : NoZeroDivisors R
v : n → R
h : Nontrivial R
refine : ∀ (i : n), 0 < star (v i) * v i ↔ v i ≠ 0
⊢ ((LE.le (α := (i : n) → R) 0 fun (i : n) ↦ star (v i) * v i) ∧ ∃ (i : n), 0 < star (v i) * v i) ↔ ∃ (a : n), v a ≠ 0

Tactic:
refine (and_iff_right fun i => star_mul_self_nonneg (v i)).trans <| exists_congr fun i => ?_

Premises used: and_iff_right, star_mul_self_nonneg, exists_congr, Iff.trans
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : PartialOrder R
inst_2 : NonUnitalRing R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : NoZeroDivisors R
v : n → R
h : Nontrivial R
i : n
mp : 0 < star (v i) * v i → v i ≠ 0
mpr : v i ≠ 0 → 0 < star (v i) * v i
⊢ 0 < star (v i) * v i ↔ v i ≠ 0

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : PartialOrder R
inst_2 : NonUnitalRing R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : NoZeroDivisors R
v : n → R
h_1 : Nontrivial R
i : n
h : 0 < star (v i) * v i
hv : v i = 0
⊢ False

Tactic:
simp [hv] at h
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : PartialOrder R
inst_2 : NonUnitalRing R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : NoZeroDivisors R
v : n → R
h : Nontrivial R
i : n
⊢ v i ≠ 0 → 0 < star (v i) * v i

Tactic:
(star_mul_self_pos <| .of_ne_zero ·)

Premises used: IsRegular.of_ne_zero, star_mul_self_pos
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : PartialOrder R
inst_2 : NonUnitalRing R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : NoZeroDivisors R
v : n → R
h : Nontrivial R
i : n
⊢ v i ≠ 0 → 0 < star (v i) * v i

Tactic:
exact (star_mul_self_pos <| .of_ne_zero ·)

Premises used: star_mul_self_pos
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : PartialOrder R
inst_2 : NonUnitalRing R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : NoZeroDivisors R
v : n → R
⊢ 0 < v ⬝ᵥ star v ↔ v ≠ 0

Tactic:
simpa using dotProduct_star_self_pos_iff (v := star v)

Premises used: Matrix.dotProduct_star_self_pos_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Dual
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommSemiring K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
inst_7 : DecidableEq ι₁
inst_8 : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
u : V₁ →ₗ[K] V₂
a :
  ∀ (i : ι₁) (j : ι₂),
    Eq.{u_1 + 1} (α := K)
      ((toMatrix B₂.dualBasis B₁.dualBasis : (a : Dual K V₂ →ₗ[K] Dual K V₁) → Matrix ι₁ ι₂ K)
          ((Dual.transpose : (a : V₁ →ₗ[K] V₂) → Dual K V₂ →ₗ[K] Dual K V₁) u) i j :
        K)
      (((toMatrix B₁ B₂ : (a : V₁ →ₗ[K] V₂) → Matrix ι₂ ι₁ K) u)ᵀ i j : K)
⊢ Eq (α := Matrix ι₁ ι₂ K)
    ((toMatrix B₂.dualBasis B₁.dualBasis : (a : Dual K V₂ →ₗ[K] Dual K V₁) → Matrix ι₁ ι₂ K)
        ((Dual.transpose : (a : V₁ →ₗ[K] V₂) → Dual K V₂ →ₗ[K] Dual K V₁) u) :
      Matrix ι₁ ι₂ K)
    (((toMatrix B₁ B₂ : (a : V₁ →ₗ[K] V₂) → Matrix ι₂ ι₁ K) u)ᵀ : Matrix ι₁ ι₂ K)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Dual
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommSemiring K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
inst_7 : DecidableEq ι₁
inst_8 : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
u : V₁ →ₗ[K] V₂
i : ι₁
j : ι₂
⊢ Eq.{u_1 + 1} (α := K)
    ((toMatrix B₂.dualBasis B₁.dualBasis : (a : Dual K V₂ →ₗ[K] Dual K V₁) → Matrix ι₁ ι₂ K)
        ((Dual.transpose : (a : V₁ →ₗ[K] V₂) → Dual K V₂ →ₗ[K] Dual K V₁) u) i j :
      K)
    (((toMatrix B₁ B₂ : (a : V₁ →ₗ[K] V₂) → Matrix ι₂ ι₁ K) u)ᵀ i j : K)

Tactic:
simp only [LinearMap.toMatrix_apply, Module.Dual.transpose_apply, B₁.dualBasis_repr,
    B₂.dualBasis_apply, Matrix.transpose_apply, LinearMap.comp_apply]

Premises used: LinearMap.comp_apply, Module.Dual.transpose_apply, Module.Basis.dualBasis_apply, Module.Basis.dualBasis_repr, Matrix.transpose_apply, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Dual
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommSemiring K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
inst_7 : DecidableEq ι₁
inst_8 : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
M : Matrix ι₁ ι₂ K
a :
  Eq (α := Matrix ι₂ ι₁ K)
    ((LinearMap.toMatrix B₁.dualBasis B₂.dualBasis : (a : Dual K V₁ →ₗ[K] Dual K V₂) → Matrix ι₂ ι₁ K)
        ((toLin B₁.dualBasis B₂.dualBasis : (a : Matrix ι₂ ι₁ K) → Dual K V₁ →ₗ[K] Dual K V₂) Mᵀ) :
      Matrix ι₂ ι₁ K)
    ((LinearMap.toMatrix B₁.dualBasis B₂.dualBasis : (a : Dual K V₁ →ₗ[K] Dual K V₂) → Matrix ι₂ ι₁ K)
        ((Dual.transpose : (a : V₂ →ₗ[K] V₁) → Dual K V₁ →ₗ[K] Dual K V₂)
          ((toLin B₂ B₁ : (a : Matrix ι₁ ι₂ K) → V₂ →ₗ[K] V₁) M)) :
      Matrix ι₂ ι₁ K)
⊢ Eq (α := Dual K V₁ →ₗ[K] Dual K V₂)
    ((toLin B₁.dualBasis B₂.dualBasis : (a : Matrix ι₂ ι₁ K) → Dual K V₁ →ₗ[K] Dual K V₂) Mᵀ :
      Dual K V₁ →ₗ[K] Dual K V₂)
    ((Dual.transpose : (a : V₂ →ₗ[K] V₁) → Dual K V₁ →ₗ[K] Dual K V₂)
        ((toLin B₂ B₁ : (a : Matrix ι₁ ι₂ K) → V₂ →ₗ[K] V₁) M) :
      Dual K V₁ →ₗ[K] Dual K V₂)

Tactic:
apply (LinearMap.toMatrix B₁.dualBasis B₂.dualBasis).injective

Premises used: Module.Basis.dualBasis, LinearEquiv.injective, LinearMap.toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Dual
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommSemiring K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
inst_7 : DecidableEq ι₁
inst_8 : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
M : Matrix ι₁ ι₂ K
a :
  Mᵀ =
    (LinearMap.toMatrix B₁.dualBasis B₂.dualBasis : (a : Dual K V₁ →ₗ[K] Dual K V₂) → Matrix ι₂ ι₁ K)
      ((Dual.transpose : (a : V₂ →ₗ[K] V₁) → Dual K V₁ →ₗ[K] Dual K V₂)
        ((toLin B₂ B₁ : (a : Matrix ι₁ ι₂ K) → V₂ →ₗ[K] V₁) M))
a₁ :
  Mᵀ =
    ((LinearMap.toMatrix B₂ B₁ : (a : V₂ →ₗ[K] V₁) → Matrix ι₁ ι₂ K)
        ((toLin B₂ B₁ : (a : Matrix ι₁ ι₂ K) → V₂ →ₗ[K] V₁) M))ᵀ
a₂ a₃ : Mᵀ = Mᵀ
⊢ Eq (α := Matrix ι₂ ι₁ K)
    ((LinearMap.toMatrix B₁.dualBasis B₂.dualBasis : (a : Dual K V₁ →ₗ[K] Dual K V₂) → Matrix ι₂ ι₁ K)
        ((toLin B₁.dualBasis B₂.dualBasis : (a : Matrix ι₂ ι₁ K) → Dual K V₁ →ₗ[K] Dual K V₂) Mᵀ) :
      Matrix ι₂ ι₁ K)
    ((LinearMap.toMatrix B₁.dualBasis B₂.dualBasis : (a : Dual K V₁ →ₗ[K] Dual K V₂) → Matrix ι₂ ι₁ K)
        ((Dual.transpose : (a : V₂ →ₗ[K] V₁) → Dual K V₁ →ₗ[K] Dual K V₂)
          ((toLin B₂ B₁ : (a : Matrix ι₁ ι₂ K) → V₂ →ₗ[K] V₁) M)) :
      Matrix ι₂ ι₁ K)

Tactic:
rw [LinearMap.toMatrix_toLin, LinearMap.toMatrix_transpose, LinearMap.toMatrix_toLin]

Premises used: LinearMap.toMatrix_transpose, LinearMap.toMatrix_toLin
-- Module: Mathlib.LinearAlgebra.Matrix.Dual
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
v w : n → R
h :
  ∀ (i : n),
    Eq (α := R)
      (({ toFun := dotProduct (v + w), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i :
            (a : R) → R)
          1 :
        R)
      ((HAdd.hAdd (α := Dual R (n → R)) { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ : (n → R) →ₗ[R] R }
                { toFun := dotProduct w, map_add' := ⋯, map_smul' := ⋯ : (n → R) →ₗ[R] R } ∘ₗ
              LinearMap.single R (fun (i : n) ↦ R) i :
            (a : R) → R)
          1 :
        R)
⊢ { toFun := dotProduct (v + w), map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := Dual R (n → R)) { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ : (n → R) →ₗ[R] R }
      { toFun := dotProduct w, map_add' := ⋯, map_smul' := ⋯ : (n → R) →ₗ[R] R }

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Dual
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
v w : n → R
i : n
⊢ Eq (α := R)
    (({ toFun := dotProduct (v + w), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i :
          (a : R) → R)
        1 :
      R)
    ((HAdd.hAdd (α := Dual R (n → R)) { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ : (n → R) →ₗ[R] R }
              { toFun := dotProduct w, map_add' := ⋯, map_smul' := ⋯ : (n → R) →ₗ[R] R } ∘ₗ
            LinearMap.single R (fun (i : n) ↦ R) i :
          (a : R) → R)
        1 :
      R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Dual
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
t : R
v : n → R
h :
  ∀ (i : n),
    Eq (α := R)
      (({ toFun := dotProduct (t • v), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i :
            (a : R) → R)
          1 :
        R)
      ((HSMul.hSMul (α := R) (β := Dual R (n → R)) ((RingHom.id R : (a : R) → R) t : R)
                { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ : (n → R) →ₗ[R] R } ∘ₗ
              LinearMap.single R (fun (i : n) ↦ R) i :
            (a : R) → R)
          1 :
        R)
⊢ { toFun := dotProduct (t • v), map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := R) (β := Dual R (n → R)) ((RingHom.id R : (a : R) → R) t : R)
      { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ : (n → R) →ₗ[R] R }

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Dual
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
t : R
v : n → R
i : n
⊢ Eq (α := R)
    (({ toFun := dotProduct (t • v), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i :
          (a : R) → R)
        1 :
      R)
    ((HSMul.hSMul (α := R) (β := Dual R (n → R)) ((RingHom.id R : (a : R) → R) t : R)
              { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ : (n → R) →ₗ[R] R } ∘ₗ
            LinearMap.single R (fun (i : n) ↦ R) i :
          (a : R) → R)
        1 :
      R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Dual
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → R
⊢ (fun (f : Dual R (n → R)) (i : n) ↦
        ((f : (a : n → R) → R)
            (((LinearMap.single R (fun (a : n) ↦ R) i : R →ₗ[R] (i : n) → R) : (a : R) → (i : n) → R) 1 : (i : n) → R) :
          R))
      ((fun (v : n → R) ↦ ({ toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ } : (n → R) →ₗ[R] R)) v) =
    v

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Dual
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
f : Dual R (n → R)
h :
  ∀ (i : n),
    Eq (α := R)
      ((((fun (v : n → R) ↦ ({ toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ } : (n → R) →ₗ[R] R))
                  ((fun (f : Dual R (n → R)) (i : n) ↦
                      ((f : (a : n → R) → R)
                          (((LinearMap.single R (fun (a : n) ↦ R) i : R →ₗ[R] (i : n) → R) : (a : R) → (i : n) → R) 1 :
                            (i : n) → R) :
                        R))
                    f) ∘ₗ
                LinearMap.single R (fun (i : n) ↦ R) i :
              R →ₗ[R] R) :
            (a : R) → R)
          1 :
        R)
      ((f ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i : (a : R) → R) 1 : R)
⊢ (fun (v : n → R) ↦ ({ toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ } : (n → R) →ₗ[R] R))
      ((fun (f : Dual R (n → R)) (i : n) ↦
          ((f : (a : n → R) → R)
              (((LinearMap.single R (fun (a : n) ↦ R) i : R →ₗ[R] (i : n) → R) : (a : R) → (i : n) → R) 1 :
                (i : n) → R) :
            R))
        f) =
    f

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Dual
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
f : Dual R (n → R)
i : n
⊢ Eq (α := R)
    ((((fun (v : n → R) ↦ ({ toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ } : (n → R) →ₗ[R] R))
                ((fun (f : Dual R (n → R)) (i : n) ↦
                    ((f : (a : n → R) → R)
                        (((LinearMap.single R (fun (a : n) ↦ R) i : R →ₗ[R] (i : n) → R) : (a : R) → (i : n) → R) 1 :
                          (i : n) → R) :
                      R))
                  f) ∘ₗ
              LinearMap.single R (fun (i : n) ↦ R) i :
            R →ₗ[R] R) :
          (a : R) → R)
        1 :
      R)
    ((f ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i : (a : R) → R) 1 : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.FiniteDimensional
Goal:
m : Type u_1
n : Type u_2
R : Type v
inst : Field R
inst_1 : Finite m
inst_2 : Finite n
⊢ FiniteDimensional R (Matrix m n R)

Tactic:
Module.Finite.matrix

Premises used: Module.Finite.matrix
-- Module: Mathlib.LinearAlgebra.Matrix.FiniteDimensional
Goal:
K : Type u_1
inst : Field K
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module K W
inst_6 : FiniteDimensional K W
⊢ FiniteDimensional K (V →ₗ[K] W)

Tactic:
Module.Finite.linearMap _ _ _ _

Premises used: Module.Finite.linearMap
-- Module: Mathlib.LinearAlgebra.Matrix.FiniteDimensional
Goal:
K : Type u_1
inst : Field K
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module K W
inst_6 : FiniteDimensional K W
A : Type u_4
inst_7 : Ring A
inst_8 : Algebra K A
inst_9 : Module A V
inst_10 : IsScalarTower K A V
inst_11 : Module A W
inst_12 : IsScalarTower K A W
⊢ FiniteDimensional K (V →ₗ[A] W)

Tactic:
FiniteDimensional.of_injective (restrictScalarsₗ K A V W K) (restrictScalars_injective _)

Premises used: FiniteDimensional.of_injective, LinearMap.restrictScalarsₗ, LinearMap.restrictScalars_injective
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : R
A B : FixedDetMatrix n R m
h : (↑A : Matrix n n R) = (↑B : Matrix n n R)
mk :
  ∀ (val : Matrix n n R) (property : val.det = m)
    (h : (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val property) : Matrix n n R) = (↑B : Matrix n n R)),
    Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val property = B
⊢ A = B

Tactic:
cases A
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : R
B : FixedDetMatrix n R m
val : Matrix n n R
property : val.det = m
h : (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val property) : Matrix n n R) = (↑B : Matrix n n R)
mk :
  ∀ (val_1 : Matrix n n R) (property_1 : val_1.det = m)
    (h :
      (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val property) : Matrix n n R) =
        (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val_1 property_1) : Matrix n n R)),
    Eq (α := FixedDetMatrix n R m) (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val property)
      (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val_1 property_1)
⊢ Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val property = B

Tactic:
cases B
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : R
val : Matrix n n R
property : val.det = m
val_1 : Matrix n n R
property_1 : val_1.det = m
h :
  (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val property) : Matrix n n R) =
    (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val_1 property_1) : Matrix n n R)
⊢ Eq (α := FixedDetMatrix n R m) (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val property)
    (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val_1 property_1)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : R
A B : FixedDetMatrix n R m
h : ∀ (i j : n), (↑A : Matrix n n R) i j = (↑B : Matrix n n R) i j
h₁ : (↑A : Matrix n n R) = (↑B : Matrix n n R)
⊢ A = B

Tactic:
apply ext'

Premises used: FixedDetMatrices.ext'
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : R
A B : FixedDetMatrix n R m
h h₁ : ∀ (i j : n), (↑A : Matrix n n R) i j = (↑B : Matrix n n R) i j
⊢ (↑A : Matrix n n R) = (↑B : Matrix n n R)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : R
A B : FixedDetMatrix n R m
h : ∀ (i j : n), (↑A : Matrix n n R) i j = (↑B : Matrix n n R) i j
i j : n
⊢ (↑A : Matrix n n R) i j = (↑B : Matrix n n R) i j

Tactic:
apply h
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : R
g : SpecialLinearGroup n R
A : FixedDetMatrix n R m
⊢ ((↑g : Matrix n n R) * (↑A : Matrix n n R)).det = m

Tactic:
simp only [det_mul, SpecialLinearGroup.det_coe, A.2, one_mul]

Premises used: Matrix.SpecialLinearGroup.det_coe, Matrix.det_mul, one_mul, Subtype.property
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : R
g : SpecialLinearGroup n R
A : FixedDetMatrix n R m
⊢ g • A = Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) ((↑g : Matrix n n R) * (↑A : Matrix n n R)) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : R
x y : SpecialLinearGroup n R
b : FixedDetMatrix n R m
simp_rw :
  Eq (α := FixedDetMatrix n R m)
    (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) ((↑(x * y) : Matrix n n R) * (↑b : Matrix n n R)) ⋯)
    (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m)
      ((↑x : Matrix n n R) * ((↑y : Matrix n n R) * (↑b : Matrix n n R))) ⋯)
simp_rw₁ :
  Eq (α := FixedDetMatrix n R m)
    (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) ((↑(x * y) : Matrix n n R) * (↑b : Matrix n n R)) ⋯)
    (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m)
      ((↑x : Matrix n n R) * (↑y : Matrix n n R) * (↑b : Matrix n n R)) ⋯)
⊢ (x * y) • b = x • y • b

Tactic:
simp_rw [smul_def, ← mul_assoc, coe_mul]

Premises used: mul_assoc, FixedDetMatrices.smul_def, Matrix.SpecialLinearGroup.coe_mul
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : R
b : FixedDetMatrix n R m
⊢ Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) ((↑1 : Matrix n n R) * (↑b : Matrix n n R)) ⋯ = b

Tactic:
simp only [coe_one, one_mul, Subtype.coe_eta]

Premises used: Matrix.SpecialLinearGroup.coe_one, Subtype.coe_eta, one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : R
g : SpecialLinearGroup n R
A : FixedDetMatrix n R m
rw rw₁ :
  (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) ((↑g : Matrix n n R) * (↑A : Matrix n n R)) ⋯) :
      Matrix n n R) =
    (↑g : Matrix n n R) * (↑A : Matrix n n R)
⊢ (↑(g • A) : Matrix n n R) = (↑g : Matrix n n R) * (↑A : Matrix n n R)

Tactic:
rw [smul_def]

Premises used: FixedDetMatrices.smul_def
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0
this :
  (↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0
rw : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0|
⊢ |(↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0|

Tactic:
rw [this, abs_eq_self.mpr (Int.emod_nonneg (A.1 0 0) h)]

Premises used: Iff.mpr, OfNat.ofNat, Subtype.val, abs_eq_self, Int.emod_nonneg