awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Diagonal (hypothesis)
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
⊢ 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})
have hu : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Diagonal (hypothesis)
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})
⊢ 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})
have hd : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Diagonal (hypothesis)
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}
⊢ 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})
have 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))
Tactic: have B₁ := iSup_range_single_eq_iInf_ker_proj K (fun _ : m => K) hd hu (Set.toFinite _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Diagonal (goal)
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))
⊢ 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})
have 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})
Tactic: have B₂ := iInfKerProjEquiv K (fun _ ↦ K) hd hu
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Diagonal (goal)
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)
⊢ 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})
have 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)
Tactic: rw [LinearMap.rank, range_diagonal, B₁, ← @rank_fun' K]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Diagonal (goal)
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)
⊢ 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)
have 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
Tactic: apply LinearEquiv.rank_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ v = w
have h₁ : ∀ (x : n), v x = w x
Tactic: funext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ v x = w x
have h₁ : v ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1 = w x
Tactic: rw [← dotProduct_single_one v x, ← dotProduct_single_one w x, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ v x = w x
have h₂ : v ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1 = w ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1
Tactic: rw [← dotProduct_single_one v x, ← dotProduct_single_one w x, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ v x = w x
have h₃ : w ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1 = w ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1
Tactic: rw [← dotProduct_single_one v x, ← dotProduct_single_one w x, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ v x = w x
have h₁ : v ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1 = w x
Tactic: classical rw [← dotProduct_single_one v x, ← dotProduct_single_one w x, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ v x = w x
have h₂ : v ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1 = w ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1
Tactic: classical rw [← dotProduct_single_one v x, ← dotProduct_single_one w x, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ v x = w x
have h₃ : w ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1 = w ⬝ᵥ Pi.single (M := fun (a : n) ↦ R) x 1
Tactic: classical rw [← dotProduct_single_one v x, ← dotProduct_single_one w x, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ u ⬝ᵥ w ≤ v ⬝ᵥ w
have unfold : LE.le.{u_4} (α := R) (∑ i : n, u i * w i) (∑ i : n, v i * w i)
Tactic: unfold dotProduct
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ LE.le.{u_4} (α := R) (∑ i : n, u i * w i) (∑ i : n, v i * w i)
have h : ∀ (i : n), Membership.mem (γ := Finset n) Finset.univ i → 0 ≤ w i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ LE.le.{u_4} (α := R) (∑ i : n, u i * w i) (∑ i : n, v i * w i)
have h₁ : ∀ (i : n), Membership.mem (γ := Finset n) Finset.univ i → u i ≤ v i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ w ⬝ᵥ u ≤ w ⬝ᵥ v
have unfold : LE.le.{u_4} (α := R) (∑ i : n, w i * u i) (∑ i : n, w i * v i)
Tactic: unfold dotProduct
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ LE.le.{u_4} (α := R) (∑ i : n, w i * u i) (∑ i : n, w i * v i)
have h : ∀ (i : n), Membership.mem (γ := Finset n) Finset.univ i → 0 ≤ w i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ LE.le.{u_4} (α := R) (∑ i : n, w i * u i) (∑ i : n, w i * v i)
have h₁ : ∀ (i : n), Membership.mem (γ := Finset n) Finset.univ i → u i ≤ v i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ Aᴴ * A * B = 0 ↔ A * B = 0
have refine : ∀ (h : Aᴴ * A * B = 0), A * B = 0
Tactic: refine ⟨fun h => ?_, fun h => by simp only [Matrix.mul_assoc, h, Matrix.mul_zero]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (hypothesis)
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
⊢ A * B = 0
have h₁ : Bᴴ * (Aᴴ * A * B) = Bᴴ * 0
Tactic: apply_fun (Bᴴ * ·) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ A * B = 0
have rwa : ∀ (h : Bᴴ * (Aᴴ * 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ A * B = 0
have rwa₁ : ∀ (h : Bᴴ * (Aᴴ * (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ A * B = 0
have rwa₂ : ∀ (h : Bᴴ * Aᴴ * (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ A * B = 0
have rwa₃ : ∀ (h : (A * B)ᴴ * (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ A * B = 0
have rwa₄ : ∀ (h : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ B * (A * Aᴴ) = 0 ↔ B * A = 0
have rw : (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ B * (A * Aᴴ) = 0 ↔ B * A = 0
have rw₁ : (A * Aᴴ)ᴴ * Bᴴ = 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ B * (A * Aᴴ) = 0 ↔ B * A = 0
have rw₂ : Aᴴᴴ * Aᴴ * Bᴴ = 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ B * (A * Aᴴ) = 0 ↔ B * A = 0
have rw₃ : A * Aᴴ * Bᴴ = 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ B * (A * Aᴴ) = 0 ↔ B * A = 0
have rw₄ : Aᴴ * Bᴴ = 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ B * (A * Aᴴ) = 0 ↔ B * A = 0
have rw₅ : (B * 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ B * (A * Aᴴ) = 0 ↔ B * A = 0
have rw₆ : B * 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (hypothesis)
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 < star v ⬝ᵥ v ↔ v ≠ 0
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
have refine : (LT.lt (α := n → R) 0 fun (i : n) ↦ star (v i) * v i) ↔ v ≠ 0
Tactic: refine (Fintype.sum_pos_iff_of_nonneg fun i => star_mul_self_nonneg _).trans ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ (LT.lt (α := n → R) 0 fun (i : n) ↦ star (v i) * v i) ↔ v ≠ 0
have 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
Tactic: simp_rw [Pi.lt_def, Function.ne_iff, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
have refine : ∀ (i : n), 0 < star (v i) * v i ↔ v i ≠ 0
Tactic: refine (and_iff_right fun i => star_mul_self_nonneg (v i)).trans <| exists_congr fun i => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ 0 < star (v i) * v i ↔ v i ≠ 0
have mp : 0 < star (v i) * v i → v i ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.DotProduct (goal)
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
⊢ 0 < star (v i) * v i ↔ v i ≠ 0
have mpr : v i ≠ 0 → 0 < star (v i) * v i
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Dual (goal)
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₂
⊢ 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)
have 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)
Tactic: ext i j