set questions

Stream: new members

[Joseph O]

Is there a function to get all the subsets of a set? I am trying to prove that something has more subsets than elements in the set

[Kyle Miller]

docs#set.powerset

It's got special notation if you want to use it: 𝒫 s

[Joseph O]

Oh nice

[Joseph O]

How could I construct a goal saying that the number of subsets is greater than the number of elements in the set.

[Joseph O]

Also, how could I denote a set with infinite elements. I am trying to construct the proof for there is no biggest infinity, but I am a bit confused about how to construct the proof statement

[Arthur Paulino]

Joseph O said:

I am trying to construct the proof for there is no biggest infinity

Are you aiming at aleph numbers?
Probably #xy, but I think you want to prove something along the lines of "given a set of any size, there exists an even bigger set"

[Arthur Paulino]

(Of course that's a guess, but I think you need to be more precise about what you mean by "no biggest infinity")

[Joseph O]

In reply to this post, that's pretty much exactly what I want to do

[Joseph O]

And yes, the aleph numbers seem like I want

[Joseph O]

Does lean have lemmas and functions for the aleph numbers?

[Kyle Miller]

docs#cardinal.aleph (I searched for "aleph" in the search box)

[Kyle Miller]

Are you wanting to work with sets specifically, or are types ok? When X is a type, set X is the type of all subsets of X. docs#cardinal.mk gives the cardinality of a type.

[Kyle Miller]

Every element of set X can be coerced to be a type, and you can get the cardinality of that, so it's fine working sets, but I just thought I'd ask.

[Arthur Paulino]

Yeah, the questions I asked weren't very good, sorry. I intended to pose them as somewhat contrasting goals, meaning that you probably don't want to involve aleph numbers in your proof. Although that's the concept that comes to my mind when one talks about "bigger/smaller infinitiy"

[Joseph O]

Kyle Miller said:

Are you wanting to work with sets specifically, or are types ok? When X is a type, set X is the type of all subsets of X. docs#cardinal.mk gives the cardinality of a type.

Why doesnt cardinal.mk return a number?

[Joseph O]

Like I dont really get this image.png

[Joseph O]

Im blindly putting things together but this is sorta what I want (this currently has a type error)

theorem no_largest_inf {α : Type} (inf : (set α)) : 𝒫 inf ≥ cardinal.mk inf := sorry

[Joseph O]

How do I make this actually work?

[Arthur Paulino]

You won't find many results about ≥ or > in mathlib. The API is built with < and ≤ instead

If you want to prove that, for any set s, the cardinality of s is less than or equal to the cardinality of the power-set of s, you don't need to talk about infinite sets

[Joseph O]

But the whole point is it being with infinite sets

[Joseph O]

how does this look?

theorem no_largest_inf {α : Type} (inf : (set α)) : cardinal.mk inf ≤ cardinal.mk (𝒫 inf) :=
begin
  sorry,
end

[Arthur Paulino]

Just pasting it with the import that works on my pc:

import set_theory.cardinal

theorem no_largest_inf {α : Type} (inf : (set α)) : cardinal.mk inf ≤ cardinal.mk (𝒫 inf) :=
begin
  sorry,
end

Notice that you calling the set inf doesn't make it infinite

[Joseph O]

Yeah I was thinking that. Does this mean I have to use aleph numbers?

[Arthur Paulino]

No I think you still need to formulate your problem better, mathematically

[Joseph O]

Ok this is what I am trying to prove: Take an infinity containing a set of something; I can create a larger infinity by making an infinity that contains the subsets of the smaller infinity (oh god that was terrible, I doubt its very mathematical)

[Arthur Paulino]

Do you have a link to a precise statement of this result? Maybe in some introductory material on set theory, a Wikipedia page or something like that

[Joseph O]

Im essentially trying to prove Cantor's theorem

[Joseph O]

https://en.wikipedia.org/wiki/Cantor's_theorem

[Joseph O]

Every set is smaller than its power set

[Arthur Paulino]

Then you've stated the theorem properly already

[Joseph O]

But it works for infinite sets?

[Arthur Paulino]

Notice that the theorem stated as you did is actually more general than if you wanted to talk about infinite sets, specifically

[Joseph O]

Maybe I could prove this theorem, and then use it for infinite sets?

[Joseph O]

Should I rename it to cantors_theorem, or set_lt_powerset

[Joseph O]

As for no naming conflicts

[Joseph O]

Hmm there doesnt seem to be a cantor_theorem

[Jireh Loreaux]

docs#function.cantor_surjective

[Jireh Loreaux]

This is the Cantor theorem you are referring to.

[Jireh Loreaux]

Of course, there are a variety of ways to phrase it. You could take this theorem and translate it into the language of cardinality.

[Joseph O]

I guess I will try and attempt it myself.

[Joseph O]

But why is it called cantor_surjective?

[Jireh Loreaux]

Click the link. It says there are no surjective functions from a set to it's power set (although it is phrased in terms of types: no surjective function from a type to the type of sets of that type)

[Jireh Loreaux]

Notice that docs#function.cantor_injective is also a variation of the Cantor theorem. We can't call them all cantor_theorem because that would be a naming conflict.

[Jireh Loreaux]

There's also docs#cardinal.cantor' which is specifically about cardinal numbers.

[Kyle Miller]

Going off topic, I just wanted to mention the Lawvere fixed-point theorem, which I think is pretty neat. cantor_surjective is an easy corollary of it. (Though the theorem is more interesting in other Cartesian closed categories where the exponential object isn't just α → β, since due to cardinality there's not much you can do with this version except prove contradictions.)

theorem lawvere {α β : Sort*} (ϕ : α → (α → β)) (hϕ : function.surjective ϕ)
  (f : β → β) : ∃ s, f s = s :=
begin
  let q : α → β := λ a, f (ϕ a a),
  obtain ⟨p, hp⟩ := hϕ q,
  use ϕ p p,
  calc f (ϕ p p) = q p : rfl
             ... = ϕ p p : by rw hp
end

theorem cantor_surjective' {α : Type*} (ϕ : α → (α → Prop)) : ¬ function.surjective ϕ :=
begin
  intro hϕ,
  -- get the fixed point of logical negation!
  simpa using lawvere ϕ hϕ (λ p, ¬ p),
end

-- recall that `set α` is defined to be `α → Prop`
theorem cantor_surjective {α : Type*} (ϕ : α → set α) : ¬ function.surjective ϕ :=
cantor_surjective' ϕ

[Eric Wieser]

Joseph O said:

how does this look?

Here's an easy proof of that in terms of docs#cardinal.cantor

import set_theory.cardinal.basic
open_locale cardinal

-- this should maybe be in mathlib: #13786
@[simp] theorem cardinal.mk_powerset {α : Type} (s : (set α)) : #(𝒫 s) = 2 ^ #↥s :=
by rw [cardinal.mk_congr (equiv.set.powerset s), cardinal.mk_set]

theorem cardinal.mk_le_mk_powerset {α : Type} (s : (set α)) : #s < #(𝒫 s) :=
begin
  rw cardinal.mk_powerset,
  exact cardinal.cantor _,
end

The key trick here is discovering docs#equiv.set.powerset, which I found with library_search. I made a PR with an expansion of #(𝒫 s) in #13786

[Joseph O]

The version of the proof I learned had to do with surjective functions, so I might try and prove the first.

[Joseph O]

Jireh Loreaux said:

This is the Cantor theorem you are referring to.

Not exact actually. That is cantor’s diagonal argument. I am trying to prove the one saying every set is smaller than its powerset

[Eric Wieser]

Yes, but that proof is much better stated in terms of α and set α than it is in terms of ↥S and ↥(𝒫 S)

[Eric Wieser]

An important skill when using Lean is to know when the math word "set" means set α, and when it means Type u

[Joseph O]

So if I have type a, set a is all the subsets?

[Riccardo Brasca]

set a is the type of sets whose elements have type a. There is so such a thing as "subset of a type", there are sets (whose elements must have the same type) and subsets of sets.

[Riccardo Brasca]

(there are subtypes)

[Riccardo Brasca]

https://leanprover-community.github.io/theories/sets.html

[Joseph O]

Do they work the same way?

[Joseph O]

It actually seems like it,

[Joseph O]

Eric Wieser said:

Joseph O said:

how does this look?

Here's an easy proof of that in terms of docs#cardinal.cantor

import set_theory.cardinal.basic
open_locale cardinal

-- this should maybe be in mathlib: #13786
@[simp] theorem cardinal.mk_powerset {α : Type} (s : (set α)) : #(𝒫 s) = 2 ^ #↥s :=
by rw [cardinal.mk_congr (equiv.set.powerset s), cardinal.mk_set]

theorem cardinal.mk_le_mk_powerset {α : Type} (s : (set α)) : #s < #(𝒫 s) :=
begin
  rw cardinal.mk_powerset,
  exact cardinal.cantor _,
end

The key trick here is discovering docs#equiv.set.powerset, which I found with library_search. I made a PR with an expansion of #(𝒫 s) in #13786

How does that prove that a set is smaller than its powerset. I guess that makes sense, because of the a < 2 ^ a

[Riccardo Brasca]

I think that first of all you should decide how to state this in type theory. Your mathematical statement is that # s < # (𝒫 s) for any set s. I think that the equivalent in type theory is # α < # (set α), for α : Type u, but if you prefer you can state it for sets, it's just the the library for cardinals it is written for cardinals of types (of course if you have a set you also have a type, so at the end it doesn't matter, but you have to choose how to state your result).

[Joseph O]

Hmm for some reason my lean cant find #, isnt it imported from set_theory.cardinal.basic?

[Eric Wieser]

open_locale cardinal

[Eric Wieser]

It's notation for docs#cardinal.mk

[Joseph O]

What does that do?

[Eric Wieser]

Eric Wieser said:

open_locale cardinal

It runs all the commands in the locale, which are the commands that turn on the notation

[Joseph O]

Got it.

[Mauricio Collares]

Joseph O said:

Jireh Loreaux said:

This is the Cantor theorem you are referring to.

Not exact actually. That is cantor’s diagonal argument. I am trying to prove the one saying every set is smaller than its powerset

Cantor's proof that every set is smaller than its powerset is also a diagonal argument. You can check that docs#function.cantor_surjective is not about $\mathbb{R}$ being non-enumerable.

[Mauricio Collares]

https://en.wikipedia.org/wiki/Cantor%27s_diagonal_argument#General_sets

[Joseph O]

Aha you are right it is the diagonal argument. My original goal was essentially: If we have an infinite set, the set containing the subsets of the infinite set, essentially the powerset is larger. Using surjectivity I believe, but we didn't use a diagonal argument.

[Joseph O]

So this is what I want to prove

theorem cantor_theorem {α : Type} (f : α → (set α)): ¬function.surjective f :=
begin
  sorry,
end

[Joseph O]

(deleted)

[Riccardo Brasca]

First of all write down an extremely detailed mathematical proof. With pen and paper, not in Lean

[Joseph O]

Riccardo Brasca said:

https://leanprover-community.github.io/theories/sets.html

Besides this link, is there a nice guide in sets that would tell me how to represent

$$B = \{ x \in A | x \notin f(A) \}$$

[Yaël Dillies]

set B := {x | x ∉ range f}

[Johan Commelin]

@Joseph O Is A a set or a Type?

[Joseph O]

Its a Type

[Johan Commelin]

Ok, then range f is indeed what you want. Otherwise there is f '' A.

[Joseph O]

How does it represent the range f(A)?

[Joseph O]

does it infer the A?

[Joseph O]

Yaël Dillies said:

set B := {x | x ∉ range f}

Also, how is that valid, as I never declared an x

[Joseph O]

Aha, looking on the side, it seems that it is infered B: set (set α) := {x : set α | x ∉ range f}

[Yaël Dillies]

f : α → set α is enough for Lean to infer that range f : set (set α), which is enough to infer that x : set α, which is enough to infer that B : set (set α).

[Kevin Buzzard]

Unification is cool :-)

[Joseph O]

wow

[Joseph O]

how come when i do have ξ : α, I get two goals?

[Joseph O]

MWE:

import init.data.set
import set_theory.cardinal.basic

open set
open nat
open_locale cardinal

theorem cantor_theorem {α : Type} (f : α → (set α)): ¬function.surjective f :=
begin
  set B := {x | x ∉ range f},
  have ξ : α,
end

[Eric Wieser]

Your first goal is the value of ξ

[Eric Wieser]

Your second goal is the original goal you started with

[Joseph O]

Why? Im trying to do this part of the proof image.png

[Yaël Dillies]

Imagine α = empty. Then you cannot do have ξ : α, out of thin air.

[Eric Wieser]

Joseph O said:

Why?

have h : p, means "create a new goal with target p, and put h : p in the existing goal.

Joseph O said:

Im trying to do this part of the proof image.png

This isn't a proof, this is a statement. The previous or following sentence will say why such an ξ exists, and you have to translate that sentence to lean too

[Kevin Buzzard]

"there exists xi such that..." is not have xi, it's have h : \exists \xi, <property that xi has>

[Joseph O]

So I did by_contradiction, which assumes f is surjective, which means there exists ∃ ξ, ξ ∈ α

by_contradiction,
  have h : ∃ ξ, ξ ∈ α

but it is failing to satisfy some sort of type class instance

[Eric Wieser]

ξ ∈ α is nonsense

[Eric Wieser]

It would be like writing (n : ℕ) (hn : n ∈ ℕ)

[Joseph O]

Is it already inferred?

[Eric Wieser]

I think have ξ : α, was the correct thing to write here

[Eric Wieser]

Joseph O said:

Is it already inferred?

No, it's just meaningless. ∈ is defined on sets, α is a type

[Eric Wieser]

If you insist on writing the ∈ symbol, you can write ξ ∈ (set.univ : set α), i.e. "ξ is in the set consisting of all possible values of α".

[Eric Wieser]

This is of course useless, because by definition everything is in set.univ.

[Joseph O]

Hmm but then that keeps making two goals. How would you represent this in lean?

[Eric Wieser]

Yes, it's making two goals because you have to tell lean why ξ : α exists

[Joseph O]

It exists if f is surjective

[Eric Wieser]

Great, you need to work out how to tell lean that

[Joseph O]

I would think with exact?

[Eric Wieser]

Joseph O said:

It exists if f is surjective

What's the maths proof?

[Joseph O]

image.png

[Eric Wieser]

Because as hand-waved, your statement is false. id : empty -> empty is surjective (docs#function.surjective_id), but there is no element of empty

[Eric Wieser]

(double dollars $$ for latex in Zulip - please do this instead of using an image)

[Ruben Van de Velde]

https://en.wikipedia.org/wiki/Cantor%27s_theorem#Proof ?

[Joseph O]

Suppose to the contrary that ${\displaystyle f}$ is surjective. Then there exists ${\displaystyle \xi \in A}$ such that ${\displaystyle f(\xi )=B}$.

[Joseph O]

I suppose this with by_contradiction

[Eric Wieser]

That proof has missed the (trivial) step between the . and the "Then", which lean wants you to spell out

[Eric Wieser]

Perhaps rw function.surjective at h will help you see what's going on?

[Ruben Van de Velde]

Joseph O said:

Riccardo Brasca said:

https://leanprover-community.github.io/theories/sets.html

Besides this link, is there a nice guide in sets that would tell me how to represent

$$B = \{ x \in A | x \notin f(A) \}$$

Btw, this is not the B from the wikipedia proof

[Joseph O]

Oh wait it should have been f(x)

[Ruben Van de Velde]

Which is

  set B := {x : α | x ∉ f x},

[Joseph O]

That makes sense

[Joseph O]

Eric Wieser said:

Perhaps rw function.surjective at h will help you see what's going on?

It seems like ξ doesn't nessacerily have to exist

[Eric Wieser]

What's your goal state look like after that rewrite?

[Joseph O]

α: Type
f: α → set α
B: set α := {x : α | x ∉ f x}
h: ∀ (b : set α), ∃ (a : α), f a = b
⊢ false

[Joseph O]

(this is without xi)

[Eric Wieser]

Your h says that for every b, there exists an a

[Eric Wieser]

So if you're following the proof you pasted above, you want to set b = B, right?

[Eric Wieser]

Do you remember how to do that?

[Joseph O]

Do I use the have tactic?

[Eric Wieser]

Sure, that's as good a way as any

[Eric Wieser]

In fact, if you start with have : ∃ (a : α), f a = B,, then library_search will remind you how to prove that (if you don't already know)

[Joseph O]

i did this:

set B := {x : α | x ∉ f x},
  by_contradiction,
  have : ∃ (a : α), f a = B,
  {
    exact h B,
  },

it seemed to work

[Joseph O]

for the second goal, the proof statement was

α: Type
f: α → set α
B: set α := {x : α | x ∉ f x}
h: function.surjective f
this: ∃ (ξ : α), f ξ = B
⊢ false

[Joseph O]

And in the Wikipedia, the next this is said was

But by construction, ${\displaystyle \xi \in B\iff \xi \notin f(\xi )=B}$.

[Joseph O]

(deleted)

[Joseph O]

(deleted)

[Joseph O]

How can I destruct this to bring ξ into scope?

[Joseph O]

Or How can I just bring it into scope in general

[Damiano Testa]

I think that cases this will do what you want. Likely, rcases? this will give you a helpful Try this: ... that might also be closer that what you really want!

[Joseph O]

thanks

[Joseph O]

nvm

[Joseph O]

What do you think of this proof?

theorem cantor_surjective {α : Type} (f : α → (set α)) :
  ¬function.surjective f :=
begin
  set B := {x : α | x ∉ f x},
  by_contradiction,
  have : ∃ (ξ : α), f ξ = B,
  { exact h B, },
  { rcases this with ⟨ξ, _⟩,
    have : ξ ∈ B ↔ ξ ∉ f(ξ),
    { exact mem_set_of, },
    { rw this_h at this,
      exact not_p_iff_not_p _ this, } }
end

is it ok?

[Joseph O]

It definitely doesn't compete with mathlib's proof

[Arthur Paulino]

If it translates your reasoning well then it's definitely a good achievement. The proofs that go to mathlib are highly golfed and sometimes hard to grasp

[Riccardo Brasca]

A nice aspect of formalization is that if Lean says "goals accomplished" then the proof is OK :)

It's never too late to golf a proof, but at the beginning I wouldn't bother too much

[Joseph O]

Yeah I am still very new to lean

[Joseph O]

can someone explain how this proof works?

theorem mk_le_of_injective {α : Type} {β : Type} {f : α → β}
  (hf : function.injective f) :
  #α ≤ #β := ⟨⟨f, hf⟩⟩

[Riccardo Brasca]

This works because # α ≤ # β means by definition that there f : α → β injective.

[Joseph O]

oh but what about the nested structures. Frankly I'm confused

[Joseph O]

oh its bc of this, right?
image.png

[Arthur Paulino]

It's better if you post code so we don't have to lose sight of everything else to see what you're posting

[Joseph O]

Well thats just from mathlib

[Arthur Paulino]

Still, opening an image grays out everything else on Zulip :(

[Riccardo Brasca]

The first ⟨...⟩ takes care of nonempty. You can go in tactic mode (bewteen begin and end) and see what refine ⟨_⟩ does.

[Joseph O]

refine ⟨_⟩ makes the goal intof is injective or smth, but then the last structure.... I'm still so confused

[Riccardo Brasca]

Basically, to prove that something is nonempty you can exhibit an element. But if you look at the precise definition of docs#nonempty you see that it is a structure, with only one constructor. This looks complicated, but in practice you have to write the element you've found inside ⟨ ⟩. You can also write refine nonempty.intro _.

[Riccardo Brasca]

Now the goal is α ↪ β, so you have to produce an element of this type.

[Riccardo Brasca]

If you look at the definition of docs#function.embedding, you see that to produce an embedding you have to produce two things: a function and a proof that this function is injective.

[Riccardo Brasca]

⟨_, _⟩ allows you to give these elements once at a time.

[Riccardo Brasca]

Try refine ⟨_, _⟩, you'll have two goals. The first will be a function, and you can close it with exact f.

[Riccardo Brasca]

Then you have to prove that the f you gave is injective, and this is hf.

[Riccardo Brasca]

⟨⟨f, hf⟩⟩ is just a way to compress all this stuff.

[Riccardo Brasca]

But really, mathlib proofs are not easy to read, don't spend too much time on them. You will get there anyway at some point.

[Riccardo Brasca]

Especially proofs that are mathematically irrelevant, like this one (there is literally nothing to prove) are highly compressed, using only term mode.

[Arthur Paulino]

If your proof is accepted and is not unnecessarily long or slow, then it's fine. We trust on Lean's kernel

[Joseph O]

Riccardo Brasca said:

Basically, to prove that something is nonempty you can exhibit an element. But if you look at the precise definition of docs#nonempty you see that it is a structure, with only one constructor. This looks complicated, but in practice you have to write the element you've found inside ⟨ ⟩. You can also write refine nonempty.intro _.

But what are we saying is nonempty

[Joseph O]

a or b?

[Eric Wieser]

We're saying the type α ↪ β is nonempty

[Joseph O]

And why does it produce a type of function.embedding?

[Joseph O]

Where did that come from

[Riccardo Brasca]

To prove that α ↪ β is nonempty you need to find an element of type α ↪ β.

[Riccardo Brasca]

If x : α ↪ β is such an element, then exact nonempty.intro x is a proof of nonempty α ↪ β. This can be shortened to exact ⟨x⟩, or ⟨x⟩ in term mode.

[Riccardo Brasca]

Lean is asking to prove nonempty (α ↪ β) because this is the definition of #α ≤ #β.

[Riccardo Brasca]

(the literal definition of docs#cardinal.has_le is more complicated because #α is defined on equivalence classes of types, so one has to check that this definition makes sense)

[Riccardo Brasca]

But again, I think you are focusing too much on the Lean code instead of the actual math. What is your definition of #α ≤ #β (feel free to think that α and β are sets, forgetting about type theory)?

[Joseph O]

Actually I get it now. Thanks for your help!

[Joseph O]

I find that this proof makes the most sense for a beginner

theorem mk_le_of_injective {α β : Type} {f : α → β}
  (hf : function.injective f) :
  #α ≤ #β :=
begin
  refine nonempty.intro _,
  refine ⟨_, _⟩,
  exact f,
  apply hf,
end

[Joseph O]

Like me

[Kyle Miller]

If you don't want to figure out the names of your constructors (like nonempty.intro), you can use tactic#fsplit

theorem mk_le_of_injective {α β : Type} {f : α → β}
  (hf : function.injective f) :
  #α ≤ #β :=
begin
  fsplit,
  fsplit,
  exact f,
  exact hf,
end

It creates a new goal for each argument that the constructor needs. (fsplit is like tactic#split but makes sure that the goals are in a useful order. split can be backwards.)

[Kyle Miller]

Or, if you don't want to prove it since you know it's just a bunch of splits and exacts, there's tactic#tidy, which tries to make progress using some basic tactics.

theorem mk_le_of_injective {α β : Type} {f : α → β}
  (hf : function.injective f) :
  #α ≤ #β :=
begin
  tidy,
end

[Joseph O]

Oh wow thanks

[Kyle Miller]

Here's a fun one:

theorem mk_le_of_injective {α β : Type} {f : α → β}
  (hf : function.injective f) :
  #α ≤ #β :=
begin
  repeat { fsplit <|> assumption }
end

[Kyle Miller]

That means "repeatedly try doing fsplit or assumption until one of them fails".

[Joseph O]

:astonished:

[Joseph O]

will assumption always work?

[Joseph O]

Which do you reccomend to a begginer

[Kyle Miller]

It's for doing exact foo when foo is one of the hypotheses.

[Kyle Miller]

but you don't have to specify the hypothesis.

[Kyle Miller]

theorem mk_le_of_injective {α β : Type} {f : α → β}
  (hf : function.injective f) :
  #α ≤ #β :=
begin
  fsplit,
  fsplit,
  assumption,
  assumption,
end

[Arthur Paulino]

If you want to know what tidy did, you can use tidy? and it will be shown as a (clickable) Try this: ⋯ snippet in the infoview

[Kyle Miller]

I don't have a recommendation about assumption vs exact. I use both :shrug:

What assumption essentially does is try doing exact for each hypothesis one at a time until one succeeds. (To be completely accurate: it looks for a hypothesis where exact should succeed and does exact with it.)

[Patrick Johnson]

assumption is better in repeated segments of the proof where parameters may vary (for example ; assumption or repeat { assumption }), but I would say that exact is generally better, because it's faster. Consider the following example where assumption fails, but exact works:

example {n : ℕ} (h₁ : n = 0 + 10 ^ 5) (h₂ : n = 10 ^ 5) : n = 10 ^ 5 :=
begin
  assumption, -- fails
  exact h₂,   -- works
end

[Kyle Miller]

Huh, even with none transparency assumption would fail here.

namespace tactic

/-- `find_same_type t es` tries to find in es an expression with type definitionally equal to t -/
meta def find_same_type' (tr : transparency) : expr → list expr → tactic expr
| e []         := failed
| e (H :: Hs) :=
  do t ← infer_type H,
     (unify e t tr >> return H) <|> find_same_type' e Hs

meta def find_assumption' (tr : transparency) (e : expr) : tactic expr :=
do ctx ← local_context, find_same_type' tr e ctx

meta def assumption'' : tactic unit :=
do { ctx ← local_context,
     t   ← target,
     H   ← find_same_type' transparency.none t ctx,
     exact H }
<|> fail "assumption tactic failed"

meta def interactive.assumption'' := tactic.assumption

end tactic

example {n : ℕ} (h₁ : n = 0 + 10 ^ 5) (h₂ : n = 10 ^ 5) : n = 10 ^ 5 :=
begin
  assumption'', -- fails
  -- deep recursion was detected at 'expression equality test'
end

I wonder if that's a bug in unify or if this is unavoidable?

[Patrick Johnson]

Kyle Miller said:

meta def interactive.assumption'' := tactic.assumption

Do you see it? :)

[Kyle Miller]

I better configure myself to use semireducible transparency