Why does my lean4 code get an error

Stream: lean4

[Notification Bot]

This topic was moved to #new members > Why does my lean4 code get an error by Patrick Massot.

[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

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  ```

[grandxuan pan]

type mismatch
dvd_lcm mem_b
has type
id (b_i k b i) ∣ (b_values k b).lcm id : Prop
but is expected to have type
b i ∣ Finset.fold Nat.lcm 1 b (indices k) : Prop

[Kenny Lau]

are the right hand sides the same?

[Kenny Lau]

#new members > Why does my lean4 code get an error @ 💬