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

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

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

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

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

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

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

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

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

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

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

State before:
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 }
Tactic:
simp only [Subtype.mk_eq_mk]
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 }
⊢ i = j

State before:
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 }
⊢ i = j
Tactic:
apply (Fin.castIso h').injective
State after:
case refine'_2.mk.mk.a
α : 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 }
⊢ (Fin.castIso h') i = (Fin.castIso h') j

State before:
case refine'_2.mk.mk.a
α : 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 }
⊢ (Fin.castIso h') i = (Fin.castIso h') j
Tactic:
rw [not_lt] at hi hj
State after:
case refine'_2.mk.mk.a
α : 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
hi : m ≤ ↑i
j : Fin n
hj✝ : ¬p j
hj : m ≤ ↑j
hij : g { val := i, property := hi✝ } = g { val := j, property := hj✝ }
⊢ (Fin.castIso h') i = (Fin.castIso h') j

State before:
case refine'_2.mk.mk.a
α : 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
hi : m ≤ ↑i
j : Fin n
hj✝ : ¬p j
hj : m ≤ ↑j
hij : g { val := i, property := hi✝ } = g { val := j, property := hj✝ }
⊢ (Fin.castIso h') i = (Fin.castIso h') j
Tactic:
have hi' : m ≤ (Fin.castIso h') i := by simp only [Fin.coe_orderIso_apply]; exact hi
State after:
case refine'_2.mk.mk.a
α : 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
hi : m ≤ ↑i
j : Fin n
hj✝ : ¬p j
hj : m ≤ ↑j
hij : g { val := i, property := hi✝ } = g { val := j, property := hj✝ }
hi' : m ≤ ↑((Fin.castIso h') i)
⊢ (Fin.castIso h') i = (Fin.castIso h') j

State before:
case refine'_2.mk.mk.a
α : 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
hi : m ≤ ↑i
j : Fin n
hj✝ : ¬p j
hj : m ≤ ↑j
hij : g { val := i, property := hi✝ } = g { val := j, property := hj✝ }
hi' : m ≤ ↑((Fin.castIso h') i)
⊢ (Fin.castIso h') i = (Fin.castIso h') j
Tactic:
have hj' : m ≤ (Fin.castIso h') j := by simp only [Fin.coe_orderIso_apply]; exact hj
State after:
case refine'_2.mk.mk.a
α : 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
hi : m ≤ ↑i
j : Fin n
hj✝ : ¬p j
hj : m ≤ ↑j
hij : g { val := i, property := hi✝ } = g { val := j, property := hj✝ }
hi' : m ≤ ↑((Fin.castIso h') i)
hj' : m ≤ ↑((Fin.castIso h') j)
⊢ (Fin.castIso h') i = (Fin.castIso h') j

State before:
case refine'_2.mk.mk.a
α : 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
hi : m ≤ ↑i
j : Fin n
hj✝ : ¬p j
hj : m ≤ ↑j
hij : g { val := i, property := hi✝ } = g { val := j, property := hj✝ }
hi' : m ≤ ↑((Fin.castIso h') i)
hj' : m ≤ ↑((Fin.castIso h') j)
⊢ (Fin.castIso h') i = (Fin.castIso h') j
Tactic:
let hij' := z.inj' (Subtype.coe_injective hij)
State after:
case refine'_2.mk.mk.a
α : 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
hi : m ≤ ↑i
j : Fin n
hj✝ : ¬p j
hj : m ≤ ↑j
hij : g { val := i, property := hi✝ } = g { val := j, property := hj✝ }
hi' : m ≤ ↑((Fin.castIso h') i)
hj' : m ≤ ↑((Fin.castIso h') j)
hij' : Fin.subNat m ((Fin.castIso h') ↑{ val := i, property := hi✝ }) ⋯ =
  Fin.subNat m ((Fin.castIso h') ↑{ val := j, property := hj✝ }) ⋯ :=
  z.inj' (Subtype.coe_injective hij)
⊢ (Fin.castIso h') i = (Fin.castIso h') j

State before:
case refine'_2.mk.mk.a
α : 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
hi : m ≤ ↑i
j : Fin n
hj✝ : ¬p j
hj : m ≤ ↑j
hij : g { val := i, property := hi✝ } = g { val := j, property := hj✝ }
hi' : m ≤ ↑((Fin.castIso h') i)
hj' : m ≤ ↑((Fin.castIso h') j)
hij' : Fin.subNat m ((Fin.castIso h') ↑{ val := i, property := hi✝ }) ⋯ =
  Fin.subNat m ((Fin.castIso h') ↑{ val := j, property := hj✝ }) ⋯ :=
  z.inj' (Subtype.coe_injective hij)
⊢ (Fin.castIso h') i = (Fin.castIso h') j
Tactic:
simp only at hij'
State after:
case refine'_2.mk.mk.a
α : 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
hi : m ≤ ↑i
j : Fin n
hj✝ : ¬p j
hj : m ≤ ↑j
hij : g { val := i, property := hi✝ } = g { val := j, property := hj✝ }
hi' : m ≤ ↑((Fin.castIso h') i)
hj' : m ≤ ↑((Fin.castIso h') j)
hij' : Fin.subNat m ((Fin.castIso h') i) ⋯ = Fin.subNat m ((Fin.castIso h') j) ⋯ := z.inj' (Subtype.coe_injective hij)
⊢ (Fin.castIso h') i = (Fin.castIso h') j

State before:
case refine'_2.mk.mk.a
α : 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
hi : m ≤ ↑i
j : Fin n
hj✝ : ¬p j
hj : m ≤ ↑j
hij : g { val := i, property := hi✝ } = g { val := j, property := hj✝ }
hi' : m ≤ ↑((Fin.castIso h') i)
hj' : m ≤ ↑((Fin.castIso h') j)
hij' : Fin.subNat m ((Fin.castIso h') i) ⋯ = Fin.subNat m ((Fin.castIso h') j) ⋯ := z.inj' (Subtype.coe_injective hij)
⊢ (Fin.castIso h') i = (Fin.castIso h') j
Tactic:
rw [← Fin.addNat_subNat hi', ← Fin.addNat_subNat hj', hij']
State after:
no goals

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) ⋯))
i : Fin n
hi✝ : ¬p i
hi : m ≤ ↑i
j : Fin n
hj✝ : ¬p j
hj : m ≤ ↑j
hij : g { val := i, property := hi✝ } = g { val := j, property := hj✝ }
⊢ m ≤ ↑((Fin.castIso h') i)
Tactic:
simp only [Fin.coe_orderIso_apply]
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) ⋯))
i : Fin n
hi✝ : ¬p i
hi : m ≤ ↑i
j : Fin n
hj✝ : ¬p j
hj : m ≤ ↑j
hij : g { val := i, property := hi✝ } = g { val := j, property := hj✝ }
⊢ m ≤ ↑i

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) ⋯))
i : Fin n
hi✝ : ¬p i
hi : m ≤ ↑i
j : Fin n
hj✝ : ¬p j
hj : m ≤ ↑j
hij : g { val := i, property := hi✝ } = g { val := j, property := hj✝ }
⊢ m ≤ ↑i
Tactic:
exact hi
State after:
no goals

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) ⋯))
i : Fin n
hi✝ : ¬p i
hi : m ≤ ↑i
j : Fin n
hj✝ : ¬p j
hj : m ≤ ↑j
hij : g { val := i, property := hi✝ } = g { val := j, property := hj✝ }
hi' : m ≤ ↑((Fin.castIso h') i)
⊢ m ≤ ↑((Fin.castIso h') j)
Tactic:
simp only [Fin.coe_orderIso_apply]
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) ⋯))
i : Fin n
hi✝ : ¬p i
hi : m ≤ ↑i
j : Fin n
hj✝ : ¬p j
hj : m ≤ ↑j
hij : g { val := i, property := hi✝ } = g { val := j, property := hj✝ }
hi' : m ≤ ↑((Fin.castIso h') i)
⊢ m ≤ ↑j

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) ⋯))
i : Fin n
hi✝ : ¬p i
hi : m ≤ ↑i
j : Fin n
hj✝ : ¬p j
hj : m ≤ ↑j
hij : g { val := i, property := hi✝ } = g { val := j, property := hj✝ }
hi' : m ≤ ↑((Fin.castIso h') i)
⊢ m ≤ ↑j
Tactic:
exact hj
State after:
no goals

State before:
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' }
Tactic:
intro i j hi hj hij
State after:
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) ⋯))
i j : Fin n
hi : p i
hj : ¬p j
hij : f { val := i, property := hi } = g { val := j, property := hj }
⊢ False

State before:
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) ⋯))
i j : Fin n
hi : p i
hj : ¬p j
hij : f { val := i, property := hi } = g { val := j, property := hj }
⊢ False
Tactic:
suffices f ⟨i, hi⟩ ∉ s by
  apply this
  rw [hij]
  simp only [Set.coe_setOf, Set.mem_setOf_eq, Fin.castIso_apply,
    toFun_eq_coe, Subtype.coe_prop, g]
State after:
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) ⋯))
i j : Fin n
hi : p i
hj : ¬p j
hij : f { val := i, property := hi } = g { val := j, property := hj }
⊢ f { val := i, property := hi } ∉ s

State before:
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) ⋯))
i j : Fin n
hi : p i
hj : ¬p j
hij : f { val := i, property := hi } = g { val := j, property := hj }
⊢ f { val := i, property := hi } ∉ s
Tactic:
simp only [f, ← Set.mem_compl_iff, Subtype.coe_prop]
State after:
no goals

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) ⋯))
i j : Fin n
hi : p i
hj : ¬p j
hij : f { val := i, property := hi } = g { val := j, property := hj }
this : f { val := i, property := hi } ∉ s
⊢ False
Tactic:
apply this
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) ⋯))
i j : Fin n
hi : p i
hj : ¬p j
hij : f { val := i, property := hi } = g { val := j, property := hj }
this : f { val := i, property := hi } ∉ s
⊢ f { val := i, property := hi } ∈ s

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) ⋯))
i j : Fin n
hi : p i
hj : ¬p j
hij : f { val := i, property := hi } = g { val := j, property := hj }
this : f { val := i, property := hi } ∉ s
⊢ f { val := i, property := hi } ∈ s
Tactic:
rw [hij]
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) ⋯))
i j : Fin n
hi : p i
hj : ¬p j
hij : f { val := i, property := hi } = g { val := j, property := hj }
this : f { val := i, property := hi } ∉ s
⊢ g { val := j, property := hj } ∈ s

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) ⋯))
i j : Fin n
hi : p i
hj : ¬p j
hij : f { val := i, property := hi } = g { val := j, property := hj }
this : f { val := i, property := hi } ∉ s
⊢ g { val := j, property := hj } ∈ s
Tactic:
simp only [Set.coe_setOf, Set.mem_setOf_eq, Fin.castIso_apply,
  toFun_eq_coe, Subtype.coe_prop, g]
State after:
no goals

State before:
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ᶜ)
Tactic:
ext ⟨i, hi⟩
State after:
case h.left.h.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 : ℕ
hi : i < m
⊢ (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' := ⋯ })
      { val := i, isLt := hi } =
    (Function.Embedding.trans x (subtype sᶜ)) { val := i, isLt := hi }

State before:
case h.left.h.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 : ℕ
hi : i < m
⊢ (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' := ⋯ })
      { val := i, isLt := hi } =
    (Function.Embedding.trans x (subtype sᶜ)) { 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
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 : ℕ
hi : i < m
⊢ (if hi_1 : p ((Fin.castLEEmb ⋯) { val := i, isLt := hi }) then
      f { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := hi_1 }
    else g { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := hi_1 }) =
    (subtype sᶜ) (x { val := i, isLt := hi })

State before:
case h.left.h.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 : ℕ
hi : i < m
⊢ (if hi_1 : p ((Fin.castLEEmb ⋯) { val := i, isLt := hi }) then
      f { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := hi_1 }
    else g { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := hi_1 }) =
    (subtype sᶜ) (x { val := i, isLt := hi })
Tactic:
rw [dite_eq_iff]
State after:
case h.left.h.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 : ℕ
hi : i < m
⊢ (∃ (h_1 : p ((Fin.castLEEmb ⋯) { val := i, isLt := hi })),
      f { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := h_1 } =
        (subtype sᶜ) (x { val := i, isLt := hi })) ∨
    ∃ (h_1 : ¬p ((Fin.castLEEmb ⋯) { val := i, isLt := hi })),
      g { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := h_1 } =
        (subtype sᶜ) (x { val := i, isLt := hi })

State before:
case h.left.h.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 : ℕ
hi : i < m
⊢ (∃ (h_1 : p ((Fin.castLEEmb ⋯) { val := i, isLt := hi })),
      f { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := h_1 } =
        (subtype sᶜ) (x { val := i, isLt := hi })) ∨
    ∃ (h_1 : ¬p ((Fin.castLEEmb ⋯) { val := i, isLt := hi })),
      g { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := h_1 } =
        (subtype sᶜ) (x { val := i, isLt := hi })
Tactic:
apply Or.intro_left
State after:
case h.left.h.mk.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) ⋯))
i : ℕ
hi : i < m
⊢ ∃ (h_1 : p ((Fin.castLEEmb ⋯) { val := i, isLt := hi })),
    f { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := h_1 } = (subtype sᶜ) (x { val := i, isLt := hi })

State before:
case h.left.h.mk.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) ⋯))
i : ℕ
hi : i < m
⊢ ∃ (h_1 : p ((Fin.castLEEmb ⋯) { val := i, isLt := hi })),
    f { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := h_1 } = (subtype sᶜ) (x { val := i, isLt := hi })
Tactic:
use hi
State after:
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) ⋯))
i : ℕ
hi : i < m
⊢ f { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := hi } = (subtype sᶜ) (x { val := i, isLt := hi })

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) ⋯))
i : ℕ
hi : i < m
⊢ f { val := (Fin.castLEEmb ⋯) { val := i, isLt := hi }, property := hi } = (subtype sᶜ) (x { val := i, isLt := hi })
Tactic:
rfl
State after:
no goals

State before:
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)
Tactic:
ext ⟨j, hj⟩
State after:
case h.right.h.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) ⋯))
j : ℕ
hj : j < k
⊢ (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' := ⋯ }))
      { val := j, isLt := hj } =
    (Function.Embedding.trans z (subtype s)) { val := j, isLt := hj }

State before:
case h.right.h.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) ⋯))
j : ℕ
hj : j < k
⊢ (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' := ⋯ }))
      { val := j, isLt := hj } =
    (Function.Embedding.trans z (subtype s)) { val := j, isLt := hj }
Tactic:
simp only [Fin.natAddEmb_toEmbedding, gt_iff_lt, Set.coe_setOf, Set.mem_setOf_eq, toFun_eq_coe,
  Fin.castIso_apply, trans_apply, coeFn_mk, Fin.natAdd_mk, Equiv.coe_toEmbedding,
  RelIso.coe_fn_toEquiv, Fin.cast_mk, add_lt_iff_neg_left, not_lt_zero', ↓reduceDite,
  Fin.subNat_mk, add_tsub_cancel_left, p, f, g]
State after:
case h.right.h.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) ⋯))
j : ℕ
hj : j < k
⊢ ↑(z { val := j, isLt := ⋯ }) = (subtype s) (z { val := j, isLt := hj })

State before:
case h.right.h.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) ⋯))
j : ℕ
hj : j < k
⊢ ↑(z { val := j, isLt := ⋯ }) = (subtype s) (z { val := j, isLt := hj })
Tactic:
rfl
State after:
no goals