awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.DualNumber (goal)
Goal:
R n : Type
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A B : Matrix n n (DualNumber R)
⊢ ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst ((A * B) i j),
      (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd ((A * B) i j)) =
    HMul.hMul (α := DualNumber (Matrix n n R)) (β := DualNumber (Matrix n n R))
      (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (A i j),
          (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (A i j)) :
        Matrix n n R × Matrix n n R)
      (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (B i j),
          (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (B i j)) :
        Matrix n n R × Matrix n n R)
have h1 : ∀ (i j : n),
  fst (M := Matrix n n R)
      ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst ((A * B) i j),
        (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd ((A * B) i j))
      i j =
    fst
      (HMul.hMul (α := DualNumber (Matrix n n R)) (β := DualNumber (Matrix n n R))
        (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (A i j),
            (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (A i j)) :
          Matrix n n R × Matrix n n R)
        (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (B i j),
            (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (B i j)) :
          Matrix n n R × Matrix n n R))
      i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.DualNumber (goal)
Goal:
R n : Type
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A B : Matrix n n (DualNumber R)
h1 :
  ∀ (i j : n),
    fst (M := Matrix n n R)
        ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst ((A * B) i j),
          (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd ((A * B) i j))
        i j =
      fst
        (HMul.hMul (α := DualNumber (Matrix n n R)) (β := DualNumber (Matrix n n R))
          (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (A i j),
              (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (A i j)) :
            Matrix n n R × Matrix n n R)
          (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (B i j),
              (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (B i j)) :
            Matrix n n R × Matrix n n R))
        i j
⊢ ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst ((A * B) i j),
      (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd ((A * B) i j)) =
    HMul.hMul (α := DualNumber (Matrix n n R)) (β := DualNumber (Matrix n n R))
      (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (A i j),
          (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (A i j)) :
        Matrix n n R × Matrix n n R)
      (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (B i j),
          (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (B i j)) :
        Matrix n n R × Matrix n n R)
have h2 : ∀ (i j : n),
  snd (R := Matrix n n R)
      ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst ((A * B) i j),
        (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd ((A * B) i j))
      i j =
    snd
      (HMul.hMul (α := DualNumber (Matrix n n R)) (β := DualNumber (Matrix n n R))
        (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (A i j),
            (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (A i j)) :
          Matrix n n R × Matrix n n R)
        (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (B i j),
            (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (B i j)) :
          Matrix n n R × Matrix n n R))
      i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.DualNumber (goal)
Goal:
R n : Type
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A B : Matrix n n (DualNumber R)
i j : n
⊢ fst (M := Matrix n n R)
      ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst ((A * B) i j),
        (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd ((A * B) i j))
      i j =
    fst
      (HMul.hMul (α := DualNumber (Matrix n n R)) (β := DualNumber (Matrix n n R))
        (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (A i j),
            (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (A i j)) :
          Matrix n n R × Matrix n n R)
        (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (B i j),
            (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (B i j)) :
          Matrix n n R × Matrix n n R))
      i j
have h1 : Eq (α := R) (fst (M := R) (∑ j_1 : n, A i j_1 * B j_1 j)) (∑ j_1 : n, fst (A i j_1) * fst (B j_1 j))
Tactic: dsimp [mul_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.DualNumber (goal)
Goal:
R n : Type
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A B : Matrix n n (DualNumber R)
i j : n
⊢ Eq (α := R) (fst (M := R) (∑ j_1 : n, A i j_1 * B j_1 j)) (∑ j_1 : n, fst (A i j_1) * fst (B j_1 j))
have h1 : Eq (α := R) (∑ i_1 : n, fst (A i i_1 * B i_1 j)) (∑ j_1 : n, fst (A i j_1) * fst (B j_1 j))
Tactic: simp_rw [fst_sum]
-- Lean 4 proof step from Mathlib.Data.Matrix.DualNumber (goal)
Goal:
R n : Type
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A B : Matrix n n (DualNumber R)
i j : n
⊢ snd (R := Matrix n n R)
      ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst ((A * B) i j),
        (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd ((A * B) i j))
      i j =
    snd
      (HMul.hMul (α := DualNumber (Matrix n n R)) (β := DualNumber (Matrix n n R))
        (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (A i j),
            (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (A i j)) :
          Matrix n n R × Matrix n n R)
        (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (B i j),
            (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (B i j)) :
          Matrix n n R × Matrix n n R))
      i j
have h2 : snd (R := Matrix n n R)
    ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst ((A * B) i j),
      (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd ((A * B) i j))
    i j =
  (HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        (fst (M := Matrix n n R)
            ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (A i j),
              (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (A i j)) :
          Matrix n n R)
        (snd (R := Matrix n n R)
            ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (B i j),
              (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (B i j)) :
          Matrix n n R) +
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        (snd (R := Matrix n n R)
            ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (A i j),
              (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (A i j)) :
          Matrix n n R)
        (fst (M := Matrix n n R)
            ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (B i j),
              (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (B i j)) :
          Matrix n n R))
    i j
Tactic: simp_rw [snd_mul, smul_eq_mul, op_smul_eq_mul]
-- Lean 4 proof step from Mathlib.Data.Matrix.DualNumber (goal)
Goal:
R n : Type
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A B : Matrix n n (DualNumber R)
i j : n
⊢ snd (R := Matrix n n R)
      ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst ((A * B) i j),
        (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd ((A * B) i j))
      i j =
    (HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
          (fst (M := Matrix n n R)
              ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (A i j),
                (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (A i j)) :
            Matrix n n R)
          (snd (R := Matrix n n R)
              ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (B i j),
                (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (B i j)) :
            Matrix n n R) +
        HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
          (snd (R := Matrix n n R)
              ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (A i j),
                (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (A i j)) :
            Matrix n n R)
          (fst (M := Matrix n n R)
              ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ fst (B i j),
                (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ snd (B i j)) :
            Matrix n n R))
      i j
have h2 : ∑ x : n, (fst (A i x) * snd (B x j) + snd (A i x) * fst (B x j)) =
  HAdd.hAdd (α := R) (∑ x : n, fst (A i x) * snd (B x j)) (∑ x : n, snd (A i x) * fst (B x j))
Tactic: simp only [mul_apply, snd_sum, DualNumber.snd_mul, snd_mk, of_apply, fst_mk, add_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.DualNumber (goal)
Goal:
R n : Type
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A B : Matrix n n (DualNumber R)
i j : n
⊢ ∑ x : n, (fst (A i x) * snd (B x j) + snd (A i x) * fst (B x j)) =
    HAdd.hAdd (α := R) (∑ x : n, fst (A i x) * snd (B x j)) (∑ x : n, snd (A i x) * fst (B x j))
have h2 : Eq (α := R) (∑ x : n, (fst (A i x) * snd (B x j) + snd (A i x) * fst (B x j)))
  (∑ x : n, (fst (A i x) * snd (B x j) + snd (A i x) * fst (B x j)))
Tactic: rw [← Finset.sum_add_distrib]
-- Lean 4 proof step from Mathlib.Data.Matrix.DualNumber (goal)
Goal:
R n : Type
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
r : R
⊢ Eq (α := DualNumber (Matrix n n R))
    (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦
          fst (M := R) ((algebraMap R (Matrix n n (DualNumber R)) : (a : R) → Matrix n n (DualNumber R)) r i j),
        (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦
          snd (R := R) ((algebraMap R (Matrix n n (DualNumber R)) : (a : R) → Matrix n n (DualNumber R)) r i j)) :
      Matrix n n R × Matrix n n R)
    ((algebraMap R (DualNumber (Matrix n n R)) : (a : R) → DualNumber (Matrix n n R)) r : DualNumber (Matrix n n R))
have simp_rw : Eq (α := DualNumber (Matrix n n R))
  (((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ diagonal (fun (m : n) ↦ r) i j,
      (of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ 0) :
    Matrix n n R × Matrix n n R)
  (inl (diagonal fun (m : n) ↦ r) : TrivSqZeroExt (Matrix n n R) (Matrix n n R))
Tactic: simp_rw [algebraMap_eq_inl', algebraMap_eq_diagonal, Pi.algebraMap_def,
      Algebra.algebraMap_self_apply, algebraMap_eq_inl, ← diagonal_map (inl_zero R), map_apply,
      fst_inl, snd_inl]
-- 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 : Semiring α
A : Matrix n n α
B : Matrix n m α
inst_3 : Invertible A
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (A * B) = B
have rw : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A * B = B
Tactic: rw [← Matrix.mul_assoc, invOf_mul_self, Matrix.one_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 : Semiring α
A : Matrix n n α
B : Matrix n m α
inst_3 : Invertible A
rw : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A * B = B
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (A * B) = B
have rw₁ : 1 * B = B
Tactic: rw [← Matrix.mul_assoc, invOf_mul_self, Matrix.one_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 : Semiring α
A : Matrix n n α
B : Matrix n m α
inst_3 : Invertible A
rw : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A * B = B
rw₁ : 1 * B = B
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (A * B) = B
have rw₂ : B = B
Tactic: rw [← Matrix.mul_assoc, invOf_mul_self, Matrix.one_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 : Semiring α
A : Matrix n n α
B : Matrix n m α
inst_3 : Invertible A
⊢ A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) = B
have rw : A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B = B
Tactic: rw [← Matrix.mul_assoc, mul_invOf_self, Matrix.one_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 : Semiring α
A : Matrix n n α
B : Matrix n m α
inst_3 : Invertible A
rw : A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B = B
⊢ A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) = B
have rw₁ : 1 * B = B
Tactic: rw [← Matrix.mul_assoc, mul_invOf_self, Matrix.one_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 : Semiring α
A : Matrix n n α
B : Matrix n m α
inst_3 : Invertible A
rw : A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B = B
rw₁ : 1 * B = B
⊢ A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) = B
have rw₂ : B = B
Tactic: rw [← Matrix.mul_assoc, mul_invOf_self, Matrix.one_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 : Semiring α
A : Matrix m n α
B : Matrix n n α
inst_3 : Invertible B
⊢ A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one B _ * B = A
have rw : A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one B _ * B) = A
Tactic: rw [Matrix.mul_assoc, invOf_mul_self, Matrix.mul_one]
-- 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 : Semiring α
A : Matrix m n α
B : Matrix n n α
inst_3 : Invertible B
rw : A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one B _ * B) = A
⊢ A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one B _ * B = A
have rw₁ : A * 1 = A
Tactic: rw [Matrix.mul_assoc, invOf_mul_self, Matrix.mul_one]
-- 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 : Semiring α
A : Matrix m n α
B : Matrix n n α
inst_3 : Invertible B
rw : A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one B _ * B) = A
rw₁ : A * 1 = A
⊢ A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one B _ * B = A
have rw₂ : A = A
Tactic: rw [Matrix.mul_assoc, invOf_mul_self, Matrix.mul_one]
-- 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 : Semiring α
A : Matrix m n α
B : Matrix n n α
inst_3 : Invertible B
⊢ A * B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one B _ = A
have rw : A * (B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one B _) = A
Tactic: rw [Matrix.mul_assoc, mul_invOf_self, Matrix.mul_one]
-- 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 : Semiring α
A : Matrix m n α
B : Matrix n n α
inst_3 : Invertible B
rw : A * (B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one B _) = A
⊢ A * B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one B _ = A
have rw₁ : A * 1 = A
Tactic: rw [Matrix.mul_assoc, mul_invOf_self, Matrix.mul_one]
-- 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 : Semiring α
A : Matrix m n α
B : Matrix n n α
inst_3 : Invertible B
rw : A * (B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one B _) = A
rw₁ : A * 1 = A
⊢ A * B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one B _ = A
have rw₂ : A = A
Tactic: rw [Matrix.mul_assoc, mul_invOf_self, Matrix.mul_one]
-- 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 : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst_3 : Invertible C
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * A = B ↔ A = C * B
have refine_1 : ∀ (h : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * A = B), A = C * B
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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 : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst_3 : Invertible C
refine_1 : ∀ (h : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * A = B), A = C * B
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * A = B ↔ A = C * B
have refine_2 : ∀ (h : A = C * B), @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * A = B
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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 : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst_3 : Invertible C
h : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * A = B
⊢ A = C * B
have refine_1 : A = C * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * A)
Tactic: rw [← h, Matrix.mul_invOf_cancel_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 : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst_3 : Invertible C
h : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * A = B
refine_1 : A = C * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * A)
⊢ A = C * B
have refine_1₁ : A = A
Tactic: rw [← h, Matrix.mul_invOf_cancel_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 : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst_3 : Invertible C
h : A = C * B
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * A = B
have refine_2 : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * (C * B) = B
Tactic: rw [h, Matrix.invOf_mul_cancel_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 : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst_3 : Invertible C
h : A = C * B
refine_2 : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * (C * B) = B
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * A = B
have refine_2₁ : B = B
Tactic: rw [h, Matrix.invOf_mul_cancel_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 : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst_3 : Invertible C
⊢ C * A = B ↔ A = @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * B
have rw : B = C * A ↔ A = @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * B
Tactic: rw [eq_comm, ← Matrix.invOf_mul_eq_iff_eq_mul_left, eq_comm]
-- 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 : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst_3 : Invertible C
rw : B = C * A ↔ A = @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * B
⊢ C * A = B ↔ A = @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * B
have rw₁ : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * B = A ↔
  A = @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * B
Tactic: rw [eq_comm, ← Matrix.invOf_mul_eq_iff_eq_mul_left, eq_comm]
-- 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 : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst_3 : Invertible C
rw : B = C * A ↔ A = @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * B
rw₁ :
  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * B = A ↔
    A = @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * B
⊢ C * A = B ↔ A = @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * B
have rw₂ : A = @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * B ↔
  A = @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * B
Tactic: rw [eq_comm, ← Matrix.invOf_mul_eq_iff_eq_mul_left, eq_comm]
-- 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 : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst_3 : Invertible C
⊢ A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ = B ↔ A = B * C
have refine_1 : ∀ (h : A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ = B), A = B * C
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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 : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst_3 : Invertible C
refine_1 : ∀ (h : A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ = B), A = B * C
⊢ A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ = B ↔ A = B * C
have refine_2 : ∀ (h : A = B * C), A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ = B
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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 : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst_3 : Invertible C
h : A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ = B
⊢ A = B * C
have refine_1 : A = A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * C
Tactic: rw [← h, Matrix.invOf_mul_cancel_right]
-- 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 : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst_3 : Invertible C
h : A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ = B
refine_1 : A = A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * C
⊢ A = B * C
have refine_1₁ : A = A
Tactic: rw [← h, Matrix.invOf_mul_cancel_right]
-- 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 : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst_3 : Invertible C
h : A = B * C
⊢ A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ = B
have refine_2 : B * C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ = B
Tactic: rw [h, Matrix.mul_invOf_cancel_right]
-- 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 : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst_3 : Invertible C
h : A = B * C
refine_2 : B * C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ = B
⊢ A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ = B
have refine_2₁ : B = B
Tactic: rw [h, Matrix.mul_invOf_cancel_right]
-- 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 : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst_3 : Invertible C
⊢ A * C = B ↔ A = B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _
have rw : B = A * C ↔ A = B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _
Tactic: rw [eq_comm, ← Matrix.mul_invOf_eq_iff_eq_mul_right, eq_comm]