Type mismatch for the "same type"?

Stream: new members

[White Chen]

I want to prove that the set of x satisfying:

$$x_1+2x_2+3x_3=0$$

is a submodule of F^3, but get error like:

type mismatch
  cvm
has type
  c • v ∈ m : Prop
but is expected to have type
  c • v ∈ m : Prop

Here is the Lean code:

import Mathlib.Tactic
-- set_option pp.all true
variable {F : Type*} (a b : ℝ) [Field F]
variable {V : Type _} [AddCommGroup V] [Module F V]
example [Module F (Fin 3 → F)] {m : Set (Fin 3 → F)}
        (h : ∀ x, x 0 + 2 * x 1 + 3 * x 2 = 0 ↔ x ∈ m)
        : ∃ n : Submodule F (Fin 3 → F), m = n := by
  let s : Submodule F (Fin 3 → F) := {
      carrier := m
      zero_mem' := by sorry   -- zero_mem' and add_mem' are ok.
      add_mem' := by sorry
      smul_mem' := by
        rintro c v vm
        simp at *
        have h' : (c • v) 0 + 2 * (c • v) 1 + 3 * (c • v) 2 = 0 := by
          sorry

        -- ⊢ c • v ∈ m

        -- apply (h (c • v)).mp     -- failed to unify c • v ∈ m with c • v ∈ m
        -- exact (h (c • v)).mp h'  -- type mismatch for c • v ∈ m and c • v ∈ m
        convert (h (c • v)).mp
        constructor
        · intro cvm h'
          exact cvm                 -- still type mismatch
        · intro h''
          exact h'' h'              -- still type mismatch
  }
  use s; rfl

After referring to failed to unify identical things?, I tried set_option pp.all true. And the error message become something terrible (I'm sorry for posting such long thing):

type mismatch
  cvm
has type
  @Membership.mem.{u_1, u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
    (Set.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F))
    (@Set.instMembershipSet.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F))
    (@HSMul.hSMul.{u_1, u_1, u_1} F (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
      (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
      (@instHSMul.{u_1, u_1} F (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
        -- Starting from here, there's a difference.
        (@SMulZeroClass.toSMul.{u_1, u_1} F (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
          (@AddMonoid.toZero.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
            (@AddCommMonoid.toAddMonoid.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
              (@Pi.addCommMonoid.{0, u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)))
                (fun (a : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) => F)
                fun (i : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) =>
                @NonUnitalNonAssocSemiring.toAddCommMonoid.{u_1} F
                  (@NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring.{u_1} F
                    (@NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring.{u_1} F
                      (@NonUnitalCommRing.toNonUnitalNonAssocCommRing.{u_1} F
                        (@CommRing.toNonUnitalCommRing.{u_1} F
                          (@EuclideanDomain.toCommRing.{u_1} F (@Field.toEuclideanDomain.{u_1} F inst✝³)))))))))
          (@SMulWithZero.toSMulZeroClass.{u_1, u_1} F (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
            (@MonoidWithZero.toZero.{u_1} F
              (@Semiring.toMonoidWithZero.{u_1} F
                (@DivisionSemiring.toSemiring.{u_1} F
                  (@Semifield.toDivisionSemiring.{u_1} F (@Field.toSemifield.{u_1} F inst✝³)))))
            (@AddMonoid.toZero.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
              (@AddCommMonoid.toAddMonoid.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
                (@Pi.addCommMonoid.{0, u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)))
                  (fun (a : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) => F)
                  fun (i : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) =>
                  @NonUnitalNonAssocSemiring.toAddCommMonoid.{u_1} F
                    (@NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring.{u_1} F
                      (@NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring.{u_1} F
                        (@NonUnitalCommRing.toNonUnitalNonAssocCommRing.{u_1} F
                          (@CommRing.toNonUnitalCommRing.{u_1} F
                            (@EuclideanDomain.toCommRing.{u_1} F (@Field.toEuclideanDomain.{u_1} F inst✝³)))))))))
            (@MulActionWithZero.toSMulWithZero.{u_1, u_1} F (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
              (@Semiring.toMonoidWithZero.{u_1} F
                (@DivisionSemiring.toSemiring.{u_1} F
                  (@Semifield.toDivisionSemiring.{u_1} F (@Field.toSemifield.{u_1} F inst✝³))))
              (@AddMonoid.toZero.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
                (@AddCommMonoid.toAddMonoid.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
                  (@Pi.addCommMonoid.{0, u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)))
                    (fun (a : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) => F)
                    fun (i : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) =>
                    @NonUnitalNonAssocSemiring.toAddCommMonoid.{u_1} F
                      (@NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring.{u_1} F
                        (@NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring.{u_1} F
                          (@NonUnitalCommRing.toNonUnitalNonAssocCommRing.{u_1} F
                            (@CommRing.toNonUnitalCommRing.{u_1} F
                              (@EuclideanDomain.toCommRing.{u_1} F (@Field.toEuclideanDomain.{u_1} F inst✝³)))))))))
              (@Module.toMulActionWithZero.{u_1, u_1} F (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
                (@DivisionSemiring.toSemiring.{u_1} F
                  (@Semifield.toDivisionSemiring.{u_1} F (@Field.toSemifield.{u_1} F inst✝³)))
                (@Pi.addCommMonoid.{0, u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)))
                  (fun (a : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) => F)
                  fun (i : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) =>
                  @NonUnitalNonAssocSemiring.toAddCommMonoid.{u_1} F
                    (@NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring.{u_1} F
                      (@NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring.{u_1} F
                        (@NonUnitalCommRing.toNonUnitalNonAssocCommRing.{u_1} F
                          (@CommRing.toNonUnitalCommRing.{u_1} F
                            (@EuclideanDomain.toCommRing.{u_1} F (@Field.toEuclideanDomain.{u_1} F inst✝³)))))))
                inst✝)))))
      c v)
    m : Prop
but is expected to have type
  @Membership.mem.{u_1, u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
    (Set.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F))
    (@Set.instMembershipSet.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F))
    (@HSMul.hSMul.{u_1, u_1, u_1} F (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
      (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
      (@instHSMul.{u_1, u_1} F (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
        -- Starting from here, there's a difference.
        (@Pi.instSMul.{u_1, 0, u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) F
          (fun (a : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) => F)
          fun (i : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) =>
          @Algebra.toSMul.{u_1, u_1} F F (@Semifield.toCommSemiring.{u_1} F (@Field.toSemifield.{u_1} F inst✝³))
            (@DivisionSemiring.toSemiring.{u_1} F
              (@Semifield.toDivisionSemiring.{u_1} F (@Field.toSemifield.{u_1} F inst✝³)))
            (@Algebra.id.{u_1} F (@Semifield.toCommSemiring.{u_1} F (@Field.toSemifield.{u_1} F inst✝³)))))
      c v)
    m : Prop

I can only tell from the information above that these two types are indeed different, but I cannot obtain any more information.

[Matthew Ballard]

convert rfl in place of rfl might give more info

[Patrick Massot]

The [Module F (Fin 3 → F)] is bound to create issues.

[Patrick Massot]

This puts in the game a totally unspecified F-module structure on Fin 3 → F having nothing to do with the one you intend and Lean already knows about, hence creating conflicts that confuse Lean.