awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
this_1 :
  ∀ (i : m),
    Eq (α := Submodule K (m → K))
      (ker (M₂ := K)
        (proj (φ := fun (a : m) ↦ K) i ∘ₗ (toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w) :
          (m → K) →ₗ[K] K))
      (comap (R₂ := K) (M₂ := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)) (ker (proj (φ := fun (a : m) ↦ K) i)))
this : Subset.{u_1} (α := Set m) univ ({i : m | w i = 0} ∪ {i : m | w i = 0}ᶜ)
⊢ Eq (α := Submodule K (m → K)) (⨅ (i : m), ⨅ (_ : w i ≠ 0), ker (proj (φ := fun (a : m) ↦ K) i))
    (⨆ (i : m),
      ⨆ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))

Tactic:
exact (iSup_range_single_eq_iInf_ker_proj K (fun _ : m => K) disjoint_compl_right this
    (Set.toFinite _)).symm

Premises used: LinearMap.iSup_range_single_eq_iInf_ker_proj, Set.toFinite, disjoint_compl_right, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
rw :
  Eq (α := Submodule K (m → K))
    (⨆ (i : m),
      Submodule.map (M := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w))
        (LinearMap.range (LinearMap.single K (fun (a : m) ↦ K) i)))
    (⨆ (i : m), ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
⊢ Eq (α := Submodule K (m → K))
    (LinearMap.range (R := K) (M := m → K) (τ₁₂ := RingHom.id K)
      ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)))
    (⨆ (i : m), ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))

Tactic:
rw [← Submodule.map_top, ← iSup_range_single, Submodule.map_iSup]

Premises used: Submodule.map_iSup, LinearMap.iSup_range_single, Submodule.map_top
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
e_s :
  Eq (α := m → Submodule K (m → K))
    (fun (i : m) ↦
      Submodule.map (M := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w))
        (LinearMap.range (LinearMap.single K (fun (a : m) ↦ K) i)))
    fun (i : m) ↦ ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i)
⊢ Eq (α := Submodule K (m → K))
    (⨆ (i : m),
      Submodule.map (M := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w))
        (LinearMap.range (LinearMap.single K (fun (a : m) ↦ K) i)))
    (⨆ (i : m), ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
e_s :
  ∀ (i : m),
    Eq (α := Submodule K (m → K))
      (Submodule.map (M := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w))
        (LinearMap.range (LinearMap.single K (fun (a : m) ↦ K) i)))
      (⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
⊢ Eq (α := m → Submodule K (m → K))
    (fun (i : m) ↦
      Submodule.map (M := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w))
        (LinearMap.range (LinearMap.single K (fun (a : m) ↦ K) i)))
    fun (i : m) ↦ ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i)

Tactic:
funext i
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
i : m
e_s :
  Eq (α := Submodule K (m → K))
    (LinearMap.range (M := K)
      ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w) ∘ₗ LinearMap.single K (fun (a : m) ↦ K) i :
        K →ₗ[K] m → K))
    (⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
e_s₁ :
  (HSMul.hSMul (β := K →ₗ[K] (i : m) → K) (w i) (LinearMap.single K (fun (x : m) ↦ K) i : K →ₗ[K] (i : m) → K)).range =
    ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i)
e_s₂ e_s₃ :
  (HSMul.hSMul (β := K →ₗ[K] (i : m) → K) (w i) (LinearMap.single K (fun (x : m) ↦ K) i : K →ₗ[K] (i : m) → K)).range =
    (HSMul.hSMul (β := K →ₗ[K] (i : m) → K) (w i) (LinearMap.single K (fun (x : m) ↦ K) i : K →ₗ[K] (i : m) → K)).range
⊢ Eq (α := Submodule K (m → K))
    (Submodule.map (M := m → K) (σ₁₂ := RingHom.id K) ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w))
      (LinearMap.range (LinearMap.single K (fun (a : m) ↦ K) i)))
    (⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))

Tactic:
rw [← LinearMap.range_comp, diagonal_comp_single, ← range_smul']

Premises used: LinearMap.range_comp, LinearMap.range_smul', Matrix.diagonal_comp_single
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Field K
inst_2 : DecidableEq m
inst_3 : DecidableEq K
w : m → K
rw rw₁ : Subset.{u_1} (α := Set m) univ univ
⊢ Subset.{u_1} (α := Set m) univ ({i : m | w i = 0}ᶜ ∪ {i : m | w i = 0})

Tactic:
rw [Set.compl_union_self]

Premises used: Set.compl_union_self
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Field K
inst_2 : DecidableEq m
inst_3 : DecidableEq K
w : m → K
⊢ Subset.{u_1} (α := Set m) univ ({i : m | w i = 0}ᶜ ∪ {i : m | w i = 0})

Tactic:
have hu : univ ⊆ { i : m | w i = 0 }ᶜ ∪ { i : m | w i = 0 } := by rw [Set.compl_union_self]
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Field K
inst_2 : DecidableEq m
inst_3 : DecidableEq K
w : m → K
hu : Subset.{u_1} (α := Set m) univ ({i : m | w i = 0}ᶜ ∪ {i : m | w i = 0})
⊢ Disjoint.{u_1} (α := Set m) {i : m | w i ≠ 0} {i : m | w i = 0}

Tactic:
have hd : Disjoint { i : m | w i ≠ 0 } { i : m | w i = 0 } := disjoint_compl_left
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Field K
inst_2 : DecidableEq m
inst_3 : DecidableEq K
w : m → K
hu : Subset.{u_1} (α := Set m) univ ({i : m | w i = 0}ᶜ ∪ {i : m | w i = 0})
hd : Disjoint.{u_1} (α := Set m) {i : m | w i ≠ 0} {i : m | w i = 0}
⊢ Eq (α := Submodule K ((i : m) → (fun (x : m) ↦ K) i))
    (⨆ (i : m), ⨆ (_ : Membership.mem (γ := Set m) {i : m | w i ≠ 0} i), range (single K (fun (x : m) ↦ K) i))
    (⨅ (i : m), ⨅ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), ker (proj (φ := fun (x : m) ↦ K) i))

Tactic:
have B₁ := iSup_range_single_eq_iInf_ker_proj K (fun _ : m => K) hd hu (Set.toFinite _)
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Field K
inst_2 : DecidableEq m
inst_3 : DecidableEq K
w : m → K
hu : Subset.{u_1} (α := Set m) univ ({i : m | w i = 0}ᶜ ∪ {i : m | w i = 0})
hd : Disjoint.{u_1} (α := Set m) {i : m | w i ≠ 0} {i : m | w i = 0}
B₁ :
  Eq (α := Submodule K ((i : m) → (fun (x : m) ↦ K) i))
    (⨆ (i : m), ⨆ (_ : Membership.mem (γ := Set m) {i : m | w i ≠ 0} i), range (single K (fun (x : m) ↦ K) i))
    (⨅ (i : m), ⨅ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), ker (proj (φ := fun (x : m) ↦ K) i))
have :
  ∀
    (B₂ :
      ↥(⨅ (i : m), ⨅ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), ker (proj (φ := fun (x : m) ↦ K) i)) ≃ₗ[K]
        (i : (↑{i : m | w i ≠ 0} : Type u_1)) → (fun (x : m) ↦ K) (↑i : m)),
    rank (K := K) (V := m → K) (V' := m → K) ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (Matrix.diagonal w)) =
      (↑(Fintype.card.{u_1} { i : m // w i ≠ 0 }) : Cardinal.{max u u_1})
⊢ rank (K := K) (V := m → K) (V' := m → K) ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (Matrix.diagonal w)) =
    (↑(Fintype.card.{u_1} { i : m // w i ≠ 0 }) : Cardinal.{max u u_1})

Tactic:
have B₂ := iInfKerProjEquiv K (fun _ ↦ K) hd hu
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Field K
inst_2 : DecidableEq m
inst_3 : DecidableEq K
w : m → K
hu : Subset.{u_1} (α := Set m) univ ({i : m | w i = 0}ᶜ ∪ {i : m | w i = 0})
hd : Disjoint.{u_1} (α := Set m) {i : m | w i ≠ 0} {i : m | w i = 0}
B₁ :
  Eq (α := Submodule K ((i : m) → (fun (x : m) ↦ K) i))
    (⨆ (i : m), ⨆ (_ : Membership.mem (γ := Set m) {i : m | w i ≠ 0} i), range (single K (fun (x : m) ↦ K) i))
    (⨅ (i : m), ⨅ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), ker (proj (φ := fun (x : m) ↦ K) i))
B₂ :
  ↥(⨅ (i : m), ⨅ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), ker (proj (φ := fun (x : m) ↦ K) i)) ≃ₗ[K]
    (i : (↑{i : m | w i ≠ 0} : Type u_1)) → (fun (x : m) ↦ K) (↑i : m)
rw :
  Module.rank K
      ↥(⨅ (i : m), ⨅ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), ker (proj (φ := fun (x : m) ↦ K) i)) =
    Module.rank K ({ i : m // w i ≠ 0 } → K)
⊢ rank (K := K) (V := m → K) (V' := m → K) ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (Matrix.diagonal w)) =
    (↑(Fintype.card.{u_1} { i : m // w i ≠ 0 }) : Cardinal.{max u u_1})

Tactic:
rw [LinearMap.rank, range_diagonal, B₁, ← @rank_fun' K]

Premises used: LinearMap.rank, Matrix.range_diagonal, rank_fun'
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Field K
inst_2 : DecidableEq m
inst_3 : DecidableEq K
w : m → K
hu : Subset.{u_1} (α := Set m) univ ({i : m | w i = 0}ᶜ ∪ {i : m | w i = 0})
hd : Disjoint.{u_1} (α := Set m) {i : m | w i ≠ 0} {i : m | w i = 0}
B₁ :
  Eq (α := Submodule K ((i : m) → (fun (x : m) ↦ K) i))
    (⨆ (i : m), ⨆ (_ : Membership.mem (γ := Set m) {i : m | w i ≠ 0} i), range (single K (fun (x : m) ↦ K) i))
    (⨅ (i : m), ⨅ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), ker (proj (φ := fun (x : m) ↦ K) i))
B₂ :
  ↥(⨅ (i : m), ⨅ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), ker (proj (φ := fun (x : m) ↦ K) i)) ≃ₗ[K]
    (i : (↑{i : m | w i ≠ 0} : Type u_1)) → (fun (x : m) ↦ K) (↑i : m)
f :
  ↥(⨅ (i : m), ⨅ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), ker (proj (φ := fun (x : m) ↦ K) i)) ≃ₗ[K]
    { i : m // w i ≠ 0 } → K
⊢ Module.rank K
      ↥(⨅ (i : m), ⨅ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), ker (proj (φ := fun (x : m) ↦ K) i)) =
    Module.rank K ({ i : m // w i ≠ 0 } → K)

Tactic:
apply LinearEquiv.rank_eq

Premises used: LinearEquiv.rank_eq
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Field K
inst_2 : DecidableEq m
inst_3 : DecidableEq K
w : m → K
hu : Subset.{u_1} (α := Set m) univ ({i : m | w i = 0}ᶜ ∪ {i : m | w i = 0})
hd : Disjoint.{u_1} (α := Set m) {i : m | w i ≠ 0} {i : m | w i = 0}
B₁ :
  Eq (α := Submodule K ((i : m) → (fun (x : m) ↦ K) i))
    (⨆ (i : m), ⨆ (_ : Membership.mem (γ := Set m) {i : m | w i ≠ 0} i), range (single K (fun (x : m) ↦ K) i))
    (⨅ (i : m), ⨅ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), ker (proj (φ := fun (x : m) ↦ K) i))
B₂ :
  ↥(⨅ (i : m), ⨅ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), ker (proj (φ := fun (x : m) ↦ K) i)) ≃ₗ[K]
    (i : (↑{i : m | w i ≠ 0} : Type u_1)) → (fun (x : m) ↦ K) (↑i : m)
⊢ ↥(⨅ (i : m), ⨅ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), ker (proj (φ := fun (x : m) ↦ K) i)) ≃ₗ[K]
    { i : m // w i ≠ 0 } → K

Tactic:
apply B₂
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Semiring R
inst_1 : Fintype n
v w : n → R
h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u
h₁ : ∀ (x : n), v x = w x
⊢ v = w

Tactic:
funext x
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Semiring R
inst_1 : Fintype n
v w : n → R
h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u
x : n
h₁ : v ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1 = w x
h₂ : v ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1 = w ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1
h₃ h₄ : w ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1 = w ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1
⊢ v x = w x

Tactic:
rw [← dotProduct_single_one v x, ← dotProduct_single_one w x, h]

Premises used: dotProduct_single_one
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Semiring R
inst_1 : Fintype n
v w : n → R
h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u
x : n
h₁ : v ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1 = w x
h₂ : v ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1 = w ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1
h₃ h₄ : w ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1 = w ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1
⊢ v x = w x

Tactic:
classical rw [← dotProduct_single_one v x, ← dotProduct_single_one w x, h]
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Semiring R
inst_1 : Fintype n
v w : n → R
⊢ (∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u) ↔ v = w

Tactic:
⟨fun h => dotProduct_eq v w h, fun h _ => h ▸ rfl⟩

Premises used: Eq.rec, dotProduct_eq, Iff.intro, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Semiring R
inst_1 : Fintype n
v : n → R
h : ∀ (w : n → R), v ⬝ᵥ w = 0
⊢ v = 0

Tactic:
dotProduct_eq _ _ fun u => (h u).symm ▸ (zero_dotProduct u).symm

Premises used: dotProduct_eq
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Semiring R
inst_1 : Fintype n
v : n → R
⊢ (∀ (w : n → R), v ⬝ᵥ w = 0) ↔ v = 0

Tactic:
⟨fun h => dotProduct_eq_zero v h, fun h w => h.symm ▸ zero_dotProduct w⟩

Premises used: dotProduct_eq_zero, zero_dotProduct, Eq.rec, Iff.intro, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Fintype n
v w : n → R
hv : 0 ≤ v
hw : 0 ≤ w
⊢ 0 ≤ v ⬝ᵥ w

Tactic:
Finset.sum_nonneg (fun i _ => mul_nonneg (hv i) (hw i))

Premises used: mul_nonneg, dotProduct, Finset.sum_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Fintype n
u v w : n → R
huv : u ≤ v
hw : 0 ≤ w
unfold : LE.le.{u_4} (α := R) (∑ i : n, u i * w i) (∑ i : n, v i * w i)
⊢ u ⬝ᵥ w ≤ v ⬝ᵥ w

Tactic:
unfold dotProduct

Premises used: dotProduct
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Fintype n
u v w : n → R
huv : u ≤ v
hw : 0 ≤ w
h : ∀ (i : n), Membership.mem (γ := Finset n) Finset.univ i → 0 ≤ w i
h₁ : ∀ (i : n), Membership.mem (γ := Finset n) Finset.univ i → u i ≤ v i
⊢ LE.le.{u_4} (α := R) (∑ i : n, u i * w i) (∑ i : n, v i * w i)

Tactic:
gcongr
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Fintype n
u v w : n → R
huv : u ≤ v
hw : 0 ≤ w
i : n
h : Membership.mem (γ := Finset n) Finset.univ i
⊢ 0 ≤ w i

Tactic:
apply_rules
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Fintype n
u v w : n → R
huv : u ≤ v
hw : 0 ≤ w
i : n
h : Membership.mem (γ := Finset n) Finset.univ i
⊢ u i ≤ v i

Tactic:
apply_rules
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Fintype n
u v w : n → R
huv : u ≤ v
hw : 0 ≤ w
unfold : LE.le.{u_4} (α := R) (∑ i : n, w i * u i) (∑ i : n, w i * v i)
⊢ w ⬝ᵥ u ≤ w ⬝ᵥ v

Tactic:
unfold dotProduct

Premises used: dotProduct
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Fintype n
u v w : n → R
huv : u ≤ v
hw : 0 ≤ w
h : ∀ (i : n), Membership.mem (γ := Finset n) Finset.univ i → 0 ≤ w i
h₁ : ∀ (i : n), Membership.mem (γ := Finset n) Finset.univ i → u i ≤ v i
⊢ LE.le.{u_4} (α := R) (∑ i : n, w i * u i) (∑ i : n, w i * v i)

Tactic:
gcongr
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : Ring R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
v : n → R
⊢ (∀ (i : n), Membership.mem (γ := Finset n) Finset.univ i → v i * v i = 0) ↔ v = 0

Tactic:
simp [funext_iff]

Premises used: funext_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
v : n → R
⊢ 0 ≤ star v ⬝ᵥ v

Tactic:
Fintype.sum_nonneg fun _ => star_mul_self_nonneg _

Premises used: dotProduct, star_mul_self_nonneg, Fintype.sum_nonneg
-- 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
v : n → R
⊢ 0 ≤ v ⬝ᵥ star v

Tactic:
Fintype.sum_nonneg fun _ => mul_star_self_nonneg _

Premises used: dotProduct, mul_star_self_nonneg, Fintype.sum_nonneg
-- 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
⊢ Eq (α := n → R) (fun (x : n) ↦ star (v x) * v x) 0 ↔ v = 0

Tactic:
simp [funext_iff, mul_eq_zero]

Premises used: funext_iff, mul_eq_zero
-- 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
⊢ Eq (α := n → R) (fun (x : n) ↦ v x * star (v x)) 0 ↔ v = 0

Tactic:
simp [funext_iff, mul_eq_zero]

Premises used: funext_iff, mul_eq_zero
-- Module: Mathlib.LinearAlgebra.Matrix.DotProduct
Goal:
m : Type u_1
R : Type u_4
inst : Fintype m
inst_1 : PartialOrder R
inst_2 : NonUnitalRing R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
inst_5 : NoZeroDivisors R
n : Type u_5
A : Matrix m n R
⊢ Aᴴ * A = 0 ↔ A = 0

Tactic:
⟨fun h => Matrix.ext fun i j =>
    (congr_fun <| dotProduct_star_self_eq_zero.1 <| Matrix.ext_iff.2 h j j) i,
  fun h => h ▸ Matrix.mul_zero _⟩

Premises used: Iff.mpr, dotProduct_star_self_eq_zero, Eq.rec, Matrix.mul_zero, Iff.intro, Iff.mp, Matrix.ext_iff, congr_fun, OfNat.ofNat, Eq.symm, Matrix.conjTranspose, Matrix.ext
-- 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
m : Type u_5
A : Matrix m n R
⊢ A * Aᴴ = 0 ↔ A = 0

Tactic:
⟨fun h => Matrix.ext fun i j =>
    (congr_fun <| dotProduct_self_star_eq_zero.1 <| Matrix.ext_iff.2 h i i) j,
  fun h => h ▸ Matrix.zero_mul _⟩

Premises used: Iff.mpr, Eq.rec, Iff.intro, Iff.mp, Matrix.zero_mul, Matrix.ext_iff, dotProduct_self_star_eq_zero, congr_fun, OfNat.ofNat, Eq.symm, Matrix.conjTranspose, Matrix.ext
-- 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
p : Type u_5
A : Matrix m n R
B : Matrix n p R
h : A * B = 0
⊢ Aᴴ * A * B = 0

Tactic:
simp only [Matrix.mul_assoc, h, Matrix.mul_zero]

Premises used: Matrix.mul_assoc, Matrix.mul_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
p : Type u_5
A : Matrix m n R
B : Matrix n p R
refine : ∀ (h : Aᴴ * A * B = 0), A * B = 0
⊢ Aᴴ * A * B = 0 ↔ A * B = 0

Tactic:
refine ⟨fun h => ?_, fun h => by simp only [Matrix.mul_assoc, h, Matrix.mul_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
p : Type u_5
A : Matrix m n R
B : Matrix n p R
h : Aᴴ * A * B = 0
⊢ Bᴴ * (Aᴴ * A * B) = Bᴴ * 0

Tactic:
apply_fun (Bᴴ * ·) at h

Premises used: HMul.hMul, Matrix.conjTranspose
-- 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
p : Type u_5
A : Matrix m n R
B : Matrix n p R
h : Bᴴ * (Aᴴ * A * B) = Bᴴ * 0
rwa : ∀ (h : Bᴴ * (Aᴴ * A * B) = 0), A * B = 0
rwa₁ : ∀ (h : Bᴴ * (Aᴴ * (A * B)) = 0), A * B = 0
rwa₂ : ∀ (h : Bᴴ * Aᴴ * (A * B) = 0), A * B = 0
rwa₃ : ∀ (h : (A * B)ᴴ * (A * B) = 0), A * B = 0
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (h : A * B = 0), A * B = 0
⊢ A * B = 0

Tactic:
rwa [Matrix.mul_zero, Matrix.mul_assoc, ← Matrix.mul_assoc, ← conjTranspose_mul,
    conjTranspose_mul_self_eq_zero] at h

Premises used: Matrix.mul_assoc, Matrix.mul_zero, Matrix.conjTranspose_mul_self_eq_zero, Matrix.conjTranspose_mul
-- 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
p : Type u_5
A : Matrix m n R
B : Matrix m p R
⊢ A * Aᴴ * B = 0 ↔ Aᴴ * B = 0

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

Premises used: Matrix.conjTranspose, Matrix.conjTranspose_mul_self_mul_eq_zero, Matrix.conjTranspose_conjTranspose
-- 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
p : Type u_5
A : Matrix m n R
B : Matrix p m R
rw : (B * (A * Aᴴ))ᴴ = 0 ↔ B * A = 0
rw₁ : (A * Aᴴ)ᴴ * Bᴴ = 0 ↔ B * A = 0
rw₂ : Aᴴᴴ * Aᴴ * Bᴴ = 0 ↔ B * A = 0
rw₃ : A * Aᴴ * Bᴴ = 0 ↔ B * A = 0
rw₄ : Aᴴ * Bᴴ = 0 ↔ B * A = 0
rw₅ : (B * A)ᴴ = 0 ↔ B * A = 0
rw₆ rw₇ : B * A = 0 ↔ B * A = 0
⊢ B * (A * Aᴴ) = 0 ↔ B * A = 0

Tactic:
rw [← conjTranspose_eq_zero, conjTranspose_mul, conjTranspose_mul, conjTranspose_conjTranspose,
    self_mul_conjTranspose_mul_eq_zero, ← conjTranspose_mul, conjTranspose_eq_zero]

Premises used: Matrix.conjTranspose_eq_zero, Matrix.self_mul_conjTranspose_mul_eq_zero, Matrix.conjTranspose_conjTranspose, Matrix.conjTranspose_mul
-- 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
p : Type u_5
A : Matrix m n R
B : Matrix p n R
⊢ B * (Aᴴ * A) = 0 ↔ B * Aᴴ = 0

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

Premises used: Matrix.conjTranspose, Matrix.conjTranspose_conjTranspose, Matrix.mul_self_mul_conjTranspose_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 : n → R
⊢ (Aᴴ * A) *ᵥ v = 0 ↔ A *ᵥ v = 0

Tactic:
simpa only [← Matrix.replicateCol_mulVec, replicateCol_eq_zero] using
    conjTranspose_mul_self_mul_eq_zero A (replicateCol (Fin 1) v)

Premises used: Matrix.replicateCol, Matrix.replicateCol_mulVec, Matrix.replicateCol_eq_zero, OfNat.ofNat, Matrix.conjTranspose_mul_self_mul_eq_zero, Fin
-- 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
⊢ (A * Aᴴ) *ᵥ v = 0 ↔ Aᴴ *ᵥ v = 0

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

Premises used: Matrix.conjTranspose_mul_self_mulVec_eq_zero, Matrix.conjTranspose, Matrix.conjTranspose_conjTranspose