Why does my lean4 code get an error

Stream: new members

[grandxuan pan]

import Mathlib.Data.Real.Basic

import Mathlib.Analysis.Calculus.Deriv.Basic

import Mathlib.Data.Nat.Basic

import Mathlib.Data.Nat.GCD.Basic

import Mathlib.Data.Finset.Basic

import Mathlib.Data.Fintype.Basic

import Mathlib.Algebra.BigOperators.Intervals

import Mathlib.Algebra.GCDMonoid.Finset

open List

open Finset Nat

open Nat

namespace NumberTheory

variable (k : ℕ) (hk : 1 ≤ k)

variable (hk0 : 0 < k := Nat.lt_of_lt_of_le (by decide) hk)

variable (i : Fin k)

variable (a : Fin k → ℕ) (b : Fin k → ℕ)

variable (ha_range : ∀ i, i ∈ Set.Icc (1 : ℕ) k)

variable (ha : ∀ i, a i > 0) (hb : ∀ i, b i > 0)

variable (N : Type) [CancelCommMonoidWithZero N] [NormalizedGCDMonoid N]

variable [inst1 : CancelCommMonoidWithZero N]

variable [inst2 : NormalizedGCDMonoid N]

variable (ha_inj : Function.Injective a)

variable (ha_inji : Function.Injective b)

def a₀ : ℕ := a ⟨0, hk0⟩

def b₀ : ℕ := b ⟨0, hk0⟩

def a_i (i : Fin k) : ℕ := a i

def b_i (i : Fin k) : ℕ := b i

example (i : Fin k) : ℕ := a i  -- aᵢ

example (i : Fin k) : ℕ := b i  -- bᵢ

variable (h_coprime : ∀ (i : Fin k), gcd (a i) (b i) = 1)

def indices (k : ℕ) : Finset (Fin k) := Finset.univ

def b_values : Finset ℕ := Finset.image b (indices k)

def m (k : ℕ) (b : Fin k → ℕ) : ℕ := Finset.fold lcm 1 b (indices k)
--lemma izj (i : Fink) : i ∈ indices k := by
--exact Finset.mem_univ i

lemma mem_indices (i : Fin k) : i ∈ indices k := by

 exact Finset.mem_univ i

lemma b_dvd_m (i : Fin k) : b_i ∣ m k b := by

  unfold m

  have mem_b : b i ∈ b_values k b := by

    unfold b_values

    unfold indices

    rw [Finset.mem_image]

    use i

    constructor

    . exact Finset.mem_univ i

    . rfl

  unfold b_i

  exact Finset.dvd_lcm (s := b_values k b) (f := id) (b := b_i) mem_b

end NumberTheory```

[grandxuan pan]

Why does my lean4 code get an error at exact Finset.dvd_lcm (s := b_values k b) (f := id) (b := b_i) mem_b Application type mismatch: In the application
@dvd_lcm ℕ ℕ ?m.20702 ?m.20703 (b_values k b) id b_i
the argument
b_i
has type
(k : ℕ) → (Fin k → ℕ) → Fin k → ℕ : Type
but is expected to have type

[Serhii Khoma (srghma)]

failed to synthesize NormalizedGCDMonoid ℕ

[Ruben Van de Velde]

The error you're quoting half of is fairly clear: b_i is not a valid argument here. Maybe b i is what you meant, but then there's still other issues

[Ruben Van de Velde]

The "failed to synthesize" error can be solved by adding the right import, but the exact turns out not to match the goal either

[Ruben Van de Velde]

(and a maintainer should probably move this thread to #new members)

[grandxuan pan]

Thank you, thank you—I see now where I was wrong. In other words, what I need here is a natural-number type, but b－i is not of that kind. So my question now is: how can I convert a number of type b－i into the N type?

[Notification Bot]

This topic was moved here from #lean4 > Why does my lean4 code get an error by Patrick Massot.

[grandxuan pan]

` ``import Mathlib.Algebra.Group.Defs  

import Mathlib.Data.Real.Basic    

import Mathlib.Analysis.Calculus.Deriv.Basic  

import Mathlib.Data.Nat.Basic

import Mathlib.Data.Nat.GCD.Basic

import Mathlib.Data.Finset.Basic  

import Mathlib.Data.Fintype.Basic  

import Mathlib.Algebra.BigOperators.Intervals

import Mathlib.Algebra.GCDMonoid.Finset

import Mathlib.Algebra.GCDMonoid.Nat

open List  

open Finset Nat

open Nat

namespace NumberTheory

variable (k : ℕ) (hk : 1 ≤ k)

variable (hk0 : 0 < k := Nat.lt_of_lt_of_le (by decide) hk)

variable (i : Fin k)

variable (a : Fin k → ℕ) (b : Fin k → ℕ)  

variable (ha_range : ∀ i, i ∈ Set.Icc (1 : ℕ) k)

variable (ha : ∀ i, a i > 0) (hb : ∀ i, b i > 0)

variable (N : Type) [CancelCommMonoidWithZero N] [NormalizedGCDMonoid N]

variable [inst1 : CancelCommMonoidWithZero N]

variable [inst2 : NormalizedGCDMonoid N]

variable (ha_inj : Function.Injective a)

variable (ha_inji : Function.Injective b)

def a₀ : ℕ := a ⟨0, hk0⟩

def b₀ : ℕ := b ⟨0, hk0⟩

def a_i (i : Fin k) : ℕ := a i

example (i : Fin k) : ℕ := a i  -- aᵢ

def b_i (i : Fin k) : ℕ := b i

theorem id_eq_b_i : id (b_i k b i) = b_i k b i := rfl

variable (h_coprime : ∀ (i : Fin k), Nat.gcd (a i) (b i) = 1)

def indices (k : ℕ) : Finset (Fin k) := Finset.univ

def b_values : Finset ℕ := Finset.image b (indices k)

def m (k : ℕ) (b : Fin k → ℕ) : ℕ := fold Nat.lcm 1 b (indices k)  
--lemma izj (i : Fink) : i ∈ indices k := by
--exact Finset.mem_univ i  为什么我的这种写法是错误的，但是下面的是正确的？

lemma mem_indices (i : Fin k) : i ∈ indices k := by

exact Finset.mem_univ i

lemma b_dvd_m (i : Fin k) : (b_i k b i) ∣ m k b := by

unfold m

have mem_b : b i∈ b_values k b := by

unfold b_values

unfold indices

rw [Finset.mem_image]

use i

constructor

. exact Finset.mem_univ i  

. rfl

unfold b_i

#check (b_i  k b i )

have id_eq : id (b_i k b i) = b_i k b i := by

rfl

exact Finset.dvd_lcm  (s := b_values k b) (f := id) (b := b_i k b i) mem_b

end NumberTheory` ``

[Kenny Lau]

@grandxuan pan the backticks go on a newline