Application Type Mismatch

Stream: lean4

[Bockman Cheung]

Hi, I'm a new lean user, and I ran into this problem when I tried to prove a lemma:

class pattern_n (F : Type*) [Field F] (f : ℕ × ℕ → F) (n : ℕ) : Prop where

  topBordZeros : ∀ m, f (0,m) = 0

  topBordOnes : ∀ m, f (1,m) =1

  botBordOnes_n : ∀ m, f (n, m) = 1

  botBordZeros_n : ∀ i, ∀ m,  i ≥ n+1 → (f (i,m) = 0)

  diamond : ∀ i, ∀ m,  i ≤ n-1 → f (i+1,m) * f (i+1,m+1)-1 = f (i+2,m)*f (i,m+1)

class nzPattern_n (F : Type*) [Field F] (f : ℕ × ℕ → F) (n : ℕ) extends pattern_n F f n where

  non_zero : ∀ i, ∀ m, 1 ≤ i → i ≤ n → f (i,m) ≠ 0

lemma pattern_nContinuant1 (F : Type*) [Field F] (f : ℕ×ℕ → F) (n: ℕ) [nzPattern_n F f n] : ∀ i, i ≤ n-1 → ∀m, f (i+2,m) = f (2,m+i)*f (i+1,m) - f (i,m) := by

  intro i

  induction i with

  | zero =>

  simp

  intro m

  have h₀ : f (0, m) = 0 := by exact pattern_n.topBordZeros n m

  have h₁ : f (1, m) = 1 := by exact pattern_n.topBordOnes n m

  rw [h₀, h₁]

  simp

  | succ k ih =>

  intro h m

 have h₂ : f (k + 1, m + 1) ≠ 0 := by exact nzPattern_n.non_zero (k+1) (m+1) h /- error -/

I'm thinking if I could fix the definition of the class nzPattern_n to make the types match. However I don't know how to do this. Is my idea feasible? This is the lemma in latex.

Captura-de-pantalla-2024-08-18-202624.png

[Andrés Goens]

Hi @Bockman Cheung , welcome to Zulip and Lean!

Usually, the error is pretty helpful in figuring out the issue. Maybe you can show the error (and not just /- error -/) to help people figure out what the issue is.

It also seems like you have a long example there (and you haven't put the whole file either, it's missing at least some imports), it's usually helpful to try and give people the shortest (minimal) working example of the problem you're having, so that we don't have to understand all the context of what you're doing that's not relevant to the problem you're having