no goals
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
⊢ ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
simpa only [ne_eq, not_exists, not_forall, not_and] using h
case inl.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hx : x = f
hy : y = f
⊢ ∀ (i : ι), x i = y i → x = y

case inl.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hx : x = f
hy : y ∈ s
⊢ ∀ (i : ι), x i = y i → x = y

case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hx : x ∈ s
hy : y = f
⊢ ∀ (i : ι), x i = y i → x = y

case inr.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hx : x ∈ s
hy : y ∈ s
⊢ ∀ (i : ι), x i = y i → x = y
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x : (i : ι) → β i
hx : x ∈ insert f s
y : (i : ι) → β i
hy : y ∈ insert f s
⊢ ∀ (i : ι), x i = y i → x = y
cases' hx with hx hx <;> cases' hy with hy hy
no goals
case inl.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hx : x = f
hy : y = f
⊢ ∀ (i : ι), x i = y i → x = y
simp [hx, hy]
case inl.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
y : (i : ι) → β i
hy : y ∈ s
⊢ ∀ (i : ι), f i = y i → f = y
case inl.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hx : x = f
hy : y ∈ s
⊢ ∀ (i : ι), x i = y i → x = y
subst x
no goals
case inl.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
y : (i : ι) → β i
hy : y ∈ s
⊢ ∀ (i : ι), f i = y i → f = y
exact fun i e => (hf i y hy e.symm).elim
case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x : (i : ι) → β i
hx : x ∈ s
⊢ ∀ (i : ι), x i = f i → x = f
case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hx : x ∈ s
hy : y = f
⊢ ∀ (i : ι), x i = y i → x = y
subst y
no goals
case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x : (i : ι) → β i
hx : x ∈ s
⊢ ∀ (i : ι), x i = f i → x = f
exact fun i e => (hf i x hx e).elim
no goals
case inr.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
h✝ : ¬∃ i, ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
h : ∀ (i : ι), ∃ y, ∀ (x : (i : ι) → β i), x ∈ s → x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι) (x_1 : (i : ι) → β i), x_1 ∈ s → x_1 x ≠ f x
x y : (i : ι) → β i
hx : x ∈ s
hy : y ∈ s
⊢ ∀ (i : ι), x i = y i → x = y
exact hs x hx y hy
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
i : ι
e : ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
f : β i → (i : ι) → β i
hf : ∀ (x : β i), f x ∈ s ∧ f x i = x
j : ι
a b : β i
e' : (fun a => f a j) a = (fun a => f a j) b
sa : f a ∈ s
ea : f a i = a
⊢ a = b
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
i : ι
e : ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
f : β i → (i : ι) → β i
hf : ∀ (x : β i), f x ∈ s ∧ f x i = x
j : ι
a b : β i
e' : (fun a => f a j) a = (fun a => f a j) b
⊢ a = b
let ⟨sa, ea⟩ := hf a
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
i : ι
e : ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
f : β i → (i : ι) → β i
hf : ∀ (x : β i), f x ∈ s ∧ f x i = x
j : ι
a b : β i
e' : (fun a => f a j) a = (fun a => f a j) b
sa : f a ∈ s
ea : f a i = a
sb : f b ∈ s
eb : f b i = b
⊢ a = b
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
i : ι
e : ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
f : β i → (i : ι) → β i
hf : ∀ (x : β i), f x ∈ s ∧ f x i = x
j : ι
a b : β i
e' : (fun a => f a j) a = (fun a => f a j) b
sa : f a ∈ s
ea : f a i = a
⊢ a = b
let ⟨sb, eb⟩ := hf b
no goals
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : s ∈ Function.Embedding.sets β
ms : ∀ (a : Set ((i : ι) → β i)), a ∈ Function.Embedding.sets β → s ⊆ a → a = s
i : ι
e : ∀ (y : β i), ∃ x, x ∈ s ∧ x i = y
f : β i → (i : ι) → β i
hf : ∀ (x : β i), f x ∈ s ∧ f x i = x
j : ι
a b : β i
e' : (fun a => f a j) a = (fun a => f a j) b
sa : f a ∈ s
ea : f a i = a
sb : f b ∈ s
eb : f b i = b
⊢ a = b
rw [← ea, ← eb, hs _ sa _ sb _ e']