internlm/Lean-Github huggingface dataset:
Theorem: may_extend
Proof 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
Proof 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
Theorem: may_extend
Proof 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
Proof 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
Theorem: may_extend
Proof 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
Proof state after:
no goals
Theorem: may_extend
Proof 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
Proof state after:
no goals
Theorem: may_extend
Proof 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
Proof 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
Theorem: may_extend
Proof 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⟩
Proof 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 }
Theorem: may_extend
Proof 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
Proof state after:
no goals
Theorem: may_extend
Proof 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α)
Proof 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
Theorem: may_extend
Proof 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α)
Proof 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
Theorem: may_extend
Proof 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
Proof 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
Theorem: may_extend
Proof 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'
Proof 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
Theorem: may_extend
Proof 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]
Proof 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
Theorem: may_extend
Proof 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']
Proof 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')
Theorem: may_extend
Proof 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⟩
Proof 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 }
Theorem: may_extend
Proof 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
Proof state after:
no goals
Theorem: may_extend_with'
Proof state before:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
⊢ ∃ x',
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ) ∧
      Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
          (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
        Function.Embedding.trans z (subtype s)
Tactic:
let h' := Eq.trans h (add_comm m k)
Proof state after:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
⊢ ∃ x',
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ) ∧
      Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
          (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
        Function.Embedding.trans z (subtype s)
Theorem: may_extend_with'
Proof state before:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
⊢ ∃ x',
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ) ∧
      Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
          (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
        Function.Embedding.trans z (subtype s)
Tactic:
let p := fun i : Fin n => i.val < m
Proof state after:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
⊢ ∃ x',
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ) ∧
      Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
          (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
        Function.Embedding.trans z (subtype s)
Theorem: may_extend_with'
Proof state before:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
⊢ ∃ x',
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ) ∧
      Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
          (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
        Function.Embedding.trans z (subtype s)
Tactic:
let f : {i : Fin n | p i} → α := fun i => x.toFun (Fin.castLT i.val i.prop)
Proof state after:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
⊢ ∃ x',
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ) ∧
      Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
          (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
        Function.Embedding.trans z (subtype s)
Theorem: may_extend_with'
Proof state before:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
⊢ ∃ x',
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ) ∧
      Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
          (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
        Function.Embedding.trans z (subtype s)
Tactic:
let g : {i : Fin n | ¬p i} → α := fun i =>
  z.toFun (Fin.subNat m (Fin.castIso h' i.val) (by simpa [h] using not_lt.mp (Subtype.mem i)))
Proof state after:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
⊢ ∃ x',
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ) ∧
      Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
          (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
        Function.Embedding.trans z (subtype s)
Theorem: may_extend_with'
Proof state before:
case h
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
⊢ Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding
        { toFun := fun i => if hi : p i then f { val := i, property := hi } else g { val := i, property := hi },
          inj' := ⋯ } =
      Function.Embedding.trans x (subtype sᶜ) ∧
    Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
        (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv)
          { toFun := fun i => if hi : p i then f { val := i, property := hi } else g { val := i, property := hi },
            inj' := ⋯ }) =
      Function.Embedding.trans z (subtype s)
Tactic:
constructor
Proof state after:
case h.left
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
⊢ Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding
      { toFun := fun i => if hi : p i then f { val := i, property := hi } else g { val := i, property := hi },
        inj' := ⋯ } =
    Function.Embedding.trans x (subtype sᶜ)

case h.right
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
⊢ Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv)
        { toFun := fun i => if hi : p i then f { val := i, property := hi } else g { val := i, property := hi },
          inj' := ⋯ }) =
    Function.Embedding.trans z (subtype s)
Theorem: may_extend_with'
Proof state before:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
i : ↑{i | ¬p i}
⊢ m ≤ ↑((Fin.castIso h') ↑i)
Tactic:
simpa [h] using not_lt.mp (Subtype.mem i)
Proof state after:
no goals
Theorem: may_extend_with'
Proof state before:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
⊢ Function.Injective fun i => if hi : p i then f { val := i, property := hi } else g { val := i, property := hi }
Tactic:
refine' Function.Injective.dite p _ _ _
Proof state after:
case refine'_1
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
⊢ Function.Injective f

case refine'_2
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
⊢ Function.Injective g

case refine'_3
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
⊢ ∀ {x x' : Fin n} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ g { val := x', property := hx' }
Theorem: may_extend_with'
Proof state before:
case refine'_1
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
⊢ Function.Injective f
Tactic:
rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
Proof state after:
case refine'_1.mk.mk
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
i : Fin n
hi : p i
j : Fin n
hj : p j
hij : f { val := i, property := hi } = f { val := j, property := hj }
⊢ { val := i, property := hi } = { val := j, property := hj }
Theorem: may_extend_with'
Proof state before:
case refine'_1.mk.mk
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
i : Fin n
hi : p i
j : Fin n
hj : p j
hij : f { val := i, property := hi } = f { val := j, property := hj }
⊢ { val := i, property := hi } = { val := j, property := hj }
Tactic:
simpa only [Subtype.mk_eq_mk, Fin.ext_iff] using x.inj' (Subtype.coe_injective hij)
Proof state after:
no goals
Theorem: may_extend_with'
Proof state before:
case refine'_2
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
⊢ Function.Injective g
Tactic:
rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
Proof state after:
case refine'_2.mk.mk
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
i : Fin n
hi : ¬p i
j : Fin n
hj : ¬p j
hij : g { val := i, property := hi } = g { val := j, property := hj }
⊢ { val := i, property := hi } = { val := j, property := hj }