awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M
have inr : Nonempty n → Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M
Tactic: cases isEmpty_or_nonempty n
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M
have inr : ∀ (i : n), Membership.mem (γ := Set (Matrix n n α)) (Set.range (ι := α) (⇑(scalar n) : (a : α) → Matrix n n α)) M
Tactic: obtain ⟨i⟩ := ‹Nonempty n›
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
have inr : ∀ (j k : n), (scalar n : (a : α) → Matrix n n α) (M i i) j k = M j k
Tactic: refine ⟨M i i, Matrix.ext fun j k => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ (scalar n : (a : α) → Matrix n n α) (M i i) j k = M j k
have inr : diagonal (fun (x : n) ↦ M i i) j k = M j k
Tactic: simp only [scalar_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ diagonal (fun (x : n) ↦ M i i) j k = M j k
have inr : diagonal (fun (x : n) ↦ M i i) j j = M j j
Tactic: obtain rfl | hkl := Decidable.eq_or_ne j k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ diagonal (fun (x : n) ↦ M i i) j k = M j k
have inr₁ : ∀ (hkl : j ≠ k), diagonal (fun (x : n) ↦ M i i) j k = M j k
Tactic: obtain rfl | hkl := Decidable.eq_or_ne j k
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ diagonal (fun (x : n) ↦ M i i) j j = M j j
have inr : M i i = M j j
Tactic: rw [diagonal_apply_eq]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ M i i = M j j
have inr : M i i = M i i
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ M i i = M j j
have inr₁ : ∀ (hij : i ≠ j), M i i = M j j
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ diagonal (fun (x : n) ↦ M i i) j k = M j k
have inr : 0 = M j k
Tactic: rw [diagonal_apply_ne _ hkl]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ 0 = M j k
have inr : ∀ (hkl : i ≠ k), 0 = M i k
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
Cleared hypotheses: j, hkl
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ 0 = M j k
have inr₁ : ∀ (hij : i ≠ j), 0 = M j k
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ 0 = M i k
have inr : Eq.{u_7 + 1} (α := α) 0 0
Tactic: rw [col_eq_zero_of_commute_single (hM hkl.symm) hkl]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ 0 = M j k
have inr : Eq.{u_7 + 1} (α := α) 0 0
Tactic: rw [row_eq_zero_of_commute_single (hM hij) hkl.symm]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
have 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 α)
Tactic: refine ⟨fun ⟨r, hr⟩ i j _ => hr ▸ Commute.symm ?_, mem_range_scalar_of_commute_single⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ Commute (S := Matrix n n α) ((scalar n : (a : α) → Matrix n n α) r : Matrix n n α) (single i j 1 : Matrix n n α)
have rw : HSMul.hSMul (β := Matrix n n α) r (single i j 1) = HSMul.hSMul (β := Matrix n n α) (MulOpposite.op r) (single i j 1)
Tactic: rw [scalar_commute_iff]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
have 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 α)
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⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ Commute (S := Matrix n n α) ((scalar n : (a : α) → Matrix n n α) r : Matrix n n α) (single i j 1 : Matrix n n α)
have rw : HSMul.hSMul (β := Matrix n n α) r (single i j 1) = HSMul.hSMul (β := Matrix n n α) (MulOpposite.op r) (single i j 1)
Tactic: rw [scalar_commute_iff]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Semiring α
x : Matrix n n α
⊢ 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
have 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
Tactic: simp_rw [Set.mem_image, Semigroup.mem_center_iff]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
have 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
Tactic: refine ⟨fun hx ↦ ?_, fun ⟨x, hx, eq⟩ y ↦ eq ▸ scalar_commute x (hx · |>.symm) y |>.symm⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ ∃ (x_1 : α), (∀ (g : α), g * x_1 = x_1 * g) ∧ (scalar n : (a : α) → Matrix n n α) x_1 = x
have refine : Nonempty n → ∀ (i : n), ∃ (x_2 : α), (∀ (g : α), g * x_2 = x_2 * g) ∧ (scalar n : (a : α) → Matrix n n α) x_2 = x
Tactic: refine (isEmpty_or_nonempty n).elim (fun _ ↦ ⟨0, by simp [nontriviality]⟩) fun ⟨i⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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
⊢ ∃ (x_1 : α), (∀ (g : α), g * x_1 = x_1 * g) ∧ (scalar n : (a : α) → Matrix n n α) x_1 = x
have 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 α)
Tactic: obtain ⟨x, rfl⟩ := mem_range_scalar_iff_commute_single'.mpr fun _ _ ↦ hx _
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
n : Type u_3
R : Type u_5
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommSemiring R
⊢ Eq (α := Set (Matrix n n R)) (Set.center (Matrix n n R)) (Set.range (ι := R) (⇑(scalar n) : (a : R) → Matrix n n R))
have 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))
Tactic: rw [center_eq_scalar_image, Set.center_eq_univ, Set.image_univ]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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))
⊢ Eq (α := Set (Matrix n n R)) (Set.center (Matrix n n R)) (Set.range (ι := R) (⇑(scalar n) : (a : R) → Matrix n n R))
have 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))
Tactic: rw [center_eq_scalar_image, Set.center_eq_univ, Set.image_univ]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
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))
⊢ Eq (α := Set (Matrix n n R)) (Set.center (Matrix n n R)) (Set.range (ι := R) (⇑(scalar n) : (a : R) → Matrix n n R))
have 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))
Tactic: rw [center_eq_scalar_image, Set.center_eq_univ, Set.image_univ]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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
⊢ Eq (α := Matrix n o A →ₗ[R] Matrix l o A) (mulLeftLinearMap o R (a * b))
    (mulLeftLinearMap o R a ∘ₗ mulLeftLinearMap o R b)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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 : IsScalarTower R A A
a : Matrix m n A
b : Matrix n o A
⊢ Eq (α := Matrix l m A →ₗ[R] Matrix l o A) (mulRightLinearMap l R (a * b))
    (mulRightLinearMap l R b ∘ₗ mulRightLinearMap l R a)
have h : ∀ (x : Matrix l m A) (i : l) (j : o),
  Eq.{u_6 + 1} (α := A) ((mulRightLinearMap l R (a * b) : (a : Matrix l m A) → Matrix l o A) x i j : A)
    ((mulRightLinearMap l R b ∘ₗ mulRightLinearMap l R a : (a : Matrix l m A) → Matrix l o A) x i j : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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 : CommSemiring R
inst_3 : NonUnitalSemiring A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
a : Matrix l m A
b : Matrix n o A
⊢ Eq (α := Matrix m n A →ₗ[R] Matrix l o A) (mulLeftLinearMap o R a ∘ₗ mulRightLinearMap m R b)
    (mulRightLinearMap l R b ∘ₗ mulLeftLinearMap n R a)
have h : ∀ (c : Matrix m n A),
  Eq (α := Matrix l o A)
    ((mulLeftLinearMap o R a ∘ₗ mulRightLinearMap m R b : (a : Matrix m n A) → Matrix l o A) c : Matrix l o A)
    ((mulRightLinearMap l R b ∘ₗ mulLeftLinearMap n R a : (a : Matrix m n A) → Matrix l o A) c : Matrix l o A)
Tactic: ext c : 1
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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 : Semiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : Nonempty n
a : Matrix l m A
⊢ Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R a) 0 ↔ a = 0
have mp : Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R a) 0 → a = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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 : Semiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : Nonempty n
a : Matrix l m A
mp : Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R a) 0 → a = 0
⊢ Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R a) 0 ↔ a = 0
have mpr : a = 0 → Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R a) 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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 : Semiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : Nonempty n
a : Matrix l m A
h : Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R a) 0
⊢ a = 0
have mp : ∀ (inhabited_h : Inhabited n), a = 0
Tactic: inhabit n
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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 : Semiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : Nonempty n
a : Matrix l m A
h : Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R a) 0
inhabited_h : Inhabited n
⊢ a = 0
have mp : ∀ (i : l) (j : m), a i j = 0 i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (hypothesis)
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 : Semiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : Nonempty n
a : Matrix l m A
h : Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R a) 0
inhabited_h : Inhabited n
i : l
j : m
⊢ a i j = 0 i j
have h₁ : Eq (α := Matrix l n A)
  ((mulLeftLinearMap n R a : (a : Matrix m n A) → Matrix l n A) (Matrix.single j default 1) : Matrix l n A)
  ((0 : (a : Matrix m n A) → Matrix l n A) (Matrix.single j default 1) : Matrix l n A)
Tactic: replace h := DFunLike.congr_fun h (Matrix.single j (default : n) 1)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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 : Semiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : Nonempty n
a : Matrix l m A
h : Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R a) 0
inhabited_h : Inhabited n
i : l
j : m
⊢ a i j = 0 i j
have mp : ∀
  (h :
    Eq (α := Matrix l n A)
      ((mulLeftLinearMap n R a : (a : Matrix m n A) → Matrix l n A) (Matrix.single j default 1) : Matrix l n A)
      ((0 : (a : Matrix m n A) → Matrix l n A) (Matrix.single j default 1) : Matrix l n A)),
  a i j = 0 i j
Tactic: classical
    replace h := DFunLike.congr_fun h (Matrix.single j (default : n) 1)
    simpa using Matrix.ext_iff.2 h i default
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
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 : Semiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : Nonempty n
a : Matrix l m A
h : a = 0
⊢ Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R a) 0
have mpr : Eq (α := Matrix m n A →ₗ[R] Matrix l n A) (mulLeftLinearMap n R 0) 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Semiring R
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
a : Matrix m m A
k : ℕ
⊢ HPow.hPow (α := Matrix m n A →ₗ[R] Matrix m n A) (β := ℕ) (mulLeftLinearMap n R a) 0 =
    mulLeftLinearMap n R (HPow.hPow (β := ℕ) a 0)
have rw : Eq (α := Matrix m n A →ₗ[R] Matrix m n A) 1 (mulLeftLinearMap n R (HPow.hPow (β := ℕ) a 0))
Tactic: rw [pow_zero, pow_zero, mulLeftLinearMap_one, Module.End.one_eq_id]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Semiring R
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
a : Matrix m m A
k : ℕ
rw : Eq (α := Matrix m n A →ₗ[R] Matrix m n A) 1 (mulLeftLinearMap n R (HPow.hPow (β := ℕ) a 0))
⊢ HPow.hPow (α := Matrix m n A →ₗ[R] Matrix m n A) (β := ℕ) (mulLeftLinearMap n R a) 0 =
    mulLeftLinearMap n R (HPow.hPow (β := ℕ) a 0)
have rw₁ : Eq (α := Matrix m n A →ₗ[R] Matrix m n A) 1 (mulLeftLinearMap n R 1)
Tactic: rw [pow_zero, pow_zero, mulLeftLinearMap_one, Module.End.one_eq_id]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Semiring R
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
a : Matrix m m A
k : ℕ
rw : Eq (α := Matrix m n A →ₗ[R] Matrix m n A) 1 (mulLeftLinearMap n R (HPow.hPow (β := ℕ) a 0))
rw₁ : Eq (α := Matrix m n A →ₗ[R] Matrix m n A) 1 (mulLeftLinearMap n R 1)
⊢ HPow.hPow (α := Matrix m n A →ₗ[R] Matrix m n A) (β := ℕ) (mulLeftLinearMap n R a) 0 =
    mulLeftLinearMap n R (HPow.hPow (β := ℕ) a 0)
have rw₂ : Eq (α := Matrix m n A →ₗ[R] Matrix m n A) 1 LinearMap.id
Tactic: rw [pow_zero, pow_zero, mulLeftLinearMap_one, Module.End.one_eq_id]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Semiring R
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
a : Matrix m m A
k : ℕ
rw : Eq (α := Matrix m n A →ₗ[R] Matrix m n A) 1 (mulLeftLinearMap n R (HPow.hPow (β := ℕ) a 0))
rw₁ : Eq (α := Matrix m n A →ₗ[R] Matrix m n A) 1 (mulLeftLinearMap n R 1)
rw₂ : Eq (α := Matrix m n A →ₗ[R] Matrix m n A) 1 LinearMap.id
⊢ HPow.hPow (α := Matrix m n A →ₗ[R] Matrix m n A) (β := ℕ) (mulLeftLinearMap n R a) 0 =
    mulLeftLinearMap n R (HPow.hPow (β := ℕ) a 0)
have rw₃ : Eq (α := Matrix m n A →ₗ[R] Matrix m n A) LinearMap.id LinearMap.id
Tactic: rw [pow_zero, pow_zero, mulLeftLinearMap_one, Module.End.one_eq_id]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
Goal:
m : Type u_2
n_1 : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Semiring R
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
a : Matrix m m A
k n : ℕ
⊢ HPow.hPow (α := Matrix m n_1 A →ₗ[R] Matrix m n_1 A) (mulLeftLinearMap n_1 R a) (n + 1) =
    mulLeftLinearMap n_1 R (a ^ (n + 1))
have rw : HPow.hPow (α := Matrix m n_1 A →ₗ[R] Matrix m n_1 A) (mulLeftLinearMap n_1 R a) n * mulLeftLinearMap n_1 R a =
  mulLeftLinearMap n_1 R (a ^ (n + 1))
Tactic: rw [pow_succ, pow_succ, mulLeftLinearMap_mul, Module.End.mul_eq_comp, pow_mulLeftLinearMap]
-- Lean 4 proof step from Mathlib.Data.Matrix.Bilinear (goal)
Goal:
m : Type u_2
n_1 : Type u_3
R : Type u_5
A : Type u_6
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : Semiring R
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
a : Matrix m m A
k n : ℕ
rw :
  HPow.hPow (α := Matrix m n_1 A →ₗ[R] Matrix m n_1 A) (mulLeftLinearMap n_1 R a) n * mulLeftLinearMap n_1 R a =
    mulLeftLinearMap n_1 R (a ^ (n + 1))
⊢ HPow.hPow (α := Matrix m n_1 A →ₗ[R] Matrix m n_1 A) (mulLeftLinearMap n_1 R a) (n + 1) =
    mulLeftLinearMap n_1 R (a ^ (n + 1))
have rw₁ : HPow.hPow (α := Matrix m n_1 A →ₗ[R] Matrix m n_1 A) (mulLeftLinearMap n_1 R a) n * mulLeftLinearMap n_1 R a =
  mulLeftLinearMap n_1 R (a ^ n * a)
Tactic: rw [pow_succ, pow_succ, mulLeftLinearMap_mul, Module.End.mul_eq_comp, pow_mulLeftLinearMap]