internlm/Lean-Github huggingface dataset:
Theorem: Smt.Reconstruct.Builtin.cnfItePos3
Proof state before:
c a b : Prop
h : Decidable c
h✝ : ¬c
hite : ¬¬if c then a else b
hite' : if c then a else b
⊢ a ∨ b
Tactic:
exact Or.inr hite'
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.cnfItePos3
Proof state before:
c a b : Prop
h : Decidable c
h✝ : c
hite : ¬¬if c then a else b
hite' : if c then a else b
⊢ a ∨ b
Tactic:
exact Or.inl hite'
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.cnfIteNeg1
Proof state before:
c a b : Prop
h : Decidable c
⊢ (if c then a else b) ∨ ¬c ∨ ¬a
Tactic:
apply orImplies
Proof state after:
case a
c a b : Prop
h : Decidable c
⊢ (¬if c then a else b) → ¬c ∨ ¬a
Theorem: Smt.Reconstruct.Builtin.cnfIteNeg1
Proof state before:
case a
c a b : Prop
h : Decidable c
⊢ (¬if c then a else b) → ¬c ∨ ¬a
Tactic:
intro hnite
Proof state after:
case a
c a b : Prop
h : Decidable c
hnite : ¬if c then a else b
⊢ ¬c ∨ ¬a
Theorem: Smt.Reconstruct.Builtin.cnfIteNeg1
Proof state before:
case a
c a b : Prop
h : Decidable c
hnite : ¬if c then a else b
⊢ ¬c ∨ ¬a
Tactic:
match h with
| isTrue _    => exact Or.inr hnite
| isFalse hnc => exact Or.inl hnc
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.cnfIteNeg1
Proof state before:
c a b : Prop
h : Decidable c
h✝ : c
hnite : ¬if c then a else b
⊢ ¬c ∨ ¬a
Tactic:
exact Or.inr hnite
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.cnfIteNeg1
Proof state before:
c a b : Prop
h : Decidable c
hnc : ¬c
hnite : ¬if c then a else b
⊢ ¬c ∨ ¬a
Tactic:
exact Or.inl hnc
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.cnfIteNeg2
Proof state before:
c a b : Prop
h : Decidable c
⊢ (if c then a else b) ∨ c ∨ ¬b
Tactic:
apply orImplies
Proof state after:
case a
c a b : Prop
h : Decidable c
⊢ (¬if c then a else b) → c ∨ ¬b
Theorem: Smt.Reconstruct.Builtin.cnfIteNeg2
Proof state before:
case a
c a b : Prop
h : Decidable c
⊢ (¬if c then a else b) → c ∨ ¬b
Tactic:
intro hnite
Proof state after:
case a
c a b : Prop
h : Decidable c
hnite : ¬if c then a else b
⊢ c ∨ ¬b
Theorem: Smt.Reconstruct.Builtin.cnfIteNeg2
Proof state before:
case a
c a b : Prop
h : Decidable c
hnite : ¬if c then a else b
⊢ c ∨ ¬b
Tactic:
match h with
| isFalse _ => exact Or.inr hnite
| isTrue hc => exact Or.inl hc
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.cnfIteNeg2
Proof state before:
c a b : Prop
h : Decidable c
h✝ : ¬c
hnite : ¬if c then a else b
⊢ c ∨ ¬b
Tactic:
exact Or.inr hnite
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.cnfIteNeg2
Proof state before:
c a b : Prop
h : Decidable c
hc : c
hnite : ¬if c then a else b
⊢ c ∨ ¬b
Tactic:
exact Or.inl hc
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.cnfIteNeg3
Proof state before:
c a b : Prop
h : Decidable c
⊢ (if c then a else b) ∨ ¬a ∨ ¬b
Tactic:
apply orImplies
Proof state after:
case a
c a b : Prop
h : Decidable c
⊢ (¬if c then a else b) → ¬a ∨ ¬b
Theorem: Smt.Reconstruct.Builtin.cnfIteNeg3
Proof state before:
case a
c a b : Prop
h : Decidable c
⊢ (¬if c then a else b) → ¬a ∨ ¬b
Tactic:
intro hnite
Proof state after:
case a
c a b : Prop
h : Decidable c
hnite : ¬if c then a else b
⊢ ¬a ∨ ¬b
Theorem: Smt.Reconstruct.Builtin.cnfIteNeg3
Proof state before:
case a
c a b : Prop
h : Decidable c
hnite : ¬if c then a else b
⊢ ¬a ∨ ¬b
Tactic:
match h with
| isFalse _ => exact Or.inr hnite
| isTrue _  => exact Or.inl hnite
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.cnfIteNeg3
Proof state before:
c a b : Prop
h : Decidable c
h✝ : ¬c
hnite : ¬if c then a else b
⊢ ¬a ∨ ¬b
Tactic:
exact Or.inr hnite
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.cnfIteNeg3
Proof state before:
c a b : Prop
h : Decidable c
h✝ : c
hnite : ¬if c then a else b
⊢ ¬a ∨ ¬b
Tactic:
exact Or.inl hnite
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.scopes
Proof state before:
⊢ ∀ {ps : List Prop} {q : Prop}, impliesN ps q → andN ps → q
Tactic:
intros ps q h
Proof state after:
ps : List Prop
q : Prop
h : impliesN ps q
⊢ andN ps → q
Theorem: Smt.Reconstruct.Builtin.scopes
Proof state before:
ps : List Prop
q : Prop
h : impliesN ps q
⊢ andN ps → q
Tactic:
match ps with
| []   => intro; exact h
| [p]  => unfold andN
          unfold impliesN at h
          exact h
| p₁::p₂::ps => unfold andN
                unfold impliesN at h
                intro ⟨hp₁, hps⟩
                revert hps
                exact scopes (h hp₁)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.scopes
Proof state before:
ps : List Prop
q : Prop
h : impliesN [] q
⊢ andN [] → q
Tactic:
intro
Proof state after:
ps : List Prop
q : Prop
h : impliesN [] q
a✝ : andN []
⊢ q
Theorem: Smt.Reconstruct.Builtin.scopes
Proof state before:
ps : List Prop
q : Prop
h : impliesN [] q
a✝ : andN []
⊢ q
Tactic:
exact h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.scopes
Proof state before:
ps : List Prop
q p : Prop
h : impliesN [p] q
⊢ andN [p] → q
Tactic:
unfold andN
Proof state after:
ps : List Prop
q p : Prop
h : impliesN [p] q
⊢ p → q
Theorem: Smt.Reconstruct.Builtin.scopes
Proof state before:
ps : List Prop
q p : Prop
h : impliesN [p] q
⊢ p → q
Tactic:
unfold impliesN at h
Proof state after:
ps : List Prop
q p : Prop
h : p → impliesN [] q
⊢ p → q
Theorem: Smt.Reconstruct.Builtin.scopes
Proof state before:
ps : List Prop
q p : Prop
h : p → impliesN [] q
⊢ p → q
Tactic:
exact h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Builtin.scopes
Proof state before:
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : impliesN (p₁ :: p₂ :: ps) q
⊢ andN (p₁ :: p₂ :: ps) → q
Tactic:
unfold andN
Proof state after:
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : impliesN (p₁ :: p₂ :: ps) q
⊢ p₁ ∧ andN (p₂ :: ps) → q
Theorem: Smt.Reconstruct.Builtin.scopes
Proof state before:
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : impliesN (p₁ :: p₂ :: ps) q
⊢ p₁ ∧ andN (p₂ :: ps) → q
Tactic:
unfold impliesN at h
Proof state after:
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : p₁ → impliesN (p₂ :: ps) q
⊢ p₁ ∧ andN (p₂ :: ps) → q
Theorem: Smt.Reconstruct.Builtin.scopes
Proof state before:
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : p₁ → impliesN (p₂ :: ps) q
⊢ p₁ ∧ andN (p₂ :: ps) → q
Tactic:
intro ⟨hp₁, hps⟩
Proof state after:
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : p₁ → impliesN (p₂ :: ps) q
hp₁ : p₁
hps : andN (p₂ :: ps)
⊢ q
Theorem: Smt.Reconstruct.Builtin.scopes
Proof state before:
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : p₁ → impliesN (p₂ :: ps) q
hp₁ : p₁
hps : andN (p₂ :: ps)
⊢ q
Tactic:
revert hps
Proof state after:
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : p₁ → impliesN (p₂ :: ps) q
hp₁ : p₁
⊢ andN (p₂ :: ps) → q
Theorem: Smt.Reconstruct.Builtin.scopes
Proof state before:
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : p₁ → impliesN (p₂ :: ps) q
hp₁ : p₁
⊢ andN (p₂ :: ps) → q
Tactic:
exact scopes (h hp₁)
Proof state after:
no goals
Theorem: resolution
Proof state before:
p q r : Bool
⊢ (p || q) = true → (!p || r) = true → (q || r) = true
Tactic:
intro hpq
Proof state after:
p q r : Bool
hpq : (p || q) = true
⊢ (!p || r) = true → (q || r) = true
Theorem: resolution
Proof state before:
p q r : Bool
hpq : (p || q) = true
⊢ (!p || r) = true → (q || r) = true
Tactic:
intro hnpr
Proof state after:
p q r : Bool
hpq : (p || q) = true
hnpr : (!p || r) = true
⊢ (q || r) = true
Theorem: resolution
Proof state before:
p q r : Bool
hpq : (p || q) = true
hnpr : (!p || r) = true
⊢ (q || r) = true
Tactic:
cases p <;> cases r <;> simp_all
Proof state after:
no goals
Theorem: addition
Proof state before:
p q : Bool
⊢ p = true → (p || q) = true
Tactic:
simp_all
Proof state after:
no goals
Theorem: triv
Proof state before:
p : Bool
⊢ p = true → p = true
Tactic:
simp_all
Proof state after:
no goals
Theorem: simplification
Proof state before:
p q : Bool
⊢ (p && q) = true → p = true
Tactic:
cases p <;> simp_all
Proof state after:
no goals
Theorem: length
Proof state before:
⊢ "a".length = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: hypothetical_syllogism
Proof state before:
p q r : Bool
⊢ (p = true → q = true) → (q = true → r = true) → p = true → r = true
Tactic:
simp_all
Proof state after:
no goals
Theorem: prop_ext
Proof state before:
p q : Bool
⊢ (p = true ↔ q = true) → (p == q) = true
Tactic:
intro ⟨hpq, hqp⟩
Proof state after:
p q : Bool
hpq : p = true → q = true
hqp : q = true → p = true
⊢ (p == q) = true
Theorem: prop_ext
Proof state before:
p q : Bool
hpq : p = true → q = true
hqp : q = true → p = true
⊢ (p == q) = true
Tactic:
cases p <;> cases q <;> simp_all
Proof state after:
no goals
Theorem: xor_comm_2
Proof state before:
x y : BitVec 2
⊢ x ^^^ y = y ^^^ x
Tactic:
sorry
Proof state after:
no goals
Theorem: xor_comm_4p4
Proof state before:
x y : BitVec (4 + 4)
⊢ x ^^^ y = y ^^^ x
Tactic:
sorry
Proof state after:
no goals
Theorem: trace_pow_two_fin_four
Proof state before:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ (A ^ 2).trace =
    A 0 0 ^ 2 + A 1 1 ^ 2 + A 2 2 ^ 2 + A 3 3 ^ 2 + 2 * A 0 1 * A 1 0 + 2 * A 0 2 * A 2 0 + 2 * A 0 3 * A 3 0 +
          2 * A 1 2 * A 2 1 +
        2 * A 1 3 * A 3 1 +
      2 * A 2 3 * A 3 2
Tactic:
simp_rw [Matrix.trace_fin_four, pow_two, mul_apply, Fin.sum_univ_four]
Proof state after:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ A 0 0 * A 0 0 + A 0 1 * A 1 0 + A 0 2 * A 2 0 + A 0 3 * A 3 0 +
          (A 1 0 * A 0 1 + A 1 1 * A 1 1 + A 1 2 * A 2 1 + A 1 3 * A 3 1) +
        (A 2 0 * A 0 2 + A 2 1 * A 1 2 + A 2 2 * A 2 2 + A 2 3 * A 3 2) +
      (A 3 0 * A 0 3 + A 3 1 * A 1 3 + A 3 2 * A 2 3 + A 3 3 * A 3 3) =
    A 0 0 * A 0 0 + A 1 1 * A 1 1 + A 2 2 * A 2 2 + A 3 3 * A 3 3 + 2 * A 0 1 * A 1 0 + 2 * A 0 2 * A 2 0 +
            2 * A 0 3 * A 3 0 +
          2 * A 1 2 * A 2 1 +
        2 * A 1 3 * A 3 1 +
      2 * A 2 3 * A 3 2
Theorem: trace_pow_two_fin_four
Proof state before:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ A 0 0 * A 0 0 + A 0 1 * A 1 0 + A 0 2 * A 2 0 + A 0 3 * A 3 0 +
          (A 1 0 * A 0 1 + A 1 1 * A 1 1 + A 1 2 * A 2 1 + A 1 3 * A 3 1) +
        (A 2 0 * A 0 2 + A 2 1 * A 1 2 + A 2 2 * A 2 2 + A 2 3 * A 3 2) +
      (A 3 0 * A 0 3 + A 3 1 * A 1 3 + A 3 2 * A 2 3 + A 3 3 * A 3 3) =
    A 0 0 * A 0 0 + A 1 1 * A 1 1 + A 2 2 * A 2 2 + A 3 3 * A 3 3 + 2 * A 0 1 * A 1 0 + 2 * A 0 2 * A 2 0 +
            2 * A 0 3 * A 3 0 +
          2 * A 1 2 * A 2 1 +
        2 * A 1 3 * A 3 1 +
      2 * A 2 3 * A 3 2
Tactic:
ring
Proof state after:
no goals
Theorem: trace_pow_three_fin_four
Proof state before:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ A 0 0 * (A 0 0 * A 0 0 + A 0 1 * A 1 0 + A 0 2 * A 2 0 + A 0 3 * A 3 0) +
                A 0 1 * (A 1 0 * A 0 0 + A 1 1 * A 1 0 + A 1 2 * A 2 0 + A 1 3 * A 3 0) +
              A 0 2 * (A 2 0 * A 0 0 + A 2 1 * A 1 0 + A 2 2 * A 2 0 + A 2 3 * A 3 0) +
            A 0 3 * (A 3 0 * A 0 0 + A 3 1 * A 1 0 + A 3 2 * A 2 0 + A 3 3 * A 3 0) +
          (A 1 0 * (A 0 0 * A 0 1 + A 0 1 * A 1 1 + A 0 2 * A 2 1 + A 0 3 * A 3 1) +
                A 1 1 * (A 1 0 * A 0 1 + A 1 1 * A 1 1 + A 1 2 * A 2 1 + A 1 3 * A 3 1) +
              A 1 2 * (A 2 0 * A 0 1 + A 2 1 * A 1 1 + A 2 2 * A 2 1 + A 2 3 * A 3 1) +
            A 1 3 * (A 3 0 * A 0 1 + A 3 1 * A 1 1 + A 3 2 * A 2 1 + A 3 3 * A 3 1)) +
        (A 2 0 * (A 0 0 * A 0 2 + A 0 1 * A 1 2 + A 0 2 * A 2 2 + A 0 3 * A 3 2) +
              A 2 1 * (A 1 0 * A 0 2 + A 1 1 * A 1 2 + A 1 2 * A 2 2 + A 1 3 * A 3 2) +
            A 2 2 * (A 2 0 * A 0 2 + A 2 1 * A 1 2 + A 2 2 * A 2 2 + A 2 3 * A 3 2) +
          A 2 3 * (A 3 0 * A 0 2 + A 3 1 * A 1 2 + A 3 2 * A 2 2 + A 3 3 * A 3 2)) +
      (A 3 0 * (A 0 0 * A 0 3 + A 0 1 * A 1 3 + A 0 2 * A 2 3 + A 0 3 * A 3 3) +
            A 3 1 * (A 1 0 * A 0 3 + A 1 1 * A 1 3 + A 1 2 * A 2 3 + A 1 3 * A 3 3) +
          A 3 2 * (A 2 0 * A 0 3 + A 2 1 * A 1 3 + A 2 2 * A 2 3 + A 2 3 * A 3 3) +
        A 3 3 * (A 3 0 * A 0 3 + A 3 1 * A 1 3 + A 3 2 * A 2 3 + A 3 3 * A 3 3)) =
    A 0 0 * (A 0 0 ^ 2 + A 0 1 * A 1 0 + A 0 2 * A 2 0 + A 0 3 * A 3 0) +
                                  A 1 1 * (A 1 1 ^ 2 + A 0 1 * A 1 0 + A 1 2 * A 2 1 + A 1 3 * A 3 1) +
                                A 2 2 * (A 2 2 ^ 2 + A 0 2 * A 2 0 + A 1 2 * A 2 1 + A 2 3 * A 3 2) +
                              A 3 3 * (A 3 3 ^ 2 + A 0 3 * A 3 0 + A 1 3 * A 3 1 + A 2 3 * A 3 2) +
                            A 1 0 * (A 0 0 * A 0 1 + A 0 1 * A 1 1 + A 0 2 * A 2 1 + A 0 3 * A 3 1) +
                          A 2 0 * (A 0 0 * A 0 2 + A 0 1 * A 1 2 + A 0 2 * A 2 2 + A 0 3 * A 3 2) +
                        A 0 1 * (A 0 0 * A 1 0 + A 1 0 * A 1 1 + A 1 2 * A 2 0 + A 1 3 * A 3 0) +
                      A 3 0 * (A 0 0 * A 0 3 + A 0 1 * A 1 3 + A 0 2 * A 2 3 + A 0 3 * A 3 3) +
                    A 2 1 * (A 0 2 * A 1 0 + A 1 1 * A 1 2 + A 1 2 * A 2 2 + A 1 3 * A 3 2) +
                  A 0 2 * (A 0 0 * A 2 0 + A 1 0 * A 2 1 + A 2 0 * A 2 2 + A 2 3 * A 3 0) +
                A 3 1 * (A 0 3 * A 1 0 + A 1 1 * A 1 3 + A 1 2 * A 2 3 + A 1 3 * A 3 3) +
              A 1 2 * (A 0 1 * A 2 0 + A 1 1 * A 2 1 + A 2 1 * A 2 2 + A 2 3 * A 3 1) +
            A 0 3 * (A 0 0 * A 3 0 + A 1 0 * A 3 1 + A 2 0 * A 3 2 + A 3 0 * A 3 3) +
          A 3 2 * (A 0 3 * A 2 0 + A 1 3 * A 2 1 + A 2 2 * A 2 3 + A 2 3 * A 3 3) +
        A 1 3 * (A 0 1 * A 3 0 + A 1 1 * A 3 1 + A 2 1 * A 3 2 + A 3 1 * A 3 3) +
      A 2 3 * (A 0 2 * A 3 0 + A 1 2 * A 3 1 + A 2 2 * A 3 2 + A 3 2 * A 3 3)
Tactic:
ring
Proof state after:
no goals
Theorem: sq_trace_fin_four
Proof state before:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ A.trace ^ 2 =
    A 0 0 ^ 2 + A 1 1 ^ 2 + A 2 2 ^ 2 + A 3 3 ^ 2 + 2 * A 0 0 * A 1 1 + 2 * A 0 0 * A 2 2 + 2 * A 0 0 * A 3 3 +
          2 * A 1 1 * A 2 2 +
        2 * A 1 1 * A 3 3 +
      2 * A 2 2 * A 3 3
Tactic:
rw [trace_fin_four, pow_two]
Proof state after:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ (A 0 0 + A 1 1 + A 2 2 + A 3 3) * (A 0 0 + A 1 1 + A 2 2 + A 3 3) =
    A 0 0 ^ 2 + A 1 1 ^ 2 + A 2 2 ^ 2 + A 3 3 ^ 2 + 2 * A 0 0 * A 1 1 + 2 * A 0 0 * A 2 2 + 2 * A 0 0 * A 3 3 +
          2 * A 1 1 * A 2 2 +
        2 * A 1 1 * A 3 3 +
      2 * A 2 2 * A 3 3
Theorem: sq_trace_fin_four
Proof state before:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ (A 0 0 + A 1 1 + A 2 2 + A 3 3) * (A 0 0 + A 1 1 + A 2 2 + A 3 3) =
    A 0 0 ^ 2 + A 1 1 ^ 2 + A 2 2 ^ 2 + A 3 3 ^ 2 + 2 * A 0 0 * A 1 1 + 2 * A 0 0 * A 2 2 + 2 * A 0 0 * A 3 3 +
          2 * A 1 1 * A 2 2 +
        2 * A 1 1 * A 3 3 +
      2 * A 2 2 * A 3 3
Tactic:
ring
Proof state after:
no goals
Theorem: Matrix.one_fin_four
Proof state before:
R : Type u_1
inst✝ : CommRing R
⊢ 1 = of ![![1, 0, 0, 0], ![0, 1, 0, 0], ![0, 0, 1, 0], ![0, 0, 0, 1]]
Tactic:
ext i j
Proof state after:
case a
R : Type u_1
inst✝ : CommRing R
i j : Fin 4
⊢ 1 i j = of ![![1, 0, 0, 0], ![0, 1, 0, 0], ![0, 0, 1, 0], ![0, 0, 0, 1]] i j
Theorem: Matrix.one_fin_four
Proof state before:
case a
R : Type u_1
inst✝ : CommRing R
i j : Fin 4
⊢ 1 i j = of ![![1, 0, 0, 0], ![0, 1, 0, 0], ![0, 0, 1, 0], ![0, 0, 0, 1]] i j
Tactic:
fin_cases i <;> fin_cases j <;> rfl
Proof state after:
no goals
Theorem: Matrix.det_fin_four
Proof state before:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ A.det =
    A 0 0 * A 1 1 * A 2 2 * A 3 3 - A 0 0 * A 1 1 * A 2 3 * A 3 2 - A 0 0 * A 1 2 * A 2 1 * A 3 3 +
                                              A 0 0 * A 1 2 * A 2 3 * A 3 1 +
                                            A 0 0 * A 1 3 * A 2 1 * A 3 2 -
                                          A 0 0 * A 1 3 * A 2 2 * A 3 1 -
                                        A 0 1 * A 1 0 * A 2 2 * A 3 3 +
                                      A 0 1 * A 1 0 * A 2 3 * A 3 2 +
                                    A 0 1 * A 1 2 * A 2 0 * A 3 3 -
                                  A 0 1 * A 1 2 * A 2 3 * A 3 0 -
                                A 0 1 * A 1 3 * A 2 0 * A 3 2 +
                              A 0 1 * A 1 3 * A 2 2 * A 3 0 +
                            A 0 2 * A 1 0 * A 2 1 * A 3 3 -
                          A 0 2 * A 1 0 * A 2 3 * A 3 1 -
                        A 0 2 * A 1 1 * A 2 0 * A 3 3 +
                      A 0 2 * A 1 1 * A 2 3 * A 3 0 +
                    A 0 2 * A 1 3 * A 2 0 * A 3 1 -
                  A 0 2 * A 1 3 * A 2 1 * A 3 0 -
                A 0 3 * A 1 0 * A 2 1 * A 3 2 +
              A 0 3 * A 1 0 * A 2 2 * A 3 1 +
            A 0 3 * A 1 1 * A 2 0 * A 3 2 -
          A 0 3 * A 1 1 * A 2 2 * A 3 0 -
        A 0 3 * A 1 2 * A 2 0 * A 3 1 +
      A 0 3 * A 1 2 * A 2 1 * A 3 0
Tactic:
rw [Matrix.det_succ_row_zero]
Proof state after:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ ∑ j : Fin (Nat.succ 3), (-1) ^ ↑j * A 0 j * (A.submatrix Fin.succ j.succAbove).det =
    A 0 0 * A 1 1 * A 2 2 * A 3 3 - A 0 0 * A 1 1 * A 2 3 * A 3 2 - A 0 0 * A 1 2 * A 2 1 * A 3 3 +
                                              A 0 0 * A 1 2 * A 2 3 * A 3 1 +
                                            A 0 0 * A 1 3 * A 2 1 * A 3 2 -
                                          A 0 0 * A 1 3 * A 2 2 * A 3 1 -
                                        A 0 1 * A 1 0 * A 2 2 * A 3 3 +
                                      A 0 1 * A 1 0 * A 2 3 * A 3 2 +
                                    A 0 1 * A 1 2 * A 2 0 * A 3 3 -
                                  A 0 1 * A 1 2 * A 2 3 * A 3 0 -
                                A 0 1 * A 1 3 * A 2 0 * A 3 2 +
                              A 0 1 * A 1 3 * A 2 2 * A 3 0 +
                            A 0 2 * A 1 0 * A 2 1 * A 3 3 -
                          A 0 2 * A 1 0 * A 2 3 * A 3 1 -
                        A 0 2 * A 1 1 * A 2 0 * A 3 3 +
                      A 0 2 * A 1 1 * A 2 3 * A 3 0 +
                    A 0 2 * A 1 3 * A 2 0 * A 3 1 -
                  A 0 2 * A 1 3 * A 2 1 * A 3 0 -
                A 0 3 * A 1 0 * A 2 1 * A 3 2 +
              A 0 3 * A 1 0 * A 2 2 * A 3 1 +
            A 0 3 * A 1 1 * A 2 0 * A 3 2 -
          A 0 3 * A 1 1 * A 2 2 * A 3 0 -
        A 0 3 * A 1 2 * A 2 0 * A 3 1 +
      A 0 3 * A 1 2 * A 2 1 * A 3 0
Theorem: Matrix.det_fin_four
Proof state before:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
h10 : Fin.succAbove 1 0 = 0
h11 : Fin.succAbove 1 1 = 2
h12 : Fin.succAbove 1 2 = 3
h20 : Fin.succAbove 2 0 = 0
h21 : Fin.succAbove 2 1 = 1
h22 : Fin.succAbove 2 2 = 3
h30 : Fin.succAbove 3 0 = 0
h31 : Fin.succAbove 3 1 = 1
h32 : Fin.succAbove 3 2 = 2
s0 : Fin.succ 0 = 1
s1 : Fin.succ 1 = 2
s2 : Fin.succ 2 = 3
a0 : (-1) ^ ↑0 = 1
a1 : (-1) ^ ↑1 = -1
a2 : (-1) ^ ↑2 = 1
a3 : (-1) ^ ↑3 = -1
⊢ 1 * A 0 0 *
            (A 1 1 * A 2 2 * A 3 3 - A 1 1 * A 2 3 * A 3 2 - A 1 2 * A 2 1 * A 3 3 + A 1 2 * A 2 3 * A 3 1 +
                A 1 3 * A 2 1 * A 3 2 -
              A 1 3 * A 2 2 * A 3 1) +
          -1 * A 0 1 *
            (A 1 0 * A 2 2 * A 3 3 - A 1 0 * A 2 3 * A 3 2 - A 1 2 * A 2 0 * A 3 3 + A 1 2 * A 2 3 * A 3 0 +
                A 1 3 * A 2 0 * A 3 2 -
              A 1 3 * A 2 2 * A 3 0) +
        1 * A 0 2 *
          (A 1 0 * A 2 1 * A 3 3 - A 1 0 * A 2 3 * A 3 1 - A 1 1 * A 2 0 * A 3 3 + A 1 1 * A 2 3 * A 3 0 +
              A 1 3 * A 2 0 * A 3 1 -
            A 1 3 * A 2 1 * A 3 0) +
      -1 * A 0 3 *
        (A 1 0 * A 2 1 * A 3 2 - A 1 0 * A 2 2 * A 3 1 - A 1 1 * A 2 0 * A 3 2 + A 1 1 * A 2 2 * A 3 0 +
            A 1 2 * A 2 0 * A 3 1 -
          A 1 2 * A 2 1 * A 3 0) =
    A 0 0 * A 1 1 * A 2 2 * A 3 3 - A 0 0 * A 1 1 * A 2 3 * A 3 2 - A 0 0 * A 1 2 * A 2 1 * A 3 3 +
                                              A 0 0 * A 1 2 * A 2 3 * A 3 1 +
                                            A 0 0 * A 1 3 * A 2 1 * A 3 2 -
                                          A 0 0 * A 1 3 * A 2 2 * A 3 1 -
                                        A 0 1 * A 1 0 * A 2 2 * A 3 3 +
                                      A 0 1 * A 1 0 * A 2 3 * A 3 2 +
                                    A 0 1 * A 1 2 * A 2 0 * A 3 3 -
                                  A 0 1 * A 1 2 * A 2 3 * A 3 0 -
                                A 0 1 * A 1 3 * A 2 0 * A 3 2 +
                              A 0 1 * A 1 3 * A 2 2 * A 3 0 +
                            A 0 2 * A 1 0 * A 2 1 * A 3 3 -
                          A 0 2 * A 1 0 * A 2 3 * A 3 1 -
                        A 0 2 * A 1 1 * A 2 0 * A 3 3 +
                      A 0 2 * A 1 1 * A 2 3 * A 3 0 +
                    A 0 2 * A 1 3 * A 2 0 * A 3 1 -
                  A 0 2 * A 1 3 * A 2 1 * A 3 0 -
                A 0 3 * A 1 0 * A 2 1 * A 3 2 +
              A 0 3 * A 1 0 * A 2 2 * A 3 1 +
            A 0 3 * A 1 1 * A 2 0 * A 3 2 -
          A 0 3 * A 1 1 * A 2 2 * A 3 0 -
        A 0 3 * A 1 2 * A 2 0 * A 3 1 +
      A 0 3 * A 1 2 * A 2 1 * A 3 0
Tactic:
ring
Proof state after:
no goals
Theorem: Matrix.det_fin_four
Proof state before:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
h10 : Fin.succAbove 1 0 = 0
h11 : Fin.succAbove 1 1 = 2
h12 : Fin.succAbove 1 2 = 3
h20 : Fin.succAbove 2 0 = 0
h21 : Fin.succAbove 2 1 = 1
h22 : Fin.succAbove 2 2 = 3
h30 : Fin.succAbove 3 0 = 0
h31 : Fin.succAbove 3 1 = 1
h32 : Fin.succAbove 3 2 = 2
s0 : Fin.succ 0 = 1
s1 : Fin.succ 1 = 2
s2 : Fin.succ 2 = 3
⊢ Even ↑0
Tactic:
decide
Proof state after:
no goals
Theorem: Matrix.det_fin_four
Proof state before:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
h10 : Fin.succAbove 1 0 = 0
h11 : Fin.succAbove 1 1 = 2
h12 : Fin.succAbove 1 2 = 3
h20 : Fin.succAbove 2 0 = 0
h21 : Fin.succAbove 2 1 = 1
h22 : Fin.succAbove 2 2 = 3
h30 : Fin.succAbove 3 0 = 0
h31 : Fin.succAbove 3 1 = 1
h32 : Fin.succAbove 3 2 = 2
s0 : Fin.succ 0 = 1
s1 : Fin.succ 1 = 2
s2 : Fin.succ 2 = 3
a0 : (-1) ^ ↑0 = 1
⊢ Odd ↑1
Tactic:
decide
Proof state after:
no goals
Theorem: Matrix.det_fin_four
Proof state before:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
h10 : Fin.succAbove 1 0 = 0
h11 : Fin.succAbove 1 1 = 2
h12 : Fin.succAbove 1 2 = 3
h20 : Fin.succAbove 2 0 = 0
h21 : Fin.succAbove 2 1 = 1
h22 : Fin.succAbove 2 2 = 3
h30 : Fin.succAbove 3 0 = 0
h31 : Fin.succAbove 3 1 = 1
h32 : Fin.succAbove 3 2 = 2
s0 : Fin.succ 0 = 1
s1 : Fin.succ 1 = 2
s2 : Fin.succ 2 = 3
a0 : (-1) ^ ↑0 = 1
a1 : (-1) ^ ↑1 = -1
⊢ Even ↑2
Tactic:
decide
Proof state after:
no goals
Theorem: Matrix.det_fin_four
Proof state before:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
h10 : Fin.succAbove 1 0 = 0
h11 : Fin.succAbove 1 1 = 2
h12 : Fin.succAbove 1 2 = 3
h20 : Fin.succAbove 2 0 = 0
h21 : Fin.succAbove 2 1 = 1
h22 : Fin.succAbove 2 2 = 3
h30 : Fin.succAbove 3 0 = 0
h31 : Fin.succAbove 3 1 = 1
h32 : Fin.succAbove 3 2 = 2
s0 : Fin.succ 0 = 1
s1 : Fin.succ 1 = 2
s2 : Fin.succ 2 = 3
a0 : (-1) ^ ↑0 = 1
a1 : (-1) ^ ↑1 = -1
a2 : (-1) ^ ↑2 = 1
⊢ Odd ↑3
Tactic:
decide
Proof state after:
no goals
Theorem: MatrixCookbook.eq_487
Proof state before:
ι : Type ?u.263
R : Type u_2
l : Type ?u.269
m : Type u_1
n✝ : Type ?u.275
p : Type ?u.278
q : Type ?u.281
r : Type ?u.284
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n✝
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n✝
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
X : Matrix m m R
n : ℕ
hx : (X - 1).det ≠ 0
⊢ (X ^ n - 1) * (X - 1)⁻¹ = ∑ i ∈ Finset.range n, X ^ i
Tactic:
rw [← geom_sum_mul X n, mul_nonsing_inv_cancel_right _ _ hx.isUnit]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_494
Proof state before:
ι : Type ?u.2962
R : Type ?u.2965
l : Type ?u.2968
m : Type ?u.2971
n : Type u_1
p : Type ?u.2977
q : Type ?u.2980
r : Type ?u.2983
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix n n ℝ
⊢ exp ℝ A = ∑' (n_1 : ℕ), (↑n_1 !)⁻¹ • A ^ n_1
Tactic:
rw [exp_eq_tsum]
Proof state after:
no goals