Theorem: may_extend (Jordan/Mathlib/Extensions.lean)

State before:
α : Type u_1
m n : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
x : Fin m ↪ α
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
Tactic:
induction' n with n hrec
State after:
case zero
α : Type u_1
m : ℕ
x : Fin m ↪ α
hmn : m ≤ zero
hα : ↑zero ≤ PartENat.card α
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x

case succ
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x

State before:
case zero
α : Type u_1
m : ℕ
x : Fin m ↪ α
hmn : m ≤ zero
hα : ↑zero ≤ PartENat.card α
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
Tactic:
simp only [Nat.zero_eq, nonpos_iff_eq_zero] at hmn
State after:
case zero
α : Type u_1
m : ℕ
x : Fin m ↪ α
hmn✝ : m ≤ zero
hα : ↑zero ≤ PartENat.card α
hmn : m = 0
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn✝).toEmbedding x' = x

State before:
case zero
α : Type u_1
m : ℕ
x : Fin m ↪ α
hmn✝ : m ≤ zero
hα : ↑zero ≤ PartENat.card α
hmn : m = 0
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn✝).toEmbedding x' = x
Tactic:
let w : Fin 0 ↪ α := Function.Embedding.ofIsEmpty
State after:
case zero
α : Type u_1
m : ℕ
x : Fin m ↪ α
hmn✝ : m ≤ zero
hα : ↑zero ≤ PartENat.card α
hmn : m = 0
w : Fin 0 ↪ α := Function.Embedding.ofIsEmpty
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn✝).toEmbedding x' = x

State before:
case zero
α : Type u_1
m : ℕ
x : Fin m ↪ α
hmn✝ : m ≤ zero
hα : ↑zero ≤ PartENat.card α
hmn : m = 0
w : Fin 0 ↪ α := Function.Embedding.ofIsEmpty
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn✝).toEmbedding x' = x
Tactic:
use w
State after:
case h
α : Type u_1
m : ℕ
x : Fin m ↪ α
hmn✝ : m ≤ zero
hα : ↑zero ≤ PartENat.card α
hmn : m = 0
w : Fin 0 ↪ α := Function.Embedding.ofIsEmpty
⊢ Function.Embedding.trans (Fin.castLEEmb hmn✝).toEmbedding w = x

State before:
case h
α : Type u_1
m : ℕ
x : Fin m ↪ α
hmn✝ : m ≤ zero
hα : ↑zero ≤ PartENat.card α
hmn : m = 0
w : Fin 0 ↪ α := Function.Embedding.ofIsEmpty
⊢ Function.Embedding.trans (Fin.castLEEmb hmn✝).toEmbedding w = x
Tactic:
ext ⟨i, hi⟩
State after:
case h.h.mk
α : Type u_1
m : ℕ
x : Fin m ↪ α
hmn✝ : m ≤ zero
hα : ↑zero ≤ PartENat.card α
hmn : m = 0
w : Fin 0 ↪ α := Function.Embedding.ofIsEmpty
i : ℕ
hi : i < m
⊢ (Function.Embedding.trans (Fin.castLEEmb hmn✝).toEmbedding w) { val := i, isLt := hi } = x { val := i, isLt := hi }

State before:
case h.h.mk
α : Type u_1
m : ℕ
x : Fin m ↪ α
hmn✝ : m ≤ zero
hα : ↑zero ≤ PartENat.card α
hmn : m = 0
w : Fin 0 ↪ α := Function.Embedding.ofIsEmpty
i : ℕ
hi : i < m
⊢ (Function.Embedding.trans (Fin.castLEEmb hmn✝).toEmbedding w) { val := i, isLt := hi } = x { val := i, isLt := hi }
Tactic:
exfalso
State after:
case h.h.mk
α : Type u_1
m : ℕ
x : Fin m ↪ α
hmn✝ : m ≤ zero
hα : ↑zero ≤ PartENat.card α
hmn : m = 0
w : Fin 0 ↪ α := Function.Embedding.ofIsEmpty
i : ℕ
hi : i < m
⊢ False

State before:
case h.h.mk
α : Type u_1
m : ℕ
x : Fin m ↪ α
hmn✝ : m ≤ zero
hα : ↑zero ≤ PartENat.card α
hmn : m = 0
w : Fin 0 ↪ α := Function.Embedding.ofIsEmpty
i : ℕ
hi : i < m
⊢ False
Tactic:
rw [hmn] at hi
State after:
case h.h.mk
α : Type u_1
m : ℕ
x : Fin m ↪ α
hmn✝ : m ≤ zero
hα : ↑zero ≤ PartENat.card α
hmn : m = 0
w : Fin 0 ↪ α := Function.Embedding.ofIsEmpty
i : ℕ
hi : i < 0
⊢ False

State before:
case h.h.mk
α : Type u_1
m : ℕ
x : Fin m ↪ α
hmn✝ : m ≤ zero
hα : ↑zero ≤ PartENat.card α
hmn : m = 0
w : Fin 0 ↪ α := Function.Embedding.ofIsEmpty
i : ℕ
hi : i < 0
⊢ False
Tactic:
exact Nat.not_lt_zero i hi
State after:
no goals

State before:
case succ
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
Tactic:
cases Nat.eq_or_lt_of_le hmn with
| inl h =>
  use (Equiv.toEmbedding (Fin.castIso h.symm).toEquiv).trans x
  ext ⟨i, hi⟩
  simp
| inr h =>
  obtain ⟨y, hy⟩ :=
    hrec (Nat.le_of_lt_succ h) (le_trans (PartENat.coe_le_coe.mpr (le_succ n)) hα)
  obtain ⟨a, ha⟩ :=
    gimme_another y (lt_of_lt_of_le (PartENat.coe_lt_coe.mpr (Nat.lt_succ_self n)) hα)
  obtain ⟨x', hx', _⟩ := may_extend_with y a ha
  use x'; rw [← hy]; rw [← hx']
  ext ⟨i, hi⟩; rfl
State after:
no goals

State before:
case succ.inl
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m = succ n
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
Tactic:
use (Equiv.toEmbedding (Fin.castIso h.symm).toEquiv).trans x
State after:
case h
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m = succ n
⊢ Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x) =
    x

State before:
case h
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m = succ n
⊢ Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x) =
    x
Tactic:
ext ⟨i, hi⟩
State after:
case h.h.mk
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m = succ n
i : ℕ
hi : i < m
⊢ (Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding
        (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x))
      { val := i, isLt := hi } =
    x { val := i, isLt := hi }

State before:
case h.h.mk
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m = succ n
i : ℕ
hi : i < m
⊢ (Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding
        (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x))
      { val := i, isLt := hi } =
    x { val := i, isLt := hi }
Tactic:
simp
State after:
no goals

State before:
case succ.inr
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m < succ n
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
Tactic:
obtain ⟨y, hy⟩ :=
  hrec (Nat.le_of_lt_succ h) (le_trans (PartENat.coe_le_coe.mpr (le_succ n)) hα)
State after:
case succ.inr.intro
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m < succ n
y : Fin n ↪ α
hy : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y = x
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x

State before:
case succ.inr.intro
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m < succ n
y : Fin n ↪ α
hy : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y = x
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
Tactic:
obtain ⟨a, ha⟩ :=
  gimme_another y (lt_of_lt_of_le (PartENat.coe_lt_coe.mpr (Nat.lt_succ_self n)) hα)
State after:
case succ.inr.intro.intro
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m < succ n
y : Fin n ↪ α
hy : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y = x
a : α
ha : a ∉ Set.range ⇑y
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x

State before:
case succ.inr.intro.intro
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m < succ n
y : Fin n ↪ α
hy : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y = x
a : α
ha : a ∉ Set.range ⇑y
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
Tactic:
obtain ⟨x', hx', _⟩ := may_extend_with y a ha
State after:
case succ.inr.intro.intro.intro.intro
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m < succ n
y : Fin n ↪ α
hy : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y = x
a : α
ha : a ∉ Set.range ⇑y
x' : Fin (succ n) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = y
right✝ : x' { val := n, isLt := ⋯ } = a
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x

State before:
case succ.inr.intro.intro.intro.intro
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m < succ n
y : Fin n ↪ α
hy : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y = x
a : α
ha : a ∉ Set.range ⇑y
x' : Fin (succ n) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = y
right✝ : x' { val := n, isLt := ⋯ } = a
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
Tactic:
use x'
State after:
case h
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m < succ n
y : Fin n ↪ α
hy : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y = x
a : α
ha : a ∉ Set.range ⇑y
x' : Fin (succ n) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = y
right✝ : x' { val := n, isLt := ⋯ } = a
⊢ Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x

State before:
case h
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m < succ n
y : Fin n ↪ α
hy : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y = x
a : α
ha : a ∉ Set.range ⇑y
x' : Fin (succ n) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = y
right✝ : x' { val := n, isLt := ⋯ } = a
⊢ Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
Tactic:
rw [← hy]
State after:
case h
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m < succ n
y : Fin n ↪ α
hy : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y = x
a : α
ha : a ∉ Set.range ⇑y
x' : Fin (succ n) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = y
right✝ : x' { val := n, isLt := ⋯ } = a
⊢ Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y

State before:
case h
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m < succ n
y : Fin n ↪ α
hy : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y = x
a : α
ha : a ∉ Set.range ⇑y
x' : Fin (succ n) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = y
right✝ : x' { val := n, isLt := ⋯ } = a
⊢ Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y
Tactic:
rw [← hx']
State after:
case h
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m < succ n
y : Fin n ↪ α
hy : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y = x
a : α
ha : a ∉ Set.range ⇑y
x' : Fin (succ n) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = y
right✝ : x' { val := n, isLt := ⋯ } = a
⊢ Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' =
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x')

State before:
case h
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m < succ n
y : Fin n ↪ α
hy : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y = x
a : α
ha : a ∉ Set.range ⇑y
x' : Fin (succ n) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = y
right✝ : x' { val := n, isLt := ⋯ } = a
⊢ Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' =
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x')
Tactic:
ext ⟨i, hi⟩
State after:
case h.h.mk
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m < succ n
y : Fin n ↪ α
hy : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y = x
a : α
ha : a ∉ Set.range ⇑y
x' : Fin (succ n) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = y
right✝ : x' { val := n, isLt := ⋯ } = a
i : ℕ
hi : i < m
⊢ (Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x') { val := i, isLt := hi } =
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x'))
      { val := i, isLt := hi }

State before:
case h.h.mk
α : Type u_1
m : ℕ
x : Fin m ↪ α
n : ℕ
hrec : ∀ (hmn : m ≤ n), ↑n ≤ PartENat.card α → ∃ x', Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x' = x
hmn : m ≤ succ n
hα : ↑(succ n) ≤ PartENat.card α
h : m < succ n
y : Fin n ↪ α
hy : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y = x
a : α
ha : a ∉ Set.range ⇑y
x' : Fin (succ n) ↪ α
hx' : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = y
right✝ : x' { val := n, isLt := ⋯ } = a
i : ℕ
hi : i < m
⊢ (Function.Embedding.trans (Fin.castLEEmb hmn).toEmbedding x') { val := i, isLt := hi } =
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x'))
      { val := i, isLt := hi }
Tactic:
rfl
State after:
no goals