[GOAL]
⊢ |exp 1 - 2244083 / 825552| ≤ 1 / 10 ^ 10
[PROOFSTEP]
apply exp_approx_start
[GOAL]
case h
⊢ |exp 1 - expNear 0 1 (2244083 / 825552)| ≤ |1| ^ 0 / ↑(Nat.factorial 0) * (1 / 10 ^ 10)
[PROOFSTEP]
iterate 13 refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
case h
⊢ |exp 1 - expNear 0 1 (2244083 / 825552)| ≤ |1| ^ 0 / ↑(Nat.factorial 0) * (1 / 10 ^ 10)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 0 + 1 = ?m.664
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 1 = ?m.664
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑1 = ?m.675
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 1 1 ((2244083 / 825552 - 1) * 1)| ≤ |1| ^ 1 / ↑(Nat.factorial 1) * (1 / 10 ^ 10 * 1)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 1 + 1 = ?m.1007
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 2 = ?m.1007
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑2 = ?m.1009
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 2 1 (((2244083 / 825552 - 1) * 1 - 1) * 2)| ≤ |1| ^ 2 / ↑(Nat.factorial 2) * (1 / 10 ^ 10 * 1 * 2)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 2 + 1 = ?m.1077
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 3 = ?m.1077
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑3 = ?m.1079
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 3 1 ((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3)| ≤
    |1| ^ 3 / ↑(Nat.factorial 3) * (1 / 10 ^ 10 * 1 * 2 * 3)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 3 + 1 = ?m.1147
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 4 = ?m.1147
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑4 = ?m.1149
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 4 1 (((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4)| ≤
    |1| ^ 4 / ↑(Nat.factorial 4) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 4 + 1 = ?m.1217
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 5 = ?m.1217
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑5 = ?m.1219
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 5 1 ((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5)| ≤
    |1| ^ 5 / ↑(Nat.factorial 5) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 5 + 1 = ?m.1287
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 6 = ?m.1287
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑6 = ?m.1289
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 6 1 (((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6)| ≤
    |1| ^ 6 / ↑(Nat.factorial 6) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 6 + 1 = ?m.1357
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 7 = ?m.1357
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑7 = ?m.1359
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 7 1 ((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7)| ≤
    |1| ^ 7 / ↑(Nat.factorial 7) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 7 + 1 = ?m.1427
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 8 = ?m.1427
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑8 = ?m.1429
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 8 1
          (((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8)| ≤
    |1| ^ 8 / ↑(Nat.factorial 8) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 8 + 1 = ?m.1497
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 9 = ?m.1497
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑9 = ?m.1499
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 9 1
          ((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) *
            9)| ≤
    |1| ^ 9 / ↑(Nat.factorial 9) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 9 + 1 = ?m.1567
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 10 = ?m.1567
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑10 = ?m.1569
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 10 1
          (((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) * 9 -
              1) *
            10)| ≤
    |1| ^ 10 / ↑(Nat.factorial 10) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 10 + 1 = ?m.1637
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 11 = ?m.1637
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑11 = ?m.1639
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 11 1
          ((((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) *
                    9 -
                  1) *
                10 -
              1) *
            11)| ≤
    |1| ^ 11 / ↑(Nat.factorial 11) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 11 + 1 = ?m.1707
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 12 = ?m.1707
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑12 = ?m.1709
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 12 1
          (((((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) *
                        9 -
                      1) *
                    10 -
                  1) *
                11 -
              1) *
            12)| ≤
    |1| ^ 12 / ↑(Nat.factorial 12) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 12 + 1 = ?m.1777
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 13 = ?m.1777
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑13 = ?m.1779
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 13 1
          ((((((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) *
                            9 -
                          1) *
                        10 -
                      1) *
                    11 -
                  1) *
                12 -
              1) *
            13)| ≤
    |1| ^ 13 / ↑(Nat.factorial 13) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13)
[PROOFSTEP]
norm_num1
[GOAL]
case h
⊢ |exp 1 - expNear 13 1 (5 / 7)| ≤ |1| ^ 13 / ↑(Nat.factorial 13) * (243243 / 390625)
[PROOFSTEP]
refine' exp_approx_end' _ (by norm_num1; rfl) _ (by norm_cast) (by simp) _
[GOAL]
⊢ 13 + 1 = ?m.2354
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 14 = ?m.2354
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑14 = ?m.2356
[PROOFSTEP]
norm_cast
[GOAL]
⊢ |1| ≤ 1
[PROOFSTEP]
simp
[GOAL]
case h
⊢ |1 - 5 / 7| ≤ 243243 / 390625 - |1| / 14 * ((14 + 1) / 14)
[PROOFSTEP]
rw [_root_.abs_one, abs_of_pos]
[GOAL]
case h
⊢ 1 - 5 / 7 ≤ 243243 / 390625 - 1 / 14 * ((14 + 1) / 14)
[PROOFSTEP]
norm_num1
[GOAL]
case h
⊢ 0 < 1 - 5 / 7
[PROOFSTEP]
norm_num1
[GOAL]
⊢ |exp 1 - 363916618873 / 133877442384| ≤ 1 / 10 ^ 20
[PROOFSTEP]
apply exp_approx_start
[GOAL]
case h
⊢ |exp 1 - expNear 0 1 (363916618873 / 133877442384)| ≤ |1| ^ 0 / ↑(Nat.factorial 0) * (1 / 10 ^ 20)
[PROOFSTEP]
iterate 21 refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
case h
⊢ |exp 1 - expNear 0 1 (363916618873 / 133877442384)| ≤ |1| ^ 0 / ↑(Nat.factorial 0) * (1 / 10 ^ 20)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 0 + 1 = ?m.3624
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 1 = ?m.3624
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑1 = ?m.3635
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 1 1 ((363916618873 / 133877442384 - 1) * 1)| ≤ |1| ^ 1 / ↑(Nat.factorial 1) * (1 / 10 ^ 20 * 1)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 1 + 1 = ?m.3967
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 2 = ?m.3967
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑2 = ?m.3969
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 2 1 (((363916618873 / 133877442384 - 1) * 1 - 1) * 2)| ≤
    |1| ^ 2 / ↑(Nat.factorial 2) * (1 / 10 ^ 20 * 1 * 2)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 2 + 1 = ?m.4037
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 3 = ?m.4037
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑3 = ?m.4039
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 3 1 ((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3)| ≤
    |1| ^ 3 / ↑(Nat.factorial 3) * (1 / 10 ^ 20 * 1 * 2 * 3)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 3 + 1 = ?m.4107
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 4 = ?m.4107
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑4 = ?m.4109
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 4 1 (((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4)| ≤
    |1| ^ 4 / ↑(Nat.factorial 4) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 4 + 1 = ?m.4177
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 5 = ?m.4177
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑5 = ?m.4179
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 5 1 ((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5)| ≤
    |1| ^ 5 / ↑(Nat.factorial 5) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 5 + 1 = ?m.4247
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 6 = ?m.4247
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑6 = ?m.4249
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 6 1 (((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6)| ≤
    |1| ^ 6 / ↑(Nat.factorial 6) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 6 + 1 = ?m.4317
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 7 = ?m.4317
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑7 = ?m.4319
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 7 1
          ((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7)| ≤
    |1| ^ 7 / ↑(Nat.factorial 7) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 7 + 1 = ?m.4387
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 8 = ?m.4387
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑8 = ?m.4389
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 8 1
          (((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) *
            8)| ≤
    |1| ^ 8 / ↑(Nat.factorial 8) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 8 + 1 = ?m.4457
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 9 = ?m.4457
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑9 = ?m.4459
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 9 1
          ((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) *
                8 -
              1) *
            9)| ≤
    |1| ^ 9 / ↑(Nat.factorial 9) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 9 + 1 = ?m.4527
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 10 = ?m.4527
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑10 = ?m.4529
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 10 1
          (((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) *
                    8 -
                  1) *
                9 -
              1) *
            10)| ≤
    |1| ^ 10 / ↑(Nat.factorial 10) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 10 + 1 = ?m.4597
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 11 = ?m.4597
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑11 = ?m.4599
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 11 1
          ((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) *
                        8 -
                      1) *
                    9 -
                  1) *
                10 -
              1) *
            11)| ≤
    |1| ^ 11 / ↑(Nat.factorial 11) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 11 + 1 = ?m.4667
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 12 = ?m.4667
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑12 = ?m.4669
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 12 1
          (((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) *
                            8 -
                          1) *
                        9 -
                      1) *
                    10 -
                  1) *
                11 -
              1) *
            12)| ≤
    |1| ^ 12 / ↑(Nat.factorial 12) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 12 + 1 = ?m.4737
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 13 = ?m.4737
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑13 = ?m.4739
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 13 1
          ((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 -
                                  1) *
                                8 -
                              1) *
                            9 -
                          1) *
                        10 -
                      1) *
                    11 -
                  1) *
                12 -
              1) *
            13)| ≤
    |1| ^ 13 / ↑(Nat.factorial 13) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 13 + 1 = ?m.4807
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 14 = ?m.4807
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑14 = ?m.4809
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 14 1
          (((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 -
                                      1) *
                                    8 -
                                  1) *
                                9 -
                              1) *
                            10 -
                          1) *
                        11 -
                      1) *
                    12 -
                  1) *
                13 -
              1) *
            14)| ≤
    |1| ^ 14 / ↑(Nat.factorial 14) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 14 + 1 = ?m.4877
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 15 = ?m.4877
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑15 = ?m.4879
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 15 1
          ((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 -
                                          1) *
                                        8 -
                                      1) *
                                    9 -
                                  1) *
                                10 -
                              1) *
                            11 -
                          1) *
                        12 -
                      1) *
                    13 -
                  1) *
                14 -
              1) *
            15)| ≤
    |1| ^ 15 / ↑(Nat.factorial 15) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 15 + 1 = ?m.4947
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 16 = ?m.4947
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑16 = ?m.4949
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 16 1
          (((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 -
                                              1) *
                                            8 -
                                          1) *
                                        9 -
                                      1) *
                                    10 -
                                  1) *
                                11 -
                              1) *
                            12 -
                          1) *
                        13 -
                      1) *
                    14 -
                  1) *
                15 -
              1) *
            16)| ≤
    |1| ^ 16 / ↑(Nat.factorial 16) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 16 + 1 = ?m.5017
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 17 = ?m.5017
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑17 = ?m.5019
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 17 1
          ((((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 -
                                                  1) *
                                                8 -
                                              1) *
                                            9 -
                                          1) *
                                        10 -
                                      1) *
                                    11 -
                                  1) *
                                12 -
                              1) *
                            13 -
                          1) *
                        14 -
                      1) *
                    15 -
                  1) *
                16 -
              1) *
            17)| ≤
    |1| ^ 17 / ↑(Nat.factorial 17) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 17 + 1 = ?m.5087
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 18 = ?m.5087
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑18 = ?m.5089
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 18 1
          (((((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) *
                                                        7 -
                                                      1) *
                                                    8 -
                                                  1) *
                                                9 -
                                              1) *
                                            10 -
                                          1) *
                                        11 -
                                      1) *
                                    12 -
                                  1) *
                                13 -
                              1) *
                            14 -
                          1) *
                        15 -
                      1) *
                    16 -
                  1) *
                17 -
              1) *
            18)| ≤
    |1| ^ 18 / ↑(Nat.factorial 18) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 * 18)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 18 + 1 = ?m.5157
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 19 = ?m.5157
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑19 = ?m.5159
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 19 1
          ((((((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) *
                                                            7 -
                                                          1) *
                                                        8 -
                                                      1) *
                                                    9 -
                                                  1) *
                                                10 -
                                              1) *
                                            11 -
                                          1) *
                                        12 -
                                      1) *
                                    13 -
                                  1) *
                                14 -
                              1) *
                            15 -
                          1) *
                        16 -
                      1) *
                    17 -
                  1) *
                18 -
              1) *
            19)| ≤
    |1| ^ 19 / ↑(Nat.factorial 19) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 * 18 * 19)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 19 + 1 = ?m.5227
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 20 = ?m.5227
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑20 = ?m.5229
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 20 1
          (((((((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) *
                                                                7 -
                                                              1) *
                                                            8 -
                                                          1) *
                                                        9 -
                                                      1) *
                                                    10 -
                                                  1) *
                                                11 -
                                              1) *
                                            12 -
                                          1) *
                                        13 -
                                      1) *
                                    14 -
                                  1) *
                                15 -
                              1) *
                            16 -
                          1) *
                        17 -
                      1) *
                    18 -
                  1) *
                19 -
              1) *
            20)| ≤
    |1| ^ 20 / ↑(Nat.factorial 20) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 * 18 * 19 * 20)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 20 + 1 = ?m.5297
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 21 = ?m.5297
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑21 = ?m.5299
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 21 1
          ((((((((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) *
                                                                    7 -
                                                                  1) *
                                                                8 -
                                                              1) *
                                                            9 -
                                                          1) *
                                                        10 -
                                                      1) *
                                                    11 -
                                                  1) *
                                                12 -
                                              1) *
                                            13 -
                                          1) *
                                        14 -
                                      1) *
                                    15 -
                                  1) *
                                16 -
                              1) *
                            17 -
                          1) *
                        18 -
                      1) *
                    19 -
                  1) *
                20 -
              1) *
            21)| ≤
    |1| ^ 21 / ↑(Nat.factorial 21) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 * 18 * 19 * 20 * 21)
[PROOFSTEP]
norm_num1
[GOAL]
case h
⊢ |exp 1 - expNear 21 1 (36295539 / 44271641)| ≤ |1| ^ 21 / ↑(Nat.factorial 21) * (311834363841 / 610351562500)
[PROOFSTEP]
refine' exp_approx_end' _ (by norm_num1; rfl) _ (by norm_cast) (by simp) _
[GOAL]
⊢ 21 + 1 = ?m.5994
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 22 = ?m.5994
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑22 = ?m.5996
[PROOFSTEP]
norm_cast
[GOAL]
⊢ |1| ≤ 1
[PROOFSTEP]
simp
[GOAL]
case h
⊢ |1 - 36295539 / 44271641| ≤ 311834363841 / 610351562500 - |1| / 22 * ((22 + 1) / 22)
[PROOFSTEP]
rw [_root_.abs_one, abs_of_pos]
[GOAL]
case h
⊢ 1 - 36295539 / 44271641 ≤ 311834363841 / 610351562500 - 1 / 22 * ((22 + 1) / 22)
[PROOFSTEP]
norm_num1
[GOAL]
case h
⊢ 0 < 1 - 36295539 / 44271641
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 2.7182818283 < 2244083 / 825552 - 1 / 10 ^ 10
[PROOFSTEP]
norm_num
[GOAL]
⊢ 1 / 10 ^ 10 + 2244083 / 825552 < 2.7182818286
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0.36787944116 < exp (-1)
[PROOFSTEP]
rw [exp_neg, lt_inv _ (exp_pos _)]
[GOAL]
⊢ exp 1 < 0.36787944116⁻¹
⊢ 0 < 0.36787944116
[PROOFSTEP]
refine' lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 exp_one_near_10).1) _
[GOAL]
⊢ 1 / 10 ^ 10 + 2244083 / 825552 < 0.36787944116⁻¹
⊢ 0 < 0.36787944116
[PROOFSTEP]
all_goals norm_num
[GOAL]
⊢ 1 / 10 ^ 10 + 2244083 / 825552 < 0.36787944116⁻¹
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0 < 0.36787944116
[PROOFSTEP]
norm_num
[GOAL]
⊢ exp (-1) < 0.3678794412
[PROOFSTEP]
rw [exp_neg, inv_lt (exp_pos _)]
[GOAL]
⊢ 0.3678794412⁻¹ < exp 1
⊢ 0 < 0.3678794412
[PROOFSTEP]
refine' lt_of_lt_of_le _ (sub_le_comm.1 (abs_sub_le_iff.1 exp_one_near_10).2)
[GOAL]
⊢ 0.3678794412⁻¹ < 2244083 / 825552 - 1 / 10 ^ 10
⊢ 0 < 0.3678794412
[PROOFSTEP]
all_goals norm_num
[GOAL]
⊢ 0.3678794412⁻¹ < 2244083 / 825552 - 1 / 10 ^ 10
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0 < 0.3678794412
[PROOFSTEP]
norm_num
[GOAL]
⊢ |log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10
[PROOFSTEP]
suffices |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
  by
  norm_num1 at *
  assumption
[GOAL]
this : |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
⊢ |log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10
[PROOFSTEP]
norm_num1 at *
[GOAL]
this : |log 2 - 287209 / 414355| ≤ 1 / 10000000000
⊢ |log 2 - 287209 / 414355| ≤ 1 / 10000000000
[PROOFSTEP]
assumption
[GOAL]
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
[PROOFSTEP]
have t : |(2⁻¹ : ℝ)| = 2⁻¹ := by rw [abs_of_pos]; norm_num
[GOAL]
⊢ |2⁻¹| = 2⁻¹
[PROOFSTEP]
rw [abs_of_pos]
[GOAL]
⊢ 0 < 2⁻¹
[PROOFSTEP]
norm_num
[GOAL]
t : |2⁻¹| = 2⁻¹
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
[PROOFSTEP]
have z := Real.abs_log_sub_add_sum_range_le (show |(2⁻¹ : ℝ)| < 1 by rw [t]; norm_num) 34
[GOAL]
t : |2⁻¹| = 2⁻¹
⊢ |2⁻¹| < 1
[PROOFSTEP]
rw [t]
[GOAL]
t : |2⁻¹| = 2⁻¹
⊢ 2⁻¹ < 1
[PROOFSTEP]
norm_num
[GOAL]
t : |2⁻¹| = 2⁻¹
z : |(Finset.sum (range 34) fun i => 2⁻¹ ^ (i + 1) / (↑i + 1)) + log (1 - 2⁻¹)| ≤ |2⁻¹| ^ (34 + 1) / (1 - |2⁻¹|)
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
[PROOFSTEP]
rw [t] at z
[GOAL]
t : |2⁻¹| = 2⁻¹
z : |(Finset.sum (range 34) fun i => 2⁻¹ ^ (i + 1) / (↑i + 1)) + log (1 - 2⁻¹)| ≤ 2⁻¹ ^ (34 + 1) / (1 - 2⁻¹)
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
[PROOFSTEP]
norm_num1 at z
[GOAL]
t : |2⁻¹| = 2⁻¹
z : |(Finset.sum (range 34) fun x => (1 / 2) ^ (x + 1) / (↑x + 1)) + log (1 / 2)| ≤ 1 / 17179869184
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
[PROOFSTEP]
rw [one_div (2 : ℝ), log_inv, ← sub_eq_add_neg, _root_.abs_sub_comm] at z
[GOAL]
t : |2⁻¹| = 2⁻¹
z : |log 2 - Finset.sum (range 34) fun x => 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
[PROOFSTEP]
apply le_trans (_root_.abs_sub_le _ _ _) (add_le_add z _)
[GOAL]
t : |2⁻¹| = 2⁻¹
z : |log 2 - Finset.sum (range 34) fun x => 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ |(Finset.sum (range 34) fun x => 2⁻¹ ^ (x + 1) / (↑x + 1)) - 287209 / 414355| ≤ 1 / 10 ^ 10 - 1 / 2 ^ 34
[PROOFSTEP]
simp_rw [sum_range_succ]
[GOAL]
t : |2⁻¹| = 2⁻¹
z : |log 2 - Finset.sum (range 34) fun x => 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ |(Finset.sum (range 0) fun x => 2⁻¹ ^ (x + 1) / (↑x + 1)) + 2⁻¹ ^ (0 + 1) / (↑0 + 1) + 2⁻¹ ^ (1 + 1) / (↑1 + 1) +
                                                                        2⁻¹ ^ (2 + 1) / (↑2 + 1) +
                                                                      2⁻¹ ^ (3 + 1) / (↑3 + 1) +
                                                                    2⁻¹ ^ (4 + 1) / (↑4 + 1) +
                                                                  2⁻¹ ^ (5 + 1) / (↑5 + 1) +
                                                                2⁻¹ ^ (6 + 1) / (↑6 + 1) +
                                                              2⁻¹ ^ (7 + 1) / (↑7 + 1) +
                                                            2⁻¹ ^ (8 + 1) / (↑8 + 1) +
                                                          2⁻¹ ^ (9 + 1) / (↑9 + 1) +
                                                        2⁻¹ ^ (10 + 1) / (↑10 + 1) +
                                                      2⁻¹ ^ (11 + 1) / (↑11 + 1) +
                                                    2⁻¹ ^ (12 + 1) / (↑12 + 1) +
                                                  2⁻¹ ^ (13 + 1) / (↑13 + 1) +
                                                2⁻¹ ^ (14 + 1) / (↑14 + 1) +
                                              2⁻¹ ^ (15 + 1) / (↑15 + 1) +
                                            2⁻¹ ^ (16 + 1) / (↑16 + 1) +
                                          2⁻¹ ^ (17 + 1) / (↑17 + 1) +
                                        2⁻¹ ^ (18 + 1) / (↑18 + 1) +
                                      2⁻¹ ^ (19 + 1) / (↑19 + 1) +
                                    2⁻¹ ^ (20 + 1) / (↑20 + 1) +
                                  2⁻¹ ^ (21 + 1) / (↑21 + 1) +
                                2⁻¹ ^ (22 + 1) / (↑22 + 1) +
                              2⁻¹ ^ (23 + 1) / (↑23 + 1) +
                            2⁻¹ ^ (24 + 1) / (↑24 + 1) +
                          2⁻¹ ^ (25 + 1) / (↑25 + 1) +
                        2⁻¹ ^ (26 + 1) / (↑26 + 1) +
                      2⁻¹ ^ (27 + 1) / (↑27 + 1) +
                    2⁻¹ ^ (28 + 1) / (↑28 + 1) +
                  2⁻¹ ^ (29 + 1) / (↑29 + 1) +
                2⁻¹ ^ (30 + 1) / (↑30 + 1) +
              2⁻¹ ^ (31 + 1) / (↑31 + 1) +
            2⁻¹ ^ (32 + 1) / (↑32 + 1) +
          2⁻¹ ^ (33 + 1) / (↑33 + 1) -
        287209 / 414355| ≤
    1 / 10 ^ 10 - 1 / 2 ^ 34
[PROOFSTEP]
norm_num
[GOAL]
t : |2⁻¹| = 2⁻¹
z : |log 2 - Finset.sum (range 34) fun x => 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ |30417026706710207 / 51397301678363663775930777600| ≤ 7011591 / 167772160000000000
[PROOFSTEP]
rw [abs_of_pos]
[GOAL]
t : |2⁻¹| = 2⁻¹
z : |log 2 - Finset.sum (range 34) fun x => 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ 30417026706710207 / 51397301678363663775930777600 ≤ 7011591 / 167772160000000000
[PROOFSTEP]
norm_num
[GOAL]
t : |2⁻¹| = 2⁻¹
z : |log 2 - Finset.sum (range 34) fun x => 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ 0 < 30417026706710207 / 51397301678363663775930777600
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0.6931471803 < 287209 / 414355 - 1 / 10 ^ 10
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 1 / 10 ^ 10 + 287209 / 414355 < 0.6931471808
[PROOFSTEP]
norm_num


[GOAL]
z w : ℂ
⊢ z < w ↔ z ≤ w ∧ ¬w ≤ z
[PROOFSTEP]
dsimp
[GOAL]
z w : ℂ
⊢ z.re < w.re ∧ z.im = w.im ↔ (z.re ≤ w.re ∧ z.im = w.im) ∧ ¬(w.re ≤ z.re ∧ w.im = z.im)
[PROOFSTEP]
rw [lt_iff_le_not_le]
[GOAL]
z w : ℂ
⊢ (z.re ≤ w.re ∧ ¬w.re ≤ z.re) ∧ z.im = w.im ↔ (z.re ≤ w.re ∧ z.im = w.im) ∧ ¬(w.re ≤ z.re ∧ w.im = z.im)
[PROOFSTEP]
tauto
[GOAL]
x y : ℝ
⊢ ↑x ≤ ↑y ↔ x ≤ y
[PROOFSTEP]
simp [le_def, ofReal']
[GOAL]
x y : ℝ
⊢ ↑x < ↑y ↔ x < y
[PROOFSTEP]
simp [lt_def, ofReal']
[GOAL]
z w : ℂ
⊢ ¬z ≤ w ↔ w.re < z.re ∨ z.im ≠ w.im
[PROOFSTEP]
rw [le_def, not_and_or, not_le]
[GOAL]
z w : ℂ
⊢ ¬z < w ↔ w.re ≤ z.re ∨ z.im ≠ w.im
[PROOFSTEP]
rw [lt_def, not_and_or, not_lt]
[GOAL]
r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ z = ↑z.re
[PROOFSTEP]
ext
[GOAL]
case a
r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ z.re = (↑z.re).re
case a r : ℝ z : ℂ hz : ↑r ≤ z ⊢ z.im = (↑z.re).im
[PROOFSTEP]
rfl
[GOAL]
case a
r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ z.im = (↑z.re).im
[PROOFSTEP]
simp only [← (Complex.le_def.1 hz).2, Complex.zero_im, Complex.ofReal_im]


[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ _root_.Disjoint (map Embedding.inl s) (map Embedding.inr t)
[PROOFSTEP]
simp_rw [disjoint_left, mem_map]
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ ∀ ⦃a : α ⊕ β⦄, (∃ a_1, a_1 ∈ s ∧ ↑Embedding.inl a_1 = a) → ¬∃ a_2, a_2 ∈ t ∧ ↑Embedding.inr a_2 = a
[PROOFSTEP]
rintro x ⟨a, _, rfl⟩ ⟨b, _, ⟨⟩⟩


[GOAL]
as bs : List Char
⊢ length ({ data := as } ++ { data := bs }) = length { data := as } + length { data := bs }
[PROOFSTEP]
rw [congr_append]
[GOAL]
as bs : List Char
⊢ length { data := { data := as }.data ++ { data := bs }.data } = length { data := as } + length { data := bs }
[PROOFSTEP]
simp only [String.length]
[GOAL]
as bs : List Char
⊢ List.length (as ++ bs) = List.length as + List.length bs
[PROOFSTEP]
exact List.length_append as bs
[GOAL]
n : ℕ
c : Char
⊢ length (replicate n c) = n
[PROOFSTEP]
simp only [String.length, String.replicate, List.length_replicate]
[GOAL]
l : List Char
⊢ length { data := l } = List.length l
[PROOFSTEP]
simp only [String.length]
[GOAL]
n : ℕ
c : Char
s : List Char
⊢ length (leftpad n c { data := s }) = max n (length { data := s })
[PROOFSTEP]
simp only [leftpad, String.length, List.leftpad_length]
[GOAL]
n : ℕ
c : Char
l : List Char
⊢ isPrefix (replicate (n - length { data := l }) c) (leftpad n c { data := l })
[PROOFSTEP]
simp only [isPrefix, replicate, leftpad, String.length, List.leftpad_prefix]
[GOAL]
n : ℕ
c : Char
l : List Char
⊢ isSuffix { data := l } (leftpad n c { data := l })
[PROOFSTEP]
simp only [isSuffix, replicate, leftpad, String.length, List.leftpad_suffix]


[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
v : n' → α
B : Fin m → n' → α
i : Fin (Nat.succ m)
j : n'
⊢ vecCons v B i j = vecCons (v j) (fun i => B i j) i
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case refine'_1
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
v : n' → α
B : Fin m → n' → α
i : Fin (Nat.succ m)
j : n'
⊢ vecCons v B 0 j = vecCons (v j) (fun i => B i j) 0
[PROOFSTEP]
simp
[GOAL]
case refine'_2
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
v : n' → α
B : Fin m → n' → α
i : Fin (Nat.succ m)
j : n'
⊢ ∀ (i : Fin m), vecCons v B (Fin.succ i) j = vecCons (v j) (fun i => B i j) (Fin.succ i)
[PROOFSTEP]
simp
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
B : Fin (Nat.succ m) → n' → α
j : n'
⊢ (vecTail fun i => B i j) = fun i => vecTail B i j
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
B : Fin (Nat.succ m) → n' → α
j : n'
x✝ : Fin m
⊢ vecTail (fun i => B i j) x✝ = vecTail B x✝ j
[PROOFSTEP]
simp [vecTail]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
⊢ vecCons x v ⬝ᵥ w = x * vecHead w + v ⬝ᵥ vecTail w
[PROOFSTEP]
simp [dotProduct, Fin.sum_univ_succ, vecHead, vecTail]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
v : Fin (Nat.succ n) → α
x : α
w : Fin n → α
⊢ v ⬝ᵥ vecCons x w = vecHead v * x + vecTail v ⬝ᵥ w
[PROOFSTEP]
simp [dotProduct, Fin.sum_univ_succ, vecHead, vecTail]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
x : α
v : Fin n → α
y : α
w : Fin n → α
⊢ vecCons x v ⬝ᵥ vecCons y w = x * y + v ⬝ᵥ w
[PROOFSTEP]
simp
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
x : α
u : Fin m → α
⊢ col (vecCons x u) = vecCons (fun x_1 => x) (col u)
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
x : α
u : Fin m → α
i : Fin (Nat.succ m)
j : Unit
⊢ col (vecCons x u) i j = vecCons (fun x_1 => x) (col u) i j
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case a.h.refine'_1
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
x : α
u : Fin m → α
i : Fin (Nat.succ m)
j : Unit
⊢ col (vecCons x u) 0 j = vecCons (fun x_1 => x) (col u) 0 j
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
case a.h.refine'_2
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
x : α
u : Fin m → α
i : Fin (Nat.succ m)
j : Unit
⊢ ∀ (i : Fin m), col (vecCons x u) (Fin.succ i) j = vecCons (fun x_1 => x) (col u) (Fin.succ i) j
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
⊢ row ![] = fun x => ![]
[PROOFSTEP]
ext
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
i✝ : Unit
x✝ : Fin 0
⊢ row ![] i✝ x✝ = ![]
[PROOFSTEP]
rfl
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
x : α
u : Fin m → α
⊢ row (vecCons x u) = fun x_1 => vecCons x u
[PROOFSTEP]
ext
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
x : α
u : Fin m → α
i✝ : Unit
x✝ : Fin (Nat.succ m)
⊢ row (vecCons x u) i✝ x✝ = vecCons x u x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
v : n' → α
A : Matrix (Fin m) n' α
⊢ (↑of (vecCons v A))ᵀ = ↑of fun i => vecCons (v i) (Aᵀ i)
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin (Nat.succ m)
⊢ (↑of (vecCons v A))ᵀ i j = ↑of (fun i => vecCons (v i) (Aᵀ i)) i j
[PROOFSTEP]
refine' Fin.cases _ _ j
[GOAL]
case a.h.refine'_1
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin (Nat.succ m)
⊢ (↑of (vecCons v A))ᵀ i 0 = ↑of (fun i => vecCons (v i) (Aᵀ i)) i 0
[PROOFSTEP]
simp
[GOAL]
case a.h.refine'_2
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin (Nat.succ m)
⊢ ∀ (i_1 : Fin m), (↑of (vecCons v A))ᵀ i (Fin.succ i_1) = ↑of (fun i => vecCons (v i) (Aᵀ i)) i (Fin.succ i_1)
[PROOFSTEP]
simp
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix m' (Fin (Nat.succ n)) α
⊢ vecTail (↑of.symm Aᵀ) = (vecTail ∘ A)ᵀ
[PROOFSTEP]
ext i j
[GOAL]
case h.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix m' (Fin (Nat.succ n)) α
i : Fin n
j : m'
⊢ vecTail (↑of.symm Aᵀ) i j = (vecTail ∘ A)ᵀ i j
[PROOFSTEP]
rfl
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
⊢ ↑of (vecCons v A) * B = ↑of (vecCons (vecMul v B) (↑of.symm (↑of A * B)))
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin (Nat.succ m)
j : o'
⊢ (↑of (vecCons v A) * B) i j = ↑of (vecCons (vecMul v B) (↑of.symm (↑of A * B))) i j
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case a.h.refine'_1
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin (Nat.succ m)
j : o'
⊢ (↑of (vecCons v A) * B) 0 j = ↑of (vecCons (vecMul v B) (↑of.symm (↑of A * B))) 0 j
[PROOFSTEP]
rfl
[GOAL]
case a.h.refine'_2
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin (Nat.succ m)
j : o'
⊢ ∀ (i : Fin m),
    (↑of (vecCons v A) * B) (Fin.succ i) j = ↑of (vecCons (vecMul v B) (↑of.symm (↑of A * B))) (Fin.succ i) j
[PROOFSTEP]
simp [mul_val_succ]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
B : Fin (Nat.succ n) → o' → α
⊢ vecMul (vecCons x v) (↑of B) = x • vecHead B + vecMul v (↑of (vecTail B))
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
B : Fin (Nat.succ n) → o' → α
i : o'
⊢ vecMul (vecCons x v) (↑of B) i = (x • vecHead B + vecMul v (↑of (vecTail B))) i
[PROOFSTEP]
simp [vecMul]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
v : Fin (Nat.succ n) → α
w : o' → α
B : Fin n → o' → α
⊢ vecMul v (↑of (vecCons w B)) = vecHead v • w + vecMul (vecTail v) (↑of B)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
v : Fin (Nat.succ n) → α
w : o' → α
B : Fin n → o' → α
i : o'
⊢ vecMul v (↑of (vecCons w B)) i = (vecHead v • w + vecMul (vecTail v) (↑of B)) i
[PROOFSTEP]
simp [vecMul]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
w : o' → α
B : Fin n → o' → α
⊢ vecMul (vecCons x v) (↑of (vecCons w B)) = x • w + vecMul v (↑of B)
[PROOFSTEP]
simp
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
⊢ mulVec (↑of (vecCons v A)) w = vecCons (v ⬝ᵥ w) (mulVec (↑of A) w)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin (Nat.succ m)
⊢ mulVec (↑of (vecCons v A)) w i = vecCons (v ⬝ᵥ w) (mulVec (↑of A) w) i
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case h.refine'_1
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin (Nat.succ m)
⊢ mulVec (↑of (vecCons v A)) w 0 = vecCons (v ⬝ᵥ w) (mulVec (↑of A) w) 0
[PROOFSTEP]
simp [mulVec]
[GOAL]
case h.refine'_2
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin (Nat.succ m)
⊢ ∀ (i : Fin m), mulVec (↑of (vecCons v A)) w (Fin.succ i) = vecCons (v ⬝ᵥ w) (mulVec (↑of A) w) (Fin.succ i)
[PROOFSTEP]
simp [mulVec]
[GOAL]
α✝ : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α✝
α : Type u_1
inst✝ : CommSemiring α
A : m' → Fin (Nat.succ n) → α
x : α
v : Fin n → α
⊢ mulVec (↑of A) (vecCons x v) = x • vecHead ∘ A + mulVec (↑of (vecTail ∘ A)) v
[PROOFSTEP]
ext i
[GOAL]
case h
α✝ : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α✝
α : Type u_1
inst✝ : CommSemiring α
A : m' → Fin (Nat.succ n) → α
x : α
v : Fin n → α
i : m'
⊢ mulVec (↑of A) (vecCons x v) i = (x • vecHead ∘ A + mulVec (↑of (vecTail ∘ A)) v) i
[PROOFSTEP]
simp [mulVec, mul_comm]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
⊢ vecMulVec (vecCons x v) w = vecCons (x • w) (vecMulVec v w)
[PROOFSTEP]
ext i
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin (Nat.succ m)
x✝ : n'
⊢ vecMulVec (vecCons x v) w i x✝ = vecCons (x • w) (vecMulVec v w) i x✝
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case a.h.refine'_1
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin (Nat.succ m)
x✝ : n'
⊢ vecMulVec (vecCons x v) w 0 x✝ = vecCons (x • w) (vecMulVec v w) 0 x✝
[PROOFSTEP]
simp [vecMulVec]
[GOAL]
case a.h.refine'_2
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin (Nat.succ m)
x✝ : n'
⊢ ∀ (i : Fin m), vecMulVec (vecCons x v) w (Fin.succ i) x✝ = vecCons (x • w) (vecMulVec v w) (Fin.succ i) x✝
[PROOFSTEP]
simp [vecMulVec]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
v : m' → α
x : α
w : Fin n → α
⊢ vecMulVec v (vecCons x w) = fun i => v i • vecCons x w
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
v : m' → α
x : α
w : Fin n → α
i : m'
j : Fin (Nat.succ n)
⊢ vecMulVec v (vecCons x w) i j = (v i • vecCons x w) j
[PROOFSTEP]
rw [vecMulVec_apply, Pi.smul_apply, smul_eq_mul]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : n' → α
A : Fin m → n' → α
⊢ x • vecCons v A = vecCons (x • v) (x • A)
[PROOFSTEP]
ext i
[GOAL]
case h.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : n' → α
A : Fin m → n' → α
i : Fin (Nat.succ m)
x✝ : n'
⊢ (x • vecCons v A) i x✝ = vecCons (x • v) (x • A) i x✝
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case h.h.refine'_1
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : n' → α
A : Fin m → n' → α
i : Fin (Nat.succ m)
x✝ : n'
⊢ (x • vecCons v A) 0 x✝ = vecCons (x • v) (x • A) 0 x✝
[PROOFSTEP]
simp
[GOAL]
case h.h.refine'_2
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : n' → α
A : Fin m → n' → α
i : Fin (Nat.succ m)
x✝ : n'
⊢ ∀ (i : Fin m), (x • vecCons v A) (Fin.succ i) x✝ = vecCons (x • v) (x • A) (Fin.succ i) x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix m' n' α
i : m'
row : Fin m → m'
col : o' → n'
⊢ submatrix A (vecCons i row) col = vecCons (fun j => A i (col j)) (submatrix A row col)
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix m' n' α
i✝ : m'
row : Fin m → m'
col : o' → n'
i : Fin (Nat.succ m)
j : o'
⊢ submatrix A (vecCons i✝ row) col i j = vecCons (fun j => A i✝ (col j)) (submatrix A row col) i j
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case a.h.refine'_1
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix m' n' α
i✝ : m'
row : Fin m → m'
col : o' → n'
i : Fin (Nat.succ m)
j : o'
⊢ submatrix A (vecCons i✝ row) col 0 j = vecCons (fun j => A i✝ (col j)) (submatrix A row col) 0 j
[PROOFSTEP]
simp [submatrix]
[GOAL]
case a.h.refine'_2
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix m' n' α
i✝ : m'
row : Fin m → m'
col : o' → n'
i : Fin (Nat.succ m)
j : o'
⊢ ∀ (i : Fin m),
    submatrix A (vecCons i✝ row) col (Fin.succ i) j =
      vecCons (fun j => A i✝ (col j)) (submatrix A row col) (Fin.succ i) j
[PROOFSTEP]
simp [submatrix]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 = ↑of ![![1, 0], ![0, 1]]
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
i j : Fin 2
⊢ OfNat.ofNat 1 i j = ↑of ![![1, 0], ![0, 1]] i j
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
j : Fin 2
⊢ OfNat.ofNat 1 { val := 0, isLt := (_ : 0 < 2) } j = ↑of ![![1, 0], ![0, 1]] { val := 0, isLt := (_ : 0 < 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
j : Fin 2
⊢ OfNat.ofNat 1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } j =
    ↑of ![![1, 0], ![0, 1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑of ![![1, 0], ![0, 1]] { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑of ![![1, 0], ![0, 1]] { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑of ![![1, 0], ![0, 1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑of ![![1, 0], ![0, 1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 = ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]]
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
i j : Fin 3
⊢ OfNat.ofNat 1 i j = ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] i j
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
j : Fin 3
⊢ OfNat.ofNat 1 { val := 0, isLt := (_ : 0 < 3) } j =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 0, isLt := (_ : 0 < 3) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
j : Fin 3
⊢ OfNat.ofNat 1 { val := 1, isLt := (_ : (fun a => a < 3) 1) } j =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 1, isLt := (_ : (fun a => a < 3) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
j : Fin 3
⊢ OfNat.ofNat 1 { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } j =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 0, isLt := (_ : 0 < 3) } { val := 0, isLt := (_ : 0 < 3) } =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 0, isLt := (_ : 0 < 3) } { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 0, isLt := (_ : 0 < 3) } { val := 1, isLt := (_ : (fun a => a < 3) 1) } =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 0, isLt := (_ : 0 < 3) }
      { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.head.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 0, isLt := (_ : 0 < 3) } { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 0, isLt := (_ : 0 < 3) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 0, isLt := (_ : 0 < 3) } =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 1, isLt := (_ : (fun a => a < 3) 1) }
      { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 1, isLt := (_ : (fun a => a < 3) 1) } =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 1, isLt := (_ : (fun a => a < 3) 1) }
      { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 1, isLt := (_ : (fun a => a < 3) 1) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 1, isLt := (_ : (fun a => a < 3) 1) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.tail.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } { val := 0, isLt := (_ : 0 < 3) } =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
      { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.tail.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
      { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.tail.head.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
⊢ A = ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]]
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ A i j = ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]] i j
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ A { val := 0, isLt := (_ : 0 < 2) } j = ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]] { val := 0, isLt := (_ : 0 < 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ A { val := 1, isLt := (_ : (fun a => a < 2) 1) } j =
    ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
⊢ A { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]] { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
⊢ A { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]] { val := 0, isLt := (_ : 0 < 2) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
⊢ A { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
⊢ A { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A = ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
⊢ A i j = ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]] i j
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ A { val := 0, isLt := (_ : 0 < 3) } j =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]] { val := 0, isLt := (_ : 0 < 3) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ A { val := 1, isLt := (_ : (fun a => a < 3) 1) } j =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ A { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } j =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A { val := 0, isLt := (_ : 0 < 3) } { val := 0, isLt := (_ : 0 < 3) } =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]] { val := 0, isLt := (_ : 0 < 3) }
      { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A { val := 0, isLt := (_ : 0 < 3) } { val := 1, isLt := (_ : (fun a => a < 3) 1) } =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]] { val := 0, isLt := (_ : 0 < 3) }
      { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.head.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A { val := 0, isLt := (_ : 0 < 3) } { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]] { val := 0, isLt := (_ : 0 < 3) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 0, isLt := (_ : 0 < 3) } =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 1, isLt := (_ : (fun a => a < 3) 1) } =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.tail.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } { val := 0, isLt := (_ : 0 < 3) } =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.tail.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } { val := 1, isLt := (_ : (fun a => a < 3) 1) } =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.tail.head.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ ↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] * ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]] =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]]
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
i j : Fin 2
⊢ (↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] * ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]]) i j =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]] i j
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
j : Fin 2
⊢ (↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] * ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]]) { val := 0, isLt := (_ : 0 < 2) } j =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]]
      { val := 0, isLt := (_ : 0 < 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
j : Fin 2
⊢ (↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] * ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]]) { val := 1, isLt := (_ : (fun a => a < 2) 1) } j =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]]
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ (↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] * ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]]) { val := 0, isLt := (_ : 0 < 2) }
      { val := 0, isLt := (_ : 0 < 2) } =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]]
      { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ]
[GOAL]
case a.h.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ (↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] * ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]]) { val := 0, isLt := (_ : 0 < 2) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]]
      { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ]
[GOAL]
case a.h.tail.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ (↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] * ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]]) { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 0, isLt := (_ : 0 < 2) } =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]]
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ]
[GOAL]
case a.h.tail.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ (↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] * ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]]) { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]]
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ ↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
      ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]] =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
i j : Fin 3
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      i j =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      i j
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
j : Fin 3
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 0, isLt := (_ : 0 < 3) } j =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 0, isLt := (_ : 0 < 3) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
j : Fin 3
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } j =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
j : Fin 3
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } j =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 0, isLt := (_ : 0 < 3) } { val := 0, isLt := (_ : 0 < 3) } =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 0, isLt := (_ : 0 < 3) } { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]
[GOAL]
case a.h.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 0, isLt := (_ : 0 < 3) } { val := 1, isLt := (_ : (fun a => a < 3) 1) } =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 0, isLt := (_ : 0 < 3) } { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]
[GOAL]
case a.h.head.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 0, isLt := (_ : 0 < 3) } { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 0, isLt := (_ : 0 < 3) } { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]
[GOAL]
case a.h.tail.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 0, isLt := (_ : 0 < 3) } =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]
[GOAL]
case a.h.tail.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 1, isLt := (_ : (fun a => a < 3) 1) } =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]
[GOAL]
case a.h.tail.head.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]
[GOAL]
case a.h.tail.tail.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } { val := 0, isLt := (_ : 0 < 3) } =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]
[GOAL]
case a.h.tail.tail.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } { val := 1, isLt := (_ : (fun a => a < 3) 1) } =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]
[GOAL]
case a.h.tail.tail.head.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
a₀ a₁ b₀ b₁ : α
h₀ : a₀ = b₀
h₁ : a₁ = b₁
⊢ ![a₀, a₁] = ![b₀, b₁]
[PROOFSTEP]
subst_vars
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
b₀ b₁ : α
⊢ ![b₀, b₁] = ![b₀, b₁]
[PROOFSTEP]
rfl
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
a₀ a₁ a₂ b₀ b₁ b₂ : α
h₀ : a₀ = b₀
h₁ : a₁ = b₁
h₂ : a₂ = b₂
⊢ ![a₀, a₁, a₂] = ![b₀, b₁, b₂]
[PROOFSTEP]
subst_vars
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
b₀ b₁ b₂ : α
⊢ ![b₀, b₁, b₂] = ![b₀, b₁, b₂]
[PROOFSTEP]
rfl
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : Add α
a₀ a₁ b₀ b₁ : α
⊢ ![a₀, a₁] + ![b₀, b₁] = ![a₀ + b₀, a₁ + b₁]
[PROOFSTEP]
rw [cons_add_cons, cons_add_cons, empty_add_empty]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : Add α
a₀ a₁ a₂ b₀ b₁ b₂ : α
⊢ ![a₀, a₁, a₂] + ![b₀, b₁, b₂] = ![a₀ + b₀, a₁ + b₁, a₂ + b₂]
[PROOFSTEP]
rw [cons_add_cons, cons_add_cons, cons_add_cons, empty_add_empty]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
R : Type u_1
inst✝ : SMul R α
x : R
a₀ a₁ : α
⊢ x • ![a₀, a₁] = ![x • a₀, x • a₁]
[PROOFSTEP]
rw [smul_cons, smul_cons, smul_empty]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
R : Type u_1
inst✝ : SMul R α
x : R
a₀ a₁ a₂ : α
⊢ x • ![a₀, a₁, a₂] = ![x • a₀, x • a₁, x • a₂]
[PROOFSTEP]
rw [smul_cons, smul_cons, smul_cons, smul_empty]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₀ a₁ b₀ b₁ : α
⊢ ![a₀, a₁] ⬝ᵥ ![b₀, b₁] = a₀ * b₀ + a₁ * b₁
[PROOFSTEP]
rw [cons_dotProduct_cons, cons_dotProduct_cons, dotProduct_empty, add_zero]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₀ a₁ a₂ b₀ b₁ b₂ : α
⊢ ![a₀, a₁, a₂] ⬝ᵥ ![b₀, b₁, b₂] = a₀ * b₀ + a₁ * b₁ + a₂ * b₂
[PROOFSTEP]
rw [cons_dotProduct_cons, cons_dotProduct_cons, cons_dotProduct_cons, dotProduct_empty, add_zero, add_assoc]


[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b : α
a : α × α
h : a ∈ offDiag s
⊢ ¬Sym2.IsDiag (Quotient.mk (Sym2.Rel.setoid α) a)
[PROOFSTEP]
rw [Sym2.isDiag_iff_proj_eq]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b : α
a : α × α
h : a ∈ offDiag s
⊢ ¬a.fst = a.snd
[PROOFSTEP]
exact (mem_offDiag.1 h).2.2
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ m ∈ Finset.sym2 s ↔ ∀ (a : α), a ∈ m → a ∈ s
[PROOFSTEP]
refine mem_image.trans ⟨?_, fun h ↦ ⟨m.out, mem_product.2 ⟨h _ m.out_fst_mem, h _ m.out_snd_mem⟩, m.out_eq⟩⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ (∃ a, a ∈ s ×ˢ s ∧ Quotient.mk' a = m) → ∀ (a : α), a ∈ m → a ∈ s
[PROOFSTEP]
rintro ⟨⟨a, b⟩, h, rfl⟩
[GOAL]
case intro.mk.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ a b : α
h : (a, b) ∈ s ×ˢ s
⊢ ∀ (a_1 : α), a_1 ∈ Quotient.mk' (a, b) → a_1 ∈ s
[PROOFSTEP]
rw [Quotient.mk', @Sym2.ball _ (fun x ↦ x ∈ s)]
[GOAL]
case intro.mk.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ a b : α
h : (a, b) ∈ s ×ˢ s
⊢ a ∈ s ∧ b ∈ s
[PROOFSTEP]
rwa [mem_product] at h
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ Quotient.mk (Sym2.Rel.setoid α) (a, b) ∈ Finset.sym2 s ↔ a ∈ s ∧ b ∈ s
[PROOFSTEP]
rw [mem_sym2_iff, Sym2.ball]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ Finset.sym2 s = ∅ ↔ s = ∅
[PROOFSTEP]
rw [Finset.sym2, image_eq_empty, product_eq_empty, or_self_iff]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ Finset.Nonempty (Finset.sym2 s) ↔ Finset.Nonempty s
[PROOFSTEP]
rw [Finset.sym2, Nonempty.image_iff, nonempty_product, and_self_iff]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
inst✝ : Fintype α
⊢ Finset.sym2 univ = univ
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
inst✝ : Fintype α
a✝ : Sym2 α
⊢ a✝ ∈ Finset.sym2 univ ↔ a✝ ∈ univ
[PROOFSTEP]
simp only [mem_sym2_iff, mem_univ, implies_true]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b : α
m : Sym2 α
a : α
⊢ Finset.sym2 {a} = {Sym2.diag a}
[PROOFSTEP]
rw [Finset.sym2, singleton_product_singleton, image_singleton, Sym2.diag, Quotient.mk']
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ (∀ (b : α), b ∈ Sym2.diag a → b ∈ s) ↔ a ∈ s
[PROOFSTEP]
rw [← mem_sym2_iff]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ Sym2.diag a ∈ Finset.sym2 s ↔ a ∈ s
[PROOFSTEP]
exact mk'_mem_sym2_iff.trans <| and_self_iff _
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ Sym2.diag a ∈ Finset.sym2 s ↔ a ∈ s
[PROOFSTEP]
simp [diag_mem_sym2_mem_iff]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ image Quotient.mk' (diag s) ∪ image Quotient.mk' (offDiag s) = Finset.sym2 s
[PROOFSTEP]
rw [← image_union, diag_union_offDiag]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ image Quotient.mk' (s ×ˢ s) = Finset.sym2 s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
⊢ m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
m : Sym α Nat.zero
⊢ m ∈ Finset.sym s Nat.zero ↔ ∀ (a : α), a ∈ m → a ∈ s
[PROOFSTEP]
refine' mem_singleton.trans ⟨_, fun _ ↦ Sym.eq_nil_of_card_zero _⟩
[GOAL]
case zero
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
m : Sym α Nat.zero
⊢ m = ∅ → ∀ (a : α), a ∈ m → a ∈ s
[PROOFSTEP]
rintro rfl
[GOAL]
case zero
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
⊢ ∀ (a : α), a ∈ ∅ → a ∈ s
[PROOFSTEP]
exact fun a ha ↦ (Finset.not_mem_empty _ ha).elim
[GOAL]
case succ
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
⊢ m ∈ Finset.sym s (Nat.succ n) ↔ ∀ (a : α), a ∈ m → a ∈ s
[PROOFSTEP]
refine' mem_sup.trans ⟨_, fun h ↦ _⟩
[GOAL]
case succ.refine'_1
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
⊢ (∃ v, v ∈ s ∧ m ∈ image (Sym.cons v) (Finset.sym s n)) → ∀ (a : α), a ∈ m → a ∈ s
[PROOFSTEP]
rintro ⟨a, ha, he⟩ b hb
[GOAL]
case succ.refine'_1.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
a : α
ha : a ∈ s
he : m ∈ image (Sym.cons a) (Finset.sym s n)
b : α
hb : b ∈ m
⊢ b ∈ s
[PROOFSTEP]
rw [mem_image] at he
[GOAL]
case succ.refine'_1.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
a : α
ha : a ∈ s
he : ∃ a_1, a_1 ∈ Finset.sym s n ∧ a ::ₛ a_1 = m
b : α
hb : b ∈ m
⊢ b ∈ s
[PROOFSTEP]
obtain ⟨m, he, rfl⟩ := he
[GOAL]
case succ.refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ Finset.sym s n
hb : b ∈ a ::ₛ m
⊢ b ∈ s
[PROOFSTEP]
rw [Sym.mem_cons] at hb
[GOAL]
case succ.refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ Finset.sym s n
hb : b = a ∨ b ∈ m
⊢ b ∈ s
[PROOFSTEP]
obtain rfl | hb := hb
[GOAL]
case succ.refine'_1.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
b : α
m : Sym α n
he : m ∈ Finset.sym s n
ha : b ∈ s
⊢ b ∈ s
[PROOFSTEP]
exact ha
[GOAL]
case succ.refine'_1.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ Finset.sym s n
hb : b ∈ m
⊢ b ∈ s
[PROOFSTEP]
exact ih.1 he _ hb
[GOAL]
case succ.refine'_2
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
h : ∀ (a : α), a ∈ m → a ∈ s
⊢ ∃ v, v ∈ s ∧ m ∈ image (Sym.cons v) (Finset.sym s n)
[PROOFSTEP]
obtain ⟨a, m, rfl⟩ := m.exists_eq_cons_of_succ
[GOAL]
case succ.refine'_2.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
a : α
m : Sym α n
h : ∀ (a_1 : α), a_1 ∈ a ::ₛ m → a_1 ∈ s
⊢ ∃ v, v ∈ s ∧ a ::ₛ m ∈ image (Sym.cons v) (Finset.sym s n)
[PROOFSTEP]
exact ⟨a, h _ <| Sym.mem_cons_self _ _, mem_image_of_mem _ <| ih.2 fun b hb ↦ h _ <| Sym.mem_cons_of_mem hb⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b✝ : α
n✝ : ℕ
m : Sym α n✝
ha : a ∈ s
n : ℕ
b : α
hb : b ∈ Sym.replicate n a
⊢ b ∈ s
[PROOFSTEP]
rwa [(Sym.mem_replicate.1 hb).2]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
h : Finset.sym s n = ∅
⊢ s = ∅
[PROOFSTEP]
rw [← not_nonempty_iff_eq_empty] at h ⊢
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
h : ¬Finset.Nonempty (Finset.sym s n)
⊢ ¬Finset.Nonempty s
[PROOFSTEP]
exact fun hs ↦ h (hs.sym _)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
⊢ Finset.sym s n = ∅ ↔ n ≠ 0 ∧ s = ∅
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym α Nat.zero
⊢ Finset.sym s Nat.zero = ∅ ↔ Nat.zero ≠ 0 ∧ s = ∅
[PROOFSTEP]
exact iff_of_false (singleton_ne_empty _) fun h ↦ (h.1 rfl).elim
[GOAL]
case succ
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m : Sym α (Nat.succ n✝)
⊢ Finset.sym s (Nat.succ n✝) = ∅ ↔ Nat.succ n✝ ≠ 0 ∧ s = ∅
[PROOFSTEP]
refine ⟨fun h ↦ ⟨Nat.succ_ne_zero _, eq_empty_of_sym_eq_empty h⟩, ?_⟩
[GOAL]
case succ
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m : Sym α (Nat.succ n✝)
⊢ Nat.succ n✝ ≠ 0 ∧ s = ∅ → Finset.sym s (Nat.succ n✝) = ∅
[PROOFSTEP]
rintro ⟨_, rfl⟩
[GOAL]
case succ.intro
α : Type u_1
inst✝ : DecidableEq α
t : Finset α
a b : α
n✝ : ℕ
m : Sym α (Nat.succ n✝)
left✝ : Nat.succ n✝ ≠ 0
⊢ Finset.sym ∅ (Nat.succ n✝) = ∅
[PROOFSTEP]
exact sym_empty _
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
⊢ Finset.Nonempty (Finset.sym s n) ↔ n = 0 ∨ Finset.Nonempty s
[PROOFSTEP]
simp_rw [nonempty_iff_ne_empty, Ne.def]
  -- Porting note: using simp_rw does not work here, it does nothing...
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
⊢ ¬Finset.sym s n = ∅ ↔ n = 0 ∨ ¬s = ∅
[PROOFSTEP]
rwa [sym_eq_empty, not_and_or, not_ne_iff]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a b : α
n✝ : ℕ
m : Sym α n✝
s t : Finset α
n : ℕ
⊢ Finset.sym (s ∩ t) n = Finset.sym s n ∩ Finset.sym t n
[PROOFSTEP]
ext m
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a b : α
n✝ : ℕ
m✝ : Sym α n✝
s t : Finset α
n : ℕ
m : Sym α n
⊢ m ∈ Finset.sym (s ∩ t) n ↔ m ∈ Finset.sym s n ∩ Finset.sym t n
[PROOFSTEP]
simp only [mem_inter, mem_sym_iff, imp_and, forall_and]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ (Sym.filterNe a ↑m).snd ∈ Finset.sym s (n - ↑(Sym.filterNe a ↑m).fst)
[PROOFSTEP]
convert sym_filterNe_mem a m.2
[GOAL]
case h.e'_5.h.e'_3
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ s = erase (insert a s) a
[PROOFSTEP]
rw [erase_insert h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ (fun m =>
        { fst := (Sym.filterNe a ↑m).fst,
          snd :=
            { val := (Sym.filterNe a ↑m).snd,
              property := (_ : (Sym.filterNe a ↑m).snd ∈ Finset.sym s (n - ↑(Sym.filterNe a ↑m).fst)) } })
      ((fun m =>
          { val := Sym.fill a m.fst ↑m.snd, property := (_ : Sym.fill a m.fst ↑m.snd ∈ Finset.sym (insert a s) n) })
        { fst := i, snd := { val := m, property := hm } }) =
    { fst := i, snd := { val := m, property := hm } }
[PROOFSTEP]
refine' Function.Injective.sigma_map (Function.injective_id) (fun i ↦ _) _
[GOAL]
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ Fin (n + 1) → Type ?u.22728
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ (a : Fin (n + 1)) → { x // x ∈ Finset.sym s (n - ↑a) } → ?refine'_1 (id a)
case refine'_3
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i✝ : Fin (n + 1)
m : Sym α (n - ↑i✝)
hm : m ∈ Finset.sym s (n - ↑i✝)
i : Fin (n + 1)
⊢ Function.Injective (?refine'_2 i)
case refine'_4
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ Sigma.map id ?refine'_2
      ((fun m =>
          { fst := (Sym.filterNe a ↑m).fst,
            snd :=
              { val := (Sym.filterNe a ↑m).snd,
                property := (_ : (Sym.filterNe a ↑m).snd ∈ Finset.sym s (n - ↑(Sym.filterNe a ↑m).fst)) } })
        ((fun m =>
            { val := Sym.fill a m.fst ↑m.snd, property := (_ : Sym.fill a m.fst ↑m.snd ∈ Finset.sym (insert a s) n) })
          { fst := i, snd := { val := m, property := hm } })) =
    Sigma.map id ?refine'_2 { fst := i, snd := { val := m, property := hm } }
[PROOFSTEP]
exact fun i ↦ Sym α (n - i)
[GOAL]
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ (a : Fin (n + 1)) → { x // x ∈ Finset.sym s (n - ↑a) } → Sym α (n - ↑(id a))
case refine'_3
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i✝ : Fin (n + 1)
m : Sym α (n - ↑i✝)
hm : m ∈ Finset.sym s (n - ↑i✝)
i : Fin (n + 1)
⊢ Function.Injective (?refine'_2 i)
case refine'_4
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ Sigma.map id ?refine'_2
      ((fun m =>
          { fst := (Sym.filterNe a ↑m).fst,
            snd :=
              { val := (Sym.filterNe a ↑m).snd,
                property := (_ : (Sym.filterNe a ↑m).snd ∈ Finset.sym s (n - ↑(Sym.filterNe a ↑m).fst)) } })
        ((fun m =>
            { val := Sym.fill a m.fst ↑m.snd, property := (_ : Sym.fill a m.fst ↑m.snd ∈ Finset.sym (insert a s) n) })
          { fst := i, snd := { val := m, property := hm } })) =
    Sigma.map id ?refine'_2 { fst := i, snd := { val := m, property := hm } }
[PROOFSTEP]
swap
[GOAL]
case refine'_3
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i✝ : Fin (n + 1)
m : Sym α (n - ↑i✝)
hm : m ∈ Finset.sym s (n - ↑i✝)
i : Fin (n + 1)
⊢ Function.Injective (?refine'_2 i)
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ (a : Fin (n + 1)) → { x // x ∈ Finset.sym s (n - ↑a) } → Sym α (n - ↑(id a))
case refine'_4
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ Sigma.map id ?refine'_2
      ((fun m =>
          { fst := (Sym.filterNe a ↑m).fst,
            snd :=
              { val := (Sym.filterNe a ↑m).snd,
                property := (_ : (Sym.filterNe a ↑m).snd ∈ Finset.sym s (n - ↑(Sym.filterNe a ↑m).fst)) } })
        ((fun m =>
            { val := Sym.fill a m.fst ↑m.snd, property := (_ : Sym.fill a m.fst ↑m.snd ∈ Finset.sym (insert a s) n) })
          { fst := i, snd := { val := m, property := hm } })) =
    Sigma.map id ?refine'_2 { fst := i, snd := { val := m, property := hm } }
[PROOFSTEP]
exact Subtype.coe_injective
[GOAL]
case refine'_4
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ Sigma.map id (fun i a => ↑a)
      ((fun m =>
          { fst := (Sym.filterNe a ↑m).fst,
            snd :=
              { val := (Sym.filterNe a ↑m).snd,
                property := (_ : (Sym.filterNe a ↑m).snd ∈ Finset.sym s (n - ↑(Sym.filterNe a ↑m).fst)) } })
        ((fun m =>
            { val := Sym.fill a m.fst ↑m.snd, property := (_ : Sym.fill a m.fst ↑m.snd ∈ Finset.sym (insert a s) n) })
          { fst := i, snd := { val := m, property := hm } })) =
    Sigma.map id (fun i a => ↑a) { fst := i, snd := { val := m, property := hm } }
[PROOFSTEP]
refine Eq.trans ?_ (Sym.filter_ne_fill a _ ?_)
[GOAL]
case refine'_4.refine_1
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ Sigma.map id (fun i a => ↑a)
      ((fun m =>
          { fst := (Sym.filterNe a ↑m).fst,
            snd :=
              { val := (Sym.filterNe a ↑m).snd,
                property := (_ : (Sym.filterNe a ↑m).snd ∈ Finset.sym s (n - ↑(Sym.filterNe a ↑m).fst)) } })
        ((fun m =>
            { val := Sym.fill a m.fst ↑m.snd, property := (_ : Sym.fill a m.fst ↑m.snd ∈ Finset.sym (insert a s) n) })
          { fst := i, snd := { val := m, property := hm } })) =
    Sym.filterNe a
      (Sym.fill a (Sigma.map id (fun i a => ↑a) { fst := i, snd := { val := m, property := hm } }).fst
        (Sigma.map id (fun i a => ↑a) { fst := i, snd := { val := m, property := hm } }).snd)
case refine'_4.refine_2
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ ¬a ∈ (Sigma.map id (fun i a => ↑a) { fst := i, snd := { val := m, property := hm } }).snd
[PROOFSTEP]
exacts [rfl, h ∘ mem_sym_iff.1 hm a]