# Zulip Chat Archive

## Stream: new members

### Topic: showing injectivity

#### Adeeb K (Apr 28 2020 at 18:51):

I have a definition of a function using the if-then-else pattern, and I want to break it up into cases based on that definition. How can I do so? The context is that I am trying to show a function is injective

#### Adeeb K (Apr 28 2020 at 18:52):

Here is all I have so far

#### Adeeb K (Apr 28 2020 at 18:52):

```
import tactic
def injective {X Y} (f : X → Y) := ∀ x₁ x₂, f x₁ = f x₂ → x₁ = x₂
def range {X Y} (f : X → Y) := { y | ∃ x, f x = y }
theorem comp_inj_is_inj
{X Y Z} (f : X → Y) (g : Y → Z)
(p1 : injective f)
(p2 : injective g)
: injective (g ∘ f)
:= begin
introv x p3,
change g (f x) = g (f x₂) at p3,
apply p1,
apply p2,
apply p3,
end
lemma succ_greater_than_nat (n : ℕ) : nat.succ n > n
:=
begin
rw nat.succ_eq_add_one,
linarith
end
lemma pred_exists (n : ℕ) (p: n > 0) : exists k, nat.succ k = n
:=
begin
induction n with d hd,
{linarith,},
{
existsi d,
refl
}
end
-- forgot library function, lifted from square root prime code
-- credit to github user dm1237
lemma succ_eq_add_one (n : ℕ) : nat.succ n = n + 1 :=
begin
exact rfl,
end
-- forgot library function
lemma my_le_trans
(j k m : ℕ)
(p1: k < m)
(p2: j ≤ k)
: j < m - 1
:=
begin
intros,
-- try induction?
sorry,
end
lemma inequality_fact
(j m : ℕ)
(p: j < m)
: j - 1 < m - 1
:= begin
intros,
sorry
end
/--
Type of pairs (k,p) where k
is a natural number and p is a witness to the proof that k < n.
-/
def finite_subset (n : ℕ) := Σ' k, k < n
/--
Every pair that lives in finite_subest m lives in finite_subset n
where m < n
-/
def lift_finite (m n : ℕ) (p : m < n) : finite_subset m → finite_subset n
:= λ k, ⟨k.1, lt.trans k.2 p⟩
/--
Application of lift_finite from m to m + 1
-/
def lift_one
(m : ℕ)
: finite_subset m → finite_subset (m + 1)
:= (lift_finite m (m+1) (succ_greater_than_nat m))
lemma lift_one_fst {m} (j : finite_subset m) : (lift_one m j).fst = j.fst
:=
begin
refl,
end
/--
The lifting function is injective
-/
theorem lift_finite_injective (m n : ℕ) (p : m < n) :
injective (lift_finite m n p)
:= begin
/- pf sketch
-- suppose f x1 = f x2 = < k, pf: k < n >
-- we know x1 = < l , pf: k < m > and x2 = < j , pf: j < m >
-- note that (f x1).1 = (f x2).1 = k
-- furthermore, k < m < n
-- then x1 = < k, pf: k < m > = x2
-- done
-/
introv x p2,
cases x,
cases x₂,
cases p2,
refl,
end
/--
The lifting from m to m + 1 injective
-/
lemma lift_one_injective (m : ℕ)
: injective (lift_one m)
:= begin
apply lift_finite_injective m (m + 1) (succ_greater_than_nat m),
end
lemma ext_iff (n : ℕ) (a b : finite_subset n) : a = b ↔ a.1 = b.1 :=
begin
cases a,
cases b,
split,
{ intro h, rw h},
{ intro h, cases h, refl,}
end
def relabel
(m k : ℕ)
(p: k < m)
: finite_subset m → finite_subset (m - 1)
:= λ j, if H : j.1 ≤ k then ⟨j.1, my_le_trans j.1 k m p H ⟩ else ⟨j.1 - 1, inequality_fact j.1 m j.2⟩
/-
This formalizes the notion that when f is injective and misses k
in the codomain then when we relabel to bring m to m - 1,
composition is injective
-/
lemma relabel_with_inj_f_misses_k_is_inj
(m k : ℕ)
(p: k < m)
(f: finite_subset m → finite_subset m)
(inj: injective f)
: injective ((relabel m k p) ∘ f)
:=
begin
intros x,
intros,
sorry,
end
--proof that f : [m + 2] -> [m + 1] restricted
--to [m + 1] = {0, 1, ..., m} does not hit f(m + 1)
lemma miss_proof
{m} (f : finite_subset (m + 2) → finite_subset (m + 1))
(inj : injective f)
{pf: m + 1 < m + 2}
: ∀ j : finite_subset (m + 1), (f ∘ lift_one (m + 1)) j ≠ f ⟨m + 1, pf⟩
:= begin
introv p,
change f (lift_one (m+1) j) = f ⟨m + 1, pf⟩ at p,
let p2 := inj (lift_one (m+1) j) ⟨m + 1, pf⟩,
let p3 := p2 p,
rw ext_iff at p3,
rw lift_one_fst at p3,
let p4 := j.2,
linarith,
end
lemma relabel_inj
(m k : ℕ)
(p: k < m)
(f: finite_subset (m + 2) → finite_subset (m + 1))
(inj: injective f)
{pf} (miss: ∀ j : finite_subset (m + 1), (f ∘ lift_one (m + 1)) j ≠ ⟨k, pf⟩ )
: injective ((relabel (m + 1) k pf) ∘ f ∘ lift_one (m + 1))
:=
begin
introv x,
let y := x₂,
intros,
change (relabel (m + 1) k pf (f (lift_one (m + 1) x))) = (relabel (m + 1) k pf (f (lift_one (m + 1) x₂))) at a,
let x_l := (lift_one (m + 1) x),
let y_l := (lift_one (m + 1) x₂),
change relabel (m + 1) k pf (f x_l) = relabel (m + 1) k pf (f y_l) at a,
let r_x_l := relabel (m + 1) k pf (f x_l),
let r_y_l := relabel (m + 1) k pf (f y_l),
change r_x_l = r_y_l at a,
sorry,
end
/--
Pigeonhole principle, induction on n
-/
theorem pigeonhole_principle
(n m : ℕ)
(f : finite_subset n → finite_subset m)
: (n > m) → ¬(injective f)
:= begin
intros n_gt_m f_injective,
induction n with d hd,
{ linarith, /- case d = 0 -/ },
let g := f ∘ (lift_one d),
let hd' := hd g,
rcases lt_or_eq_of_le (nat.lt_succ_iff.1 n_gt_m) with h | rfl,
{ /- case where d > m -/
/- prove injective g -/
apply hd' h,
let g_injective := comp_inj_is_inj (lift_one d) f (lift_one_injective d) f_injective,
exact g_injective,
},
{ /- case where d = m -/
/- prove f : finite_subset (nat.succ m) → finite_subset m is not injective -/
induction m with l hl,
{
let e:= f ⟨0,_ ⟩,
let e2 := e.2,
linarith,
exact n_gt_m,
},
let k := f ⟨l + 1, succ_greater_than_nat (l + 1)⟩, -- let k = f(l + 1)
let violator := f ∘ (lift_one (l + 1)),
let restriction := (relabel (l + 1) k.1 k.2) ∘ violator,
let violator_is_inj := comp_inj_is_inj (lift_one (l + 1)) f (lift_one_injective (l + 1)) f_injective,
let res_is_inj := relabel_with_inj_f_misses_k_is_inj (l + 1) k.1 k.2 violator violator_is_inj,
/- contradiction, since restriction: [m] → [m - 1] is injective,
but this can't be true IH
-/
refine hl _ _ _ _ ,
{
intros,
linarith,
},
{
exact restriction,
},
{
exact succ_greater_than_nat _,
},
{
exact res_is_inj,
},
}
end
```

#### Adeeb K (Apr 28 2020 at 18:53):

I am trying to prove `relabel_inj`

. It uses the definition of `relabel`

.

#### Adeeb K (Apr 28 2020 at 18:57):

Should I cut down the size of the code block?

#### Adeeb K (Apr 28 2020 at 19:08):

I tried cases but that seems to come from if I do induction on k?

#### Kevin Buzzard (Apr 28 2020 at 19:08):

Try the `split_ifs`

tactic

#### Adeeb K (Apr 28 2020 at 19:09):

so `split_ifs at a`

, where `a : relabel (m + 1) k pf (f x_l) = relabel (m + 1) k pf (f y_l)`

?

#### Adeeb K (Apr 28 2020 at 19:09):

I'm getting this error:

```
no if-then-else expressions to split
```

#### Reid Barton (Apr 28 2020 at 19:10):

I think this lemma will benefit from some strategic planning and maybe writing out a proof on paper first.

#### Kevin Buzzard (Apr 28 2020 at 19:10):

https://leanprover-community.github.io/mathlib_docs/tactics.html#split_ifs

#### Adeeb K (Apr 28 2020 at 19:10):

I did write out a proof on paper

#### Reid Barton (Apr 28 2020 at 19:10):

Okay, what did you do at this point then?

#### Reid Barton (Apr 28 2020 at 19:11):

There is a better way to go about this than forging ahead with case splits here--I don't know whether it is a "spoiler" though.

#### Adeeb K (Apr 28 2020 at 19:11):

at this point, I split the proof into two cases based on the definition of `relabel`

. Either the RHS = LHS ≤ k or RHS = LHS > k

#### Adeeb K (Apr 28 2020 at 19:12):

then, by `miss_proof`

, we know that RHS = LHS != k

#### Reid Barton (Apr 28 2020 at 19:12):

So you are splitting based on the *output* of `relabel`

?

#### Adeeb K (Apr 28 2020 at 19:12):

yes

#### Reid Barton (Apr 28 2020 at 19:12):

Okay, that is better than what I thought you were intending, but not what `split_if`

s does.

#### Reid Barton (Apr 28 2020 at 19:13):

Still, I think breaking things down into more lemmas would help.

#### Adeeb K (Apr 28 2020 at 19:14):

then I should be able to conclude that either `f x_l = f y_l`

or `(< (f x_1) - 1, (f x_1).snd >) = (< (f y_1) - 1, (f y_1).snd >)`

, both of which would give me that `x = y`

by injectivity of `lift_one`

and `f`

#### Adeeb K (Apr 28 2020 at 19:15):

I'm not sure how to split this into lemmas, or at least it isn't _immediately_ obvious to me how to do so

#### Reid Barton (Apr 28 2020 at 19:15):

Adeeb K said:

then, by

`miss_proof`

, we know that RHS = LHS != k

Actually, this is not true, is it?

#### Adeeb K (Apr 28 2020 at 19:15):

It should be by `miss_proof`

we gave earlier

#### Reid Barton (Apr 28 2020 at 19:16):

Adeeb K said:

then I should be able to conclude that either

`f x_l = f y_l`

or`(< (f x_1) - 1, (f x_1).snd >) = (< (f y_1) - 1, (f y_1).snd >)`

, both of which would give me that`x = y`

by injectivity of`lift_one`

and`f`

How do you know that both `f x_1`

and `f y_1`

fall into the same case of `relabel`

?

#### Reid Barton (Apr 28 2020 at 19:16):

Adeeb K said:

It should be by

`miss_proof`

we gave earlier

But this is about the input of `relabel`

, not the output of `relabel`

.

#### Adeeb K (Apr 28 2020 at 19:16):

this whole proof to show that the composition is injective is to lead up to a contradiction in pigeonhole principle - I end up getting this whole thing is an injective function from `[m + 1]`

to `[m]`

which is a contradiction according to my inductive hypothesis

#### Adeeb K (Apr 28 2020 at 19:16):

because `f x_1 = f y_1`

#### Adeeb K (Apr 28 2020 at 19:17):

by injectivity of `lift_one`

and `f`

right?

#### Reid Barton (Apr 28 2020 at 19:17):

Wait, that's what you're trying to prove.

#### Adeeb K (Apr 28 2020 at 19:17):

right right

#### Adeeb K (Apr 28 2020 at 19:18):

but by the definition of relabel, they have to either be <= k or > k right? You can't be <= k and > k at the same time

#### Reid Barton (Apr 28 2020 at 19:18):

How do you know, for example, that `relabel 100 7 _ 3`

isn't equal to `relabel 100 7 _ 21`

.

#### Adeeb K (Apr 28 2020 at 19:19):

but wouldn't that imply that 2 = 20?

#### Reid Barton (Apr 28 2020 at 19:19):

Well, of course it's because `3`

doesn't equal `20`

but you have to consider this case and really use the definition of `relabel`

somehow.

#### Adeeb K (Apr 28 2020 at 19:19):

oh, so this means I should introduce a lemma

#### Reid Barton (Apr 28 2020 at 19:20):

So I think this means in your paper proof you are implicitly assuming something which is "obvious" about the behavior of `relabel`

, and you should figure out what it is and formulate it as a lemma.

#### Adeeb K (Apr 28 2020 at 19:20):

if (relabel m k p) x = (relabel m k p) y

then x, y <= k or x, y > k

#### Adeeb K (Apr 28 2020 at 19:22):

suppose not - then WLOG there exists x, y such that x <= k and y > k, but then ((relabel m k p) x).1 = x - 1 < k <= y = ((relabel m k p) y).2

#### Adeeb K (Apr 28 2020 at 19:22):

contradiction, so no such pair exist?

#### Adeeb K (Apr 28 2020 at 19:22):

though I made a leap here

#### Adeeb K (Apr 28 2020 at 19:23):

I assumed then x, y <= k or x, y > k if and only if !(x <= k and y > k)

#### Reid Barton (Apr 28 2020 at 19:23):

This is not the correct formula for `relabel`

#### Reid Barton (Apr 28 2020 at 19:25):

It is a good general direction though.

#### Adeeb K (Apr 28 2020 at 19:26):

what's not the correct formula?

#### Adeeb K (Apr 28 2020 at 19:27):

oh, the way I split it up?

#### Reid Barton (Apr 28 2020 at 19:27):

((relabel m k p) x).1 = x - 1 < k <= y = ((relabel m k p) y).2

#### Adeeb K (Apr 28 2020 at 19:27):

oh right right

#### Adeeb K (Apr 28 2020 at 19:27):

other way around

#### Adeeb K (Apr 28 2020 at 19:28):

((relabel m k p) x).1 = x <= k <= y = ((relabel m k p) y).2

which means either ((relabel m k p) x).1 < ((relabel m k p) y).2, contradiction

#### Adeeb K (Apr 28 2020 at 19:28):

or ((relabel m k p) x).1 = ((relabel m k p) y).2 = k, contradiction by `miss_proof`

#### Adeeb K (Apr 28 2020 at 19:36):

I wrote down the statement of the lemma:

#### Adeeb K (Apr 28 2020 at 19:36):

```
lemma relabel_behavior
(m k : ℕ)
(p: k < m)
{pf} (miss: ∀ j : finite_subset m, (relabel m k p) j ≠ ⟨k, pf⟩ )
: ∀ x y : finite_subset m, (x.1 ≤ k ∧ y.1 ≤ k) ∨ (x.1 > k ∧ y.1 > k)
:=
begin
sorry
end
```

#### Adeeb K (Apr 28 2020 at 19:37):

Not sure how to translate the proof above into lean - I imagine it would use a lot of transitivity of inequalities?

#### Reid Barton (Apr 28 2020 at 19:39):

Well this lemma is true but useless, because `miss`

is just false.

#### Adeeb K (Apr 28 2020 at 19:40):

it is?

#### Adeeb K (Apr 28 2020 at 19:43):

wait, how? If I have an injective function `f`

from `{0, 1, ..., m + 1}`

to `{0, 1, ..., m }`

(no such function exists, but this is a lemma that helps me set up the conclusion to pigeonhole by assuming such an injective function exists in the first place), and I restrict my domain to `{0, 1, ..., m }`

instead, then there is no element in the domain that will equal `f(m + 1)`

since `f`

is injective

#### Reid Barton (Apr 28 2020 at 19:43):

There is no `f`

in the statement of `relabel_behavior`

.

#### Adeeb K (Apr 28 2020 at 19:43):

oh right..

#### Reid Barton (Apr 28 2020 at 19:44):

But, something like it is true and useful.

#### Adeeb K (Apr 28 2020 at 19:44):

I'm not sure I see it?

#### Patrick Massot (Apr 28 2020 at 19:44):

Adeeb, it seems you should think much more seriously about the proof on paper.

#### Adeeb K (Apr 28 2020 at 19:46):

I (believe) I understand the proof, but there are a bunch of steps I think I didn't write out explicitly since they felt ''obvious''

#### Patrick Massot (Apr 28 2020 at 19:46):

But you're here to unlearn that feeling, right?

#### Adeeb K (Apr 28 2020 at 19:47):

yes

#### Reid Barton (Apr 28 2020 at 19:47):

Patrick, you make it sound like The Matrix

#### Patrick Massot (Apr 28 2020 at 19:48):

Lean: the red pill.

#### Adeeb K (Apr 28 2020 at 19:48):

Okay, so `miss`

is not true simply because if `k < m - 1`

then `k + 1 < m`

, which means that there is in fact an element for which `relabel m k p j = <k, pf>`

#### Adeeb K (Apr 28 2020 at 19:50):

and I probably don't really care about `miss`

in the first place

#### Adeeb K (Apr 28 2020 at 19:50):

what I care about is showing that either `x, y <= k`

or `x, y > k`

#### Adeeb K (Apr 28 2020 at 19:51):

So what I have now is:

```
lemma relabel_behavior
(m k : ℕ)
(p: k < m)
: ∀ x y : finite_subset m, (x.1 ≤ k ∧ y.1 ≤ k) ∨ (x.1 > k ∧ y.1 > k)
:=
begin
sorry
end
```

#### Adeeb K (Apr 28 2020 at 19:52):

is this the full 'useful' statement, or is there another detail I'm missing?

#### Adeeb K (Apr 28 2020 at 19:52):

wait wait wait one second

#### Adeeb K (Apr 28 2020 at 19:53):

sorry I meant this:

#### Adeeb K (Apr 28 2020 at 19:53):

```
lemma relabel_behavior
(m k : ℕ)
(p: k < m)
: ∀ x y : finite_subset m,
(relabel m k p) x = (relabel m k p) y
→ (x.1 ≤ k ∧ y.1 ≤ k) ∨ (x.1 > k ∧ y.1 > k)
:=
begin
sorry
end
```

#### Reid Barton (Apr 28 2020 at 19:54):

It's getting closer but still not correct.

#### Adeeb K (Apr 28 2020 at 19:54):

is there something I'm missing or am I asserting something that's too strong?

#### Reid Barton (Apr 28 2020 at 19:56):

Does the statement look true to you? Forget about the pigeonhole proof.

#### Adeeb K (Apr 28 2020 at 19:58):

uh I think it probably doesn't match the way I have relabel defined

#### Adeeb K (Apr 28 2020 at 19:58):

so it would be better like this:

#### Adeeb K (Apr 28 2020 at 19:58):

```
lemma relabel_behavior
(m k : ℕ)
(p: k < m)
: ∀ x y : finite_subset m,
(relabel m k p) x = (relabel m k p) y
→ (x.1 ≤ k ∧ y.1 ≤ k) ∨ (x.1 ≥ k ∧ y.1 ≥ k)
:=
begin
sorry
end
```

#### Adeeb K (Apr 28 2020 at 19:59):

is this closer?

#### Adeeb K (Apr 28 2020 at 20:00):

which is really 3 cases?

#### Adeeb K (Apr 28 2020 at 20:02):

Is there something really big and obvious that I'm missing, or is it more subtle?

#### Reid Barton (Apr 28 2020 at 20:03):

I think it is okay now.

#### Adeeb K (Apr 28 2020 at 20:04):

alright, cool! Then...I'm not sure how to start after maybe an `intros`

or `introv`

#### Adeeb K (Apr 28 2020 at 20:08):

I `introv p`

, which gives me the following window:

#### Adeeb K (Apr 28 2020 at 20:08):

```
1 goal
m k : ℕ,
p : k < m,
x y : finite_subset m,
p : relabel m k p x = relabel m k p y
⊢ x.fst ≤ k ∧ y.fst ≤ k ∨ x.fst ≥ k ∧ y.fst ≥ k
```

#### Adeeb K (Apr 28 2020 at 20:09):

how can I split the goal?

#### Adeeb K (Apr 28 2020 at 20:15):

actually, I'm sort of lost as to how I would get cases to examine the `relabel m k p x`

in the first place

#### Adeeb K (Apr 28 2020 at 20:36):

wait, would split_ifs help me here to split the goal or split the cases for relabel's output?

#### Kevin Buzzard (Apr 28 2020 at 20:42):

Adeeb K said:

how can I split the goal?

Have you read Theorem Proving In Lean or played the natural number game? If you don't know what to do with a goal which is just logical connectives and propositions then perhaps you've bitten off more than you can chew.

#### Reid Barton (Apr 28 2020 at 20:45):

Well, I don't think the NNG covers `if`

, does it?

#### Kevin Buzzard (Apr 28 2020 at 20:46):

I thought the question was what to do with `x.fst ≤ k ∧ y.fst ≤ k ∨ x.fst ≥ k ∧ y.fst ≥ k`

?

#### Adeeb K (Apr 28 2020 at 20:47):

Well, I'm sort of asking about both. I'm wondering how I can split up `relabel m k p x`

into cases for its output

#### Kevin Buzzard (Apr 28 2020 at 20:47):

@Adeeb K if you read the documentation for `split_ifs`

you will see exactly what it does.

#### Adeeb K (Apr 28 2020 at 20:47):

as for `x.fst ≤ k ∧ y.fst ≤ k ∨ x.fst ≥ k ∧ y.fst ≥ k`

I'll do more of the natural number game - I think I got 3-4 worlds in my last time

#### Kevin Buzzard (Apr 28 2020 at 20:47):

In particular, `split_ifs`

will only work if it can see an `if`

#### Adeeb K (Apr 28 2020 at 20:48):

and I should be able to apply it to a statement that isn't the goal?

#### Kevin Buzzard (Apr 28 2020 at 20:48):

Kevin Buzzard said:

Adeeb K if you read the documentation for

`split_ifs`

you will see exactly what it does.

#### Adeeb K (Apr 28 2020 at 20:49):

but I keep getting errors when I do so..

#### Kevin Buzzard (Apr 28 2020 at 20:49):

Kevin Buzzard said:

In particular,

`split_ifs`

will only work if it can see an`if`

#### Adeeb K (Apr 28 2020 at 20:51):

relabel is defined with an if-then-else and starts with an if. Do you mean I have to manually put the if into my expression?

#### Kevin Buzzard (Apr 28 2020 at 20:52):

Yes, it really need to be able to see an if. Can you unfold?

#### Kevin Buzzard (Apr 28 2020 at 20:54):

Some tactics work up to definitional equality, and some up to syntactic equality. In other words, some tactics will be fine if what you point them at is equal by definition to what they're expecting (e.g. `exact`

) but others will only work if what you point them at is literally the string of characters they are expecting (e.g. `rw`

or `split_ifs`

).

#### Adeeb K (Apr 28 2020 at 20:54):

I get an error for the simplify tactic failing to simplify when I `unfold at p2`

#### Kevin Buzzard (Apr 28 2020 at 20:54):

`unfold at p2`

doesn't make any sense

#### Kevin Buzzard (Apr 28 2020 at 20:54):

https://leanprover-community.github.io/mathlib_docs/tactics.html#unfold

#### Adeeb K (Apr 28 2020 at 20:56):

okay, I just read through `unfold`

. I'm not sure how to use it in this case, or what my constants as arguments would be in this case.

#### Johan Commelin (Apr 28 2020 at 20:58):

What is `p2`

?

#### Adeeb K (Apr 28 2020 at 20:58):

`p2 : relabel m k p x = relabel m k p y`

#### Johan Commelin (Apr 28 2020 at 20:59):

Did you mean `unfold relabel at p2`

?

#### Reid Barton (Apr 28 2020 at 20:59):

The documentation is written in such jargon that someone who understands it would probably already know how to use `unfold`

.

More useful would be an example or links to TPIL or similar.

#### Adeeb K (Apr 28 2020 at 21:00):

oh, that makes sense

sorry I wasn't seeing it earlier..

#### Kevin Buzzard (Apr 28 2020 at 21:01):

Yes, the documentation is a bit crappy for unfold :-/

#### Kevin Buzzard (Apr 28 2020 at 21:01):

The core tactics were only recently documented.

#### Kevin Buzzard (Apr 28 2020 at 21:07):

[makes a note to PR better docs for `unfold`

]

#### Adeeb K (Apr 28 2020 at 21:14):

thanks again

#### Adeeb K (Apr 28 2020 at 21:14):

I'll chew on some of the cases before asking for help with the main theorem

#### Adeeb K (Apr 29 2020 at 00:05):

okay right now I have two cases: `nat.sub k 0 < x.fst`

and `nat.sub k 0 = x.fst`

#### Adeeb K (Apr 29 2020 at 00:05):

suppose `p : nat.sub k 0 < x.fst`

. Is there a tactic that lets me conclude `k < x.fst`

?

#### Kenny Lau (Apr 29 2020 at 00:08):

`rw nat.sub_zero at p`

#### Adeeb K (Apr 29 2020 at 00:15):

```
rewrite tactic failed, did not find instance of the pattern in the target expression
?m_1 - 0
```

#### Kenny Lau (Apr 29 2020 at 00:15):

`erw nat.sub_zero at p`

#### Adeeb K (Apr 29 2020 at 00:16):

it still has the same error

#### Kenny Lau (Apr 29 2020 at 00:16):

`change k - 0 < x.1 at p; rw nat.sub_zero at p`

#### Kenny Lau (Apr 29 2020 at 00:17):

actually

#### Kenny Lau (Apr 29 2020 at 00:17):

`change k < x.1 at p`

#### Adeeb K (Apr 29 2020 at 00:20):

```
match failed
```

#### Adeeb K (Apr 29 2020 at 00:20):

I have *no* idea what's going on..

#### Kenny Lau (Apr 29 2020 at 00:20):

MWE

#### Adeeb K (Apr 29 2020 at 00:20):

sure thing

#### Adeeb K (Apr 29 2020 at 00:22):

```
import tactic
lemma inequality_fact
(j m : ℕ)
(p: j < m)
: j - 1 < m - 1
:= begin
intros,
sorry
end
lemma ext_iff (n : ℕ) (a b : finite_subset n) : a = b ↔ a.1 = b.1 :=
begin
cases a,
cases b,
split,
{ intro h, rw h},
{ intro h, cases h, refl,}
end
lemma relabel_behavior
(m k : ℕ)
(p: k < m)
: ∀ x y : finite_subset m,
(relabel m k p) x = (relabel m k p) y
→ (x.1 ≤ k ∧ y.1 ≤ k) ∨ (x.1 ≥ k ∧ y.1 ≥ k)
:=
begin
introv p2,
unfold relabel at p2,
split_ifs at p2,
{ left,
split,
exact h,
exact h_1,
},
{
right,
split,
{
cases lt_or_eq_of_le h,
{
let q := le_of_not_ge h_1,
cases lt_or_eq_of_le q,
{ exfalso,
let h4 := inequality_fact k y.fst h_3,
rw ext_iff at p2,
change x.fst = y.fst - 1 at p2,
let p2refl := eq.symm p2,
rw p2refl at h4,
let rw_h4 := nat.le_of_pred_lt h4,
change k < x.fst at rw_h4,
cases lt_or_eq_of_le rw_h4,
{linarith,},
{},
--change k ≤ x.fst at h4,
sorry},
{
sorry},
}, --contradiction case
{
exact le_of_eq (eq.symm h_2),
},
},
exact le_of_not_ge h_1,
},
{
right,
split,
exact le_of_not_ge h,
-- same proof but symmetric
{sorry
},
},
{
right,
split,
exact le_of_not_ge h,
exact le_of_not_ge h_1,
},
end
```

#### Adeeb K (Apr 29 2020 at 00:23):

my problem is right above `cases lt_or_eq_of_le rw_h4,`

#### Kenny Lau (Apr 29 2020 at 00:26):

`inequality_fact`

is wrong (j=0, m=1)`finite_subset`

doesn't exist`relabel`

doesn't exist

#### Kenny Lau (Apr 29 2020 at 00:28):

in the definition of `finite_subset`

:

```
def finite_subset (n : ℕ) := Σ' k, k < n
```

there's no need to use `Σ'`

: `Σ`

by itself would be fine

#### Mario Carneiro (Apr 29 2020 at 00:29):

not there

#### Mario Carneiro (Apr 29 2020 at 00:29):

you need `{k // k < n}`

there

#### Adeeb K (Apr 29 2020 at 00:32):

ooh shoot lemme give the remaining code. For `inequality_fact`

I'm aware there's a small error for the 0 case, but I was going to go back and prove the fixed version after I finished the main lemma

#### Adeeb K (Apr 29 2020 at 00:32):

I'll paste the code here again:

#### Mario Carneiro (Apr 29 2020 at 00:33):

The correct version of `inequality_fact`

is `nat.sub_lt_sub_right_iff`

#### Adeeb K (Apr 29 2020 at 00:34):

```
import tactic
def finite_subset (n : ℕ) := Σ' k, k < n
lemma inequality_fact
(j m : ℕ)
(p: j < m)
: j - 1 < m - 1
:= begin
intros,
sorry
end
lemma ext_iff (n : ℕ) (a b : finite_subset n) : a = b ↔ a.1 = b.1 :=
begin
cases a,
cases b,
split,
{ intro h, rw h},
{ intro h, cases h, refl,}
end
def relabel
(m k : ℕ)
(p: k < m)
: finite_subset m → finite_subset (m - 1)
:= λ j, if H : j.1 ≤ k then ⟨j.1, my_le_trans j.1 k m p H ⟩ else ⟨j.1 - 1, inequality_fact j.1 m j.2⟩
lemma relabel_behavior
(m k : ℕ)
(p: k < m)
: ∀ x y : finite_subset m,
(relabel m k p) x = (relabel m k p) y
→ (x.1 ≤ k ∧ y.1 ≤ k) ∨ (x.1 ≥ k ∧ y.1 ≥ k)
:=
begin
introv p2,
unfold relabel at p2,
split_ifs at p2,
{ left,
split,
exact h,
exact h_1,
},
{
right,
split,
{
cases lt_or_eq_of_le h,
{
let q := le_of_not_ge h_1,
cases lt_or_eq_of_le q,
{ exfalso,
let h4 := inequality_fact k y.fst h_3,
rw ext_iff at p2,
change x.fst = y.fst - 1 at p2,
let p2refl := eq.symm p2,
rw p2refl at h4,
let rw_h4 := nat.le_of_pred_lt h4,
change k < x.fst at rw_h4,
cases lt_or_eq_of_le rw_h4,
{linarith,},
{},
--change k ≤ x.fst at h4,
sorry},
{
sorry},
}, --contradiction case
{
exact le_of_eq (eq.symm h_2),
},
},
exact le_of_not_ge h_1,
},
{
right,
split,
exact le_of_not_ge h,
-- same proof but symmetric
{sorry
},
},
{
right,
split,
exact le_of_not_ge h,
exact le_of_not_ge h_1,
},
end
```

#### Adeeb K (Apr 29 2020 at 00:34):

@Mario Carneiro I'll substitute that in and modify accordingly then. Thanks!

#### Kenny Lau (Apr 29 2020 at 00:36):

the answer to the `nat.sub x 0`

is that you used `let`

instead of `have`

:

```
have rw_h4 := nat.le_of_pred_lt h4,
change k ≤ x.1 at rw_h4,
```

#### Kenny Lau (Apr 29 2020 at 00:36):

(also it was `\le`

not `<`

)

#### Adeeb K (Apr 29 2020 at 00:39):

okay! give me a second to change it

#### Kenny Lau (Apr 29 2020 at 00:44):

```
import tactic
lemma inequality_fact (j m : ℕ) (h : j < m) : j - 1 < m - 1 := sorry
def finite_subset (n : ℕ) := { k // k < n }
def relabel (m k : ℕ) (h : k < m) (j : finite_subset m) : finite_subset (m - 1) :=
if H : j.1 ≤ k then ⟨j.1, sorry⟩ else ⟨j.1 - 1, sorry⟩
lemma ext_iff (n : ℕ) (a b : finite_subset n) : a = b ↔ a.1 = b.1 :=
subtype.ext
lemma relabel_behavior (m k : ℕ) (h : k < m) (x y : finite_subset m) (hxy : relabel m k h x = relabel m k h y) :
(x.1 ≤ k ∧ y.1 ≤ k) ∨ (x.1 ≥ k ∧ y.1 ≥ k) :=
begin
unfold relabel at hxy,
split_ifs at hxy with hxk hyk hyk,
{ left; split; assumption },
{ right; split,
{ rw subtype.mk_eq_mk at hxy,
cases lt_or_eq_of_le hxk with hxlk hxek,
{ rw hxy at hxlk, exact absurd (nat.le_of_pred_lt hxlk) hyk },
{ exact ge_of_eq hxek } },
{ exact le_of_not_ge hyk } },
{ right; split,
{ exact le_of_not_ge hxk },
{ rw subtype.mk_eq_mk at hxy,
cases lt_or_eq_of_le hyk with hylk hyek,
{ rw ← hxy at hylk, exact absurd (nat.le_of_pred_lt hylk) hxk },
{ exact ge_of_eq hyek } } },
{ right; split; apply le_of_not_ge; assumption }
end
```

#### Kenny Lau (Apr 29 2020 at 00:44):

here's your MWE mathlib-stylized

#### Adeeb K (Apr 29 2020 at 00:48):

oh damn. Thank you so much!

#### Adeeb K (Apr 29 2020 at 01:12):

wait

#### Adeeb K (Apr 29 2020 at 01:12):

so changing the definition of `finite_subset`

introduced a few errors into my existing code. Can I give you a snippet of the stuff that has errors?

#### Kenny Lau (Apr 29 2020 at 01:12):

change `x.fst`

to `x.1`

#### Adeeb K (Apr 29 2020 at 01:13):

the errors don't pertain to that, at least not as far as I can tell?

#### Adeeb K (Apr 29 2020 at 01:13):

Here, lemme get an example

#### Adeeb K (Apr 29 2020 at 01:17):

```
import tactic
def injective {X Y} (f : X → Y) := ∀ x₁ x₂, f x₁ = f x₂ → x₁ = x₂
def finite_subset (n : ℕ) := { k // k < n }
def lift_finite (m n : ℕ) (p : m < n) : finite_subset m → finite_subset n
:= λ k, ⟨k.1, lt.trans k.2 p⟩
theorem lift_finite_injective (m n : ℕ) (p : m < n) :
injective (lift_finite m n p)
:= begin
introv x p2,
cases x,
cases x₂,
cases p2,
refl,
end
```

#### Adeeb K (Apr 29 2020 at 01:18):

here there is an error at `cases p2,`

#### Adeeb K (Apr 29 2020 at 01:18):

the error is: `cases tactic failed, unexpected failure when introducing auxiliary equatilies`

#### Reid Barton (Apr 29 2020 at 01:20):

I wonder why it ever worked.

#### Reid Barton (Apr 29 2020 at 01:20):

Anyways, I wouldn't recommend changing your definitions in the middle of working on a huge proof...

#### Kenny Lau (Apr 29 2020 at 01:20):

hmm I wonder why it doesn't work in this case

#### Adeeb K (Apr 29 2020 at 01:24):

it seems only this proof was affected. Luckily, no other proofs were affected ( as far as I can tell based on a glance at the errors)

#### Reid Barton (Apr 29 2020 at 01:24):

By the way, where did you learn `introv`

? I've never seen anyone else use it.

#### Adeeb K (Apr 29 2020 at 01:26):

I was browsing the mathlib section looking at `intro`

and `intros`

. This tactic appeared right after those, so I checked it out.

#### Adeeb K (Apr 29 2020 at 01:40):

I'm not sure how to fix `lift_finite_injective`

#### Reid Barton (Apr 29 2020 at 01:41):

Use Kevin's helpful `ext_iff`

lemma.

#### Reid Barton (Apr 29 2020 at 01:41):

This is its time to shine.

#### Adeeb K (Apr 29 2020 at 01:51):

okay, I'll try it

#### Adeeb K (Apr 29 2020 at 02:06):

okay, it did the trick

#### Adeeb K (Apr 29 2020 at 02:07):

```
theorem lift_finite_injective (m n : ℕ) (p : m < n) :
injective (lift_finite m n p)
:= begin
introv x p2,
cases x,
cases x₂,
rw ext_iff at p2,
exact (ext_iff m ⟨x_val, x_property⟩ ⟨x₂_val, x₂_property⟩).mpr p2,
end
```

#### Reid Barton (Apr 29 2020 at 02:11):

Okay. May I suggest:

```
theorem lift_finite_injective (m n : ℕ) (p : m < n) :
injective (lift_finite m n p) :=
begin
intros x₁ x₂ h,
rw ext_iff at ⊢ h,
exact h
end
```

#### Adeeb K (Apr 29 2020 at 02:12):

lemme try that

#### Adeeb K (Apr 29 2020 at 02:12):

it works!

#### Adeeb K (Apr 29 2020 at 02:12):

thank you! I'll examine the differences at these two approaches later tonight

#### Adeeb K (Apr 29 2020 at 02:13):

Right now, my plan is this:

#### Adeeb K (Apr 29 2020 at 02:16):

from `relabel_behavior`

, I know that `relabel m k p f (x_l) = relabel m k p f (y_l)`

implies `f (x_1) <= k`

and `f (y_1) <= k`

, or `f (x_1) >= k`

and `f (y_1) >= k`

#### Adeeb K (Apr 29 2020 at 02:18):

I want to make a lemma where `z <= k`

implies `(relabel m k p) z = < z, z < m>`

#### Adeeb K (Apr 29 2020 at 02:18):

and another where `z >= k`

implies `(relabel m k p) z = < z - 1, z - 1 < m >`

#### Adeeb K (Apr 29 2020 at 02:18):

this shouldn't be too hard based on the definition of `relabel`

, right?

#### Adeeb K (Apr 29 2020 at 02:31):

actually...I'm not sure how to start

#### Adeeb K (Apr 29 2020 at 08:03):

to repeat the latest from the noob questions thread

#### Adeeb K (Apr 29 2020 at 08:03):

I see. I'm getting an error from the following:

```
let h1_strict := lt_of_le_of_ne h1 m_x,
```

which is giving me the error:

```
type mismatch at application
lt_of_le_of_ne h1 m_x
term
m_x
has type
¬((f ∘ lift_one (m + 1)) x).val = (f ⟨m + 1, _⟩).val
but is expected to have type
(f ⟨m + 1, _⟩).val ≠ (f (lift_one (m + 1) x)).val
```

#### Kenny Lau (Apr 29 2020 at 08:04):

read the error

#### Adeeb K (Apr 29 2020 at 08:04):

...I have to flip the equality?

#### Mario Carneiro (Apr 29 2020 at 08:05):

`eq.symm`

or `ne.symm`

#### Adeeb K (Apr 29 2020 at 08:05):

ah, thank you

#### Adeeb K (Apr 29 2020 at 08:09):

@Kenny Lau I still don't understand how to use `dif_neg`

here now that I have proofs for `(f ⟨m + 1, _⟩).val < (f (lift_one (m + 1) x)).val`

and `(f ⟨m + 1, _⟩).val < (f (lift_one (m + 1) y)).val`

#### Kenny Lau (Apr 29 2020 at 08:10):

Kenny Lau said:

`have hnk : \not k \le ...,`

Kenny Lau said:

and after you prove it,

`rw dif_neg hnk`

#### Adeeb K (Apr 29 2020 at 08:10):

I'm getting an error. should I send an MWE?

#### Adeeb K (Apr 29 2020 at 08:13):

Here it is @Kenny Lau

```
import tactic
def injective {X Y} (f : X → Y) := ∀ x₁ x₂, f x₁ = f x₂ → x₁ = x₂
lemma succ_greater_than_nat (n : ℕ) : nat.succ n > n := sorry
def finite_subset (n : ℕ) := { k // k < n }
def lift_finite (m n : ℕ) (p : m < n) : finite_subset m → finite_subset n :=
λ k, ⟨k.1, lt.trans k.2 p⟩
def lift_one (m : ℕ) : finite_subset m → finite_subset (m + 1) := (lift_finite m (m+1) (succ_greater_than_nat m))
theorem lift_finite_injective (m n : ℕ) (p : m < n) : injective (lift_finite m n p) := sorry
lemma lift_one_injective (m : ℕ) : injective (lift_one m) := sorry
def relabel (m k : ℕ) (h : k < m) (j : finite_subset m) : finite_subset (m - 1) :=
if H : j.1 ≤ k then ⟨j.1, sorry⟩ else ⟨j.1 - 1, sorry⟩
lemma apply_relabel_lt (m k : ℕ) (hkm : k < m) (z : finite_subset m) (h2 : z.1 ≤ k) (h3 : z.1 < m - 1) : relabel m k hkm z = ⟨z.1, h3⟩ := sorry
lemma apply_relabel_gt (m k : ℕ) (hkm : k < m) (z : finite_subset m) (h2 : k < z.1) (h3 : z.1 - 1 < m - 1) : relabel m k hkm z = ⟨z.1 - 1, h3⟩ := sorry
lemma relabel_behavior (m k : ℕ) (h : k < m) (x y : finite_subset m) (hxy : relabel m k h x = relabel m k h y) : (x.1 ≤ k ∧ y.1 ≤ k) ∨ (x.1 ≥ k ∧ y.1 ≥ k) := sorry
lemma relabel_inj (m k : ℕ) (hkm : k < m + 1)
(f: finite_subset (m + 2) → finite_subset (m + 1))
(inj : injective f)
(pf : (f ⟨ m + 1, succ_greater_than_nat (m + 1)⟩ ).1 < m + 1)
(miss : ∀ j : finite_subset (m + 1), (f ∘ lift_one (m + 1)) j ≠ f ⟨m + 1, succ_greater_than_nat (m + 1)⟩ ) :
injective ((relabel (m + 1) (f ⟨m + 1, succ_greater_than_nat (m + 1)⟩).1 pf) ∘ f ∘ lift_one (m + 1)) :=
begin
intros x y h,
change (relabel (m + 1) (f ⟨ m + 1, succ_greater_than_nat (m + 1)⟩ ).1 pf (f (lift_one (m + 1) x))) = (relabel (m + 1) (f ⟨ m + 1, succ_greater_than_nat (m + 1)⟩ ).1 pf (f (lift_one (m + 1) y))) at h,
rcases relabel_behavior _ _ _ _ _ h with ⟨h1, h2⟩ | ⟨h1, h2⟩; unfold relabel at h,
{ sorry },
{
have m_x := (miss x),
replace m_x := mt subtype.eq m_x,
have m_y := (miss y),
replace m_y := mt subtype.eq m_y,
let h1_strict := lt_of_le_of_ne h1 (ne.symm m_x),
let h2_strict := lt_of_le_of_ne h2 (ne.symm m_y),
rw dif_neg h1_strict, --type mismatch at application dif_neg h1_strict
sorry },
end
```

#### Kenny Lau (Apr 29 2020 at 08:14):

what is the error

#### Adeeb K (Apr 29 2020 at 08:14):

```
type mismatch at application
dif_neg h1_strict
term
h1_strict
has type
(f ⟨m + 1, _⟩).val < (f (lift_one (m + 1) x)).val
but is expected to have type
¬?m_1
```

#### Kenny Lau (Apr 29 2020 at 08:14):

read the error

#### Kenny Lau (Apr 29 2020 at 08:14):

and read what I told you

#### Kenny Lau (Apr 29 2020 at 08:15):

Kenny Lau said:

`have hnk : \not k \le ...,`

Kenny Lau said:

and after you prove it,

`rw dif_neg hnk`

#### Kenny Lau (Apr 29 2020 at 08:15):

you need to prove `\not k \le ...`

#### Kenny Lau (Apr 29 2020 at 08:15):

first of all there's not even a `k`

in the `h1_strict`

#### Kenny Lau (Apr 29 2020 at 08:16):

also stop abbreviating terms

#### Adeeb K (Apr 29 2020 at 08:16):

what abbreviating?

#### Kenny Lau (Apr 29 2020 at 08:16):

`have m_x := (miss x),`

#### Kenny Lau (Apr 29 2020 at 08:16):

I retract my comment about `k`

#### Adeeb K (Apr 29 2020 at 08:16):

alright

#### Kenny Lau (Apr 29 2020 at 08:17):

```
type mismatch at application
dif_neg h1_strict
term
h1_strict
has type
(f ⟨m + 1, _⟩).val < (f (lift_one (m + 1) x)).val
but is expected to have type
¬?m_1
state:
m k : ℕ,
hkm : k < m + 1,
f : finite_subset (m + 2) → finite_subset (m + 1),
inj : injective f,
pf : (f ⟨m + 1, _⟩).val < m + 1,
miss : ∀ (j : finite_subset (m + 1)), (f ∘ lift_one (m + 1)) j ≠ f ⟨m + 1, _⟩,
x y : finite_subset (m + 1),
h1 : (f (lift_one (m + 1) x)).val ≥ (f ⟨m + 1, _⟩).val,
h2 : (f (lift_one (m + 1) y)).val ≥ (f ⟨m + 1, _⟩).val,
h :
dite ((f (lift_one (m + 1) x)).val ≤ (f ⟨m + 1, _⟩).val)
(λ (H : (f (lift_one (m + 1) x)).val ≤ (f ⟨m + 1, _⟩).val), ⟨(f (lift_one (m + 1) x)).val, _⟩)
(λ (H : ¬(f (lift_one (m + 1) x)).val ≤ (f ⟨m + 1, _⟩).val), ⟨(f (lift_one (m + 1) x)).val - 1, _⟩) =
dite ((f (lift_one (m + 1) y)).val ≤ (f ⟨m + 1, _⟩).val)
(λ (H : (f (lift_one (m + 1) y)).val ≤ (f ⟨m + 1, _⟩).val), ⟨(f (lift_one (m + 1) y)).val, _⟩)
(λ (H : ¬(f (lift_one (m + 1) y)).val ≤ (f ⟨m + 1, _⟩).val), ⟨(f (lift_one (m + 1) y)).val - 1, _⟩),
m_x : ¬((f ∘ lift_one (m + 1)) x).val = (f ⟨m + 1, _⟩).val,
m_y : ¬((f ∘ lift_one (m + 1)) y).val = (f ⟨m + 1, _⟩).val,
h1_strict : (f ⟨m + 1, _⟩).val < (f (lift_one (m + 1) x)).val := lt_of_le_of_ne h1 (ne.symm m_x),
h2_strict : (f ⟨m + 1, _⟩).val < (f (lift_one (m + 1) y)).val := lt_of_le_of_ne h2 (ne.symm m_y)
⊢ x = y
```

#### Kenny Lau (Apr 29 2020 at 08:17):

because this time the clause in the `dite`

is `(f (lift_one (m + 1) x)).val ≤ (f ⟨m + 1, _⟩).val`

#### Kenny Lau (Apr 29 2020 at 08:17):

so you need to prove `¬(f (lift_one (m + 1) x)).val ≤ (f ⟨m + 1, _⟩).val`

#### Kenny Lau (Apr 29 2020 at 08:17):

which to you is equivalent to `... > ...`

#### Kenny Lau (Apr 29 2020 at 08:18):

but to Lean they are not definitionally equivalent

#### Adeeb K (Apr 29 2020 at 08:19):

would `not_le.mpr ((f (lift_one (m + 1) x)).val ≤ (f ⟨m + 1, _⟩).val)`

give me what I'm looking for?

#### Kenny Lau (Apr 29 2020 at 08:20):

oh and I retract my comment about `miss x`

being an abbreviation

#### Adeeb K (Apr 29 2020 at 08:20):

I library searched for a function after writing a small lemma, and that is what I got:

```
lemma lib
(x y : ℕ)
(p: x > y)
: ¬ x ≤ y
:= begin
exact not_le.mpr p,
end
```

#### Kenny Lau (Apr 29 2020 at 08:20):

but your two `let`

s should bave `have`

s because they are propositions

#### Kenny Lau (Apr 29 2020 at 08:20):

basically, the principle is that if you see a `let`

in your code then you're doing something wrong

#### Kenny Lau (Apr 29 2020 at 08:21):

yeah so use it and `dif_neg`

#### Adeeb K (Apr 29 2020 at 08:21):

alright, changed them to `have`

's. I'll ask about `have`

vs `let`

tomorrow since it's pretty late and I want to finish this theorem up as soon as I can

#### Adeeb K (Apr 29 2020 at 08:21):

okay one sec

#### Adeeb K (Apr 29 2020 at 08:22):

```
rewrite tactic failed, did not find instance of the pattern in the target expression
dite ((f (lift_one (m + 1) x)).val ≤ (f ⟨m + 1, _⟩).val) ?m_2 ?m_3
```

#### Adeeb K (Apr 29 2020 at 08:22):

this is in response to typing

```
rw dif_neg (not_le.mpr h1_strict)
```

#### Kenny Lau (Apr 29 2020 at 08:23):

did you forget `at h`

#### Adeeb K (Apr 29 2020 at 08:24):

...oh whoops

#### Adeeb K (Apr 29 2020 at 08:25):

alright, I'm not sure to go from here. This is what the goal window shows:

```
1 goal
m k : ℕ,
hkm : k < m + 1,
f : finite_subset (m + 2) → finite_subset (m + 1),
inj : injective f,
pf : (f ⟨m + 1, _⟩).val < m + 1,
miss : ∀ (j : finite_subset (m + 1)), (f ∘ lift_one (m + 1)) j ≠ f ⟨m + 1, _⟩,
x y : finite_subset (m + 1),
h1 : (f (lift_one (m + 1) x)).val ≥ (f ⟨m + 1, _⟩).val,
h2 : (f (lift_one (m + 1) y)).val ≥ (f ⟨m + 1, _⟩).val,
m_x : ¬((f ∘ lift_one (m + 1)) x).val = (f ⟨m + 1, _⟩).val,
m_y : ¬((f ∘ lift_one (m + 1)) y).val = (f ⟨m + 1, _⟩).val,
h1_strict : (f ⟨m + 1, _⟩).val < (f (lift_one (m + 1) x)).val,
h2_strict : (f ⟨m + 1, _⟩).val < (f (lift_one (m + 1) y)).val,
h :
⟨(f (lift_one (m + 1) x)).val - 1, _⟩ =
dite ((f (lift_one (m + 1) y)).val ≤ (f ⟨m + 1, _⟩).val)
(λ (H : (f (lift_one (m + 1) y)).val ≤ (f ⟨m + 1, _⟩).val), ⟨(f (lift_one (m + 1) y)).val, _⟩)
(λ (H : ¬(f (lift_one (m + 1) y)).val ≤ (f ⟨m + 1, _⟩).val), ⟨(f (lift_one (m + 1) y)).val - 1, _⟩)
⊢ x = y
```

#### Adeeb K (Apr 29 2020 at 08:26):

how do I unpack the `if-then-else`

pattern for `h`

?

#### Kenny Lau (Apr 29 2020 at 08:27):

prove the same thing for `y`

and use `dif_neg`

...

#### Adeeb K (Apr 29 2020 at 08:28):

ah right right

#### Adeeb K (Apr 29 2020 at 08:30):

so if I have `h : ⟨(f (lift_one (m + 1) x)).val - 1, _⟩ = ⟨(f (lift_one (m + 1) y)).val - 1, _⟩,`

, then I can conclude that `(f (lift_one (m + 1) x)).val - 1 = (f (lift_one (m + 1) y)).val - 1`

by extensionality right?

#### Kenny Lau (Apr 29 2020 at 08:32):

right

#### Adeeb K (Apr 29 2020 at 08:36):

uh so at this point, I have basically that $q - 1 = r - 1$, where $q, r \in \mathbb{N}$. When I used `library_search`

, I came up with nothing for `q - 1 = r - 1`

implies `q = r`

.

#### Adeeb K (Apr 29 2020 at 08:36):

Is there something small (or large) that I'm missing to make that statement?

#### Kevin Buzzard (Apr 29 2020 at 08:37):

It's not true

#### Kevin Buzzard (Apr 29 2020 at 08:38):

Using subtraction on naturals is not a good idea in general

#### Adeeb K (Apr 29 2020 at 08:38):

is it because there isn't closure in the naturals under subtraction?

#### Kevin Buzzard (Apr 29 2020 at 08:38):

No, it's because by definition there is closure in the naturals under subtraction

#### Kevin Buzzard (Apr 29 2020 at 08:38):

Which means that what you're using can't be actual subtraction

#### Kevin Buzzard (Apr 29 2020 at 08:39):

0-1=1-1=0 in the naturals

#### Kevin Buzzard (Apr 29 2020 at 08:39):

According to lean

#### Adeeb K (Apr 29 2020 at 08:39):

oh I see

#### Adeeb K (Apr 29 2020 at 08:40):

uh, so based on this step...I'm stuck then?

#### Kevin Buzzard (Apr 29 2020 at 08:40):

I haven't been following the details I'm afraid

#### Adeeb K (Apr 29 2020 at 08:40):

well basically I have this:

```
h : ⟨(f (lift_one (m + 1) x)).val - 1, _⟩.val = ⟨(f (lift_one (m + 1) y)).val - 1, _⟩.val
```

#### Kevin Buzzard (Apr 29 2020 at 08:41):

I'm "at work" right now so am only glancing at the chat

#### Adeeb K (Apr 29 2020 at 08:41):

ah alright

#### Kevin Buzzard (Apr 29 2020 at 08:41):

I have a meeting in 4 minutes :-/

#### Adeeb K (Apr 29 2020 at 08:41):

ah gotcha, have fun then!

#### Adeeb K (Apr 29 2020 at 08:51):

question

#### Adeeb K (Apr 29 2020 at 08:52):

if I have `h : LHS = RHS`

, how can I assign a name to the left hand side? That is, can I have `have left_hand_side := LHS`

?

#### Adeeb K (Apr 29 2020 at 08:53):

I'm trying to say `have LHS := ⟨(f (lift_one (m + 1) x)).val - 1, _⟩`

, but I keep getting the following error:

```
invalid constructor ⟨...⟩, expected type must be known
```

#### Adeeb K (Apr 29 2020 at 09:13):

I got it

#### Adeeb K (Apr 29 2020 at 09:13):

another question though:

#### Adeeb K (Apr 29 2020 at 09:14):

Suppose I have `h_jump : (f (lift_one (m + 1) x)).val = (f (lift_one (m + 1) y)).val`

. And I also have the extensionality theorem:

```
lemma ext_iff (n : ℕ) (a b : finite_subset n) : a = b ↔ a.1 = b.1 :=
begin
cases a,
cases b,
split,
{ intro h, rw h},
{ intro h, cases h, refl,}
end
```

#### Adeeb K (Apr 29 2020 at 09:15):

how would I conclude that `(f (lift_one (m + 1) x)) = (f (lift_one (m + 1) y))`

?

#### Kenny Lau (Apr 29 2020 at 09:15):

`rw \l ext_iff`

#### Adeeb K (Apr 29 2020 at 09:16):

oh, so the `\l`

just says to use the implication in the other direction then?

#### Kenny Lau (Apr 29 2020 at 09:18):

right

#### Kevin Buzzard (Apr 29 2020 at 09:55):

Deleted

#### Adeeb K (Apr 29 2020 at 10:03):

thanks again for all the help!

Last updated: May 14 2021 at 00:42 UTC