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

State before:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = x ∧ x' { val := n, isLt := ⋯ } = a
Tactic:
let p := fun i : Fin n.succ => i.val < n
State after:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = x ∧ x' { val := n, isLt := ⋯ } = a

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
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = x ∧ x' { val := n, isLt := ⋯ } = a
Tactic:
let f : {i : Fin n.succ | i.val < n} → α := fun i => x.toFun (Fin.castLT i.val i.prop)
State after:
α : 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 ⋯)
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = x ∧ x' { val := n, isLt := ⋯ } = a

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 ⋯)
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = x ∧ x' { val := n, isLt := ⋯ } = a
Tactic:
let f' : {i : Fin n.succ | ¬p i} ↪ α := {
  toFun := fun ⟨_, _⟩ => a
  inj' := by
    rintro ⟨i, hi⟩ ⟨j, hj⟩ _
    simp only [Subtype.mk_eq_mk, Fin.ext_iff]
    rw [Nat.eq_of_lt_succ_of_not_lt i.prop hi, Nat.eq_of_lt_succ_of_not_lt j.prop hj] }
State after:
α : 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', Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = x ∧ x' { val := n, isLt := ⋯ } = a

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' := ⋯ }
⊢ 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 ∧
    { 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:
constructor
State after:
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

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

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⟩ _
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 }

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]
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

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]
State after:
no goals

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
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' }

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
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 }

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]
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

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

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 _]
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

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) = ↑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
Tactic:
rw [← Fin.coe_castLT j _]
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) = ↑(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

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]
State after:
no goals

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'
State after:
no goals

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
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'✝ }

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]
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'✝ }

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

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

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⟩
State after:
no goals

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⟩
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 }

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]
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 }

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]
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 }

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
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 }

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
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 }

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
State after:
no goals

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']
State after:
no goals