internlm/Lean-Github huggingface dataset:
Theorem: may_extend_with'
Proof 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]
Proof state after:
case refine'_2.mk.mk
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
i : Fin n
hi : ¬p i
j : Fin n
hj : ¬p j
hij : g { val := i, property := hi } = g { val := j, property := hj }
⊢ i = j
Theorem: may_extend_with'
Proof 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
Proof 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
Theorem: may_extend_with'
Proof 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
Proof 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
Theorem: may_extend_with'
Proof 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
Proof 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
Theorem: may_extend_with'
Proof 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
Proof 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
Theorem: may_extend_with'
Proof 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)
Proof 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
Theorem: may_extend_with'
Proof 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'
Proof 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
Theorem: may_extend_with'
Proof 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']
Proof state after:
no goals
Theorem: may_extend_with'
Proof state before:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
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]
Proof state after:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
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
Theorem: may_extend_with'
Proof state before:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
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
Proof state after:
no goals
Theorem: may_extend_with'
Proof state before:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
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]
Proof state after:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
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
Theorem: may_extend_with'
Proof state before:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
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
Proof state after:
no goals
Theorem: may_extend_with'
Proof 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
Proof 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
Theorem: may_extend_with'
Proof 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]
Proof 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
Theorem: may_extend_with'
Proof 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]
Proof state after:
no goals
Theorem: may_extend_with'
Proof state before:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
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
Proof state after:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
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
Theorem: may_extend_with'
Proof state before:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
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]
Proof state after:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
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
Theorem: may_extend_with'
Proof state before:
α : Type u_1
m n k : ℕ
s : Set α
z : Fin k ↪ ↑s
h : n = m + k
x : Fin m ↪ ↑sᶜ
h' : n = k + m := h.trans (add_comm m k)
p : Fin n → Prop := fun i => ↑i < m
f : ↑{i | p i} → α := fun i => ↑(x.toFun (Fin.castLT ↑i ⋯))
g : ↑{i | ¬p i} → α := fun i => ↑(z.toFun (Fin.subNat m ((Fin.castIso h') ↑i) ⋯))
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]
Proof state after:
no goals
Theorem: may_extend_with'
Proof 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⟩
Proof 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 }
Theorem: may_extend_with'
Proof 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]
Proof 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 })
Theorem: may_extend_with'
Proof 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]
Proof 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 })
Theorem: may_extend_with'
Proof 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
Proof 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 })
Theorem: may_extend_with'
Proof 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
Proof 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 })