What is this weird error?

Stream: new members

[Ilmārs Cīrulis]

The sorry in the last line is underlined with red and error message don't know how to synthesize placeholder for argument 'α' is shown. :(

import Mathlib

def determinant: ∀ {n}, Matrix (Fin n) (Fin n) ℝ → ℝ
| 0, _ => 1
| _ + 1, M => ∑ i, ((-1) ^ i.1 * M 0 i * determinant (M.submatrix Fin.succ i.succAbove))

theorem determinant_expanded_by_first_two_rows {n} (M: Matrix (Fin (n + 2)) (Fin (n + 2)) ℝ):
  determinant M = ∑ (i: Fin (n + 2)), ∑ (j: Fin (n + 1)),
  if j.castSucc < i
  then (-1) ^ (i.val + j.val) * (M 0 j.castSucc * M 1 i - M 1 j.succ * M 0 i) * determinant (M.submatrix (Fin.succ ∘ Fin.succ) (i.succAbove ∘ j.succAbove))
  else 0 := by
  rw [determinant]
  conv =>
    lhs
    arg 2
    intro i
    rw [determinant]
    rw [Finset.mul_sum]
    rw [Finset.sum_fin_eq_sum_range]
    arg 2
    intro j
    simp
    congr
    . intro h
      arg 2
      arg 1
      rw [Fin.succAbove]
      simp
    . skip
  conv =>
    rhs
    arg 2
    intro i
    rw [Finset.sum_fin_eq_sum_range]
  rw [Finset.sum_fin_eq_sum_range]
  rw [Finset.sum_fin_eq_sum_range]
  sorry

[Eric Wieser]

Replacing the sorry with

  recover skip
  sorry
  sorry

fixes it

[Ruben Van de Velde]

It could help to reduce your code as much as possible while still having the error

[Ruben Van de Velde]

In your case that's up to

    intro j
    simp
    congr

and removing the congr fixes the issue as well

[Ilmārs Cīrulis]

Yes, I just wanted to comment about it.

Thank you!

[Eric Wieser]

This strikes me as a bug somewhere, so thanks for posting about it; but without a much more minimal example, it probably won't be fixed any time soon

[Ilmārs Cīrulis]

I will try to make it smaller

[Ilmārs Cīrulis]

Ok, a bit smaller.

import Mathlib

def determinant: ∀ {n}, Matrix (Fin n) (Fin n) ℝ → ℝ
| 0, _ => 1
| n + 1, M => ∑ (i: Fin (n + 1)), determinant (M.submatrix Fin.succ i.succAbove)

theorem determinant_expanded_by_first_two_rows {n} (M: Matrix (Fin (n + 2)) (Fin (n + 2)) ℝ):
  determinant M = 42 := by
  conv =>
    lhs
    rw [determinant]
    rw [Finset.sum_fin_eq_sum_range]
    arg 2
    intro i1
    congr
    . skip
    . skip
  sorry

[Ilmārs Cīrulis]

and again a bit smaller

import Mathlib

theorem T: ∑ (_: Fin 1), 42 = 42 := by
  conv =>
    lhs
    rw [Finset.sum_fin_eq_sum_range]
    arg 2
    intro i
    congr
  sorry

[Ilmārs Cīrulis]

Ok, this is the smaller I could make it.

Hopefully this will be useful.

[Damiano Testa]

Smaller in this context probably refers to reducing the imports, ideally to not import anything in mathlib at all.

[Ilmārs Cīrulis]

Ok... will try to think smth.

[Eric Wieser]

That's enough for me, thanks!

[Eric Wieser]

theorem T: (fun i => if h : i < 1 then 42 else 0) = fun i => 42 := by
  conv =>
    lhs
    intro i
    congr
  sorry

[Eric Wieser]

No imports needed

[Eric Wieser]

Filed as lean4#6179