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 }
⊢ ↑(Fin.castLT i ?m.8352) = ↑(Fin.castLT j ?m.8372)

α : 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 }
⊢ ↑j < ?m.8371

α : 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

α : 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
Tactic:
rw [x.inj' hij]
Proof state after:
no goals