awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Dual (goal)
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommSemiring K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
inst_7 : DecidableEq ι₁
inst_8 : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
M : Matrix ι₁ ι₂ K
⊢ Eq (α := Dual K V₁ →ₗ[K] Dual K V₂)
    ((toLin B₁.dualBasis B₂.dualBasis : (a : Matrix ι₂ ι₁ K) → Dual K V₁ →ₗ[K] Dual K V₂) Mᵀ :
      Dual K V₁ →ₗ[K] Dual K V₂)
    ((Dual.transpose : (a : V₂ →ₗ[K] V₁) → Dual K V₁ →ₗ[K] Dual K V₂)
        ((toLin B₂ B₁ : (a : Matrix ι₁ ι₂ K) → V₂ →ₗ[K] V₁) M) :
      Dual K V₁ →ₗ[K] Dual K V₂)
have a : Eq (α := Matrix ι₂ ι₁ K)
  ((LinearMap.toMatrix B₁.dualBasis B₂.dualBasis : (a : Dual K V₁ →ₗ[K] Dual K V₂) → Matrix ι₂ ι₁ K)
      ((toLin B₁.dualBasis B₂.dualBasis : (a : Matrix ι₂ ι₁ K) → Dual K V₁ →ₗ[K] Dual K V₂) Mᵀ) :
    Matrix ι₂ ι₁ K)
  ((LinearMap.toMatrix B₁.dualBasis B₂.dualBasis : (a : Dual K V₁ →ₗ[K] Dual K V₂) → Matrix ι₂ ι₁ K)
      ((Dual.transpose : (a : V₂ →ₗ[K] V₁) → Dual K V₁ →ₗ[K] Dual K V₂)
        ((toLin B₂ B₁ : (a : Matrix ι₁ ι₂ K) → V₂ →ₗ[K] V₁) M)) :
    Matrix ι₂ ι₁ K)
Tactic: apply (LinearMap.toMatrix B₁.dualBasis B₂.dualBasis).injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Dual (goal)
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommSemiring K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
inst_7 : DecidableEq ι₁
inst_8 : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
M : Matrix ι₁ ι₂ K
⊢ Eq (α := Matrix ι₂ ι₁ K)
    ((LinearMap.toMatrix B₁.dualBasis B₂.dualBasis : (a : Dual K V₁ →ₗ[K] Dual K V₂) → Matrix ι₂ ι₁ K)
        ((toLin B₁.dualBasis B₂.dualBasis : (a : Matrix ι₂ ι₁ K) → Dual K V₁ →ₗ[K] Dual K V₂) Mᵀ) :
      Matrix ι₂ ι₁ K)
    ((LinearMap.toMatrix B₁.dualBasis B₂.dualBasis : (a : Dual K V₁ →ₗ[K] Dual K V₂) → Matrix ι₂ ι₁ K)
        ((Dual.transpose : (a : V₂ →ₗ[K] V₁) → Dual K V₁ →ₗ[K] Dual K V₂)
          ((toLin B₂ B₁ : (a : Matrix ι₁ ι₂ K) → V₂ →ₗ[K] V₁) M)) :
      Matrix ι₂ ι₁ K)
have a : Mᵀ =
  (LinearMap.toMatrix B₁.dualBasis B₂.dualBasis : (a : Dual K V₁ →ₗ[K] Dual K V₂) → Matrix ι₂ ι₁ K)
    ((Dual.transpose : (a : V₂ →ₗ[K] V₁) → Dual K V₁ →ₗ[K] Dual K V₂)
      ((toLin B₂ B₁ : (a : Matrix ι₁ ι₂ K) → V₂ →ₗ[K] V₁) M))
Tactic: rw [LinearMap.toMatrix_toLin, LinearMap.toMatrix_transpose, LinearMap.toMatrix_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Dual (goal)
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommSemiring K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
inst_7 : DecidableEq ι₁
inst_8 : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
M : Matrix ι₁ ι₂ K
a :
  Mᵀ =
    (LinearMap.toMatrix B₁.dualBasis B₂.dualBasis : (a : Dual K V₁ →ₗ[K] Dual K V₂) → Matrix ι₂ ι₁ K)
      ((Dual.transpose : (a : V₂ →ₗ[K] V₁) → Dual K V₁ →ₗ[K] Dual K V₂)
        ((toLin B₂ B₁ : (a : Matrix ι₁ ι₂ K) → V₂ →ₗ[K] V₁) M))
⊢ Eq (α := Matrix ι₂ ι₁ K)
    ((LinearMap.toMatrix B₁.dualBasis B₂.dualBasis : (a : Dual K V₁ →ₗ[K] Dual K V₂) → Matrix ι₂ ι₁ K)
        ((toLin B₁.dualBasis B₂.dualBasis : (a : Matrix ι₂ ι₁ K) → Dual K V₁ →ₗ[K] Dual K V₂) Mᵀ) :
      Matrix ι₂ ι₁ K)
    ((LinearMap.toMatrix B₁.dualBasis B₂.dualBasis : (a : Dual K V₁ →ₗ[K] Dual K V₂) → Matrix ι₂ ι₁ K)
        ((Dual.transpose : (a : V₂ →ₗ[K] V₁) → Dual K V₁ →ₗ[K] Dual K V₂)
          ((toLin B₂ B₁ : (a : Matrix ι₁ ι₂ K) → V₂ →ₗ[K] V₁) M)) :
      Matrix ι₂ ι₁ K)
have a₁ : Mᵀ =
  ((LinearMap.toMatrix B₂ B₁ : (a : V₂ →ₗ[K] V₁) → Matrix ι₁ ι₂ K)
      ((toLin B₂ B₁ : (a : Matrix ι₁ ι₂ K) → V₂ →ₗ[K] V₁) M))ᵀ
Tactic: rw [LinearMap.toMatrix_toLin, LinearMap.toMatrix_transpose, LinearMap.toMatrix_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Dual (goal)
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommSemiring K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
inst_7 : DecidableEq ι₁
inst_8 : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
M : Matrix ι₁ ι₂ K
a :
  Mᵀ =
    (LinearMap.toMatrix B₁.dualBasis B₂.dualBasis : (a : Dual K V₁ →ₗ[K] Dual K V₂) → Matrix ι₂ ι₁ K)
      ((Dual.transpose : (a : V₂ →ₗ[K] V₁) → Dual K V₁ →ₗ[K] Dual K V₂)
        ((toLin B₂ B₁ : (a : Matrix ι₁ ι₂ K) → V₂ →ₗ[K] V₁) M))
a₁ :
  Mᵀ =
    ((LinearMap.toMatrix B₂ B₁ : (a : V₂ →ₗ[K] V₁) → Matrix ι₁ ι₂ K)
        ((toLin B₂ B₁ : (a : Matrix ι₁ ι₂ K) → V₂ →ₗ[K] V₁) M))ᵀ
⊢ Eq (α := Matrix ι₂ ι₁ K)
    ((LinearMap.toMatrix B₁.dualBasis B₂.dualBasis : (a : Dual K V₁ →ₗ[K] Dual K V₂) → Matrix ι₂ ι₁ K)
        ((toLin B₁.dualBasis B₂.dualBasis : (a : Matrix ι₂ ι₁ K) → Dual K V₁ →ₗ[K] Dual K V₂) Mᵀ) :
      Matrix ι₂ ι₁ K)
    ((LinearMap.toMatrix B₁.dualBasis B₂.dualBasis : (a : Dual K V₁ →ₗ[K] Dual K V₂) → Matrix ι₂ ι₁ K)
        ((Dual.transpose : (a : V₂ →ₗ[K] V₁) → Dual K V₁ →ₗ[K] Dual K V₂)
          ((toLin B₂ B₁ : (a : Matrix ι₁ ι₂ K) → V₂ →ₗ[K] V₁) M)) :
      Matrix ι₂ ι₁ K)
have a₂ : Mᵀ = Mᵀ
Tactic: rw [LinearMap.toMatrix_toLin, LinearMap.toMatrix_transpose, LinearMap.toMatrix_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Dual (goal)
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
v w : n → R
⊢ { toFun := dotProduct (v + w), map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := Dual R (n → R)) { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ : (n → R) →ₗ[R] R }
      { toFun := dotProduct w, map_add' := ⋯, map_smul' := ⋯ : (n → R) →ₗ[R] R }
have h : ∀ (i : n),
  Eq (α := R)
    (({ toFun := dotProduct (v + w), map_add' := sorry, map_smul' := sorry } ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i :
          (a : R) → R)
        1 :
      R)
    ((HAdd.hAdd (α := Dual R (n → R)) { toFun := dotProduct v, map_add' := sorry, map_smul' := sorry : (n → R) →ₗ[R] R }
              { toFun := dotProduct w, map_add' := sorry, map_smul' := sorry : (n → R) →ₗ[R] R } ∘ₗ
            LinearMap.single R (fun (i : n) ↦ R) i :
          (a : R) → R)
        1 :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Dual (goal)
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
t : R
v : n → R
⊢ { toFun := dotProduct (t • v), map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := R) (β := Dual R (n → R)) ((RingHom.id R : (a : R) → R) t : R)
      { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ : (n → R) →ₗ[R] R }
have h : ∀ (i : n),
  Eq (α := R)
    (({ toFun := dotProduct (t • v), map_add' := sorry, map_smul' := sorry } ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i :
          (a : R) → R)
        1 :
      R)
    ((HSMul.hSMul (α := R) (β := Dual R (n → R)) ((RingHom.id R : (a : R) → R) t : R)
              { toFun := dotProduct v, map_add' := sorry, map_smul' := sorry : (n → R) →ₗ[R] R } ∘ₗ
            LinearMap.single R (fun (i : n) ↦ R) i :
          (a : R) → R)
        1 :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Dual (goal)
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
f : Dual R (n → R)
⊢ (fun (v : n → R) ↦ ({ toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ } : (n → R) →ₗ[R] R))
      ((fun (f : Dual R (n → R)) (i : n) ↦
          ((f : (a : n → R) → R)
              (((LinearMap.single R (fun (a : n) ↦ R) i : R →ₗ[R] (i : n) → R) : (a : R) → (i : n) → R) 1 :
                (i : n) → R) :
            R))
        f) =
    f
have h : ∀ (i : n),
  Eq (α := R)
    ((((fun (v : n → R) ↦ ({ toFun := dotProduct v, map_add' := sorry, map_smul' := sorry } : (n → R) →ₗ[R] R))
                ((fun (f : Dual R (n → R)) (i : n) ↦
                    ((f : (a : n → R) → R)
                        (((LinearMap.single R (fun (a : n) ↦ R) i : R →ₗ[R] (i : n) → R) : (a : R) → (i : n) → R) 1 :
                          (i : n) → R) :
                      R))
                  f) ∘ₗ
              LinearMap.single R (fun (i : n) ↦ R) i :
            R →ₗ[R] R) :
          (a : R) → R)
        1 :
      R)
    ((f ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i : (a : R) → R) 1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : R
A B : FixedDetMatrix n R m
h : (↑A : Matrix n n R) = (↑B : Matrix n n R)
⊢ A = B
have mk : ∀ (val : Matrix n n R) (property : val.det = m)
  (h : (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val property) : Matrix n n R) = (↑B : Matrix n n R)),
  Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val property = B
Tactic: cases A
Cleared hypotheses: A, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : R
B : FixedDetMatrix n R m
val : Matrix n n R
property : val.det = m
h : (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val property) : Matrix n n R) = (↑B : Matrix n n R)
⊢ Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val property = B
have mk : ∀ (val_1 : Matrix n n R) (property_1 : val_1.det = m)
  (h :
    (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val property) : Matrix n n R) =
      (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val_1 property_1) : Matrix n n R)),
  Eq (α := FixedDetMatrix n R m) (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val property)
    (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) val_1 property_1)
Tactic: cases B
Cleared hypotheses: B, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : R
A B : FixedDetMatrix n R m
h : ∀ (i j : n), (↑A : Matrix n n R) i j = (↑B : Matrix n n R) i j
⊢ A = B
have h₁ : (↑A : Matrix n n R) = (↑B : Matrix n n R)
Tactic: apply ext'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : R
x y : SpecialLinearGroup n R
b : FixedDetMatrix n R m
⊢ (x * y) • b = x • y • b
have simp_rw : Eq (α := FixedDetMatrix n R m)
  (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) ((↑(x * y) : Matrix n n R) * (↑b : Matrix n n R)) sorry)
  (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m)
    ((↑x : Matrix n n R) * ((↑y : Matrix n n R) * (↑b : Matrix n n R))) sorry)
Tactic: simp_rw [smul_def, ← mul_assoc, coe_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : R
x y : SpecialLinearGroup n R
b : FixedDetMatrix n R m
simp_rw :
  Eq (α := FixedDetMatrix n R m)
    (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) ((↑(x * y) : Matrix n n R) * (↑b : Matrix n n R)) ⋯)
    (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m)
      ((↑x : Matrix n n R) * ((↑y : Matrix n n R) * (↑b : Matrix n n R))) ⋯)
⊢ (x * y) • b = x • y • b
have simp_rw₁ : Eq (α := FixedDetMatrix n R m)
  (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) ((↑(x * y) : Matrix n n R) * (↑b : Matrix n n R)) sorry)
  (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m)
    ((↑x : Matrix n n R) * (↑y : Matrix n n R) * (↑b : Matrix n n R)) sorry)
Tactic: simp_rw [smul_def, ← mul_assoc, coe_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : R
g : SpecialLinearGroup n R
A : FixedDetMatrix n R m
⊢ (↑(g • A) : Matrix n n R) = (↑g : Matrix n n R) * (↑A : Matrix n n R)
have rw : (↑(Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = m) ((↑g : Matrix n n R) * (↑A : Matrix n n R)) sorry) : Matrix n n R) =
  (↑g : Matrix n n R) * (↑A : Matrix n n R)
Tactic: rw [smul_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0
this :
  (↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0
⊢ |(↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0|
have rw : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0|
Tactic: rw [this, abs_eq_self.mpr (Int.emod_nonneg (A.1 0 0) h)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0
⊢ |(↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0|
have suffices : (↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 =
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0
Tactic: suffices ((reduceStep A).1 1 0) = A.1 0 0 % A.1 1 0 by
    rw [this, abs_eq_self.mpr (Int.emod_nonneg (A.1 0 0) h)]
    exact Int.emod_lt_abs (A.1 0 0) h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0
⊢ (↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0
have simp_rw : HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℤ) (!![0, -1; 1, 0] : Matrix (Fin 2) (Fin 2) ℤ)
    (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℤ)
      (!![1, -((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0); 0, 1] :
        Matrix (Fin 2) (Fin 2) ℤ)
      (↑A : Matrix (Fin 2) (Fin 2) ℤ))
    1 0 =
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 +
    -((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 * ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0))
Tactic: simp_rw [Int.emod_def, sub_eq_add_neg, reduceStep, smul_coe, coe_T_zpow, S]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Sort u_3
base : (A : FixedDetMatrix (Fin 2) ℤ m) → (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 → C A
step : (A : FixedDetMatrix (Fin 2) ℤ m) → (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0 → C (reduceStep A) → C A
A : FixedDetMatrix (Fin 2) ℤ m
⊢ C A
have pos : (h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0) → C A
Tactic: by_cases h : (A.1 1 0) = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Sort u_3
base : (A : FixedDetMatrix (Fin 2) ℤ m) → (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 → C A
step : (A : FixedDetMatrix (Fin 2) ℤ m) → (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0 → C (reduceStep A) → C A
A : FixedDetMatrix (Fin 2) ℤ m
pos : (h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0) → C A
⊢ C A
have neg : (h : ¬(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0) → C A
Tactic: by_cases h : (A.1 1 0) = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ¬(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ ((↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0).natAbs < ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0).natAbs
have zify : |(↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0|
Tactic: zify
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ¬(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ ((↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0).natAbs < ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0).natAbs
have exact : |(↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0|
Tactic: decreasing_by
    zify
    exact reduce_aux h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
a : FixedDetMatrix (Fin 2) ℤ m
h : ¬(↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ ((↑(reduceStep a) : Matrix (Fin 2) (Fin 2) ℤ) 1 0).natAbs < ((↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0).natAbs
have zify : |(↑(reduceStep a) : Matrix (Fin 2) (Fin 2) ℤ) 1 0| < |(↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0|
Tactic: zify
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
ha : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
⊢ reduce A = T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A
have rw : (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
    if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
      T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A
    else T ^ (-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • S • S • A
  else reduce (reduceStep A)) =
  T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A
Tactic: rw [reduce]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
ha : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
⊢ (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
      if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
        T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A
      else T ^ (-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • S • S • A
    else reduce (reduceStep A)) =
    T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A
have simp : (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
    if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
      (T ^ ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1))⁻¹ • A
    else T ^ (-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) • S • S • A
  else reduce (reduceStep A)) =
  (T ^ ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1))⁻¹ • A
Tactic: simp only [zpow_neg, Int.ediv_neg, neg_neg] at *
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
ha : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
⊢ (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
      if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
        (T ^ ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1))⁻¹ • A
      else T ^ (-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) • S • S • A
    else reduce (reduceStep A)) =
    (T ^ ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1))⁻¹ • A
have simp_rw : (if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
    (T ^ ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1))⁻¹ • A
  else T ^ (-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) • S • S • A) =
  (T ^ ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1))⁻¹ • A
Tactic: simp_rw [if_pos hc, if_pos ha]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
ha : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
⊢ reduce A = T ^ (-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • S • S • A
have rw : (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
    if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
      T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A
    else T ^ (-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • S • S • A
  else reduce (reduceStep A)) =
  T ^ (-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • S • S • A
Tactic: rw [reduce]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
ha : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
⊢ (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
      if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
        T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A
      else T ^ (-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • S • S • A
    else reduce (reduceStep A)) =
    T ^ (-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • S • S • A
have simp : (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
    if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
      (T ^ ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1))⁻¹ • A
    else T ^ (-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) • S • S • A
  else reduce (reduceStep A)) =
  T ^ (-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) • S • S • A
Tactic: simp only [zpow_neg, Int.ediv_neg, neg_neg] at *
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
ha : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
⊢ (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
      if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
        (T ^ ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1))⁻¹ • A
      else T ^ (-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) • S • S • A
    else reduce (reduceStep A)) =
    T ^ (-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) • S • S • A
have simp_rw : (if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
    (T ^ ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1))⁻¹ • A
  else T ^ (-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) • S • S • A) =
  T ^ (-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) • S • S • A
Tactic: simp_rw [if_pos hc, if_neg ha]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0
⊢ reduce (reduceStep A) = reduce A
have symm : reduce A = reduce (reduceStep A)
Tactic: symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0
⊢ reduce A = reduce (reduceStep A)
have rw : (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
    if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
      T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A
    else T ^ (-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • S • S • A
  else reduce (reduceStep A)) =
  reduce (reduceStep A)
Tactic: rw [reduce, if_neg hc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0
rw :
  (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
      if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
        T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A
      else T ^ (-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • S • S • A
    else reduce (reduceStep A)) =
    reduce (reduceStep A)
⊢ reduce A = reduce (reduceStep A)
have rw₁ : reduce (reduceStep A) = reduce (reduceStep A)
Tactic: rw [reduce, if_neg hc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : A ∈ reps m
i j : Fin 2
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) i j ∈ Finset.Icc (-|m|) |m|
have suffices : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) i j| ≤ |m|
Tactic: suffices |A.1 i j| ≤ |m| from Finset.mem_Icc.mpr <| abs_le.mp this