awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
i j k : n
M : Matrix n n α
hM : Commute (single i j 1) M
hkj : k ≠ j
this : HMul.hMul (α := Matrix n n α) (single i j 1) M i k = HMul.hMul (β := Matrix n n α) M (single i j 1) i k
⊢ M j k = 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
i j k : n
M : Matrix n n α
hM : Commute (single i j 1) M
hki : k ≠ i
⊢ HMul.hMul (α := Matrix n n α) (single i j 1) M k j = HMul.hMul (β := Matrix n n α) M (single i j 1) k j

Tactic:
have := ext_iff.mpr hM k j
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
i j k : n
M : Matrix n n α
hM : Commute (single i j 1) M
hki : k ≠ i
this : HMul.hMul (α := Matrix n n α) (single i j 1) M k j = HMul.hMul (β := Matrix n n α) M (single i j 1) k j
⊢ M k i = 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
i j : n
M : Matrix n n α
hM : Commute (single i j 1) M
⊢ HMul.hMul (α := Matrix n n α) (single i j 1) M i j = HMul.hMul (β := Matrix n n α) M (single i j 1) i j

Tactic:
have := ext_iff.mpr hM i j
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
i j : n
M : Matrix n n α
hM : Commute (single i j 1) M
this : HMul.hMul (α := Matrix n n α) (single i j 1) M i j = HMul.hMul (β := Matrix n n α) M (single i j 1) i j
⊢ M i i = M j j

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
hM : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
inl : IsEmpty n → Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M
inr :
  Nonempty n → Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M
⊢ Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M

Tactic:
cases isEmpty_or_nonempty n

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
hM : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
h : IsEmpty n
⊢ Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M

Tactic:
⟨0, Subsingleton.elim _ _⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
hM : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
h : IsEmpty n
⊢ Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M

Tactic:
exact ⟨0, Subsingleton.elim _ _⟩
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
hM : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
h : Nonempty n
inr : ∀ (i : n), Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M
⊢ Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M

Tactic:
obtain ⟨i⟩ := ‹Nonempty n›

Premises used: Nonempty
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
hM : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
h : Nonempty n
i : n
⊢ Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M

Tactic:
⟨M i i, Matrix.ext fun j k => ?_⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, Matrix.ext
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
hM : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
h : Nonempty n
i : n
inr : ∀ (j k : n), (scalar n : (a : α) → Matrix n n α) (M i i) j k = M j k
⊢ Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M

Tactic:
refine ⟨M i i, Matrix.ext fun j k => ?_⟩
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
hM : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
h : Nonempty n
i j k : n
inr : diagonal (fun (x : n) ↦ M i i) j k = M j k
⊢ (scalar n : (a : α) → Matrix n n α) (M i i) j k = M j k

Tactic:
simp only [scalar_apply]

Premises used: Matrix.scalar_apply
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
hM : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
h : Nonempty n
i j k : n
inr : diagonal (fun (x : n) ↦ M i i) j j = M j j
inr₁ : ∀ (hkl : j ≠ k), diagonal (fun (x : n) ↦ M i i) j k = M j k
⊢ diagonal (fun (x : n) ↦ M i i) j k = M j k

Tactic:
obtain rfl | hkl := Decidable.eq_or_ne j k

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
hM : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
h : Nonempty n
i j : n
inr : M i i = M j j
⊢ diagonal (fun (x : n) ↦ M i i) j j = M j j

Tactic:
rw [diagonal_apply_eq]

Premises used: Matrix.diagonal_apply_eq
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
hM : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
h : Nonempty n
i j : n
inr : M i i = M i i
inr₁ : ∀ (hij : i ≠ j), M i i = M j j
⊢ M i i = M j j

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
hM : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
h : Nonempty n
i : n
⊢ M i i = M i i

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
hM : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
h : Nonempty n
i j : n
hij : i ≠ j
⊢ M i i = M j j

Tactic:
diag_eq_of_commute_single (hM hij)

Premises used: Matrix.diag_eq_of_commute_single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
hM : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
h : Nonempty n
i j : n
hij : i ≠ j
⊢ M i i = M j j

Tactic:
exact diag_eq_of_commute_single (hM hij)

Premises used: Matrix.diag_eq_of_commute_single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
hM : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
h : Nonempty n
i j k : n
hkl : j ≠ k
inr : 0 = M j k
⊢ diagonal (fun (x : n) ↦ M i i) j k = M j k

Tactic:
rw [diagonal_apply_ne _ hkl]

Premises used: Matrix.diagonal_apply_ne
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
hM : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
h : Nonempty n
i j k : n
hkl : j ≠ k
inr : ∀ (hkl : i ≠ k), 0 = M i k
inr₁ : ∀ (hij : i ≠ j), 0 = M j k
⊢ 0 = M j k

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
hM : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
h : Nonempty n
i k : n
hkl : i ≠ k
inr inr₁ : Eq.{u_7 + 1} (α := α) 0 0
⊢ 0 = M i k

Tactic:
rw [col_eq_zero_of_commute_single (hM hkl.symm) hkl]

Premises used: Ne.symm, Matrix.col_eq_zero_of_commute_single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
hM : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
h : Nonempty n
i j k : n
hkl : j ≠ k
hij : i ≠ j
inr inr₁ : Eq.{u_7 + 1} (α := α) 0 0
⊢ 0 = M j k

Tactic:
rw [row_eq_zero_of_commute_single (hM hij) hkl.symm]

Premises used: Ne.symm, Matrix.row_eq_zero_of_commute_single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
⊢ Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M ↔
    ∀ (i j : n), i ≠ j → Commute (single i j 1) M

Tactic:
⟨fun ⟨r, hr⟩ i j _ => hr ▸ Commute.symm ?_, mem_range_scalar_of_commute_single⟩

Premises used: _private.0.Matrix.mem_range_scalar_iff_commute_single.match_1, Commute, Eq.rec, Matrix.mem_range_scalar_of_commute_single, Commute.symm, Iff.intro, OfNat.ofNat, Matrix.single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
refine :
  Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M →
    ∀ (i j : n),
      i ≠ j →
        ∀ (r : α) (hr : (scalar n : (a : α) → Matrix n n α) r = M),
          Commute (S := Matrix n n α) ((scalar n : (a : α) → Matrix n n α) r : Matrix n n α)
            (single i j 1 : Matrix n n α)
⊢ Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M ↔
    ∀ (i j : n), i ≠ j → Commute (single i j 1) M

Tactic:
refine ⟨fun ⟨r, hr⟩ i j _ => hr ▸ Commute.symm ?_, mem_range_scalar_of_commute_single⟩
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
h : Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M
i j : n
h_1 : i ≠ j
r : α
hr : (scalar n : (a : α) → Matrix n n α) r = M
rw :
  HSMul.hSMul (β := Matrix n n α) r (single i j 1) = HSMul.hSMul (β := Matrix n n α) (MulOpposite.op r) (single i j 1)
⊢ Commute (S := Matrix n n α) ((scalar n : (a : α) → Matrix n n α) r : Matrix n n α) (single i j 1 : Matrix n n α)

Tactic:
rw [scalar_commute_iff]

Premises used: Matrix.scalar_commute_iff
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
h : Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M
i j : n
h_1 : i ≠ j
r : α
hr : (scalar n : (a : α) → Matrix n n α) r = M
⊢ HSMul.hSMul (β := Matrix n n α) r (single i j 1) = HSMul.hSMul (β := Matrix n n α) (MulOpposite.op r) (single i j 1)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
⊢ Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M ↔
    ∀ (i j : n), Commute (single i j 1) M

Tactic:
⟨fun ⟨r, hr⟩ i j => hr ▸ Commute.symm ?_,
    fun hM => mem_range_scalar_iff_commute_single.mpr <| fun i j _ => hM i j⟩

Premises used: Iff.mpr, _private.0.Matrix.mem_range_scalar_iff_commute_single.match_1, Commute, Eq.rec, Matrix.mem_range_scalar_iff_commute_single, Commute.symm, Iff.intro, OfNat.ofNat, Matrix.single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
refine :
  Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M →
    ∀ (i j : n) (r : α) (hr : (scalar n : (a : α) → Matrix n n α) r = M),
      Commute (S := Matrix n n α) ((scalar n : (a : α) → Matrix n n α) r : Matrix n n α) (single i j 1 : Matrix n n α)
⊢ Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M ↔
    ∀ (i j : n), Commute (single i j 1) M

Tactic:
refine ⟨fun ⟨r, hr⟩ i j => hr ▸ Commute.symm ?_,
    fun hM => mem_range_scalar_iff_commute_single.mpr <| fun i j _ => hM i j⟩
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
h : Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M
i j : n
r : α
hr : (scalar n : (a : α) → Matrix n n α) r = M
rw :
  HSMul.hSMul (β := Matrix n n α) r (single i j 1) = HSMul.hSMul (β := Matrix n n α) (MulOpposite.op r) (single i j 1)
⊢ Commute (S := Matrix n n α) ((scalar n : (a : α) → Matrix n n α) r : Matrix n n α) (single i j 1 : Matrix n n α)

Tactic:
rw [scalar_commute_iff]

Premises used: Matrix.scalar_commute_iff
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
M : Matrix n n α
h : Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M
i j : n
r : α
hr : (scalar n : (a : α) → Matrix n n α) r = M
⊢ HSMul.hSMul (β := Matrix n n α) r (single i j 1) = HSMul.hSMul (β := Matrix n n α) (MulOpposite.op r) (single i j 1)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
x : Matrix n n α
simp_rw :
  (∀ (g : Matrix n n α), g * x = x * g) ↔
    ∃ (x_1 : α), (∀ (g : α), g * x_1 = x_1 * g) ∧ (scalar n : (a : α) → Matrix n n α) x_1 = x
⊢ Membership.mem (γ := Set (Matrix n n α)) (Set.center (Matrix n n α)) x ↔
    Membership.mem (γ := Set (Matrix n n α)) ((⇑(scalar n) : (a : α) → Matrix n n α) '' Set.center α) x

Tactic:
simp_rw [Set.mem_image, Semigroup.mem_center_iff]

Premises used: Set.mem_image, Semigroup.mem_center_iff
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
x : Matrix n n α
⊢ (∀ (g : Matrix n n α), g * x = x * g) ↔
    ∃ (x_1 : α), (∀ (g : α), g * x_1 = x_1 * g) ∧ (scalar n : (a : α) → Matrix n n α) x_1 = x

Tactic:
⟨fun hx ↦ ?_, fun ⟨x, hx, eq⟩ y ↦ eq ▸ scalar_commute x (hx · |>.symm) y |>.symm⟩

Premises used: _private.0.Matrix.center_eq_scalar_image.match_2, HMul.hMul, Iff.intro, Eq
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
x : Matrix n n α
refine :
  ∀ (hx : ∀ (g : Matrix n n α), g * x = x * g),
    ∃ (x_1 : α), (∀ (g : α), g * x_1 = x_1 * g) ∧ (scalar n : (a : α) → Matrix n n α) x_1 = x
⊢ (∀ (g : Matrix n n α), g * x = x * g) ↔
    ∃ (x_1 : α), (∀ (g : α), g * x_1 = x_1 * g) ∧ (scalar n : (a : α) → Matrix n n α) x_1 = x

Tactic:
refine ⟨fun hx ↦ ?_, fun ⟨x, hx, eq⟩ y ↦ eq ▸ scalar_commute x (hx · |>.symm) y |>.symm⟩
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
x : Matrix n n α
hx : ∀ (g : Matrix n n α), g * x = x * g
h : IsEmpty n
⊢ (∀ (g : α), g * 0 = 0 * g) ∧ (scalar n : (a : α) → Matrix n n α) 0 = x

Tactic:
simp [nontriviality]
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
x : Matrix n n α
hx : ∀ (g : Matrix n n α), g * x = x * g
refine :
  Nonempty n → ∀ (i : n), ∃ (x_2 : α), (∀ (g : α), g * x_2 = x_2 * g) ∧ (scalar n : (a : α) → Matrix n n α) x_2 = x
⊢ ∃ (x_1 : α), (∀ (g : α), g * x_1 = x_1 * g) ∧ (scalar n : (a : α) → Matrix n n α) x_1 = x

Tactic:
refine (isEmpty_or_nonempty n).elim (fun _ ↦ ⟨0, by simp [nontriviality]⟩) fun ⟨i⟩ ↦ ?_

Premises used: isEmpty_or_nonempty, Or.elim
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
x : Matrix n n α
hx : ∀ (g : Matrix n n α), g * x = x * g
h : Nonempty n
i : n
obtain :
  ∀ (x : α)
    (hx :
      ∀ (g : Matrix n n α),
        HMul.hMul (β := Matrix n n α) g ((scalar n : (a : α) → Matrix n n α) x : Matrix n n α) =
          HMul.hMul (α := Matrix n n α) ((scalar n : (a : α) → Matrix n n α) x : Matrix n n α) g),
    ∃ (x_1 : α),
      (∀ (g : α), g * x_1 = x_1 * g) ∧
        Eq (α := Matrix n n α) ((scalar n : (a : α) → Matrix n n α) x_1 : Matrix n n α)
          ((scalar n : (a : α) → Matrix n n α) x : Matrix n n α)
⊢ ∃ (x_1 : α), (∀ (g : α), g * x_1 = x_1 * g) ∧ (scalar n : (a : α) → Matrix n n α) x_1 = x

Tactic:
obtain ⟨x, rfl⟩ := mem_range_scalar_iff_commute_single'.mpr fun _ _ ↦ hx _

Premises used: Iff.mpr, Matrix.mem_range_scalar_iff_commute_single', OfNat.ofNat, rfl, Matrix.single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
h : Nonempty n
i : n
x : α
hx :
  ∀ (g : Matrix n n α),
    HMul.hMul (β := Matrix n n α) g ((scalar n : (a : α) → Matrix n n α) x : Matrix n n α) =
      HMul.hMul (α := Matrix n n α) ((scalar n : (a : α) → Matrix n n α) x : Matrix n n α) g
⊢ (∀ (g : α), g * x = x * g) ∧
    Eq (α := Matrix n n α) ((scalar n : (a : α) → Matrix n n α) x : Matrix n n α)
      ((scalar n : (a : α) → Matrix n n α) x : Matrix n n α)

Tactic:
simpa using fun r ↦ congr($(hx (single i i r)) i i)

Premises used: congrArg, id, Matrix.single
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
h : Nonempty n
i : n
x : α
hx :
  ∀ (g : Matrix n n α),
    HMul.hMul (β := Matrix n n α) g ((scalar n : (a : α) → Matrix n n α) x : Matrix n n α) =
      HMul.hMul (α := Matrix n n α) ((scalar n : (a : α) → Matrix n n α) x : Matrix n n α) g
⊢ ∃ (x_1 : α),
    (∀ (g : α), g * x_1 = x_1 * g) ∧
      Eq (α := Matrix n n α) ((scalar n : (a : α) → Matrix n n α) x_1 : Matrix n n α)
        ((scalar n : (a : α) → Matrix n n α) x : Matrix n n α)

Tactic:
exact ⟨x, by simpa using fun r ↦ congr($(hx (single i i r)) i i)⟩
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
⊢ Eq (α := Submonoid (Matrix n n α)) (Submonoid.center (Matrix n n α))
    (Submonoid.map (F := α →+* Matrix n n α) (scalar n) (Submonoid.center α))

Tactic:
SetLike.coe_injective center_eq_scalar_image

Premises used: SetLike.coe_injective, Matrix.center_eq_scalar_image
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
⊢ Eq (α := Subsemigroup (Matrix n n α)) (Subsemigroup.center (Matrix n n α) : Subsemigroup (Matrix n n α))
    (Subsemigroup.map (↑(↑(scalar n) : α →* Matrix n n α) : α →ₙ* Matrix n n α) (Subsemigroup.center α) :
      Subsemigroup (Matrix n n α))

Tactic:
SetLike.coe_injective center_eq_scalar_image

Premises used: SetLike.coe_injective, Matrix.center_eq_scalar_image
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
⊢ Eq (α := Subsemiring (Matrix n n α)) (Subsemiring.center (Matrix n n α))
    (Subsemiring.map (scalar n) (Subsemiring.center α))

Tactic:
SetLike.coe_injective center_eq_scalar_image

Premises used: SetLike.coe_injective, Matrix.center_eq_scalar_image
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
R : Type u_5
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Ring R
⊢ Eq (α := Subring (Matrix n n R)) (Subring.center (Matrix n n R)) (Subring.map (scalar n) (Subring.center R))

Tactic:
SetLike.coe_injective center_eq_scalar_image

Premises used: SetLike.coe_injective, Matrix.center_eq_scalar_image
-- Module: Mathlib.Data.Matrix.Basis
Goal:
n : Type u_3
R : Type u_5
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommSemiring R
rw :
  Eq (α := Set (Matrix n n R)) ((⇑(scalar n) : (a : R) → Matrix n n R) '' Set.center R)
    (Set.range (ι := R) (⇑(scalar n) : (a : R) → Matrix n n R))
rw₁ :
  Eq (α := Set (Matrix n n R)) (Set.image (α := R) (⇑(scalar n) : (a : R) → Matrix n n R) Set.univ)
    (Set.range (ι := R) (⇑(scalar n) : (a : R) → Matrix n n R))
rw₂ rw₃ :
  Eq (α := Set (Matrix n n R)) (Set.range (ι := R) (⇑(scalar n) : (a : R) → Matrix n n R))
    (Set.range (ι := R) (⇑(scalar n) : (a : R) → Matrix n n R))
⊢ Eq (α := Set (Matrix n n R)) (Set.center (Matrix n n R)) (Set.range (ι := R) (⇑(scalar n) : (a : R) → Matrix n n R))

Tactic:
rw [center_eq_scalar_image, Set.center_eq_univ, Set.image_univ]

Premises used: Set.image_univ, Set.center_eq_univ, Matrix.center_eq_scalar_image
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
m : Type u_2
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
⊢ Eq (α := (X : Matrix m m A) → Matrix m m A →ₗ[R] Matrix m m A) (mulLeftLinearMap m R)
    (LinearMap.mulLeft R (A := Matrix m m A))

Tactic:
rfl

Premises used: mulLeftLinearMap, LinearMap.mulLeft, rfl
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
⊢ Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R 0) 0

Tactic:
LinearMap.ext fun _ => Matrix.zero_mul _

Premises used: LinearMap.ext, Matrix.zero_mul
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
m : Type u_2
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
⊢ Eq (α := (Y : Matrix m m A) → Matrix m m A →ₗ[R] Matrix m m A) (mulRightLinearMap m R)
    (LinearMap.mulRight R (A := Matrix m m A))

Tactic:
rfl

Premises used: LinearMap.mulRight, mulRightLinearMap, rfl
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Semiring R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
⊢ Eq (α := Matrix l m A →ₗ[R] Matrix l n A) (mulRightLinearMap l R 0) 0

Tactic:
LinearMap.ext fun _ => Matrix.mul_zero _

Premises used: LinearMap.ext, Matrix.mul_zero
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
m : Type u_2
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : CommSemiring R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
⊢ Eq (α := Matrix m m A →ₗ[R] Matrix m m A →ₗ[R] Matrix m m A) (mulLinearMap R) (LinearMap.mul R (Matrix m m A))

Tactic:
rfl

Premises used: LinearMap.mk₂, LinearMap.mk₂'ₛₗ, mulLeftLinearMap, LinearMap.mk₂', rfl
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : NonUnitalSemiring A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
a : Matrix l m A
b : Matrix m n A
h :
  ∀ (x : Matrix n o A) (i : l) (j : o),
    Eq.{u_6 + 1} (α := A) ((mulLeftLinearMap o R (a * b) : (a : Matrix n o A) → Matrix l o A) x i j : A)
      ((mulLeftLinearMap o R a ∘ₗ mulLeftLinearMap o R b : (a : Matrix n o A) → Matrix l o A) x i j : A)
⊢ Eq (α := Matrix n o A →ₗ[R] Matrix l o A) (mulLeftLinearMap o R (a * b))
    (mulLeftLinearMap o R a ∘ₗ mulLeftLinearMap o R b)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Bilinear
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : NonUnitalSemiring A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
a : Matrix l m A
b : Matrix m n A
x : Matrix n o A
i : l
j : o
⊢ Eq.{u_6 + 1} (α := A) ((mulLeftLinearMap o R (a * b) : (a : Matrix n o A) → Matrix l o A) x i j : A)
    ((mulLeftLinearMap o R a ∘ₗ mulLeftLinearMap o R b : (a : Matrix n o A) → Matrix l o A) x i j : A)

Tactic:
simp only [mulLeftLinearMap_apply, LinearMap.comp_apply, Matrix.mul_assoc]

Premises used: Matrix.mul_assoc, LinearMap.comp_apply, mulLeftLinearMap_apply