awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.Invertible (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
⊢ 1 + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
      (A *
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                    (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
                C *
              V *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) +
        U * C * V *
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                    (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
                C *
              V *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)) =
    1
have rw : U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ =
  A *
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
            C *
          V *
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) +
    U * C * V *
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
            C *
          V *
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)
Tactic: rw [add_sub_assoc, add_eq_left, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Matrix.Invertible (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
⊢ U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ =
    U * C *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
            C *
          V *
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ +
      U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
            C *
          V *
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _
have simp : U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ =
  (U + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U) * C *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
            (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
        C *
      V *
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _
Tactic: simp only [← Matrix.add_mul]
-- Lean 4 proof step from Mathlib.Data.Matrix.Invertible (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
⊢ U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ =
    (U + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U) * C *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
          C *
        V *
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _
have e_a : U =
  (U + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U) * C *
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
      (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Matrix.Invertible (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
⊢ U =
    (U + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U) * C *
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
        (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _
have e_a : U * (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) =
  (U + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U) * C
Tactic: rw [← Matrix.mul_right_eq_iff_eq_mul_invOf]
-- Lean 4 proof step from Mathlib.Data.Matrix.Invertible (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                  (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
              C *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) *
      (A + U * C * V) =
    1
have simp : 1 -
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                  (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
              C *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
        A +
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * C * V) -
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                  (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
              C *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
        (U * C * V)) =
  1
Tactic: simp only [Matrix.mul_add, Matrix.sub_mul, invOf_mul_self']
-- Lean 4 proof step from Mathlib.Data.Matrix.Invertible (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
⊢ 1 -
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                    (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
                C *
              V *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
          A +
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * C * V) -
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                    (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
                C *
              V *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
          (U * C * V)) =
    1
have rw : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
          C *
        V *
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
    A =
  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * C * V) -
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
            C *
          V *
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
      (U * C * V)
Tactic: rw [sub_add, sub_eq_self, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Matrix.Invertible (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
            C *
          V *
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
      A =
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * C * V) -
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                  (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
              C *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
        (U * C * V)
have simp : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
    (U *
      (C *
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
            (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
          (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A)))))) =
  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
    (U *
      (C *
        (V -
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
            (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V))))))))
Tactic: simp only [Matrix.mul_assoc, ← Matrix.mul_sub]
-- Lean 4 proof step from Mathlib.Data.Matrix.Invertible (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
      (U *
        (C *
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
            (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A)))))) =
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
      (U *
        (C *
          (V -
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
              (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V))))))))
have e_a : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
      (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
    (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A))) =
  V -
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
        (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
      (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V)))))
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Matrix.Invertible (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
        (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
      (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A))) =
    V -
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
          (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
        (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V)))))
have e_a : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
      (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
    (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A)) +
      C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V))))) =
  V
Tactic: rw [eq_sub_iff_add_eq, ← Matrix.mul_add]
-- Lean 4 proof step from Mathlib.Data.Matrix.Invertible (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
        (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
      (C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A)) +
        C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V))))) =
    V
have e_a : C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A)) +
    C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V)))) =
  (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) * V
Tactic: rw [Matrix.invOf_mul_eq_iff_eq_mul_left]
-- Lean 4 proof step from Mathlib.Data.Matrix.Invertible (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
⊢ C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A)) +
      C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V)))) =
    (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) * V
have e_a : C * (V * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * (C * V)))) =
  C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C * V
Tactic: simp only [Matrix.add_mul, invOf_mul_self', Matrix.mul_one, add_right_inj]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
ι : Type u_10
u : m → α
s : Finset ι
v : ι → m → α
⊢ u ⬝ᵥ ∑ i ∈ s, v i = ∑ i ∈ s, u ⬝ᵥ v i
have simp : Eq.{v + 1} (α := α) (∑ x : m, ∑ i ∈ s, u x * v i x) (∑ x ∈ s, ∑ i : m, u i * v x i)
Tactic: simp only [dotProduct, Finset.sum_apply, Finset.mul_sum]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
ι : Type u_10
u : m → α
s : Finset ι
v : ι → m → α
⊢ Eq.{v + 1} (α := α) (∑ x : m, ∑ i ∈ s, u x * v i x) (∑ x ∈ s, ∑ i : m, u i * v x i)
have rw : Eq.{v + 1} (α := α) (∑ y ∈ s, ∑ x : m, u x * v y x) (∑ x ∈ s, ∑ i : m, u i * v x i)
Tactic: rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
ι : Type u_10
s : Finset ι
u : ι → m → α
v : m → α
⊢ (∑ i ∈ s, u i) ⬝ᵥ v = ∑ i ∈ s, u i ⬝ᵥ v
have simp : Eq.{v + 1} (α := α) (∑ x : m, ∑ i ∈ s, u i x * v x) (∑ x ∈ s, ∑ i : m, u x i * v i)
Tactic: simp only [dotProduct, Finset.sum_apply, Finset.sum_mul]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
ι : Type u_10
s : Finset ι
u : ι → m → α
v : m → α
⊢ Eq.{v + 1} (α := α) (∑ x : m, ∑ i ∈ s, u i x * v x) (∑ x ∈ s, ∑ i : m, u x i * v i)
have rw : Eq.{v + 1} (α := α) (∑ y ∈ s, ∑ x : m, u y x * v x) (∑ x ∈ s, ∑ i : m, u x i * v i)
Tactic: rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (hypothesis)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
⊢ diagonal v i ⬝ᵥ w = v i * w i
have this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
Tactic: have : ∀ j ≠ i, diagonal v i j * w j = 0 := fun j hij => by
    simp [diagonal_apply_ne' _ hij]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
⊢ diagonal v i ⬝ᵥ w = v i * w i
have h : v i * w i = diagonal v i i * w i
Tactic: convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
h : v i * w i = diagonal v i i * w i
⊢ diagonal v i ⬝ᵥ w = v i * w i
have convert_2 : i ∉ Finset.univ → diagonal v i i * w i = 0
Tactic: convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (hypothesis)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
⊢ v ⬝ᵥ diagonal w i = v i * w i
have this : ∀ (j : m), j ≠ i → v j * diagonal w i j = 0
Tactic: have : ∀ j ≠ i, v j * diagonal w i j = 0 := fun j hij => by
    simp [diagonal_apply_ne' _ hij]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w i j = 0
⊢ v ⬝ᵥ diagonal w i = v i * w i
have h : v i * w i = v i * diagonal w i i
Tactic: convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w i j = 0
h : v i * w i = v i * diagonal w i i
⊢ v ⬝ᵥ diagonal w i = v i * w i
have convert_2 : i ∉ Finset.univ → v i * diagonal w i i = 0
Tactic: convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (hypothesis)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
⊢ (v ⬝ᵥ fun (j : m) ↦ diagonal w j i) = v i * w i
have this : ∀ (j : m), j ≠ i → v j * diagonal w j i = 0
Tactic: have : ∀ j ≠ i, v j * diagonal w j i = 0 := fun j hij => by
    simp [diagonal_apply_ne _ hij]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w j i = 0
⊢ (v ⬝ᵥ fun (j : m) ↦ diagonal w j i) = v i * w i
have h : v i * w i = v i * diagonal w i i
Tactic: convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w j i = 0
h : v i * w i = v i * diagonal w i i
⊢ (v ⬝ᵥ fun (j : m) ↦ diagonal w j i) = v i * w i
have convert_2 : i ∉ Finset.univ → v i * diagonal w i i = 0
Tactic: convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (hypothesis)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
⊢ Pi.single (M := fun (a : m) ↦ α) i x ⬝ᵥ v = x * v i
have this : ∀ (j : m), j ≠ i → HMul.hMul (α := α) (Pi.single (M := fun (a : m) ↦ α) i x j : α) (v j) = 0
Tactic: have : ∀ j ≠ i, (Pi.single i x : m → α) j * v j = 0 := fun j hij => by
    simp [Pi.single_eq_of_ne hij]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → HMul.hMul (α := α) (Pi.single (M := fun (a : m) ↦ α) i x j : α) (v j) = 0
⊢ Pi.single (M := fun (a : m) ↦ α) i x ⬝ᵥ v = x * v i
have h : x * v i = HMul.hMul (α := α) (Pi.single (M := fun (a : m) ↦ α) i x i : α) (v i)
Tactic: convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → HMul.hMul (α := α) (Pi.single (M := fun (a : m) ↦ α) i x j : α) (v j) = 0
h : x * v i = HMul.hMul (α := α) (Pi.single (M := fun (a : m) ↦ α) i x i : α) (v i)
⊢ Pi.single (M := fun (a : m) ↦ α) i x ⬝ᵥ v = x * v i
have convert_2 : i ∉ Finset.univ → HMul.hMul (α := α) (Pi.single (M := fun (a : m) ↦ α) i x i : α) (v i) = 0
Tactic: convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (hypothesis)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
⊢ v ⬝ᵥ Pi.single (M := fun (a : m) ↦ α) i x = v i * x
have this : ∀ (j : m), j ≠ i → HMul.hMul (β := α) (v j) (Pi.single (M := fun (a : m) ↦ α) i x j : α) = 0
Tactic: have : ∀ j ≠ i, v j * (Pi.single i x : m → α) j = 0 := fun j hij => by
    simp [Pi.single_eq_of_ne hij]
-- Lean 4 proof step from Mathlib.Data.Matrix.Mul (goal)
Goal:
m : Type u_2
α : Type v
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → HMul.hMul (β := α) (v j) (Pi.single (M := fun (a : m) ↦ α) i x j : α) = 0
⊢ v ⬝ᵥ Pi.single (M := fun (a : m) ↦ α) i x = v i * x
have h : v i * x = HMul.hMul (β := α) (v i) (Pi.single (M := fun (a : m) ↦ α) i x i : α)
Tactic: convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1