awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.DualNumber
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
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
⊢ 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:
simp_rw [snd_mul, smul_eq_mul, op_smul_eq_mul]

Premises used: op_smul_eq_mul, TrivSqZeroExt.snd_mul, smul_eq_mul
-- Module: Mathlib.Data.Matrix.DualNumber
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
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))
⊢ 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 only [mul_apply, snd_sum, DualNumber.snd_mul, snd_mk, of_apply, fst_mk, add_apply]

Premises used: Matrix.add_apply, TrivSqZeroExt.snd_mk, Matrix.mul_apply, Matrix.of_apply, TrivSqZeroExt.snd_sum, DualNumber.snd_mul, TrivSqZeroExt.fst_mk
-- Module: Mathlib.Data.Matrix.DualNumber
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
h2 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)))
⊢ ∑ 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:
rw [← Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.Data.Matrix.DualNumber
Goal:
R n : Type
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
r : R
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))
⊢ 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))

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]

Premises used: Algebra.algebraMap_self_apply, TrivSqZeroExt.algebraMap_eq_inl', Matrix.map_apply, Matrix.algebraMap_eq_diagonal, TrivSqZeroExt.algebraMap_eq_inl, TrivSqZeroExt.snd_inl, TrivSqZeroExt.inl_zero, TrivSqZeroExt.fst_inl, Matrix.diagonal_map, Pi.algebraMap_def
-- Module: Mathlib.Data.Matrix.DualNumber
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) ↦ 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:
rfl
-- Module: Mathlib.Data.Matrix.Invertible
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
rw₂ rw₃ : B = B
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (A * B) = B

Tactic:
rw [← Matrix.mul_assoc, invOf_mul_self, Matrix.one_mul]

Premises used: Matrix.mul_assoc, invOf_mul_self, Matrix.one_mul
-- Module: Mathlib.Data.Matrix.Invertible
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
rw₂ rw₃ : B = B
⊢ A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) = B

Tactic:
rw [← Matrix.mul_assoc, mul_invOf_self, Matrix.one_mul]

Premises used: Matrix.mul_assoc, mul_invOf_self, Matrix.one_mul
-- Module: Mathlib.Data.Matrix.Invertible
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
rw₂ rw₃ : A = A
⊢ A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one B _ * B = A

Tactic:
rw [Matrix.mul_assoc, invOf_mul_self, Matrix.mul_one]

Premises used: Matrix.mul_assoc, invOf_mul_self, Matrix.mul_one
-- Module: Mathlib.Data.Matrix.Invertible
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
rw₂ rw₃ : A = A
⊢ A * B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one B _ = A

Tactic:
rw [Matrix.mul_assoc, mul_invOf_self, Matrix.mul_one]

Premises used: Matrix.mul_assoc, mul_invOf_self, Matrix.mul_one
-- Module: Mathlib.Data.Matrix.Invertible
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

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Matrix.Invertible
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
refine_2 : ∀ (h : A = C * B), @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * A = B
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * A = B ↔ A = C * B

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Data.Matrix.Invertible
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)
refine_1₁ refine_1₂ : A = A
⊢ A = C * B

Tactic:
rw [← h, Matrix.mul_invOf_cancel_left]

Premises used: Matrix.mul_invOf_cancel_left
-- Module: Mathlib.Data.Matrix.Invertible
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
refine_2₁ refine_2₂ : B = B
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * A = B

Tactic:
rw [h, Matrix.invOf_mul_cancel_left]

Premises used: Matrix.invOf_mul_cancel_left
-- Module: Mathlib.Data.Matrix.Invertible
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
rw₂ rw₃ :
  A = @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * B ↔
    A = @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * B
⊢ C * A = B ↔ A = @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ * B

Tactic:
rw [eq_comm, ← Matrix.invOf_mul_eq_iff_eq_mul_left, eq_comm]

Premises used: Matrix.invOf_mul_eq_iff_eq_mul_left, eq_comm
-- Module: Mathlib.Data.Matrix.Invertible
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

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Matrix.Invertible
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
refine_2 : ∀ (h : A = B * C), A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ = B
⊢ A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ = B ↔ A = B * C

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Data.Matrix.Invertible
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
refine_1₁ refine_1₂ : A = A
⊢ A = B * C

Tactic:
rw [← h, Matrix.invOf_mul_cancel_right]

Premises used: Matrix.invOf_mul_cancel_right
-- Module: Mathlib.Data.Matrix.Invertible
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
refine_2₁ refine_2₂ : B = B
⊢ A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ = B

Tactic:
rw [h, Matrix.mul_invOf_cancel_right]

Premises used: Matrix.mul_invOf_cancel_right
-- Module: Mathlib.Data.Matrix.Invertible
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
rw : B = A * C ↔ A = B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _
rw₁ :
  B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ = A ↔
    A = B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _
rw₂ rw₃ :
  A = B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ ↔
    A = B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _
⊢ A * C = B ↔ A = B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _

Tactic:
rw [eq_comm, ← Matrix.mul_invOf_eq_iff_eq_mul_right, eq_comm]

Premises used: Matrix.mul_invOf_eq_iff_eq_mul_right, eq_comm
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring α
inst_3 : StarRing α
A : Matrix n n α
inst_4 : Invertible A
inst_5 : Invertible Aᴴ
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)ᴴ =
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᴴ _

Tactic:
star_invOf _

Premises used: star_invOf
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring α
inst_3 : StarRing α
A : Matrix n n α
inst_4 : Invertible Aᴴ
rw : Invertible (star Aᴴ)
⊢ Invertible A

Tactic:
rw [← conjTranspose_conjTranspose A, ← star_eq_conjTranspose]

Premises used: Matrix.star_eq_conjTranspose, Matrix.conjTranspose_conjTranspose
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring α
inst_3 : StarRing α
A : Matrix n n α
inst_4 : Invertible Aᴴ
⊢ Invertible (star Aᴴ)

Tactic:
infer_instance
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring α
inst_3 : StarRing α
A : Matrix n n α
⊢ IsUnit Aᴴ ↔ IsUnit A

Tactic:
isUnit_star

Premises used: isUnit_star
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible A
rw : (A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)ᵀ = 1
rw₁ : Eq (α := Matrix n n α) 1ᵀ 1
rw₂ rw₃ : Eq (α := Matrix n n α) 1 1
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)ᵀ * Aᵀ = 1

Tactic:
rw [← transpose_mul, mul_invOf_self, transpose_one]

Premises used: Matrix.transpose_mul, mul_invOf_self, Matrix.transpose_one
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible A
rw : (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A)ᵀ = 1
rw₁ : Eq (α := Matrix n n α) 1ᵀ 1
rw₂ rw₃ : Eq (α := Matrix n n α) 1 1
⊢ Aᵀ * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)ᵀ = 1

Tactic:
rw [← transpose_mul, invOf_mul_self, transpose_one]

Premises used: invOf_mul_self, Matrix.transpose_mul, Matrix.transpose_one
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible A
inst_4 : Invertible Aᵀ
this : Invertible Aᵀ := A.invertibleTranspose
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _ =
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _

Tactic:
(rfl : _ = ⅟(Aᵀ))

Premises used: rfl
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible A
inst_4 : Invertible Aᵀ
this : Invertible Aᵀ := A.invertibleTranspose
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)ᵀ =
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _

Tactic:
convert! (rfl : _ = ⅟(Aᵀ))

Premises used: rfl
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible Aᵀ
rw : (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A = 1ᵀ
rw₁ :
  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A =
    (Aᵀ * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ
rw₂ :
  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A =
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * Aᵀᵀ
rw₃ rw₄ :
  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A =
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A = 1

Tactic:
rw [← transpose_one, ← mul_invOf_self Aᵀ, transpose_mul, transpose_transpose]

Premises used: Matrix.transpose_transpose, Matrix.transpose_mul, mul_invOf_self, Matrix.transpose_one, Matrix.transpose
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible Aᵀ
rw : A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ = 1ᵀ
rw₁ :
  A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ =
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _ * Aᵀ)ᵀ
rw₂ :
  A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ =
    Aᵀᵀ * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ
rw₃ rw₄ :
  A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ =
    A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ
⊢ A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ = 1

Tactic:
rw [← transpose_one, ← invOf_mul_self Aᵀ, transpose_mul, transpose_transpose]

Premises used: Matrix.transpose_transpose, invOf_mul_self, Matrix.transpose_mul, Matrix.transpose_one, Matrix.transpose
-- Module: Mathlib.Data.Matrix.Invertible
Goal:
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring α
A : Matrix n n α
⊢ IsUnit Aᵀ ↔ IsUnit A

Tactic:
simp only [← nonempty_invertible_iff_isUnit,
    (transposeInvertibleEquivInvertible A).nonempty_congr]

Premises used: Matrix.transposeInvertibleEquivInvertible, nonempty_invertible_iff_isUnit, Equiv.nonempty_congr
-- Module: Mathlib.Data.Matrix.Invertible
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
inst_7 :
  Invertible
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
      V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
⊢ 1 -
          U *
                @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                    V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
                  _ *
              V *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ +
        U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
      U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
              _ *
          V *
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ =
    1 + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
      (U *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                  V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
                _ *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ +
        U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                  V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
                _ *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)

Tactic:
abel
-- Module: Mathlib.Data.Matrix.Invertible
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
inst_7 :
  Invertible
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
      V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
e_a :
  U + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U =
    U * C *
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
        V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
⊢ 1 + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
      (U + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U) *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
              _ *
          V *
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ =
    1 + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
      U * C *
              (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U) *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
              _ *
          V *
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _

Tactic:
congr