awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
inst_5 : StarAddMonoid R
x : m → R
A B : Matrix m n R
x' : n → R
rw :
  (diagonal (star x)).vec ⬝ᵥ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B *ᵥ (diagonal x').vec =
    star (diagonal x).vec ⬝ᵥ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B *ᵥ (diagonal x').vec
rw₁ :
  ((diagonal x).map star).vec ⬝ᵥ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B *ᵥ (diagonal x').vec =
    star (diagonal x).vec ⬝ᵥ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B *ᵥ (diagonal x').vec
⊢ star x ⬝ᵥ A ⊙ B *ᵥ x' = star (diagonal x).vec ⬝ᵥ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B *ᵥ (diagonal x').vec
have rw₂ : ((diagonal x).map star).vec ⬝ᵥ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B *ᵥ (diagonal x').vec =
  ((diagonal x).map star).vec ⬝ᵥ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B *ᵥ (diagonal x').vec
Tactic: rw [dotProduct_hadamard_mulVec_eq_kronecker, ← map_diagonal_star, star_vec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.WithConv (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : InvolutiveStar α
x : WithConv (Matrix m n α)
⊢ star (star x) = x
have h : ∀ (i : m) (j : n), (star (star x)).ofConv i j = x.ofConv i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.WithConv (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : Mul α
inst_1 : StarMul α
x x_1 : WithConv (Matrix m n α)
⊢ star (x * x_1) = star x_1 * star x
have h : ∀ (i : m) (j : n), (star (x * x_1)).ofConv i j = (star x_1 * star x).ofConv i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.WithConv (hypothesis)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Semiring α
inst_1 : IsLeftCancelMulZero α
inst_2 : StarRing α
f : WithConv (Matrix m n α)
hf : IsIdempotentElem f
⊢ IsSelfAdjoint f
have hf₁ : ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1
Tactic: simp_rw [IsIdempotentElem, WithConv.ext_iff, ← Matrix.ext_iff, convMul_def, hadamard_apply,
    ← isIdempotentElem_iff, IsIdempotentElem.iff_eq_zero_or_one] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.WithConv (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Semiring α
inst_1 : IsLeftCancelMulZero α
inst_2 : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1
⊢ IsSelfAdjoint f
have rw : (star f).ofConv = f.ofConv
Tactic: rw [IsSelfAdjoint, WithConv.ext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.WithConv (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Semiring α
inst_1 : IsLeftCancelMulZero α
inst_2 : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1
⊢ (star f).ofConv = f.ofConv
have a : ∀ (i : m) (j : n), (star f).ofConv i j = f.ofConv i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.WithConv (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Semiring α
inst_1 : IsLeftCancelMulZero α
inst_2 : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1
i : m
j : n
⊢ (star f).ofConv i j = f.ofConv i j
have a : ∀ (h : f.ofConv i j = 0), (star f).ofConv i j = f.ofConv i j
Tactic: obtain (h | h) := hf i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.WithConv (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Semiring α
inst_1 : IsLeftCancelMulZero α
inst_2 : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1
i : m
j : n
a : ∀ (h : f.ofConv i j = 0), (star f).ofConv i j = f.ofConv i j
⊢ (star f).ofConv i j = f.ofConv i j
have a₁ : ∀ (h : f.ofConv i j = 1), (star f).ofConv i j = f.ofConv i j
Tactic: obtain (h | h) := hf i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.WithConv (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : CommSemiring α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
x x_1 : WithConv (Matrix m n α)
⊢ AddHom.toFun
      (LinearMap.toAddHom (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
      (x * x_1) =
    AddHom.toFun
        (LinearMap.toAddHom (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
        x *
      AddHom.toFun
        (LinearMap.toAddHom (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
        x_1
have h : ∀ (i : n) (x_2 : m),
  Eq.{u_3 + 1} (α := α)
    (((AddHom.toFun
                (LinearMap.toAddHom
                  (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
                (x * x_1)).ofConv ∘ₗ
            LinearMap.single α (fun (i : n) ↦ α) i :
          (a : α) → m → α)
        1 x_2 :
      α)
    (((AddHom.toFun
                  (LinearMap.toAddHom
                    (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
                  x *
                AddHom.toFun
                  (LinearMap.toAddHom
                    (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
                  x_1).ofConv ∘ₗ
            LinearMap.single α (fun (i : n) ↦ α) i :
          (a : α) → m → α)
        1 x_2 :
      α)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.WithConv (goal)
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : CommSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
x y : Matrix m n α
⊢ (toLin' : (a : Matrix m n α) → (n → α) →ₗ[α] m → α) (x ⊙ y) =
    (HMul.hMul (α := WithConv ((n → α) →ₗ[α] m → α)) (β := WithConv ((n → α) →ₗ[α] m → α))
        (toConv ((toLin' : (a : Matrix m n α) → (n → α) →ₗ[α] m → α) x) : WithConv ((n → α) →ₗ[α] m → α))
        (toConv ((toLin' : (a : Matrix m n α) → (n → α) →ₗ[α] m → α) y) : WithConv ((n → α) →ₗ[α] m → α))).ofConv
have h : ∀ (i : n) (x_1 : m),
  Eq.{u_3 + 1} (α := α)
    ((((toLin' : (a : Matrix m n α) → (n → α) →ₗ[α] m → α) (x ⊙ y) ∘ₗ LinearMap.single α (fun (i : n) ↦ α) i :
            α →ₗ[α] m → α) :
          (a : α) → m → α)
        1 x_1 :
      α)
    (((HMul.hMul (α := WithConv ((n → α) →ₗ[α] m → α)) (β := WithConv ((n → α) →ₗ[α] m → α))
                (toConv ((toLin' : (a : Matrix m n α) → (n → α) →ₗ[α] m → α) x) : WithConv ((n → α) →ₗ[α] m → α))
                (toConv ((toLin' : (a : Matrix m n α) → (n → α) →ₗ[α] m → α) y) :
                  WithConv ((n → α) →ₗ[α] m → α))).ofConv ∘ₗ
            LinearMap.single α (fun (i : n) ↦ α) i :
          (a : α) → m → α)
        1 x_1 :
      α)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.WithConv (goal)
Goal:
n : Type u_2
α : Type u_3
inst : CommSemiring α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix n n α
⊢ A.IsSymm ↔
    Eq (α := WithConv ((n → α) →ₗ[α] n → α))
      (star (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) A)) : WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A)) : WithConv ((n → α) →ₗ[α] n → α))
have rw : A.IsSymm ↔
  Eq (α := WithConv ((n → α) →ₗ[α] n → α))
    (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (A.map star)) : WithConv ((n → α) →ₗ[α] n → α))
    (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A)) : WithConv ((n → α) →ₗ[α] n → α))
Tactic: rw [intrinsicStar_toLin', toConv_injective.eq_iff, toLin'.injective.eq_iff,
    ← transpose_conjTranspose, star_eq_conjTranspose, conjTranspose_inj, IsSymm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.WithConv (goal)
Goal:
n : Type u_2
α : Type u_3
inst : CommSemiring α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix n n α
rw :
  A.IsSymm ↔
    Eq (α := WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (A.map star)) : WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A)) : WithConv ((n → α) →ₗ[α] n → α))
⊢ A.IsSymm ↔
    Eq (α := WithConv ((n → α) →ₗ[α] n → α))
      (star (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) A)) : WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A)) : WithConv ((n → α) →ₗ[α] n → α))
have rw₁ : A.IsSymm ↔
  Eq (α := (n → α) →ₗ[α] n → α) ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (A.map star) : (n → α) →ₗ[α] n → α)
    ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A) : (n → α) →ₗ[α] n → α)
Tactic: rw [intrinsicStar_toLin', toConv_injective.eq_iff, toLin'.injective.eq_iff,
    ← transpose_conjTranspose, star_eq_conjTranspose, conjTranspose_inj, IsSymm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.WithConv (goal)
Goal:
n : Type u_2
α : Type u_3
inst : CommSemiring α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix n n α
rw :
  A.IsSymm ↔
    Eq (α := WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (A.map star)) : WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A)) : WithConv ((n → α) →ₗ[α] n → α))
rw₁ :
  A.IsSymm ↔
    Eq (α := (n → α) →ₗ[α] n → α)
      ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (A.map star) : (n → α) →ₗ[α] n → α)
      ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A) : (n → α) →ₗ[α] n → α)
⊢ A.IsSymm ↔
    Eq (α := WithConv ((n → α) →ₗ[α] n → α))
      (star (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) A)) : WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A)) : WithConv ((n → α) →ₗ[α] n → α))
have rw₂ : A.IsSymm ↔ A.map star = star A
Tactic: rw [intrinsicStar_toLin', toConv_injective.eq_iff, toLin'.injective.eq_iff,
    ← transpose_conjTranspose, star_eq_conjTranspose, conjTranspose_inj, IsSymm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.WithConv (goal)
Goal:
n : Type u_2
α : Type u_3
inst : CommSemiring α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix n n α
rw :
  A.IsSymm ↔
    Eq (α := WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (A.map star)) : WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A)) : WithConv ((n → α) →ₗ[α] n → α))
rw₁ :
  A.IsSymm ↔
    Eq (α := (n → α) →ₗ[α] n → α)
      ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (A.map star) : (n → α) →ₗ[α] n → α)
      ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A) : (n → α) →ₗ[α] n → α)
rw₂ : A.IsSymm ↔ A.map star = star A
⊢ A.IsSymm ↔
    Eq (α := WithConv ((n → α) →ₗ[α] n → α))
      (star (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) A)) : WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A)) : WithConv ((n → α) →ₗ[α] n → α))
have rw₃ : A.IsSymm ↔ Aᵀᴴ = star A
Tactic: rw [intrinsicStar_toLin', toConv_injective.eq_iff, toLin'.injective.eq_iff,
    ← transpose_conjTranspose, star_eq_conjTranspose, conjTranspose_inj, IsSymm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.WithConv (goal)
Goal:
n : Type u_2
α : Type u_3
inst : CommSemiring α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix n n α
rw :
  A.IsSymm ↔
    Eq (α := WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (A.map star)) : WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A)) : WithConv ((n → α) →ₗ[α] n → α))
rw₁ :
  A.IsSymm ↔
    Eq (α := (n → α) →ₗ[α] n → α)
      ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (A.map star) : (n → α) →ₗ[α] n → α)
      ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A) : (n → α) →ₗ[α] n → α)
rw₂ : A.IsSymm ↔ A.map star = star A
rw₃ : A.IsSymm ↔ Aᵀᴴ = star A
⊢ A.IsSymm ↔
    Eq (α := WithConv ((n → α) →ₗ[α] n → α))
      (star (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) A)) : WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A)) : WithConv ((n → α) →ₗ[α] n → α))
have rw₄ : A.IsSymm ↔ Aᵀᴴ = Aᴴ
Tactic: rw [intrinsicStar_toLin', toConv_injective.eq_iff, toLin'.injective.eq_iff,
    ← transpose_conjTranspose, star_eq_conjTranspose, conjTranspose_inj, IsSymm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.WithConv (goal)
Goal:
n : Type u_2
α : Type u_3
inst : CommSemiring α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix n n α
rw :
  A.IsSymm ↔
    Eq (α := WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (A.map star)) : WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A)) : WithConv ((n → α) →ₗ[α] n → α))
rw₁ :
  A.IsSymm ↔
    Eq (α := (n → α) →ₗ[α] n → α)
      ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (A.map star) : (n → α) →ₗ[α] n → α)
      ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A) : (n → α) →ₗ[α] n → α)
rw₂ : A.IsSymm ↔ A.map star = star A
rw₃ : A.IsSymm ↔ Aᵀᴴ = star A
rw₄ : A.IsSymm ↔ Aᵀᴴ = Aᴴ
⊢ A.IsSymm ↔
    Eq (α := WithConv ((n → α) →ₗ[α] n → α))
      (star (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) A)) : WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A)) : WithConv ((n → α) →ₗ[α] n → α))
have rw₅ : A.IsSymm ↔ Aᵀ = A
Tactic: rw [intrinsicStar_toLin', toConv_injective.eq_iff, toLin'.injective.eq_iff,
    ← transpose_conjTranspose, star_eq_conjTranspose, conjTranspose_inj, IsSymm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.WithConv (goal)
Goal:
n : Type u_2
α : Type u_3
inst : CommSemiring α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix n n α
rw :
  A.IsSymm ↔
    Eq (α := WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (A.map star)) : WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A)) : WithConv ((n → α) →ₗ[α] n → α))
rw₁ :
  A.IsSymm ↔
    Eq (α := (n → α) →ₗ[α] n → α)
      ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (A.map star) : (n → α) →ₗ[α] n → α)
      ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A) : (n → α) →ₗ[α] n → α)
rw₂ : A.IsSymm ↔ A.map star = star A
rw₃ : A.IsSymm ↔ Aᵀᴴ = star A
rw₄ : A.IsSymm ↔ Aᵀᴴ = Aᴴ
rw₅ : A.IsSymm ↔ Aᵀ = A
⊢ A.IsSymm ↔
    Eq (α := WithConv ((n → α) →ₗ[α] n → α))
      (star (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) A)) : WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A)) : WithConv ((n → α) →ₗ[α] n → α))
have rw₆ : Aᵀ = A ↔ Aᵀ = A
Tactic: rw [intrinsicStar_toLin', toConv_injective.eq_iff, toLin'.injective.eq_iff,
    ← transpose_conjTranspose, star_eq_conjTranspose, conjTranspose_inj, IsSymm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
ih : A⁻¹ ^ n = (A ^ n)⁻¹
⊢ A⁻¹ ^ (n + 1) = (A ^ (n + 1))⁻¹
have succ : A⁻¹ ^ (n + 1) = (A ^ n * A)⁻¹
Tactic: rw [pow_succ A, mul_inv_rev, ← ih, ← pow_succ']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
ih : A⁻¹ ^ n = (A ^ n)⁻¹
succ : A⁻¹ ^ (n + 1) = (A ^ n * A)⁻¹
⊢ A⁻¹ ^ (n + 1) = (A ^ (n + 1))⁻¹
have succ₁ : A⁻¹ ^ (n + 1) = A⁻¹ * (A ^ n)⁻¹
Tactic: rw [pow_succ A, mul_inv_rev, ← ih, ← pow_succ']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
ih : A⁻¹ ^ n = (A ^ n)⁻¹
succ : A⁻¹ ^ (n + 1) = (A ^ n * A)⁻¹
succ₁ : A⁻¹ ^ (n + 1) = A⁻¹ * (A ^ n)⁻¹
⊢ A⁻¹ ^ (n + 1) = (A ^ (n + 1))⁻¹
have succ₂ : A⁻¹ ^ (n + 1) = A⁻¹ * A⁻¹ ^ n
Tactic: rw [pow_succ A, mul_inv_rev, ← ih, ← pow_succ']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
ih : A⁻¹ ^ n = (A ^ n)⁻¹
succ : A⁻¹ ^ (n + 1) = (A ^ n * A)⁻¹
succ₁ : A⁻¹ ^ (n + 1) = A⁻¹ * (A ^ n)⁻¹
succ₂ : A⁻¹ ^ (n + 1) = A⁻¹ * A⁻¹ ^ n
⊢ A⁻¹ ^ (n + 1) = (A ^ (n + 1))⁻¹
have succ₃ : A⁻¹ ^ (n + 1) = A⁻¹ ^ (n + 1)
Tactic: rw [pow_succ A, mul_inv_rev, ← ih, ← pow_succ']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
⊢ A⁻¹ ^ n = (A ^ n)⁻¹
have zero : HPow.hPow (β := ℕ) A⁻¹ 0 = (HPow.hPow (β := ℕ) A 0)⁻¹
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [pow_succ A, mul_inv_rev, ← ih, ← pow_succ']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
zero : HPow.hPow (β := ℕ) A⁻¹ 0 = (HPow.hPow (β := ℕ) A 0)⁻¹
⊢ A⁻¹ ^ n = (A ^ n)⁻¹
have succ : ∀ (n : ℕ) (ih : A⁻¹ ^ n = (A ^ n)⁻¹), A⁻¹ ^ (n + 1) = (A ^ (n + 1))⁻¹
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [pow_succ A, mul_inv_rev, ← ih, ← pow_succ']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
m n : ℕ
ha : IsUnit A.det
h : n ≤ m
⊢ A ^ (m - n) = A ^ m * (A ^ n)⁻¹
have h₁ : IsUnit (A ^ n).det
Tactic: rw [← tsub_add_cancel_of_le h, pow_add, Matrix.mul_assoc, mul_nonsing_inv,
    tsub_add_cancel_of_le h, Matrix.mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
⊢ A⁻¹ ^ m * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ m
have succ : HPow.hPow (β := ℕ) A⁻¹ 0 * A ^ (n + 1) = A ^ (n + 1) * HPow.hPow (β := ℕ) A⁻¹ 0
Tactic: rcases m with m | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
succ : HPow.hPow (β := ℕ) A⁻¹ 0 * A ^ (n + 1) = A ^ (n + 1) * HPow.hPow (β := ℕ) A⁻¹ 0
⊢ A⁻¹ ^ m * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ m
have succ₁ : ∀ (m : ℕ), A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
Tactic: rcases m with m | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
have succ : ∀ (h : A⁻¹ * A = 1) (h' : A * A⁻¹ = 1), A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
Tactic: rcases nonsing_inv_cancel_or_zero A with ⟨h, h'⟩ | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
succ : ∀ (h : A⁻¹ * A = 1) (h' : A * A⁻¹ = 1), A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
have succ₁ : ∀ (h : A⁻¹ = 0), A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
Tactic: rcases nonsing_inv_cancel_or_zero A with ⟨h, h'⟩ | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
have A₁ : A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n
Tactic: calc
        A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n := by
          simp only [pow_succ A⁻¹, pow_succ' A, Matrix.mul_assoc]
        _ = A ^ n * A⁻¹ ^ m := by simp only [h, Matrix.mul_one, IH m]
        _ = A ^ n * (A * A⁻¹) * A⁻¹ ^ m := by simp only [h', Matrix.mul_one]
        _ = A ^ (n + 1) * A⁻¹ ^ (m + 1) := by
          simp only [pow_succ A, pow_succ' A⁻¹, Matrix.mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
A₁ : A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
have A₂ : A⁻¹ ^ m * (A⁻¹ * A) * A ^ n = A ^ n * A⁻¹ ^ m
Tactic: calc
        A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n := by
          simp only [pow_succ A⁻¹, pow_succ' A, Matrix.mul_assoc]
        _ = A ^ n * A⁻¹ ^ m := by simp only [h, Matrix.mul_one, IH m]
        _ = A ^ n * (A * A⁻¹) * A⁻¹ ^ m := by simp only [h', Matrix.mul_one]
        _ = A ^ (n + 1) * A⁻¹ ^ (m + 1) := by
          simp only [pow_succ A, pow_succ' A⁻¹, Matrix.mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
A₁ : A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n
A₂ : A⁻¹ ^ m * (A⁻¹ * A) * A ^ n = A ^ n * A⁻¹ ^ m
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
have A₃ : A ^ n * A⁻¹ ^ m = A ^ n * (A * A⁻¹) * A⁻¹ ^ m
Tactic: calc
        A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n := by
          simp only [pow_succ A⁻¹, pow_succ' A, Matrix.mul_assoc]
        _ = A ^ n * A⁻¹ ^ m := by simp only [h, Matrix.mul_one, IH m]
        _ = A ^ n * (A * A⁻¹) * A⁻¹ ^ m := by simp only [h', Matrix.mul_one]
        _ = A ^ (n + 1) * A⁻¹ ^ (m + 1) := by
          simp only [pow_succ A, pow_succ' A⁻¹, Matrix.mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
A₁ : A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n
A₂ : A⁻¹ ^ m * (A⁻¹ * A) * A ^ n = A ^ n * A⁻¹ ^ m
A₃ : A ^ n * A⁻¹ ^ m = A ^ n * (A * A⁻¹) * A⁻¹ ^ m
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
have A₄ : A ^ n * (A * A⁻¹) * A⁻¹ ^ m = A ^ (n + 1) * A⁻¹ ^ (m + 1)
Tactic: calc
        A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n := by
          simp only [pow_succ A⁻¹, pow_succ' A, Matrix.mul_assoc]
        _ = A ^ n * A⁻¹ ^ m := by simp only [h, Matrix.mul_one, IH m]
        _ = A ^ n * (A * A⁻¹) * A⁻¹ ^ m := by simp only [h', Matrix.mul_one]
        _ = A ^ (n + 1) * A⁻¹ ^ (m + 1) := by
          simp only [pow_succ A, pow_succ' A⁻¹, Matrix.mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
m n : ℕ
⊢ A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
have zero : ∀ (m : ℕ), A⁻¹ ^ m * HPow.hPow (β := ℕ) A 0 = HPow.hPow (β := ℕ) A 0 * A⁻¹ ^ m
Tactic: induction n generalizing m with
  | zero => simp
  | succ n IH =>
    rcases m with m | m
    · simp
    rcases nonsing_inv_cancel_or_zero A with ⟨h, h'⟩ | h
    · calc
        A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n := by
          simp only [pow_succ A⁻¹, pow_succ' A, Matrix.mul_assoc]
        _ = A ^ n * A⁻¹ ^ m := by simp only [h, Matrix.mul_one, IH m]
        _ = A ^ n * (A * A⁻¹) * A⁻¹ ^ m := by simp only [h', Matrix.mul_one]
        _ = A ^ (n + 1) * A⁻¹ ^ (m + 1) := by
          simp only [pow_succ A, pow_succ' A⁻¹, Matrix.mul_assoc]
    · simp [h]
Cleared hypotheses: m, n