type mismatch

Stream: new members

[Kenny Lau]

has type
  @is_ring_hom.{u (max v u)} R (Π (b : ι), @ideal.quotient.{u} R _inst_1 (f b)) (@comm_ring.to_ring.{u} R _inst_1)
    (@pi.ring.{v u} ι (λ (b : ι), @ideal.quotient.{u} R _inst_1 (f b))
       (λ (i : ι),
          @comm_ring.to_ring.{u} (@ideal.quotient.{u} R _inst_1 (f i)) (@ideal.quotient.comm_ring.{u} R _inst_1 (f i))))
    (λ (x : R) (b : ι), @ideal.quotient.mk.{u} R _inst_1 (f b) x)
but is expected to have type
  @is_ring_hom.{u (max v u)} R (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i)) (@comm_ring.to_ring.{u} R _inst_1)
    (@comm_ring.to_ring.{(max v u)} (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
       (@pi.comm_ring.{v u} ι (λ (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
          (λ (i : ι), @ideal.quotient.comm_ring.{u} R _inst_1 (f i))))
    (λ (r : R) (i : ι), @ideal.quotient.mk.{u} R _inst_1 (f i) r)

[Kenny Lau]

have (@pi.ring.{v u} ι (λ (b : ι), @ideal.quotient.{u} R _inst_1 (f b))
       (λ (i : ι),
          @comm_ring.to_ring.{u} (@ideal.quotient.{u} R _inst_1 (f i)) (@ideal.quotient.comm_ring.{u} R _inst_1 (f i))))
=
(@comm_ring.to_ring.{(max v u)} (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
       (@pi.comm_ring.{v u} ι (λ (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
          (λ (i : ι), @ideal.quotient.comm_ring.{u} R _inst_1 (f i))))
, from rfl,

but this works

[Kevin Buzzard]

Is this thread supposed to be comprehensible to anyone but you?

[Kenny Lau]

type mismatch at application
  quotient.lift (⨅ (i : ι), f i) (λ (r : R) (i : ι), quotient.mk (f i) r)
term
  pi.is_ring_hom_pi (λ (i : ι) (r : R), quotient.mk (f i) r)
has type
  is_ring_hom (λ (x : R) (b : ι), quotient.mk (f b) x)
but is expected to have type
  is_ring_hom (λ (r : R) (i : ι), quotient.mk (f i) r)

[Kenny Lau]

is this more comprehensible?

[Patrick Massot]

Kenny should have a private stream all for himself

[Kevin Buzzard]

What is your question Kenny? I don't think that other people are going to be carefully scanning your output of pp.all true.

[Kenny Lau]

well, my question is that, clearly they are equal!

[Patrick Massot]

Is that a question?

[Kevin Buzzard]

Well Lean says they're not so they're not.

[Kevin Buzzard]

But because we have no way of reproducing the error, how can anyone else help?

[Kenny Lau]

then the question is, why does Lean not know that they are equal?

[Kevin Buzzard]

you're the only person who can answer that until you post a lot more context

[Kenny Lau]

import algebra.pi_instances ring_theory.ideal_operations

universes u v

variables {R : Type u} [comm_ring R] {ι : Type v}

open lattice

namespace ideal

def to_prod (f : ι → ideal R) : (⨅ i, f i).quotient → Π i, (f i).quotient :=
@@quotient.lift _ _ (⨅ i, f i) (λ r i, ideal.quotient.mk (f i) r)
  (pi.is_ring_hom_pi _ : is_ring_hom (λ (r : R) (i : ι), quotient.mk (f i) r))
  _

end ideal

[Patrick Massot]

We can sympathize, this is probably what we should do

[Kevin Buzzard]

After his last post we can now try to help :-)

[Kevin Buzzard]

So they're not the same because the implicit terms are different.

[Kenny Lau]

but they're defeq

[Kenny Lau]

as seen in my second post

[Kevin Buzzard]

Indeed, you have now explained the question coherently.

[Kevin Buzzard]

import algebra.pi_instances ring_theory.ideal_operations

universes u v

variables {R : Type u} [comm_ring R] {ι : Type v}

open lattice

namespace ideal

set_option pp.all true
def to_prod (f : ι → ideal R) : (⨅ i, f i).quotient → Π i, (f i).quotient :=
begin
  have : @is_ring_hom.{u (max v u)} R (Π (b : ι), @ideal.quotient.{u} R _inst_1 (f b)) (@comm_ring.to_ring.{u} R _inst_1)
    (@pi.ring.{v u} ι (λ (b : ι), @ideal.quotient.{u} R _inst_1 (f b))
       (λ (i : ι),
          @comm_ring.to_ring.{u} (@ideal.quotient.{u} R _inst_1 (f i)) (@ideal.quotient.comm_ring.{u} R _inst_1 (f i))))
    (λ (x : R) (b : ι), @ideal.quotient.mk.{u} R _inst_1 (f b) x)
    =
@is_ring_hom.{u (max v u)} R (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i)) (@comm_ring.to_ring.{u} R _inst_1)
    (@comm_ring.to_ring.{(max v u)} (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
       (@pi.comm_ring.{v u} ι (λ (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
          (λ (i : ι), @ideal.quotient.comm_ring.{u} R _inst_1 (f i))))
    (λ (r : R) (i : ι), @ideal.quotient.mk.{u} R _inst_1 (f i) r) := rfl,

exact @@quotient.lift _ _ (⨅ i, f i) (λ r i, ideal.quotient.mk (f i) r)
  (pi.is_ring_hom_pi _ : is_ring_hom (λ (r : R) (i : ι), quotient.mk (f i) r))
  _
  /-
  type mismatch at application
  @ideal.quotient.lift.{u (max v u)} R (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i)) _inst_1
    (@pi.comm_ring.{v u} ι (λ (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
       (λ (i : ι), @ideal.quotient.comm_ring.{u} R _inst_1 (f i)))
    (@lattice.infi.{u v+1} (@ideal.{u} R _inst_1) ι
       (@submodule.lattice.has_Inf.{u u} R R (@comm_ring.to_ring.{u} R _inst_1)
          (@ring.to_add_comm_group.{u} R (@comm_ring.to_ring.{u} R _inst_1))
          (@ring.to_module.{u} R (@comm_ring.to_ring.{u} R _inst_1)))
       (λ (i : ι), f i))
    (λ (r : R) (i : ι), @ideal.quotient.mk.{u} R _inst_1 (f i) r)
    (@pi.is_ring_hom_pi.{v u u} ι (λ (a : ι), @ideal.quotient.{u} R _inst_1 (f a))
       (λ (i : ι),
          @comm_ring.to_ring.{u} (@ideal.quotient.{u} R _inst_1 (f i)) (@ideal.quotient.comm_ring.{u} R _inst_1 (f i)))
       R
       (@comm_ring.to_ring.{u} R _inst_1)
       (λ (i : ι) (r : R), @ideal.quotient.mk.{u} R _inst_1 (f i) r)
       (λ (a : ι), @ideal.quotient.is_ring_hom_mk.{u} R _inst_1 (f a)))
term
  @pi.is_ring_hom_pi.{v u u} ι (λ (a : ι), @ideal.quotient.{u} R _inst_1 (f a))
    (λ (i : ι),
       @comm_ring.to_ring.{u} (@ideal.quotient.{u} R _inst_1 (f i)) (@ideal.quotient.comm_ring.{u} R _inst_1 (f i)))
    R
    (@comm_ring.to_ring.{u} R _inst_1)
    (λ (i : ι) (r : R), @ideal.quotient.mk.{u} R _inst_1 (f i) r)
    (λ (a : ι), @ideal.quotient.is_ring_hom_mk.{u} R _inst_1 (f a))
has type
  @is_ring_hom.{u (max v u)} R (Π (b : ι), @ideal.quotient.{u} R _inst_1 (f b)) (@comm_ring.to_ring.{u} R _inst_1)
    (@pi.ring.{v u} ι (λ (b : ι), @ideal.quotient.{u} R _inst_1 (f b))
       (λ (i : ι),
          @comm_ring.to_ring.{u} (@ideal.quotient.{u} R _inst_1 (f i)) (@ideal.quotient.comm_ring.{u} R _inst_1 (f i))))
    (λ (x : R) (b : ι), @ideal.quotient.mk.{u} R _inst_1 (f b) x)
but is expected to have type
  @is_ring_hom.{u (max v u)} R (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i)) (@comm_ring.to_ring.{u} R _inst_1)
    (@comm_ring.to_ring.{(max v u)} (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
       (@pi.comm_ring.{v u} ι (λ (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
          (λ (i : ι), @ideal.quotient.comm_ring.{u} R _inst_1 (f i))))
    (λ (r : R) (i : ι), @ideal.quotient.mk.{u} R _inst_1 (f i) r)
    -/

end

end ideal

[Kevin Buzzard]

I recommend you fill in the _

[Kenny Lau]

wat

[Kevin Buzzard]

but what do I know

[Kevin Buzzard]

Maybe some elaboration is taking place in the wrong order or some such nonsense

[Kevin Buzzard]

Do you understand why

exact @ideal.quotient.lift.{u (max v u)} R (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i)) _inst_1
    (@pi.comm_ring.{v u} ι (λ (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
       (λ (i : ι), @ideal.quotient.comm_ring.{u} R _inst_1 (f i)))
    (@lattice.infi.{u v+1} (@ideal.{u} R _inst_1) ι
       (@submodule.lattice.has_Inf.{u u} R R (@comm_ring.to_ring.{u} R _inst_1)
          (@ring.to_add_comm_group.{u} R (@comm_ring.to_ring.{u} R _inst_1))
          (@ring.to_module.{u} R (@comm_ring.to_ring.{u} R _inst_1)))
       (λ (i : ι), f i))
    (λ (r : R) (i : ι), @ideal.quotient.mk.{u} R _inst_1 (f i) r)
    (@pi.is_ring_hom_pi.{v u u} ι (λ (a : ι), @ideal.quotient.{u} R _inst_1 (f a))
       (λ (i : ι),
          @comm_ring.to_ring.{u} (@ideal.quotient.{u} R _inst_1 (f i)) (@ideal.quotient.comm_ring.{u} R _inst_1 (f i)))
       R
       (@comm_ring.to_ring.{u} R _inst_1)
       (λ (i : ι) (r : R), @ideal.quotient.mk.{u} R _inst_1 (f i) r)
       (λ (a : ι), @ideal.quotient.is_ring_hom_mk.{u} R _inst_1 (f a)))

doesn't work? I have to go and give a lecture on p-adic geometry so I can't think about this any more but this would be one way of trying to fill in the _s to see if that's the issue.

[Kevin Buzzard]

i.e. look at what the term fully elaborates to and try that instead. I just must have failed somehow.

[Kevin Buzzard]

[my error was "you got it wrong" not "these are not defeq"]

[Kenny Lau]

finally this "worked":

import algebra.pi_instances ring_theory.ideal_operations

universes u v

variables {R : Type u} [comm_ring R] {ι : Type v}

open lattice

namespace ideal

def to_pi (f : ι → ideal R) (r : R) : Π i, (f i).quotient :=
λ i, ideal.quotient.mk (f i) r

instance (f : ι → ideal R) : is_ring_hom (to_pi f) :=
pi.is_ring_hom_pi _

def to_prod (f : ι → ideal R) : (⨅ i, f i).quotient → Π i, (f i).quotient :=
@ideal.quotient.lift.{u (max v u)} R (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i)) _inst_1
    (@pi.comm_ring.{v u} ι (λ (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
       (λ (i : ι), @ideal.quotient.comm_ring.{u} R _inst_1 (f i)))
    (@lattice.infi.{u v+1} (@ideal.{u} R _inst_1) ι
       (@submodule.lattice.has_Inf.{u u} R R (@comm_ring.to_ring.{u} R _inst_1)
          (@ring.to_add_comm_group.{u} R (@comm_ring.to_ring.{u} R _inst_1))
          (@ring.to_module.{u} R (@comm_ring.to_ring.{u} R _inst_1)))
       (λ (i : ι), f i))
    (@ideal.to_pi.{u v} R _inst_1 ι f)
    (@ideal.is_ring_hom.{u v} R _inst_1 ι f)
  (λ r hr, funext $ λ i, quotient.eq_zero_iff_mem.2 $ mem_Inf.1 hr ⟨i, rfl⟩)

end ideal

[Kenny Lau]

minimzed to:

def to_prod (f : ι → ideal R) : (⨅ i, f i).quotient → Π i, (f i).quotient :=
@@ideal.quotient.lift _ _ (⨅ i, f i) (ideal.to_pi f)
    (@ideal.is_ring_hom.{u v} R _ ι f)
  (λ r hr, funext $ λ i, quotient.eq_zero_iff_mem.2 $ mem_Inf.1 hr ⟨i, rfl⟩)

[Kenny Lau]

in (@ideal.is_ring_hom.{u v} R _ ι f), turning ι into underscore creates the error

[Kenny Lau]

the R is also essential

[Kevin Buzzard]

So it's some elaborator nonsense, or do you think it's a bug?

[Kevin Buzzard]

Let's try to debug it!

[Kevin Buzzard]

Sebastian once told us some set_option to see the rfl machine trying to prove rfl

[Kevin Buzzard]

I think it was in the thread where he wrote "got into office" "checks Zulip" "leaves office again"

[Ashvni Narayanan]

I am trying to show that the principal fractional ideals form a subgroup of the group of fractional ideals.

import linear_algebra.finite_dimensional
import ring_theory.ideal.basic
import algebra.field
import ring_theory.subring
import ring_theory.integral_closure
import ring_theory.fractional_ideal
import data.rat.basic
import ring_theory.algebra
import ring_theory.algebraic

open function
open_locale classical big_operators

class number_field (K : Type*) :=
   (fld : field K)
   (alg : algebra ℚ K)
   (fd : finite_dimensional ℚ K)

def number_ring (K : Type*) [number_field K] := @integral_closure ℤ K _ (@field.to_comm_ring K _inst_1.fld) _

noncomputable theory
open_locale classical

open finite_dimensional
namespace number_field
variables (K : Type*) [number_field K]
variables [g : fraction_map (number_ring K) K ]

def principal_fractional_ideal := { P : ring.fractional_ideal g // ∃ a : (number_ring K), submodule.is_principal P.1 }

instance is_group : group (ring.fractional_ideal g) := sorry,

instance is_subgroup : subgroup (ring.fractional_ideal g) :=
begin
  use (principal_fractional_ideal g),
end

The last proof gives me the error

type mismatch at application
  principal_fractional_ideal g
term
  g
has type
  fraction_map ↥(number_ring K) K : Type u_1
but is expected to have type
  Type ? : Type (?+1)
state:
K : Type u_1,
_inst_1 : number_field K,
g : fraction_map ↥(number_ring K) K
⊢ subgroup (ring.fractional_ideal g)

Any help is appreciated, thank you!

[Adam Topaz]

Sounds like you're missing an underscore before the g.

[Adam Topaz]

Your code is not compiling for me :-/

[Adam Topaz]

Okay, looks like there were a bunch of issues.
Here's a hacked together fix.

import linear_algebra.finite_dimensional
import ring_theory.ideal.basic
import algebra.field
import ring_theory.subring
import ring_theory.integral_closure
import ring_theory.fractional_ideal
import data.rat.basic
import ring_theory.algebra
import ring_theory.algebraic

open function
open_locale classical big_operators

class number_field (K : Type*) :=
   (fld : field K)
   (alg : algebra ℚ K)
   (fd : finite_dimensional ℚ K)

namespace number_field
variables (K : Type*) [number_field K]
instance : field K := number_field.fld
instance : algebra ℚ K := number_field.alg
instance : finite_dimensional ℚ K := number_field.fd
end number_field

def number_ring (K : Type*) [number_field K] := @integral_closure ℤ K _ (@field.to_comm_ring K _inst_1.fld) _

noncomputable theory
open_locale classical

open finite_dimensional
namespace number_field
variables (K : Type*) [number_field K]
variables (g : fraction_map (number_ring K) K)

def principal_fractional_ideal := { P : ring.fractional_ideal g | ∃ a : (number_ring K), submodule.is_principal P.1 }

instance is_group : group (ring.fractional_ideal g) := sorry,

#check principal_fractional_ideal

instance is_subgroup : subgroup (ring.fractional_ideal g) :=
{ carrier := principal_fractional_ideal _ g,
  one_mem' := _,
  mul_mem' := _,
  inv_mem' := _ }

[Adam Topaz]

Note that subgroup takes a set as its carrier, whereas you defined a principal_fractional_ideal as a subtype.
Also, the field, algebra, etc. instances were not recognized since you didn't extend these classes in your definition of number field.

[Ashvni Narayanan]

Ah, I see. It seems like the _ is K. So essentially I needed g to be explicit. Thank you!

[Adam Topaz]

You need to make $K$ implicit :) (lean will figure out $K$ from $g$)

[Ashvni Narayanan]

Adam Topaz said:

You need to make $K$ implicit :) (lean will figure out $K$ from $g$)

Ah alright, thank you!

[Alex Zhang]

Why is there a type mismatch problem in the following code?

constants {α : Type*} (r : α → α → Prop)

section

parameter  transr : ∀ {x y z}, r x y → r y z → r x z

variables {a b c d e : α}

theorem t1 (h₁ : r a b) (h₂ : r b c) (h₃ : r c d) : r a d :=
transr (transr h₁ h₂) h₃

end

[Eric Wieser]

What's the error message?

[Kyle Miller]

It's somehow coming from the universe variable for α

The error message:

15:9: type mismatch at application
  transr h₁
term
  h₁
has type
  r a b
but is expected to have type
  r ?m_1 ?m_2

but with set_option pp.universes true it's

15:1: type mismatch at application
  transr ⁇ h₃
term
  h₃
has type
  r.{u_6 u_7} c d
but is expected to have type
  r.{u_2 u_3} ?m_1 ?m_2

[Kyle Miller]

This is fine:

theorem t1 {α : Type*} (r : α → α → Prop) (transr : ∀ {x y z : α}, r x y → r y z → r x z)
  {a b c d e : α} (h₁ : r a b) (h₂ : r b c) (h₃ : r c d) : r a d :=
transr (transr h₁ h₂) h₃

[Kyle Miller]

and so is this:

variables {α : Type*} (r : α → α → Prop) (transr : ∀ {x y z : α}, r x y → r y z → r x z)

theorem t1 {a b c d e : α} (h₁ : r a b) (h₂ : r b c) (h₃ : r c d) : r a d :=
transr (transr h₁ h₂) h₃

[Kyle Miller]

If you're wanting to use constants, then one thing that seems to fix it is to put things into a specific type universe:

constants {α : Type} (r : α → α → Prop)

[Alex Zhang]

I don't understand... why does the mismatch error occur :(
Could anyone give me an explanation?

[Eric Wieser]

Mixing constants and parameters like that is kind of strange

[Eric Wieser]

"there exists some global r that is impossible to prove anything about" + "allow the user to supply a proof that r is transitive" seems like nonsense to me

[Eric Wieser]

Probably they should both be variables

[Johan Commelin]

I think constants should have been delayed till the final chapter of #tpil. It's rare that one should need it. Mathlib never uses it.

[Alex Zhang]

Eric Wieser said:

Mixing constants and parameters like that is kind of strange

Yes, I mixed them purely for the purpose of learning their functionality.
According to Johan, I don't need to study "constant" then :)

[Johan Commelin]

Unless you are interested in adding new axioms to your foundations. In some sense, every use of constant should be viewed with a lot of suspicion.

[Johan Commelin]

Because it can make the whole project inconsistent.

[Mario Carneiro]

constant x : T is approximately equivalent to def x : T := sorry

[Johan Commelin]

With the difference that the latter contains the word sorry :stuck_out_tongue_wink:

[Mario Carneiro]

constant is for people who don't apologize for their actions

[Kevin Buzzard]

and, by the looks of things, want to generate universe mismatches

[Alex Zhang]

How can I fix the type mismatch problem in the following definition?

universe u

inductive vector (α : Type u) : ℕ → Type u
| nil {} : vector 0
| cons   : Π {n}, α → vector n → vector (n+1)

namespace vector
local notation h :: t := cons h t

def append {α : Type*} : Π {n m : ℕ}, vector α n → vector α m → vector α (n+m)
| 0 m v w := w

end vector

[Kevin Buzzard]

The easiest way to fix it is to define vector alpha n as {L : list alpha | L.length = n}.

[Alex Zhang]

Yes, I know that I can change the definition. As I am studying the contents of the reference book and trying various exercises, I would like to keep the above definition, which is used in the book.

[Kevin Buzzard]

Mathematically this is the same object, and it turns out that when it comes to implementation issues you have quickly run into the problem with the inductive definition, which is why I'm suggesting that you avoid it completely. As an "end user" of vectors all you need is an API for vectors, so because I can define things like nil and cons and append for my suggested definition, which I can, you do not need to care about these subtle implementation issues, which are matters for computer scientists.

[Kevin Buzzard]

"Sticking to the book" is a big mistake. This is not how to formalise mathematics.

[Kevin Buzzard]

def append {α : Type*} : Π {n m : ℕ}, vector α n → vector α m → vector α (n+m)
| 0 m v w := begin have h : 0 + m = m := nat.zero_add m, rw h, exact w, end

[Kevin Buzzard]

This compiles. But your problems are only just beginning.

[Kevin Buzzard]

The problem is that rw introduces an eq.rec into the definition, which means that it will be hard to work with in practice.

[Adam Topaz]

(deleted)

[Adam Topaz]

I think this is what you're going for?

[Adam Topaz]

sorry that's backwards

[Adam Topaz]

I think this is better?

universe u

inductive vector (α : Type u) : ℕ → Type u
| nil {} : vector 0
| cons   : Π {n}, α → vector n → vector (n+1)

namespace vector
local notation h :: t := cons h t

def append {α : Type*} : Π {n m : ℕ}, vector α n → vector α m → vector α (m + n)
| 0 m _ w := w
| (n+1) m (cons h v) w := cons h (append v w)

end vector

[Kevin Buzzard]

Adam has cheated because he has switched the natural which you're doing induction on and is now abusing Lean's definitional equality. He has used the fact that although 0 + m = m is true because of a theorem (it uses induction and hence the proof mentions nat.rec), m + 0 = m is true by definition and this fact can be abused. If Lean were to change its definition of nat then Adam's construction might stop working. what I am trying to emphasize is that you are running into questions which are "non-mathematical" here -- the answer depends on more than the objects you're working with, it depends on precisely how they have been implemented, and mathematics should not depend on such things.

[Adam Topaz]

Yes, I should have mentioned that :)

[Kevin Buzzard]

Update: Adam has edited his post and is now cheating in a new way, he has changed your n + m to m + n. The fact that this is an issue should be a red flag, although unfortunately sometimes in mathematics we have to resort to dirty tricks like this, which is exactly why mathematicians like Adam know these tricks.

[Adam Topaz]

Just to clarify: I agree with everything Kevin said in this case, but I mentioned that code in case you wanted an example of using the equation compiler

[Adam Topaz]

A better cheat would be to change your inductive definition of vector so that append can actually match the recursive definition of addition of natural numbers.

[Alex Zhang]

@Adam Topaz Could you show exact code of the "better cheat"?

[Adam Topaz]

Oh, you can just cons on the right instead of the left

[Adam Topaz]

Sorry, I'm away from the computer now so I can't write any code

[Kevin Buzzard]

The problem is that nat "appends on the right" (succ n := n+1 by definition) but list "appends on the left" (append [h] tl := h :: tl by definition). What is happening here is that if F is a function taking values in types, and a = b by definition, then F a = F b by definition, however if a = b is only true because of a theorem, then F a = F b is true because of an axiom eq.rec, and this axiom needs to be invoked whenever you move from F a to F b, which can be extremely inconvenient in Lean's type theory because of the way things are set up. Hence you either decide to see the red flags and try a new design decision, or you press on and then you have to start thinking hard about which things are true by definition and which things are only true because of theorems, which can be problematic (and can change without warning).

[Alex Zhang]

import tactic
theorem test {I J : Type*}:
∃ {K : Type*}, 1 = 1 :=
begin
  refine ⟨(I × J), _⟩,
end

This reports error :

type mismatch at application
  Exists.intro (I × J)
term
  I × J
has type
  Type (max u_1 u_2) : Type (max (u_1+1) (u_2+1))
but is expected to have type
  Type u_3 : Type (u_3+1)

Why should there be a type mismatch problem in this example? How can I fix it?

[Alex Zhang]

Perhaps I should give an explicit universe...

[Alex Zhang]

This is ok

theorem {u} test {I J : Type u}:
∃ {K : Type u}, 1 = 1 :=
begin
  refine ⟨I × I, _⟩,
end

[Eric Rodriguez]

this is the example/def vs lemma/theorem stuff we talked about before; the type of a theorem is immutable after it's set, whilst universe metavariables can change in an example/def.