α : Type ?u.49249
β : Type ?u.49252
γ : Type ?u.49255
f : α ↪ β
s : Finset α
a b : ℕ
⊢ range a ⊓ map (addRightEmbedding a) (range b) ≤ ⊥
α : Type ?u.49249
β : Type ?u.49252
γ : Type ?u.49255
f : α ↪ β
s : Finset α
a b : ℕ
⊢ _root_.Disjoint (range a) (map (addRightEmbedding a) (range b))
refine' disjoint_iff_inf_le.mpr _
α : Type ?u.49249
β : Type ?u.49252
γ : Type ?u.49255
f : α ↪ β
s : Finset α
a b k : ℕ
hk : k ∈ range a ⊓ map (addRightEmbedding a) (range b)
⊢ k ∈ ⊥
α : Type ?u.49249
β : Type ?u.49252
γ : Type ?u.49255
f : α ↪ β
s : Finset α
a b : ℕ
⊢ range a ⊓ map (addRightEmbedding a) (range b) ≤ ⊥
intro k hk
α : Type ?u.49249
β : Type ?u.49252
γ : Type ?u.49255
f : α ↪ β
s : Finset α
a b k : ℕ
hk : k < a ∧ ∃ a_1, a_1 < b ∧ ↑{ toFun := fun h => h + a, inj' := (_ : Injective fun x => x + a) } a_1 = k
⊢ k ∈ ⊥
α : Type ?u.49249
β : Type ?u.49252
γ : Type ?u.49255
f : α ↪ β
s : Finset α
a b k : ℕ
hk : k ∈ range a ⊓ map (addRightEmbedding a) (range b)
⊢ k ∈ ⊥
simp only [exists_prop, mem_range, inf_eq_inter, mem_map, addRightEmbedding, mem_inter]
  at hk
case intro.intro
α : Type ?u.49249
β : Type ?u.49252
γ : Type ?u.49255
f : α ↪ β
s : Finset α
a✝ b k : ℕ
hk : k < a✝ ∧ ∃ a, a < b ∧ ↑{ toFun := fun h => h + a✝, inj' := (_ : Injective fun x => x + a✝) } a = k
a : ℕ
left✝ : a < b
ha : ↑{ toFun := fun h => h + a✝, inj' := (_ : Injective fun x => x + a✝) } a = k
⊢ k ∈ ⊥
α : Type ?u.49249
β : Type ?u.49252
γ : Type ?u.49255
f : α ↪ β
s : Finset α
a b k : ℕ
hk : k < a ∧ ∃ a_1, a_1 < b ∧ ↑{ toFun := fun h => h + a, inj' := (_ : Injective fun x => x + a) } a_1 = k
⊢ k ∈ ⊥
obtain ⟨a, _, ha⟩ := hk.2
no goals
case intro.intro
α : Type ?u.49249
β : Type ?u.49252
γ : Type ?u.49255
f : α ↪ β
s : Finset α
a✝ b k : ℕ
hk : k < a✝ ∧ ∃ a, a < b ∧ ↑{ toFun := fun h => h + a✝, inj' := (_ : Injective fun x => x + a✝) } a = k
a : ℕ
left✝ : a < b
ha : ↑{ toFun := fun h => h + a✝, inj' := (_ : Injective fun x => x + a✝) } a = k
⊢ k ∈ ⊥
simpa [← ha] using hk.1