internlm/Lean-Github huggingface dataset:
Theorem: may_extend_with
Proof state before:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
⊢ Function.Injective fun x =>
    match x with
    | { val := val, property := property } => a
Tactic:
rintro ⟨i, hi⟩ ⟨j, hj⟩ _
Proof state after:
case mk.mk
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
i : Fin (succ n)
hi : i ∈ {i | ¬p i}
j : Fin (succ n)
hj : j ∈ {i | ¬p i}
a✝ :
  (fun x =>
        match x with
        | { val := val, property := property } => a)
      { val := i, property := hi } =
    (fun x =>
        match x with
        | { val := val, property := property } => a)
      { val := j, property := hj }
⊢ { val := i, property := hi } = { val := j, property := hj }
Theorem: may_extend_with
Proof state before:
case mk.mk
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
i : Fin (succ n)
hi : i ∈ {i | ¬p i}
j : Fin (succ n)
hj : j ∈ {i | ¬p i}
a✝ :
  (fun x =>
        match x with
        | { val := val, property := property } => a)
      { val := i, property := hi } =
    (fun x =>
        match x with
        | { val := val, property := property } => a)
      { val := j, property := hj }
⊢ { val := i, property := hi } = { val := j, property := hj }
Tactic:
simp only [Subtype.mk_eq_mk, Fin.ext_iff]
Proof state after:
case mk.mk
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
i : Fin (succ n)
hi : i ∈ {i | ¬p i}
j : Fin (succ n)
hj : j ∈ {i | ¬p i}
a✝ :
  (fun x =>
        match x with
        | { val := val, property := property } => a)
      { val := i, property := hi } =
    (fun x =>
        match x with
        | { val := val, property := property } => a)
      { val := j, property := hj }
⊢ ↑i = ↑j
Theorem: may_extend_with
Proof state before:
case mk.mk
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
i : Fin (succ n)
hi : i ∈ {i | ¬p i}
j : Fin (succ n)
hj : j ∈ {i | ¬p i}
a✝ :
  (fun x =>
        match x with
        | { val := val, property := property } => a)
      { val := i, property := hi } =
    (fun x =>
        match x with
        | { val := val, property := property } => a)
      { val := j, property := hj }
⊢ ↑i = ↑j
Tactic:
rw [Nat.eq_of_lt_succ_of_not_lt i.prop hi, Nat.eq_of_lt_succ_of_not_lt j.prop hj]
Proof state after:
no goals
Theorem: may_extend_with
Proof state before:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
⊢ Function.Injective fun i => if hi : p i then f { val := i, property := hi } else f' { val := i, property := hi }
Tactic:
apply  Function.Injective.dite p
Proof state after:
case hf
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
⊢ Function.Injective f

case hf'
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
⊢ Function.Injective ⇑f'

case im_disj
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
⊢ ∀ {x x' : Fin (succ n)} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
Theorem: may_extend_with
Proof state before:
case hf
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
⊢ Function.Injective f
Tactic:
rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
Proof state after:
case hf.mk.mk
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : Fin (succ n)
hi : p i
j : Fin (succ 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 hf.mk.mk
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : Fin (succ n)
hi : p i
j : Fin (succ n)
hj : p j
hij : f { val := i, property := hi } = f { val := j, property := hj }
⊢ { val := i, property := hi } = { val := j, property := hj }
Tactic:
rw [Subtype.mk_eq_mk]
Proof state after:
case hf.mk.mk
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : Fin (succ n)
hi : p i
j : Fin (succ n)
hj : p j
hij : f { val := i, property := hi } = f { val := j, property := hj }
⊢ i = j
Theorem: may_extend_with
Proof state before:
case hf.mk.mk
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : Fin (succ n)
hi : p i
j : Fin (succ n)
hj : p j
hij : f { val := i, property := hi } = f { val := j, property := hj }
⊢ i = j
Tactic:
apply Fin.ext
Proof state after:
case hf.mk.mk.h
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : Fin (succ n)
hi : p i
j : Fin (succ n)
hj : p j
hij : f { val := i, property := hi } = f { val := j, property := hj }
⊢ ↑i = ↑j
Theorem: may_extend_with
Proof state before:
case hf.mk.mk.h
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : Fin (succ n)
hi : p i
j : Fin (succ n)
hj : p j
hij : f { val := i, property := hi } = f { val := j, property := hj }
⊢ ↑i = ↑j
Tactic:
rw [← Fin.coe_castLT i _]
Proof state after:
case hf.mk.mk.h
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : Fin (succ n)
hi : p i
j : Fin (succ n)
hj : p j
hij : f { val := i, property := hi } = f { val := j, property := hj }
⊢ ↑(Fin.castLT i ?m.8352) = ↑j

α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : Fin (succ n)
hi : p i
j : Fin (succ n)
hj : p j
hij : f { val := i, property := hi } = f { val := j, property := hj }
⊢ ℕ

α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : Fin (succ n)
hi : p i
j : Fin (succ n)
hj : p j
hij : f { val := i, property := hi } = f { val := j, property := hj }
⊢ ↑i < ?m.8351
Theorem: may_extend_with
Proof state before:
case hf'
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
⊢ Function.Injective ⇑f'
Tactic:
exact Function.Embedding.injective f'
Proof state after:
no goals
Theorem: may_extend_with
Proof state before:
case im_disj
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
⊢ ∀ {x x' : Fin (succ n)} {hx : p x} {hx' : ¬p x'}, f { val := x, property := hx } ≠ f' { val := x', property := hx' }
Tactic:
intros
Proof state after:
case im_disj
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
x✝ x'✝ : Fin (succ n)
hx✝ : p x✝
hx'✝ : ¬p x'✝
⊢ f { val := x✝, property := hx✝ } ≠ f' { val := x'✝, property := hx'✝ }
Theorem: may_extend_with
Proof state before:
case im_disj
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
x✝ x'✝ : Fin (succ n)
hx✝ : p x✝
hx'✝ : ¬p x'✝
⊢ f { val := x✝, property := hx✝ } ≠ f' { val := x'✝, property := hx'✝ }
Tactic:
simp only [Set.coe_setOf, Set.mem_setOf_eq, toFun_eq_coe, coeFn_mk, ne_eq]
Proof state after:
case im_disj
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
x✝ x'✝ : Fin (succ n)
hx✝ : p x✝
hx'✝ : ¬p x'✝
⊢ ¬f { val := x✝, property := hx✝ } = f' { val := x'✝, property := hx'✝ }
Theorem: may_extend_with
Proof state before:
case im_disj
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
x✝ x'✝ : Fin (succ n)
hx✝ : p x✝
hx'✝ : ¬p x'✝
⊢ ¬f { val := x✝, property := hx✝ } = f' { val := x'✝, property := hx'✝ }
Tactic:
intro h
Proof state after:
case im_disj
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
x✝ x'✝ : Fin (succ n)
hx✝ : p x✝
hx'✝ : ¬p x'✝
h : f { val := x✝, property := hx✝ } = f' { val := x'✝, property := hx'✝ }
⊢ False
Theorem: may_extend_with
Proof state before:
case im_disj
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
x✝ x'✝ : Fin (succ n)
hx✝ : p x✝
hx'✝ : ¬p x'✝
h : f { val := x✝, property := hx✝ } = f' { val := x'✝, property := hx'✝ }
⊢ False
Tactic:
apply ha
Proof state after:
case im_disj
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
x✝ x'✝ : Fin (succ n)
hx✝ : p x✝
hx'✝ : ¬p x'✝
h : f { val := x✝, property := hx✝ } = f' { val := x'✝, property := hx'✝ }
⊢ a ∈ Set.range x.toFun
Theorem: may_extend_with
Proof state before:
case im_disj
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
x✝ x'✝ : Fin (succ n)
hx✝ : p x✝
hx'✝ : ¬p x'✝
h : f { val := x✝, property := hx✝ } = f' { val := x'✝, property := hx'✝ }
⊢ a ∈ Set.range x.toFun
Tactic:
refine ⟨_, h⟩
Proof state after:
no goals
Theorem: may_extend_with
Proof state before:
case h.left
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
⊢ Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding
      { toFun := fun i => if hi : p i then f { val := i, property := hi } else f' { val := i, property := hi },
        inj' := ⋯ } =
    x
Tactic:
ext ⟨i, hi⟩
Proof state after:
case h.left.h.mk
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : ℕ
hi : i < n
⊢ (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding
        { toFun := fun i => if hi : p i then f { val := i, property := hi } else f' { val := i, property := hi },
          inj' := ⋯ })
      { val := i, isLt := hi } =
    x { val := i, isLt := hi }
Theorem: may_extend_with
Proof state before:
case h.left.h.mk
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : ℕ
hi : i < n
⊢ (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding
        { toFun := fun i => if hi : p i then f { val := i, property := hi } else f' { val := i, property := hi },
          inj' := ⋯ })
      { val := i, isLt := hi } =
    x { val := i, isLt := hi }
Tactic:
simp only [trans_apply, RelEmbedding.coe_toEmbedding, Fin.castLE_mk, coeFn_mk]
Proof state after:
case h.left.h.mk
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : ℕ
hi : i < n
⊢ (if hi_1 : p ((Fin.castLEEmb ⋯) { val := i, isLt := hi }) then
      f { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := hi_1 }
    else f' { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := hi_1 }) =
    x { val := i, isLt := hi }
Theorem: may_extend_with
Proof state before:
case h.left.h.mk
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : ℕ
hi : i < n
⊢ (if hi_1 : p ((Fin.castLEEmb ⋯) { val := i, isLt := hi }) then
      f { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := hi_1 }
    else f' { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := hi_1 }) =
    x { val := i, isLt := hi }
Tactic:
rw [dite_eq_iff]
Proof state after:
case h.left.h.mk
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : ℕ
hi : i < n
⊢ (∃ (h : p ((Fin.castLEEmb ⋯) { val := i, isLt := hi })),
      f { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := h } = x { val := i, isLt := hi }) ∨
    ∃ (h : ¬p ((Fin.castLEEmb ⋯) { val := i, isLt := hi })),
      f' { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := h } = x { val := i, isLt := hi }
Theorem: may_extend_with
Proof state before:
case h.left.h.mk
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : ℕ
hi : i < n
⊢ (∃ (h : p ((Fin.castLEEmb ⋯) { val := i, isLt := hi })),
      f { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := h } = x { val := i, isLt := hi }) ∨
    ∃ (h : ¬p ((Fin.castLEEmb ⋯) { val := i, isLt := hi })),
      f' { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := h } = x { val := i, isLt := hi }
Tactic:
apply Or.intro_left
Proof state after:
case h.left.h.mk.h
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : ℕ
hi : i < n
⊢ ∃ (h : p ((Fin.castLEEmb ⋯) { val := i, isLt := hi })),
    f { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := h } = x { val := i, isLt := hi }
Theorem: may_extend_with
Proof state before:
case h.left.h.mk.h
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : ℕ
hi : i < n
⊢ ∃ (h : p ((Fin.castLEEmb ⋯) { val := i, isLt := hi })),
    f { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := h } = x { val := i, isLt := hi }
Tactic:
use hi
Proof state after:
case h
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : ℕ
hi : i < n
⊢ f { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := hi } = x { val := i, isLt := hi }
Theorem: may_extend_with
Proof state before:
case h
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
i : ℕ
hi : i < n
⊢ f { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := hi } = x { val := i, isLt := hi }
Tactic:
rfl
Proof state after:
no goals
Theorem: may_extend_with
Proof state before:
case h.right
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
⊢ { toFun := fun i => if hi : p i then f { val := i, property := hi } else f' { val := i, property := hi }, inj' := ⋯ }
      { val := n, isLt := ⋯ } =
    a
Tactic:
simp only [gt_iff_lt, Set.coe_setOf, Set.mem_setOf_eq, toFun_eq_coe,
coeFn_mk, lt_self_iff_false, ↓reduceDite, p, f, f']
Proof state after:
no goals
Theorem: may_extend
Proof 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
Proof 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
Theorem: may_extend
Proof 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
Proof 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
Theorem: may_extend
Proof 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
Proof 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
Theorem: may_extend
Proof 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
Proof 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
Theorem: may_extend
Proof 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⟩
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
⊢ (Function.Embedding.trans (Fin.castLEEmb hmn✝).toEmbedding w) { val := i, isLt := hi } = x { val := i, isLt := hi }